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 grid, slice, row sum and intermediate table is constructed. Retained cells have witnessed n=(a*e)*c and value F(a)*(H(e)*G(c)). The flat endpoint is unused. Table associativity includes N=0 and compares only positive values, not encodings. Full G009 remains broader.
Exact theorem in conservative defined notation
∀ F. ∀ G. ∀ H. ∀ n. ArithTable(0,F) → ArithTable(0,G) → ArithTable(0,H) → ∃ x. ∃ y. ∃ z. ∃ m. DirichletGrid(F,G,H,n,x) ∧ (ArithRowSums(x,y,0,S n,1,S n,S n) ∧ (ArithRowSums(x,z,0,1,S n,S n,S n) ∧ (SignedPrefixSum(y,S n,m) ∧ SignedPrefixSum(z,S n,m))))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall F G H n. (exists dst_positive_code_fubini_F dst_positive_scale_fubini_F dst_negative_code_fubini_F dst_negative_scale_fubini_F. (((F) = (((((dst_positive_code_fubini_F) + (dst_positive_scale_fubini_F)) * S ((dst_positive_code_fubini_F) + (dst_positive_scale_fubini_F)) + ((dst_positive_scale_fubini_F) + (dst_positive_scale_fubini_F))) + (((dst_negative_code_fubini_F) + (dst_negative_scale_fubini_F)) * S ((dst_negative_code_fubini_F) + (dst_negative_scale_fubini_F)) + ((dst_negative_scale_fubini_F) + (dst_negative_scale_fubini_F)))) * S ((((dst_positive_code_fubini_F) + (dst_positive_scale_fubini_F)) * S ((dst_positive_code_fubini_F) + (dst_positive_scale_fubini_F)) + ((dst_positive_scale_fubini_F) + (dst_positive_scale_fubini_F))) + (((dst_negative_code_fubini_F) + (dst_negative_scale_fubini_F)) * S ((dst_negative_code_fubini_F) + (dst_negative_scale_fubini_F)) + ((dst_negative_scale_fubini_F) + (dst_negative_scale_fubini_F)))) + ((((dst_negative_code_fubini_F) + (dst_negative_scale_fubini_F)) * S ((dst_negative_code_fubini_F) + (dst_negative_scale_fubini_F)) + ((dst_negative_scale_fubini_F) + (dst_negative_scale_fubini_F))) + (((dst_negative_code_fubini_F) + (dst_negative_scale_fubini_F)) * S ((dst_negative_code_fubini_F) + (dst_negative_scale_fubini_F)) + ((dst_negative_scale_fubini_F) + (dst_negative_scale_fubini_F)))))) /\ (forall dst_index_fubini_F. (exists pvs_le_gap_fubini_Fdomain. pvs_le_gap_fubini_Fdomain + (dst_index_fubini_F) = (0)) -> exists dst_positive_fubini_F dst_negative_fubini_F dst_value_fubini_F. ((((exists ff_h_pvs_fubini_Fentrypositive. ff_h_pvs_fubini_Fentrypositive + S (dst_positive_fubini_F) = S ((S (dst_index_fubini_F)) * dst_positive_scale_fubini_F)) /\ exists ff_q_pvs_fubini_Fentrypositive. dst_positive_code_fubini_F = ff_q_pvs_fubini_Fentrypositive * S ((S (dst_index_fubini_F)) * dst_positive_scale_fubini_F) + (dst_positive_fubini_F))) /\ (((((exists ff_h_pvs_fubini_Fentrynegative. ff_h_pvs_fubini_Fentrynegative + S (dst_negative_fubini_F) = S ((S (dst_index_fubini_F)) * dst_negative_scale_fubini_F)) /\ exists ff_q_pvs_fubini_Fentrynegative. dst_negative_code_fubini_F = ff_q_pvs_fubini_Fentrynegative * S ((S (dst_index_fubini_F)) * dst_negative_scale_fubini_F) + (dst_negative_fubini_F))) /\ (exists ge_balance_positive_fubini_Fentryvalue ge_balance_negative_fubini_Fentryvalue. (((((dst_value_fubini_F) = 2 * (ge_balance_positive_fubini_Fentryvalue) /\ (ge_balance_negative_fubini_Fentryvalue) = 0) \/ exists ge_signed_half_fubini_Fentryvaluedecode. (((dst_value_fubini_F) = 2 * ge_signed_half_fubini_Fentryvaluedecode + 1 /\ (ge_balance_positive_fubini_Fentryvalue) = 0) /\ (ge_balance_negative_fubini_Fentryvalue) = S ge_signed_half_fubini_Fentryvaluedecode))) /\ ((dst_positive_fubini_F) + ge_balance_negative_fubini_Fentryvalue = (dst_negative_fubini_F) + ge_balance_positive_fubini_Fentryvalue))))))))) -> (exists dst_positive_code_fubini_G dst_positive_scale_fubini_G dst_negative_code_fubini_G dst_negative_scale_fubini_G. (((G) = (((((dst_positive_code_fubini_G) + (dst_positive_scale_fubini_G)) * S ((dst_positive_code_fubini_G) + (dst_positive_scale_fubini_G)) + ((dst_positive_scale_fubini_G) + (dst_positive_scale_fubini_G))) + (((dst_negative_code_fubini_G) + (dst_negative_scale_fubini_G)) * S ((dst_negative_code_fubini_G) + (dst_negative_scale_fubini_G)) + ((dst_negative_scale_fubini_G) + (dst_negative_scale_fubini_G)))) * S ((((dst_positive_code_fubini_G) + (dst_positive_scale_fubini_G)) * S ((dst_positive_code_fubini_G) + (dst_positive_scale_fubini_G)) + ((dst_positive_scale_fubini_G) + (dst_positive_scale_fubini_G))) + (((dst_negative_code_fubini_G) + (dst_negative_scale_fubini_G)) * S ((dst_negative_code_fubini_G) + (dst_negative_scale_fubini_G)) + ((dst_negative_scale_fubini_G) + (dst_negative_scale_fubini_G)))) + ((((dst_negative_code_fubini_G) + (dst_negative_scale_fubini_G)) * S ((dst_negative_code_fubini_G) + (dst_negative_scale_fubini_G)) + ((dst_negative_scale_fubini_G) + (dst_negative_scale_fubini_G))) + (((dst_negative_code_fubini_G) + (dst_negative_scale_fubini_G)) * S ((dst_negative_code_fubini_G) + (dst_negative_scale_fubini_G)) + ((dst_negative_scale_fubini_G) + (dst_negative_scale_fubini_G)))))) /\ (forall dst_index_fubini_G. (exists pvs_le_gap_fubini_Gdomain. pvs_le_gap_fubini_Gdomain + (dst_index_fubini_G) = (0)) -> exists dst_positive_fubini_G dst_negative_fubini_G dst_value_fubini_G. ((((exists ff_h_pvs_fubini_Gentrypositive. ff_h_pvs_fubini_Gentrypositive + S (dst_positive_fubini_G) = S ((S (dst_index_fubini_G)) * dst_positive_scale_fubini_G)) /\ exists ff_q_pvs_fubini_Gentrypositive. dst_positive_code_fubini_G = ff_q_pvs_fubini_Gentrypositive * S ((S (dst_index_fubini_G)) * dst_positive_scale_fubini_G) + (dst_positive_fubini_G))) /\ (((((exists ff_h_pvs_fubini_Gentrynegative. ff_h_pvs_fubini_Gentrynegative + S (dst_negative_fubini_G) = S ((S (dst_index_fubini_G)) * dst_negative_scale_fubini_G)) /\ exists ff_q_pvs_fubini_Gentrynegative. dst_negative_code_fubini_G = ff_q_pvs_fubini_Gentrynegative * S ((S (dst_index_fubini_G)) * dst_negative_scale_fubini_G) + (dst_negative_fubini_G))) /\ (exists ge_balance_positive_fubini_Gentryvalue ge_balance_negative_fubini_Gentryvalue. (((((dst_value_fubini_G) = 2 * (ge_balance_positive_fubini_Gentryvalue) /\ (ge_balance_negative_fubini_Gentryvalue) = 0) \/ exists ge_signed_half_fubini_Gentryvaluedecode. (((dst_value_fubini_G) = 2 * ge_signed_half_fubini_Gentryvaluedecode + 1 /\ (ge_balance_positive_fubini_Gentryvalue) = 0) /\ (ge_balance_negative_fubini_Gentryvalue) = S ge_signed_half_fubini_Gentryvaluedecode))) /\ ((dst_positive_fubini_G) + ge_balance_negative_fubini_Gentryvalue = (dst_negative_fubini_G) + ge_balance_positive_fubini_Gentryvalue))))))))) -> (exists dst_positive_code_fubini_H dst_positive_scale_fubini_H dst_negative_code_fubini_H dst_negative_scale_fubini_H. (((H) = (((((dst_positive_code_fubini_H) + (dst_positive_scale_fubini_H)) * S ((dst_positive_code_fubini_H) + (dst_positive_scale_fubini_H)) + ((dst_positive_scale_fubini_H) + (dst_positive_scale_fubini_H))) + (((dst_negative_code_fubini_H) + (dst_negative_scale_fubini_H)) * S ((dst_negative_code_fubini_H) + (dst_negative_scale_fubini_H)) + ((dst_negative_scale_fubini_H) + (dst_negative_scale_fubini_H)))) * S ((((dst_positive_code_fubini_H) + (dst_positive_scale_fubini_H)) * S ((dst_positive_code_fubini_H) + (dst_positive_scale_fubini_H)) + ((dst_positive_scale_fubini_H) + (dst_positive_scale_fubini_H))) + (((dst_negative_code_fubini_H) + (dst_negative_scale_fubini_H)) * S ((dst_negative_code_fubini_H) + (dst_negative_scale_fubini_H)) + ((dst_negative_scale_fubini_H) + (dst_negative_scale_fubini_H)))) + ((((dst_negative_code_fubini_H) + (dst_negative_scale_fubini_H)) * S ((dst_negative_code_fubini_H) + (dst_negative_scale_fubini_H)) + ((dst_negative_scale_fubini_H) + (dst_negative_scale_fubini_H))) + (((dst_negative_code_fubini_H) + (dst_negative_scale_fubini_H)) * S ((dst_negative_code_fubini_H) + (dst_negative_scale_fubini_H)) + ((dst_negative_scale_fubini_H) + (dst_negative_scale_fubini_H)))))) /\ (forall dst_index_fubini_H. (exists pvs_le_gap_fubini_Hdomain. pvs_le_gap_fubini_Hdomain + (dst_index_fubini_H) = (0)) -> exists dst_positive_fubini_H dst_negative_fubini_H dst_value_fubini_H. ((((exists ff_h_pvs_fubini_Hentrypositive. ff_h_pvs_fubini_Hentrypositive + S (dst_positive_fubini_H) = S ((S (dst_index_fubini_H)) * dst_positive_scale_fubini_H)) /\ exists ff_q_pvs_fubini_Hentrypositive. dst_positive_code_fubini_H = ff_q_pvs_fubini_Hentrypositive * S ((S (dst_index_fubini_H)) * dst_positive_scale_fubini_H) + (dst_positive_fubini_H))) /\ (((((exists ff_h_pvs_fubini_Hentrynegative. ff_h_pvs_fubini_Hentrynegative + S (dst_negative_fubini_H) = S ((S (dst_index_fubini_H)) * dst_negative_scale_fubini_H)) /\ exists ff_q_pvs_fubini_Hentrynegative. dst_negative_code_fubini_H = ff_q_pvs_fubini_Hentrynegative * S ((S (dst_index_fubini_H)) * dst_negative_scale_fubini_H) + (dst_negative_fubini_H))) /\ (exists ge_balance_positive_fubini_Hentryvalue ge_balance_negative_fubini_Hentryvalue. (((((dst_value_fubini_H) = 2 * (ge_balance_positive_fubini_Hentryvalue) /\ (ge_balance_negative_fubini_Hentryvalue) = 0) \/ exists ge_signed_half_fubini_Hentryvaluedecode. (((dst_value_fubini_H) = 2 * ge_signed_half_fubini_Hentryvaluedecode + 1 /\ (ge_balance_positive_fubini_Hentryvalue) = 0) /\ (ge_balance_negative_fubini_Hentryvalue) = S ge_signed_half_fubini_Hentryvaluedecode))) /\ ((dst_positive_fubini_H) + ge_balance_negative_fubini_Hentryvalue = (dst_negative_fubini_H) + ge_balance_positive_fubini_Hentryvalue))))))))) -> exists T R C z. ((((exists dst_positive_code_fubini_actual_gridtable dst_positive_scale_fubini_actual_gridtable dst_negative_code_fubini_actual_gridtable dst_negative_scale_fubini_actual_gridtable. (((T) = (((((dst_positive_code_fubini_actual_gridtable) + (dst_positive_scale_fubini_actual_gridtable)) * S ((dst_positive_code_fubini_actual_gridtable) + (dst_positive_scale_fubini_actual_gridtable)) + ((dst_positive_scale_fubini_actual_gridtable) + (dst_positive_scale_fubini_actual_gridtable))) + (((dst_negative_code_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)) * S ((dst_negative_code_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)) + ((dst_negative_scale_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)))) * S ((((dst_positive_code_fubini_actual_gridtable) + (dst_positive_scale_fubini_actual_gridtable)) * S ((dst_positive_code_fubini_actual_gridtable) + (dst_positive_scale_fubini_actual_gridtable)) + ((dst_positive_scale_fubini_actual_gridtable) + (dst_positive_scale_fubini_actual_gridtable))) + (((dst_negative_code_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)) * S ((dst_negative_code_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)) + ((dst_negative_scale_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)))) + ((((dst_negative_code_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)) * S ((dst_negative_code_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)) + ((dst_negative_scale_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable))) + (((dst_negative_code_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)) * S ((dst_negative_code_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)) + ((dst_negative_scale_fubini_actual_gridtable) + (dst_negative_scale_fubini_actual_gridtable)))))) /\ (forall dst_index_fubini_actual_gridtable. (exists pvs_le_gap_fubini_actual_gridtabledomain. pvs_le_gap_fubini_actual_gridtabledomain + (dst_index_fubini_actual_gridtable) = ((S (n))*(S (n)))) -> exists dst_positive_fubini_actual_gridtable dst_negative_fubini_actual_gridtable dst_value_fubini_actual_gridtable. ((((exists ff_h_pvs_fubini_actual_gridtableentrypositive. ff_h_pvs_fubini_actual_gridtableentrypositive + S (dst_positive_fubini_actual_gridtable) = S ((S (dst_index_fubini_actual_gridtable)) * dst_positive_scale_fubini_actual_gridtable)) /\ exists ff_q_pvs_fubini_actual_gridtableentrypositive. dst_positive_code_fubini_actual_gridtable = ff_q_pvs_fubini_actual_gridtableentrypositive * S ((S (dst_index_fubini_actual_gridtable)) * dst_positive_scale_fubini_actual_gridtable) + (dst_positive_fubini_actual_gridtable))) /\ (((((exists ff_h_pvs_fubini_actual_gridtableentrynegative. ff_h_pvs_fubini_actual_gridtableentrynegative + S (dst_negative_fubini_actual_gridtable) = S ((S (dst_index_fubini_actual_gridtable)) * dst_negative_scale_fubini_actual_gridtable)) /\ exists ff_q_pvs_fubini_actual_gridtableentrynegative. dst_negative_code_fubini_actual_gridtable = ff_q_pvs_fubini_actual_gridtableentrynegative * S ((S (dst_index_fubini_actual_gridtable)) * dst_negative_scale_fubini_actual_gridtable) + (dst_negative_fubini_actual_gridtable))) /\ (exists ge_balance_positive_fubini_actual_gridtableentryvalue ge_balance_negative_fubini_actual_gridtableentryvalue. (((((dst_value_fubini_actual_gridtable) = 2 * (ge_balance_positive_fubini_actual_gridtableentryvalue) /\ (ge_balance_negative_fubini_actual_gridtableentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_gridtableentryvaluedecode. (((dst_value_fubini_actual_gridtable) = 2 * ge_signed_half_fubini_actual_gridtableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_gridtableentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_gridtableentryvalue) = S ge_signed_half_fubini_actual_gridtableentryvaluedecode))) /\ ((dst_positive_fubini_actual_gridtable) + ge_balance_negative_fubini_actual_gridtableentryvalue = (dst_negative_fubini_actual_gridtable) + ge_balance_positive_fubini_actual_gridtableentryvalue))))))))) /\ (forall dfg_grid_row_fubini_actual_grid dfg_grid_column_fubini_actual_grid dfg_grid_value_fubini_actual_grid. (exists pvs_le_gap_fubini_actual_gridrow. pvs_le_gap_fubini_actual_gridrow + (dfg_grid_row_fubini_actual_grid) = (n)) -> (exists pvs_le_gap_fubini_actual_gridcolumn. pvs_le_gap_fubini_actual_gridcolumn + (dfg_grid_column_fubini_actual_grid) = (n)) -> (exists dst_positive_code_fubini_actual_gridlookup dst_positive_scale_fubini_actual_gridlookup dst_negative_code_fubini_actual_gridlookup dst_negative_scale_fubini_actual_gridlookup dst_positive_fubini_actual_gridlookup dst_negative_fubini_actual_gridlookup. (((T) = (((((dst_positive_code_fubini_actual_gridlookup) + (dst_positive_scale_fubini_actual_gridlookup)) * S ((dst_positive_code_fubini_actual_gridlookup) + (dst_positive_scale_fubini_actual_gridlookup)) + ((dst_positive_scale_fubini_actual_gridlookup) + (dst_positive_scale_fubini_actual_gridlookup))) + (((dst_negative_code_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)) * S ((dst_negative_code_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)) + ((dst_negative_scale_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)))) * S ((((dst_positive_code_fubini_actual_gridlookup) + (dst_positive_scale_fubini_actual_gridlookup)) * S ((dst_positive_code_fubini_actual_gridlookup) + (dst_positive_scale_fubini_actual_gridlookup)) + ((dst_positive_scale_fubini_actual_gridlookup) + (dst_positive_scale_fubini_actual_gridlookup))) + (((dst_negative_code_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)) * S ((dst_negative_code_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)) + ((dst_negative_scale_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)))) + ((((dst_negative_code_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)) * S ((dst_negative_code_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)) + ((dst_negative_scale_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup))) + (((dst_negative_code_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)) * S ((dst_negative_code_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)) + ((dst_negative_scale_fubini_actual_gridlookup) + (dst_negative_scale_fubini_actual_gridlookup)))))) /\ (((((exists ff_h_pvs_fubini_actual_gridlookuppositive. ff_h_pvs_fubini_actual_gridlookuppositive + S (dst_positive_fubini_actual_gridlookup) = S ((S ((S (n))*(dfg_grid_row_fubini_actual_grid)+(dfg_grid_column_fubini_actual_grid))) * dst_positive_scale_fubini_actual_gridlookup)) /\ exists ff_q_pvs_fubini_actual_gridlookuppositive. dst_positive_code_fubini_actual_gridlookup = ff_q_pvs_fubini_actual_gridlookuppositive * S ((S ((S (n))*(dfg_grid_row_fubini_actual_grid)+(dfg_grid_column_fubini_actual_grid))) * dst_positive_scale_fubini_actual_gridlookup) + (dst_positive_fubini_actual_gridlookup))) /\ (((((exists ff_h_pvs_fubini_actual_gridlookupnegative. ff_h_pvs_fubini_actual_gridlookupnegative + S (dst_negative_fubini_actual_gridlookup) = S ((S ((S (n))*(dfg_grid_row_fubini_actual_grid)+(dfg_grid_column_fubini_actual_grid))) * dst_negative_scale_fubini_actual_gridlookup)) /\ exists ff_q_pvs_fubini_actual_gridlookupnegative. dst_negative_code_fubini_actual_gridlookup = ff_q_pvs_fubini_actual_gridlookupnegative * S ((S ((S (n))*(dfg_grid_row_fubini_actual_grid)+(dfg_grid_column_fubini_actual_grid))) * dst_negative_scale_fubini_actual_gridlookup) + (dst_negative_fubini_actual_gridlookup))) /\ (exists ge_balance_positive_fubini_actual_gridlookupvalue ge_balance_negative_fubini_actual_gridlookupvalue. (((((dfg_grid_value_fubini_actual_grid) = 2 * (ge_balance_positive_fubini_actual_gridlookupvalue) /\ (ge_balance_negative_fubini_actual_gridlookupvalue) = 0) \/ exists ge_signed_half_fubini_actual_gridlookupvaluedecode. (((dfg_grid_value_fubini_actual_grid) = 2 * ge_signed_half_fubini_actual_gridlookupvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_gridlookupvalue) = 0) /\ (ge_balance_negative_fubini_actual_gridlookupvalue) = S ge_signed_half_fubini_actual_gridlookupvaluedecode))) /\ ((dst_positive_fubini_actual_gridlookup) + ge_balance_negative_fubini_actual_gridlookupvalue = (dst_negative_fubini_actual_gridlookup) + ge_balance_positive_fubini_actual_gridlookupvalue))))))))) -> ((((~((dfg_grid_row_fubini_actual_grid)=0)) /\ (((~((dfg_grid_column_fubini_actual_grid)=0)) /\ (exists dfg_middle_fubini_actual_gridentry dfg_first_fubini_actual_gridentry dfg_last_fubini_actual_gridentry dfg_value_fubini_actual_gridentry. (((n)=((dfg_grid_row_fubini_actual_grid)*(dfg_grid_column_fubini_actual_grid))*dfg_middle_fubini_actual_gridentry) /\ (((exists dst_positive_code_fubini_actual_gridentryfirst dst_positive_scale_fubini_actual_gridentryfirst dst_negative_code_fubini_actual_gridentryfirst dst_negative_scale_fubini_actual_gridentryfirst dst_positive_fubini_actual_gridentryfirst dst_negative_fubini_actual_gridentryfirst. (((F) = (((((dst_positive_code_fubini_actual_gridentryfirst) + (dst_positive_scale_fubini_actual_gridentryfirst)) * S ((dst_positive_code_fubini_actual_gridentryfirst) + (dst_positive_scale_fubini_actual_gridentryfirst)) + ((dst_positive_scale_fubini_actual_gridentryfirst) + (dst_positive_scale_fubini_actual_gridentryfirst))) + (((dst_negative_code_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)) * S ((dst_negative_code_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)) + ((dst_negative_scale_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)))) * S ((((dst_positive_code_fubini_actual_gridentryfirst) + (dst_positive_scale_fubini_actual_gridentryfirst)) * S ((dst_positive_code_fubini_actual_gridentryfirst) + (dst_positive_scale_fubini_actual_gridentryfirst)) + ((dst_positive_scale_fubini_actual_gridentryfirst) + (dst_positive_scale_fubini_actual_gridentryfirst))) + (((dst_negative_code_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)) * S ((dst_negative_code_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)) + ((dst_negative_scale_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)))) + ((((dst_negative_code_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)) * S ((dst_negative_code_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)) + ((dst_negative_scale_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst))) + (((dst_negative_code_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)) * S ((dst_negative_code_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)) + ((dst_negative_scale_fubini_actual_gridentryfirst) + (dst_negative_scale_fubini_actual_gridentryfirst)))))) /\ (((((exists ff_h_pvs_fubini_actual_gridentryfirstpositive. ff_h_pvs_fubini_actual_gridentryfirstpositive + S (dst_positive_fubini_actual_gridentryfirst) = S ((S (dfg_grid_row_fubini_actual_grid)) * dst_positive_scale_fubini_actual_gridentryfirst)) /\ exists ff_q_pvs_fubini_actual_gridentryfirstpositive. dst_positive_code_fubini_actual_gridentryfirst = ff_q_pvs_fubini_actual_gridentryfirstpositive * S ((S (dfg_grid_row_fubini_actual_grid)) * dst_positive_scale_fubini_actual_gridentryfirst) + (dst_positive_fubini_actual_gridentryfirst))) /\ (((((exists ff_h_pvs_fubini_actual_gridentryfirstnegative. ff_h_pvs_fubini_actual_gridentryfirstnegative + S (dst_negative_fubini_actual_gridentryfirst) = S ((S (dfg_grid_row_fubini_actual_grid)) * dst_negative_scale_fubini_actual_gridentryfirst)) /\ exists ff_q_pvs_fubini_actual_gridentryfirstnegative. dst_negative_code_fubini_actual_gridentryfirst = ff_q_pvs_fubini_actual_gridentryfirstnegative * S ((S (dfg_grid_row_fubini_actual_grid)) * dst_negative_scale_fubini_actual_gridentryfirst) + (dst_negative_fubini_actual_gridentryfirst))) /\ (exists ge_balance_positive_fubini_actual_gridentryfirstvalue ge_balance_negative_fubini_actual_gridentryfirstvalue. (((((dfg_first_fubini_actual_gridentry) = 2 * (ge_balance_positive_fubini_actual_gridentryfirstvalue) /\ (ge_balance_negative_fubini_actual_gridentryfirstvalue) = 0) \/ exists ge_signed_half_fubini_actual_gridentryfirstvaluedecode. (((dfg_first_fubini_actual_gridentry) = 2 * ge_signed_half_fubini_actual_gridentryfirstvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_gridentryfirstvalue) = 0) /\ (ge_balance_negative_fubini_actual_gridentryfirstvalue) = S ge_signed_half_fubini_actual_gridentryfirstvaluedecode))) /\ ((dst_positive_fubini_actual_gridentryfirst) + ge_balance_negative_fubini_actual_gridentryfirstvalue = (dst_negative_fubini_actual_gridentryfirst) + ge_balance_positive_fubini_actual_gridentryfirstvalue))))))))) /\ (((exists dst_positive_code_fubini_actual_gridentrylast dst_positive_scale_fubini_actual_gridentrylast dst_negative_code_fubini_actual_gridentrylast dst_negative_scale_fubini_actual_gridentrylast dst_positive_fubini_actual_gridentrylast dst_negative_fubini_actual_gridentrylast. (((H) = (((((dst_positive_code_fubini_actual_gridentrylast) + (dst_positive_scale_fubini_actual_gridentrylast)) * S ((dst_positive_code_fubini_actual_gridentrylast) + (dst_positive_scale_fubini_actual_gridentrylast)) + ((dst_positive_scale_fubini_actual_gridentrylast) + (dst_positive_scale_fubini_actual_gridentrylast))) + (((dst_negative_code_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)) * S ((dst_negative_code_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)) + ((dst_negative_scale_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)))) * S ((((dst_positive_code_fubini_actual_gridentrylast) + (dst_positive_scale_fubini_actual_gridentrylast)) * S ((dst_positive_code_fubini_actual_gridentrylast) + (dst_positive_scale_fubini_actual_gridentrylast)) + ((dst_positive_scale_fubini_actual_gridentrylast) + (dst_positive_scale_fubini_actual_gridentrylast))) + (((dst_negative_code_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)) * S ((dst_negative_code_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)) + ((dst_negative_scale_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)))) + ((((dst_negative_code_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)) * S ((dst_negative_code_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)) + ((dst_negative_scale_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast))) + (((dst_negative_code_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)) * S ((dst_negative_code_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)) + ((dst_negative_scale_fubini_actual_gridentrylast) + (dst_negative_scale_fubini_actual_gridentrylast)))))) /\ (((((exists ff_h_pvs_fubini_actual_gridentrylastpositive. ff_h_pvs_fubini_actual_gridentrylastpositive + S (dst_positive_fubini_actual_gridentrylast) = S ((S (dfg_grid_column_fubini_actual_grid)) * dst_positive_scale_fubini_actual_gridentrylast)) /\ exists ff_q_pvs_fubini_actual_gridentrylastpositive. dst_positive_code_fubini_actual_gridentrylast = ff_q_pvs_fubini_actual_gridentrylastpositive * S ((S (dfg_grid_column_fubini_actual_grid)) * dst_positive_scale_fubini_actual_gridentrylast) + (dst_positive_fubini_actual_gridentrylast))) /\ (((((exists ff_h_pvs_fubini_actual_gridentrylastnegative. ff_h_pvs_fubini_actual_gridentrylastnegative + S (dst_negative_fubini_actual_gridentrylast) = S ((S (dfg_grid_column_fubini_actual_grid)) * dst_negative_scale_fubini_actual_gridentrylast)) /\ exists ff_q_pvs_fubini_actual_gridentrylastnegative. dst_negative_code_fubini_actual_gridentrylast = ff_q_pvs_fubini_actual_gridentrylastnegative * S ((S (dfg_grid_column_fubini_actual_grid)) * dst_negative_scale_fubini_actual_gridentrylast) + (dst_negative_fubini_actual_gridentrylast))) /\ (exists ge_balance_positive_fubini_actual_gridentrylastvalue ge_balance_negative_fubini_actual_gridentrylastvalue. (((((dfg_last_fubini_actual_gridentry) = 2 * (ge_balance_positive_fubini_actual_gridentrylastvalue) /\ (ge_balance_negative_fubini_actual_gridentrylastvalue) = 0) \/ exists ge_signed_half_fubini_actual_gridentrylastvaluedecode. (((dfg_last_fubini_actual_gridentry) = 2 * ge_signed_half_fubini_actual_gridentrylastvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_gridentrylastvalue) = 0) /\ (ge_balance_negative_fubini_actual_gridentrylastvalue) = S ge_signed_half_fubini_actual_gridentrylastvaluedecode))) /\ ((dst_positive_fubini_actual_gridentrylast) + ge_balance_negative_fubini_actual_gridentrylastvalue = (dst_negative_fubini_actual_gridentrylast) + ge_balance_positive_fubini_actual_gridentrylastvalue))))))))) /\ (((exists dst_positive_code_fubini_actual_gridentrymiddle dst_positive_scale_fubini_actual_gridentrymiddle dst_negative_code_fubini_actual_gridentrymiddle dst_negative_scale_fubini_actual_gridentrymiddle dst_positive_fubini_actual_gridentrymiddle dst_negative_fubini_actual_gridentrymiddle. (((G) = (((((dst_positive_code_fubini_actual_gridentrymiddle) + (dst_positive_scale_fubini_actual_gridentrymiddle)) * S ((dst_positive_code_fubini_actual_gridentrymiddle) + (dst_positive_scale_fubini_actual_gridentrymiddle)) + ((dst_positive_scale_fubini_actual_gridentrymiddle) + (dst_positive_scale_fubini_actual_gridentrymiddle))) + (((dst_negative_code_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)) * S ((dst_negative_code_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)) + ((dst_negative_scale_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)))) * S ((((dst_positive_code_fubini_actual_gridentrymiddle) + (dst_positive_scale_fubini_actual_gridentrymiddle)) * S ((dst_positive_code_fubini_actual_gridentrymiddle) + (dst_positive_scale_fubini_actual_gridentrymiddle)) + ((dst_positive_scale_fubini_actual_gridentrymiddle) + (dst_positive_scale_fubini_actual_gridentrymiddle))) + (((dst_negative_code_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)) * S ((dst_negative_code_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)) + ((dst_negative_scale_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)))) + ((((dst_negative_code_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)) * S ((dst_negative_code_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)) + ((dst_negative_scale_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle))) + (((dst_negative_code_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)) * S ((dst_negative_code_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)) + ((dst_negative_scale_fubini_actual_gridentrymiddle) + (dst_negative_scale_fubini_actual_gridentrymiddle)))))) /\ (((((exists ff_h_pvs_fubini_actual_gridentrymiddlepositive. ff_h_pvs_fubini_actual_gridentrymiddlepositive + S (dst_positive_fubini_actual_gridentrymiddle) = S ((S (dfg_middle_fubini_actual_gridentry)) * dst_positive_scale_fubini_actual_gridentrymiddle)) /\ exists ff_q_pvs_fubini_actual_gridentrymiddlepositive. dst_positive_code_fubini_actual_gridentrymiddle = ff_q_pvs_fubini_actual_gridentrymiddlepositive * S ((S (dfg_middle_fubini_actual_gridentry)) * dst_positive_scale_fubini_actual_gridentrymiddle) + (dst_positive_fubini_actual_gridentrymiddle))) /\ (((((exists ff_h_pvs_fubini_actual_gridentrymiddlenegative. ff_h_pvs_fubini_actual_gridentrymiddlenegative + S (dst_negative_fubini_actual_gridentrymiddle) = S ((S (dfg_middle_fubini_actual_gridentry)) * dst_negative_scale_fubini_actual_gridentrymiddle)) /\ exists ff_q_pvs_fubini_actual_gridentrymiddlenegative. dst_negative_code_fubini_actual_gridentrymiddle = ff_q_pvs_fubini_actual_gridentrymiddlenegative * S ((S (dfg_middle_fubini_actual_gridentry)) * dst_negative_scale_fubini_actual_gridentrymiddle) + (dst_negative_fubini_actual_gridentrymiddle))) /\ (exists ge_balance_positive_fubini_actual_gridentrymiddlevalue ge_balance_negative_fubini_actual_gridentrymiddlevalue. (((((dfg_value_fubini_actual_gridentry) = 2 * (ge_balance_positive_fubini_actual_gridentrymiddlevalue) /\ (ge_balance_negative_fubini_actual_gridentrymiddlevalue) = 0) \/ exists ge_signed_half_fubini_actual_gridentrymiddlevaluedecode. (((dfg_value_fubini_actual_gridentry) = 2 * ge_signed_half_fubini_actual_gridentrymiddlevaluedecode + 1 /\ (ge_balance_positive_fubini_actual_gridentrymiddlevalue) = 0) /\ (ge_balance_negative_fubini_actual_gridentrymiddlevalue) = S ge_signed_half_fubini_actual_gridentrymiddlevaluedecode))) /\ ((dst_positive_fubini_actual_gridentrymiddle) + ge_balance_negative_fubini_actual_gridentrymiddlevalue = (dst_negative_fubini_actual_gridentrymiddle) + ge_balance_positive_fubini_actual_gridentrymiddlevalue))))))))) /\ (exists dfg_inner_fubini_actual_gridentryproduct. ((exists sto_ap_fubini_actual_gridentryproductinner sto_an_fubini_actual_gridentryproductinner sto_bp_fubini_actual_gridentryproductinner sto_bn_fubini_actual_gridentryproductinner sto_cp_fubini_actual_gridentryproductinner sto_cn_fubini_actual_gridentryproductinner. (((((dfg_last_fubini_actual_gridentry) = 2 * (sto_ap_fubini_actual_gridentryproductinner) /\ (sto_an_fubini_actual_gridentryproductinner) = 0) \/ exists ge_signed_half_fubini_actual_gridentryproductinnerleft. (((dfg_last_fubini_actual_gridentry) = 2 * ge_signed_half_fubini_actual_gridentryproductinnerleft + 1 /\ (sto_ap_fubini_actual_gridentryproductinner) = 0) /\ (sto_an_fubini_actual_gridentryproductinner) = S ge_signed_half_fubini_actual_gridentryproductinnerleft))) /\ ((((((dfg_value_fubini_actual_gridentry) = 2 * (sto_bp_fubini_actual_gridentryproductinner) /\ (sto_bn_fubini_actual_gridentryproductinner) = 0) \/ exists ge_signed_half_fubini_actual_gridentryproductinnerright. (((dfg_value_fubini_actual_gridentry) = 2 * ge_signed_half_fubini_actual_gridentryproductinnerright + 1 /\ (sto_bp_fubini_actual_gridentryproductinner) = 0) /\ (sto_bn_fubini_actual_gridentryproductinner) = S ge_signed_half_fubini_actual_gridentryproductinnerright))) /\ ((((((dfg_inner_fubini_actual_gridentryproduct) = 2 * (sto_cp_fubini_actual_gridentryproductinner) /\ (sto_cn_fubini_actual_gridentryproductinner) = 0) \/ exists ge_signed_half_fubini_actual_gridentryproductinneroutput. (((dfg_inner_fubini_actual_gridentryproduct) = 2 * ge_signed_half_fubini_actual_gridentryproductinneroutput + 1 /\ (sto_cp_fubini_actual_gridentryproductinner) = 0) /\ (sto_cn_fubini_actual_gridentryproductinner) = S ge_signed_half_fubini_actual_gridentryproductinneroutput))) /\ ((sto_ap_fubini_actual_gridentryproductinner * sto_bp_fubini_actual_gridentryproductinner + sto_an_fubini_actual_gridentryproductinner * sto_bn_fubini_actual_gridentryproductinner) + sto_cn_fubini_actual_gridentryproductinner = (sto_ap_fubini_actual_gridentryproductinner * sto_bn_fubini_actual_gridentryproductinner + sto_an_fubini_actual_gridentryproductinner * sto_bp_fubini_actual_gridentryproductinner) + sto_cp_fubini_actual_gridentryproductinner))))))) /\ (exists sto_ap_fubini_actual_gridentryproductouter sto_an_fubini_actual_gridentryproductouter sto_bp_fubini_actual_gridentryproductouter sto_bn_fubini_actual_gridentryproductouter sto_cp_fubini_actual_gridentryproductouter sto_cn_fubini_actual_gridentryproductouter. (((((dfg_first_fubini_actual_gridentry) = 2 * (sto_ap_fubini_actual_gridentryproductouter) /\ (sto_an_fubini_actual_gridentryproductouter) = 0) \/ exists ge_signed_half_fubini_actual_gridentryproductouterleft. (((dfg_first_fubini_actual_gridentry) = 2 * ge_signed_half_fubini_actual_gridentryproductouterleft + 1 /\ (sto_ap_fubini_actual_gridentryproductouter) = 0) /\ (sto_an_fubini_actual_gridentryproductouter) = S ge_signed_half_fubini_actual_gridentryproductouterleft))) /\ ((((((dfg_inner_fubini_actual_gridentryproduct) = 2 * (sto_bp_fubini_actual_gridentryproductouter) /\ (sto_bn_fubini_actual_gridentryproductouter) = 0) \/ exists ge_signed_half_fubini_actual_gridentryproductouterright. (((dfg_inner_fubini_actual_gridentryproduct) = 2 * ge_signed_half_fubini_actual_gridentryproductouterright + 1 /\ (sto_bp_fubini_actual_gridentryproductouter) = 0) /\ (sto_bn_fubini_actual_gridentryproductouter) = S ge_signed_half_fubini_actual_gridentryproductouterright))) /\ ((((((dfg_grid_value_fubini_actual_grid) = 2 * (sto_cp_fubini_actual_gridentryproductouter) /\ (sto_cn_fubini_actual_gridentryproductouter) = 0) \/ exists ge_signed_half_fubini_actual_gridentryproductouteroutput. (((dfg_grid_value_fubini_actual_grid) = 2 * ge_signed_half_fubini_actual_gridentryproductouteroutput + 1 /\ (sto_cp_fubini_actual_gridentryproductouter) = 0) /\ (sto_cn_fubini_actual_gridentryproductouter) = S ge_signed_half_fubini_actual_gridentryproductouteroutput))) /\ ((sto_ap_fubini_actual_gridentryproductouter * sto_bp_fubini_actual_gridentryproductouter + sto_an_fubini_actual_gridentryproductouter * sto_bn_fubini_actual_gridentryproductouter) + sto_cn_fubini_actual_gridentryproductouter = (sto_ap_fubini_actual_gridentryproductouter * sto_bn_fubini_actual_gridentryproductouter + sto_an_fubini_actual_gridentryproductouter * sto_bp_fubini_actual_gridentryproductouter) + sto_cp_fubini_actual_gridentryproductouter))))))))))))))))))))) \/ ((((dfg_grid_row_fubini_actual_grid)=0 \/ ((dfg_grid_column_fubini_actual_grid)=0 \/ ~(exists pvs_factor_fubini_actual_gridentryomittednondivisor. (n) = ((dfg_grid_row_fubini_actual_grid)*(dfg_grid_column_fubini_actual_grid)) * pvs_factor_fubini_actual_gridentryomittednondivisor))) /\ ((dfg_grid_value_fubini_actual_grid)=0))))))) /\ (((((exists dst_positive_code_fubini_actual_sumsrowssource_table dst_positive_scale_fubini_actual_sumsrowssource_table dst_negative_code_fubini_actual_sumsrowssource_table dst_negative_scale_fubini_actual_sumsrowssource_table. (((T) = (((((dst_positive_code_fubini_actual_sumsrowssource_table) + (dst_positive_scale_fubini_actual_sumsrowssource_table)) * S ((dst_positive_code_fubini_actual_sumsrowssource_table) + (dst_positive_scale_fubini_actual_sumsrowssource_table)) + ((dst_positive_scale_fubini_actual_sumsrowssource_table) + (dst_positive_scale_fubini_actual_sumsrowssource_table))) + (((dst_negative_code_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)) * S ((dst_negative_code_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)) + ((dst_negative_scale_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)))) * S ((((dst_positive_code_fubini_actual_sumsrowssource_table) + (dst_positive_scale_fubini_actual_sumsrowssource_table)) * S ((dst_positive_code_fubini_actual_sumsrowssource_table) + (dst_positive_scale_fubini_actual_sumsrowssource_table)) + ((dst_positive_scale_fubini_actual_sumsrowssource_table) + (dst_positive_scale_fubini_actual_sumsrowssource_table))) + (((dst_negative_code_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)) * S ((dst_negative_code_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)) + ((dst_negative_scale_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)))) + ((((dst_negative_code_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)) * S ((dst_negative_code_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)) + ((dst_negative_scale_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table))) + (((dst_negative_code_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)) * S ((dst_negative_code_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)) + ((dst_negative_scale_fubini_actual_sumsrowssource_table) + (dst_negative_scale_fubini_actual_sumsrowssource_table)))))) /\ (forall dst_index_fubini_actual_sumsrowssource_table. (exists pvs_le_gap_fubini_actual_sumsrowssource_tabledomain. pvs_le_gap_fubini_actual_sumsrowssource_tabledomain + (dst_index_fubini_actual_sumsrowssource_table) = (0)) -> exists dst_positive_fubini_actual_sumsrowssource_table dst_negative_fubini_actual_sumsrowssource_table dst_value_fubini_actual_sumsrowssource_table. ((((exists ff_h_pvs_fubini_actual_sumsrowssource_tableentrypositive. ff_h_pvs_fubini_actual_sumsrowssource_tableentrypositive + S (dst_positive_fubini_actual_sumsrowssource_table) = S ((S (dst_index_fubini_actual_sumsrowssource_table)) * dst_positive_scale_fubini_actual_sumsrowssource_table)) /\ exists ff_q_pvs_fubini_actual_sumsrowssource_tableentrypositive. dst_positive_code_fubini_actual_sumsrowssource_table = ff_q_pvs_fubini_actual_sumsrowssource_tableentrypositive * S ((S (dst_index_fubini_actual_sumsrowssource_table)) * dst_positive_scale_fubini_actual_sumsrowssource_table) + (dst_positive_fubini_actual_sumsrowssource_table))) /\ (((((exists ff_h_pvs_fubini_actual_sumsrowssource_tableentrynegative. ff_h_pvs_fubini_actual_sumsrowssource_tableentrynegative + S (dst_negative_fubini_actual_sumsrowssource_table) = S ((S (dst_index_fubini_actual_sumsrowssource_table)) * dst_negative_scale_fubini_actual_sumsrowssource_table)) /\ exists ff_q_pvs_fubini_actual_sumsrowssource_tableentrynegative. dst_negative_code_fubini_actual_sumsrowssource_table = ff_q_pvs_fubini_actual_sumsrowssource_tableentrynegative * S ((S (dst_index_fubini_actual_sumsrowssource_table)) * dst_negative_scale_fubini_actual_sumsrowssource_table) + (dst_negative_fubini_actual_sumsrowssource_table))) /\ (exists ge_balance_positive_fubini_actual_sumsrowssource_tableentryvalue ge_balance_negative_fubini_actual_sumsrowssource_tableentryvalue. (((((dst_value_fubini_actual_sumsrowssource_table) = 2 * (ge_balance_positive_fubini_actual_sumsrowssource_tableentryvalue) /\ (ge_balance_negative_fubini_actual_sumsrowssource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumsrowssource_tableentryvaluedecode. (((dst_value_fubini_actual_sumsrowssource_table) = 2 * ge_signed_half_fubini_actual_sumsrowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumsrowssource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumsrowssource_tableentryvalue) = S ge_signed_half_fubini_actual_sumsrowssource_tableentryvaluedecode))) /\ ((dst_positive_fubini_actual_sumsrowssource_table) + ge_balance_negative_fubini_actual_sumsrowssource_tableentryvalue = (dst_negative_fubini_actual_sumsrowssource_table) + ge_balance_positive_fubini_actual_sumsrowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_actual_sumsrowsrow_table dst_positive_scale_fubini_actual_sumsrowsrow_table dst_negative_code_fubini_actual_sumsrowsrow_table dst_negative_scale_fubini_actual_sumsrowsrow_table. (((R) = (((((dst_positive_code_fubini_actual_sumsrowsrow_table) + (dst_positive_scale_fubini_actual_sumsrowsrow_table)) * S ((dst_positive_code_fubini_actual_sumsrowsrow_table) + (dst_positive_scale_fubini_actual_sumsrowsrow_table)) + ((dst_positive_scale_fubini_actual_sumsrowsrow_table) + (dst_positive_scale_fubini_actual_sumsrowsrow_table))) + (((dst_negative_code_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)))) * S ((((dst_positive_code_fubini_actual_sumsrowsrow_table) + (dst_positive_scale_fubini_actual_sumsrowsrow_table)) * S ((dst_positive_code_fubini_actual_sumsrowsrow_table) + (dst_positive_scale_fubini_actual_sumsrowsrow_table)) + ((dst_positive_scale_fubini_actual_sumsrowsrow_table) + (dst_positive_scale_fubini_actual_sumsrowsrow_table))) + (((dst_negative_code_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)))) + ((((dst_negative_code_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table))) + (((dst_negative_code_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrow_table) + (dst_negative_scale_fubini_actual_sumsrowsrow_table)))))) /\ (forall dst_index_fubini_actual_sumsrowsrow_table. (exists pvs_le_gap_fubini_actual_sumsrowsrow_tabledomain. pvs_le_gap_fubini_actual_sumsrowsrow_tabledomain + (dst_index_fubini_actual_sumsrowsrow_table) = (S n)) -> exists dst_positive_fubini_actual_sumsrowsrow_table dst_negative_fubini_actual_sumsrowsrow_table dst_value_fubini_actual_sumsrowsrow_table. ((((exists ff_h_pvs_fubini_actual_sumsrowsrow_tableentrypositive. ff_h_pvs_fubini_actual_sumsrowsrow_tableentrypositive + S (dst_positive_fubini_actual_sumsrowsrow_table) = S ((S (dst_index_fubini_actual_sumsrowsrow_table)) * dst_positive_scale_fubini_actual_sumsrowsrow_table)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrow_tableentrypositive. dst_positive_code_fubini_actual_sumsrowsrow_table = ff_q_pvs_fubini_actual_sumsrowsrow_tableentrypositive * S ((S (dst_index_fubini_actual_sumsrowsrow_table)) * dst_positive_scale_fubini_actual_sumsrowsrow_table) + (dst_positive_fubini_actual_sumsrowsrow_table))) /\ (((((exists ff_h_pvs_fubini_actual_sumsrowsrow_tableentrynegative. ff_h_pvs_fubini_actual_sumsrowsrow_tableentrynegative + S (dst_negative_fubini_actual_sumsrowsrow_table) = S ((S (dst_index_fubini_actual_sumsrowsrow_table)) * dst_negative_scale_fubini_actual_sumsrowsrow_table)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrow_tableentrynegative. dst_negative_code_fubini_actual_sumsrowsrow_table = ff_q_pvs_fubini_actual_sumsrowsrow_tableentrynegative * S ((S (dst_index_fubini_actual_sumsrowsrow_table)) * dst_negative_scale_fubini_actual_sumsrowsrow_table) + (dst_negative_fubini_actual_sumsrowsrow_table))) /\ (exists ge_balance_positive_fubini_actual_sumsrowsrow_tableentryvalue ge_balance_negative_fubini_actual_sumsrowsrow_tableentryvalue. (((((dst_value_fubini_actual_sumsrowsrow_table) = 2 * (ge_balance_positive_fubini_actual_sumsrowsrow_tableentryvalue) /\ (ge_balance_negative_fubini_actual_sumsrowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumsrowsrow_tableentryvaluedecode. (((dst_value_fubini_actual_sumsrowsrow_table) = 2 * ge_signed_half_fubini_actual_sumsrowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumsrowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumsrowsrow_tableentryvalue) = S ge_signed_half_fubini_actual_sumsrowsrow_tableentryvaluedecode))) /\ ((dst_positive_fubini_actual_sumsrowsrow_table) + ge_balance_negative_fubini_actual_sumsrowsrow_tableentryvalue = (dst_negative_fubini_actual_sumsrowsrow_table) + ge_balance_positive_fubini_actual_sumsrowsrow_tableentryvalue))))))))) /\ (forall srt_index_fubini_actual_sumsrows. (exists pvs_gap_fubini_actual_sumsrowsbound. pvs_gap_fubini_actual_sumsrowsbound + S (srt_index_fubini_actual_sumsrows) = (S n)) -> exists srt_value_fubini_actual_sumsrows. (((exists dst_positive_code_fubini_actual_sumsrowsrowentry dst_positive_scale_fubini_actual_sumsrowsrowentry dst_negative_code_fubini_actual_sumsrowsrowentry dst_negative_scale_fubini_actual_sumsrowsrowentry dst_positive_fubini_actual_sumsrowsrowentry dst_negative_fubini_actual_sumsrowsrowentry. (((R) = (((((dst_positive_code_fubini_actual_sumsrowsrowentry) + (dst_positive_scale_fubini_actual_sumsrowsrowentry)) * S ((dst_positive_code_fubini_actual_sumsrowsrowentry) + (dst_positive_scale_fubini_actual_sumsrowsrowentry)) + ((dst_positive_scale_fubini_actual_sumsrowsrowentry) + (dst_positive_scale_fubini_actual_sumsrowsrowentry))) + (((dst_negative_code_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)) * S ((dst_negative_code_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)) + ((dst_negative_scale_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)))) * S ((((dst_positive_code_fubini_actual_sumsrowsrowentry) + (dst_positive_scale_fubini_actual_sumsrowsrowentry)) * S ((dst_positive_code_fubini_actual_sumsrowsrowentry) + (dst_positive_scale_fubini_actual_sumsrowsrowentry)) + ((dst_positive_scale_fubini_actual_sumsrowsrowentry) + (dst_positive_scale_fubini_actual_sumsrowsrowentry))) + (((dst_negative_code_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)) * S ((dst_negative_code_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)) + ((dst_negative_scale_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)))) + ((((dst_negative_code_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)) * S ((dst_negative_code_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)) + ((dst_negative_scale_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry))) + (((dst_negative_code_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)) * S ((dst_negative_code_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)) + ((dst_negative_scale_fubini_actual_sumsrowsrowentry) + (dst_negative_scale_fubini_actual_sumsrowsrowentry)))))) /\ (((((exists ff_h_pvs_fubini_actual_sumsrowsrowentrypositive. ff_h_pvs_fubini_actual_sumsrowsrowentrypositive + S (dst_positive_fubini_actual_sumsrowsrowentry) = S ((S (srt_index_fubini_actual_sumsrows)) * dst_positive_scale_fubini_actual_sumsrowsrowentry)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrowentrypositive. dst_positive_code_fubini_actual_sumsrowsrowentry = ff_q_pvs_fubini_actual_sumsrowsrowentrypositive * S ((S (srt_index_fubini_actual_sumsrows)) * dst_positive_scale_fubini_actual_sumsrowsrowentry) + (dst_positive_fubini_actual_sumsrowsrowentry))) /\ (((((exists ff_h_pvs_fubini_actual_sumsrowsrowentrynegative. ff_h_pvs_fubini_actual_sumsrowsrowentrynegative + S (dst_negative_fubini_actual_sumsrowsrowentry) = S ((S (srt_index_fubini_actual_sumsrows)) * dst_negative_scale_fubini_actual_sumsrowsrowentry)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrowentrynegative. dst_negative_code_fubini_actual_sumsrowsrowentry = ff_q_pvs_fubini_actual_sumsrowsrowentrynegative * S ((S (srt_index_fubini_actual_sumsrows)) * dst_negative_scale_fubini_actual_sumsrowsrowentry) + (dst_negative_fubini_actual_sumsrowsrowentry))) /\ (exists ge_balance_positive_fubini_actual_sumsrowsrowentryvalue ge_balance_negative_fubini_actual_sumsrowsrowentryvalue. (((((srt_value_fubini_actual_sumsrows) = 2 * (ge_balance_positive_fubini_actual_sumsrowsrowentryvalue) /\ (ge_balance_negative_fubini_actual_sumsrowsrowentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumsrowsrowentryvaluedecode. (((srt_value_fubini_actual_sumsrows) = 2 * ge_signed_half_fubini_actual_sumsrowsrowentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumsrowsrowentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumsrowsrowentryvalue) = S ge_signed_half_fubini_actual_sumsrowsrowentryvaluedecode))) /\ ((dst_positive_fubini_actual_sumsrowsrowentry) + ge_balance_negative_fubini_actual_sumsrowsrowentryvalue = (dst_negative_fubini_actual_sumsrowsrowentry) + ge_balance_positive_fubini_actual_sumsrowsrowentryvalue))))))))) /\ (exists srs_slice_fubini_actual_sumsrowsrowrow_sum. ((((exists dst_positive_code_fubini_actual_sumsrowsrowrow_sumslicesource_table dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table dst_negative_code_fubini_actual_sumsrowsrowrow_sumslicesource_table dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table. (((T) = (((((dst_positive_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_fubini_actual_sumsrowsrowrow_sumslicesource_table. (exists pvs_le_gap_fubini_actual_sumsrowsrowrow_sumslicesource_tabledomain. pvs_le_gap_fubini_actual_sumsrowsrowrow_sumslicesource_tabledomain + (dst_index_fubini_actual_sumsrowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_fubini_actual_sumsrowsrowrow_sumslicesource_table dst_negative_fubini_actual_sumsrowsrowrow_sumslicesource_table dst_value_fubini_actual_sumsrowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_fubini_actual_sumsrowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_fubini_actual_sumsrowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_fubini_actual_sumsrowsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_actual_sumsrowsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_fubini_actual_sumsrowsrowrow_sumslicesource_table = ff_q_pvs_fubini_actual_sumsrowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_fubini_actual_sumsrowsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_positive_fubini_actual_sumsrowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_fubini_actual_sumsrowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_fubini_actual_sumsrowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_fubini_actual_sumsrowsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_actual_sumsrowsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_fubini_actual_sumsrowsrowrow_sumslicesource_table = ff_q_pvs_fubini_actual_sumsrowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_fubini_actual_sumsrowsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_actual_sumsrowsrowrow_sumslicesource_table) + (dst_negative_fubini_actual_sumsrowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_fubini_actual_sumsrowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_fubini_actual_sumsrowsrowrow_sumslicesource_table) = 2 * ge_signed_half_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_fubini_actual_sumsrowsrowrow_sumslicesource_table) + ge_balance_negative_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvalue = (dst_negative_fubini_actual_sumsrowsrowrow_sumslicesource_table) + ge_balance_positive_fubini_actual_sumsrowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table. (((srs_slice_fubini_actual_sumsrowsrowrow_sum) = (((((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_fubini_actual_sumsrowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_fubini_actual_sumsrowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_fubini_actual_sumsrowsrowrow_sumsliceoutput_tabledomain + (dst_index_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) = (S n)) -> exists dst_positive_fubini_actual_sumsrowsrowrow_sumsliceoutput_table dst_negative_fubini_actual_sumsrowsrowrow_sumsliceoutput_table dst_value_fubini_actual_sumsrowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_positive_fubini_actual_sumsrowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_fubini_actual_sumsrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + (dst_negative_fubini_actual_sumsrowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_fubini_actual_sumsrowsrowrow_sumsliceoutput_table) + ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_fubini_actual_sumsrowsrowrow_sumslice. (exists pvs_gap_fubini_actual_sumsrowsrowrow_sumslicebound. pvs_gap_fubini_actual_sumsrowsrowrow_sumslicebound + S (srs_index_fubini_actual_sumsrowsrowrow_sumslice) = (S n)) -> exists srs_value_fubini_actual_sumsrowsrowrow_sumslice. (((exists dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource dst_positive_fubini_actual_sumsrowsrowrow_sumsliceentrysource dst_negative_fubini_actual_sumsrowsrowrow_sumsliceentrysource. (((T) = (((((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceentrysourcepositive + S (dst_positive_fubini_actual_sumsrowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((S n) * (srt_index_fubini_actual_sumsrows)))) + ((1) * (srs_index_fubini_actual_sumsrowsrowrow_sumslice))))) * dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceentrysourcepositive. dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource = ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceentrysourcepositive * S ((S (((((0) + ((S n) * (srt_index_fubini_actual_sumsrows)))) + ((1) * (srs_index_fubini_actual_sumsrowsrowrow_sumslice))))) * dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_positive_fubini_actual_sumsrowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceentrysourcenegative + S (dst_negative_fubini_actual_sumsrowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((S n) * (srt_index_fubini_actual_sumsrows)))) + ((1) * (srs_index_fubini_actual_sumsrowsrowrow_sumslice))))) * dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceentrysourcenegative. dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentrysource = ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceentrysourcenegative * S ((S (((((0) + ((S n) * (srt_index_fubini_actual_sumsrows)))) + ((1) * (srs_index_fubini_actual_sumsrowsrowrow_sumslice))))) * dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + (dst_negative_fubini_actual_sumsrowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevalue ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevalue. (((((srs_value_fubini_actual_sumsrowsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_fubini_actual_sumsrowsrowrow_sumslice) = 2 * ge_signed_half_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevalue = (dst_negative_fubini_actual_sumsrowsrowrow_sumsliceentrysource) + ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput dst_positive_fubini_actual_sumsrowsrowrow_sumsliceentryoutput dst_negative_fubini_actual_sumsrowsrowrow_sumsliceentryoutput. (((srs_slice_fubini_actual_sumsrowsrowrow_sum) = (((((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceentryoutputpositive + S (dst_positive_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_actual_sumsrowsrowrow_sumslice)) * dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceentryoutputpositive. dst_positive_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_fubini_actual_sumsrowsrowrow_sumslice)) * dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_positive_fubini_actual_sumsrowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_fubini_actual_sumsrowsrowrow_sumsliceentryoutputnegative + S (dst_negative_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_actual_sumsrowsrowrow_sumslice)) * dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceentryoutputnegative. dst_negative_code_fubini_actual_sumsrowsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_actual_sumsrowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_fubini_actual_sumsrowsrowrow_sumslice)) * dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + (dst_negative_fubini_actual_sumsrowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvalue ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvalue. (((((srs_value_fubini_actual_sumsrowsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_fubini_actual_sumsrowsrowrow_sumslice) = 2 * ge_signed_half_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvalue = (dst_negative_fubini_actual_sumsrowsrowrow_sumsliceentryoutput) + ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_fubini_actual_sumsrowsrowrow_sumsum dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum dst_negative_code_fubini_actual_sumsrowsrowrow_sumsum dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum dst_positive_sum_fubini_actual_sumsrowsrowrow_sumsum dst_negative_sum_fubini_actual_sumsrowsrowrow_sumsum. (((srs_slice_fubini_actual_sumsrowsrowrow_sum) = (((((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum)) * S ((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum)) + ((dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)))) * S ((((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum)) * S ((dst_positive_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum)) + ((dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)))) + ((((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum))) + (((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_fubini_actual_sumsrowsrowrow_sumsumpositive fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumpositive. ((((exists fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_start. fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_start. fs_u_dst_fubini_actual_sumsrowsrowrow_sumsumpositive = fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_terminal. fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_fubini_actual_sumsrowsrowrow_sumsum) = S ((S (S n)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_terminal. fs_u_dst_fubini_actual_sumsrowsrowrow_sumsumpositive = fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_terminal * S ((S (S n)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumpositive) + (dst_positive_sum_fubini_actual_sumsrowsrowrow_sumsum))) /\ forall fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps = S n) -> exists fs_a_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps fs_r_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps fs_s_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum)) /\ exists fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_fubini_actual_sumsrowsrowrow_sumsum = fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_actual_sumsrowsrowrow_sumsum) + (fs_a_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_fubini_actual_sumsrowsrowrow_sumsumpositive = fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumpositive) + (fs_r_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_fubini_actual_sumsrowsrowrow_sumsumpositive = fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumpositive) + (fs_s_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps = fs_r_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps + fs_a_dst_fubini_actual_sumsrowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_actual_sumsrowsrowrow_sumsumnegative fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumnegative. ((((exists fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_start. fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_start. fs_u_dst_fubini_actual_sumsrowsrowrow_sumsumnegative = fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_terminal. fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_fubini_actual_sumsrowsrowrow_sumsum) = S ((S (S n)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_terminal. fs_u_dst_fubini_actual_sumsrowsrowrow_sumsumnegative = fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_terminal * S ((S (S n)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumnegative) + (dst_negative_sum_fubini_actual_sumsrowsrowrow_sumsum))) /\ forall fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps = S n) -> exists fs_a_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps fs_r_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps fs_s_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum)) /\ exists fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_fubini_actual_sumsrowsrowrow_sumsum = fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_actual_sumsrowsrowrow_sumsum) + (fs_a_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_fubini_actual_sumsrowsrowrow_sumsumnegative = fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumnegative) + (fs_r_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_fubini_actual_sumsrowsrowrow_sumsumnegative = fs_q_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_actual_sumsrowsrowrow_sumsumnegative) + (fs_s_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps = fs_r_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps + fs_a_dst_fubini_actual_sumsrowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsumresult ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsumresult. (((((srt_value_fubini_actual_sumsrows) = 2 * (ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsumresult) /\ (ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_fubini_actual_sumsrowsrowrow_sumsumresultdecode. (((srt_value_fubini_actual_sumsrows) = 2 * ge_signed_half_fubini_actual_sumsrowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsumresult) = S ge_signed_half_fubini_actual_sumsrowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_fubini_actual_sumsrowsrowrow_sumsum) + ge_balance_negative_fubini_actual_sumsrowsrowrow_sumsumresult = (dst_negative_sum_fubini_actual_sumsrowsrowrow_sumsum) + ge_balance_positive_fubini_actual_sumsrowsrowrow_sumsumresult)))))))))))))))))) /\ (((((exists dst_positive_code_fubini_actual_sumscolumnssource_table dst_positive_scale_fubini_actual_sumscolumnssource_table dst_negative_code_fubini_actual_sumscolumnssource_table dst_negative_scale_fubini_actual_sumscolumnssource_table. (((T) = (((((dst_positive_code_fubini_actual_sumscolumnssource_table) + (dst_positive_scale_fubini_actual_sumscolumnssource_table)) * S ((dst_positive_code_fubini_actual_sumscolumnssource_table) + (dst_positive_scale_fubini_actual_sumscolumnssource_table)) + ((dst_positive_scale_fubini_actual_sumscolumnssource_table) + (dst_positive_scale_fubini_actual_sumscolumnssource_table))) + (((dst_negative_code_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)) * S ((dst_negative_code_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)) + ((dst_negative_scale_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)))) * S ((((dst_positive_code_fubini_actual_sumscolumnssource_table) + (dst_positive_scale_fubini_actual_sumscolumnssource_table)) * S ((dst_positive_code_fubini_actual_sumscolumnssource_table) + (dst_positive_scale_fubini_actual_sumscolumnssource_table)) + ((dst_positive_scale_fubini_actual_sumscolumnssource_table) + (dst_positive_scale_fubini_actual_sumscolumnssource_table))) + (((dst_negative_code_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)) * S ((dst_negative_code_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)) + ((dst_negative_scale_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)))) + ((((dst_negative_code_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)) * S ((dst_negative_code_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)) + ((dst_negative_scale_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table))) + (((dst_negative_code_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)) * S ((dst_negative_code_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)) + ((dst_negative_scale_fubini_actual_sumscolumnssource_table) + (dst_negative_scale_fubini_actual_sumscolumnssource_table)))))) /\ (forall dst_index_fubini_actual_sumscolumnssource_table. (exists pvs_le_gap_fubini_actual_sumscolumnssource_tabledomain. pvs_le_gap_fubini_actual_sumscolumnssource_tabledomain + (dst_index_fubini_actual_sumscolumnssource_table) = (0)) -> exists dst_positive_fubini_actual_sumscolumnssource_table dst_negative_fubini_actual_sumscolumnssource_table dst_value_fubini_actual_sumscolumnssource_table. ((((exists ff_h_pvs_fubini_actual_sumscolumnssource_tableentrypositive. ff_h_pvs_fubini_actual_sumscolumnssource_tableentrypositive + S (dst_positive_fubini_actual_sumscolumnssource_table) = S ((S (dst_index_fubini_actual_sumscolumnssource_table)) * dst_positive_scale_fubini_actual_sumscolumnssource_table)) /\ exists ff_q_pvs_fubini_actual_sumscolumnssource_tableentrypositive. dst_positive_code_fubini_actual_sumscolumnssource_table = ff_q_pvs_fubini_actual_sumscolumnssource_tableentrypositive * S ((S (dst_index_fubini_actual_sumscolumnssource_table)) * dst_positive_scale_fubini_actual_sumscolumnssource_table) + (dst_positive_fubini_actual_sumscolumnssource_table))) /\ (((((exists ff_h_pvs_fubini_actual_sumscolumnssource_tableentrynegative. ff_h_pvs_fubini_actual_sumscolumnssource_tableentrynegative + S (dst_negative_fubini_actual_sumscolumnssource_table) = S ((S (dst_index_fubini_actual_sumscolumnssource_table)) * dst_negative_scale_fubini_actual_sumscolumnssource_table)) /\ exists ff_q_pvs_fubini_actual_sumscolumnssource_tableentrynegative. dst_negative_code_fubini_actual_sumscolumnssource_table = ff_q_pvs_fubini_actual_sumscolumnssource_tableentrynegative * S ((S (dst_index_fubini_actual_sumscolumnssource_table)) * dst_negative_scale_fubini_actual_sumscolumnssource_table) + (dst_negative_fubini_actual_sumscolumnssource_table))) /\ (exists ge_balance_positive_fubini_actual_sumscolumnssource_tableentryvalue ge_balance_negative_fubini_actual_sumscolumnssource_tableentryvalue. (((((dst_value_fubini_actual_sumscolumnssource_table) = 2 * (ge_balance_positive_fubini_actual_sumscolumnssource_tableentryvalue) /\ (ge_balance_negative_fubini_actual_sumscolumnssource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumscolumnssource_tableentryvaluedecode. (((dst_value_fubini_actual_sumscolumnssource_table) = 2 * ge_signed_half_fubini_actual_sumscolumnssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumscolumnssource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumscolumnssource_tableentryvalue) = S ge_signed_half_fubini_actual_sumscolumnssource_tableentryvaluedecode))) /\ ((dst_positive_fubini_actual_sumscolumnssource_table) + ge_balance_negative_fubini_actual_sumscolumnssource_tableentryvalue = (dst_negative_fubini_actual_sumscolumnssource_table) + ge_balance_positive_fubini_actual_sumscolumnssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_actual_sumscolumnsrow_table dst_positive_scale_fubini_actual_sumscolumnsrow_table dst_negative_code_fubini_actual_sumscolumnsrow_table dst_negative_scale_fubini_actual_sumscolumnsrow_table. (((C) = (((((dst_positive_code_fubini_actual_sumscolumnsrow_table) + (dst_positive_scale_fubini_actual_sumscolumnsrow_table)) * S ((dst_positive_code_fubini_actual_sumscolumnsrow_table) + (dst_positive_scale_fubini_actual_sumscolumnsrow_table)) + ((dst_positive_scale_fubini_actual_sumscolumnsrow_table) + (dst_positive_scale_fubini_actual_sumscolumnsrow_table))) + (((dst_negative_code_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)))) * S ((((dst_positive_code_fubini_actual_sumscolumnsrow_table) + (dst_positive_scale_fubini_actual_sumscolumnsrow_table)) * S ((dst_positive_code_fubini_actual_sumscolumnsrow_table) + (dst_positive_scale_fubini_actual_sumscolumnsrow_table)) + ((dst_positive_scale_fubini_actual_sumscolumnsrow_table) + (dst_positive_scale_fubini_actual_sumscolumnsrow_table))) + (((dst_negative_code_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)))) + ((((dst_negative_code_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table))) + (((dst_negative_code_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrow_table) + (dst_negative_scale_fubini_actual_sumscolumnsrow_table)))))) /\ (forall dst_index_fubini_actual_sumscolumnsrow_table. (exists pvs_le_gap_fubini_actual_sumscolumnsrow_tabledomain. pvs_le_gap_fubini_actual_sumscolumnsrow_tabledomain + (dst_index_fubini_actual_sumscolumnsrow_table) = (S n)) -> exists dst_positive_fubini_actual_sumscolumnsrow_table dst_negative_fubini_actual_sumscolumnsrow_table dst_value_fubini_actual_sumscolumnsrow_table. ((((exists ff_h_pvs_fubini_actual_sumscolumnsrow_tableentrypositive. ff_h_pvs_fubini_actual_sumscolumnsrow_tableentrypositive + S (dst_positive_fubini_actual_sumscolumnsrow_table) = S ((S (dst_index_fubini_actual_sumscolumnsrow_table)) * dst_positive_scale_fubini_actual_sumscolumnsrow_table)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrow_tableentrypositive. dst_positive_code_fubini_actual_sumscolumnsrow_table = ff_q_pvs_fubini_actual_sumscolumnsrow_tableentrypositive * S ((S (dst_index_fubini_actual_sumscolumnsrow_table)) * dst_positive_scale_fubini_actual_sumscolumnsrow_table) + (dst_positive_fubini_actual_sumscolumnsrow_table))) /\ (((((exists ff_h_pvs_fubini_actual_sumscolumnsrow_tableentrynegative. ff_h_pvs_fubini_actual_sumscolumnsrow_tableentrynegative + S (dst_negative_fubini_actual_sumscolumnsrow_table) = S ((S (dst_index_fubini_actual_sumscolumnsrow_table)) * dst_negative_scale_fubini_actual_sumscolumnsrow_table)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrow_tableentrynegative. dst_negative_code_fubini_actual_sumscolumnsrow_table = ff_q_pvs_fubini_actual_sumscolumnsrow_tableentrynegative * S ((S (dst_index_fubini_actual_sumscolumnsrow_table)) * dst_negative_scale_fubini_actual_sumscolumnsrow_table) + (dst_negative_fubini_actual_sumscolumnsrow_table))) /\ (exists ge_balance_positive_fubini_actual_sumscolumnsrow_tableentryvalue ge_balance_negative_fubini_actual_sumscolumnsrow_tableentryvalue. (((((dst_value_fubini_actual_sumscolumnsrow_table) = 2 * (ge_balance_positive_fubini_actual_sumscolumnsrow_tableentryvalue) /\ (ge_balance_negative_fubini_actual_sumscolumnsrow_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumscolumnsrow_tableentryvaluedecode. (((dst_value_fubini_actual_sumscolumnsrow_table) = 2 * ge_signed_half_fubini_actual_sumscolumnsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumscolumnsrow_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumscolumnsrow_tableentryvalue) = S ge_signed_half_fubini_actual_sumscolumnsrow_tableentryvaluedecode))) /\ ((dst_positive_fubini_actual_sumscolumnsrow_table) + ge_balance_negative_fubini_actual_sumscolumnsrow_tableentryvalue = (dst_negative_fubini_actual_sumscolumnsrow_table) + ge_balance_positive_fubini_actual_sumscolumnsrow_tableentryvalue))))))))) /\ (forall srt_index_fubini_actual_sumscolumns. (exists pvs_gap_fubini_actual_sumscolumnsbound. pvs_gap_fubini_actual_sumscolumnsbound + S (srt_index_fubini_actual_sumscolumns) = (S n)) -> exists srt_value_fubini_actual_sumscolumns. (((exists dst_positive_code_fubini_actual_sumscolumnsrowentry dst_positive_scale_fubini_actual_sumscolumnsrowentry dst_negative_code_fubini_actual_sumscolumnsrowentry dst_negative_scale_fubini_actual_sumscolumnsrowentry dst_positive_fubini_actual_sumscolumnsrowentry dst_negative_fubini_actual_sumscolumnsrowentry. (((C) = (((((dst_positive_code_fubini_actual_sumscolumnsrowentry) + (dst_positive_scale_fubini_actual_sumscolumnsrowentry)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowentry) + (dst_positive_scale_fubini_actual_sumscolumnsrowentry)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowentry) + (dst_positive_scale_fubini_actual_sumscolumnsrowentry))) + (((dst_negative_code_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)))) * S ((((dst_positive_code_fubini_actual_sumscolumnsrowentry) + (dst_positive_scale_fubini_actual_sumscolumnsrowentry)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowentry) + (dst_positive_scale_fubini_actual_sumscolumnsrowentry)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowentry) + (dst_positive_scale_fubini_actual_sumscolumnsrowentry))) + (((dst_negative_code_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)))) + ((((dst_negative_code_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry))) + (((dst_negative_code_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowentry) + (dst_negative_scale_fubini_actual_sumscolumnsrowentry)))))) /\ (((((exists ff_h_pvs_fubini_actual_sumscolumnsrowentrypositive. ff_h_pvs_fubini_actual_sumscolumnsrowentrypositive + S (dst_positive_fubini_actual_sumscolumnsrowentry) = S ((S (srt_index_fubini_actual_sumscolumns)) * dst_positive_scale_fubini_actual_sumscolumnsrowentry)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrowentrypositive. dst_positive_code_fubini_actual_sumscolumnsrowentry = ff_q_pvs_fubini_actual_sumscolumnsrowentrypositive * S ((S (srt_index_fubini_actual_sumscolumns)) * dst_positive_scale_fubini_actual_sumscolumnsrowentry) + (dst_positive_fubini_actual_sumscolumnsrowentry))) /\ (((((exists ff_h_pvs_fubini_actual_sumscolumnsrowentrynegative. ff_h_pvs_fubini_actual_sumscolumnsrowentrynegative + S (dst_negative_fubini_actual_sumscolumnsrowentry) = S ((S (srt_index_fubini_actual_sumscolumns)) * dst_negative_scale_fubini_actual_sumscolumnsrowentry)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrowentrynegative. dst_negative_code_fubini_actual_sumscolumnsrowentry = ff_q_pvs_fubini_actual_sumscolumnsrowentrynegative * S ((S (srt_index_fubini_actual_sumscolumns)) * dst_negative_scale_fubini_actual_sumscolumnsrowentry) + (dst_negative_fubini_actual_sumscolumnsrowentry))) /\ (exists ge_balance_positive_fubini_actual_sumscolumnsrowentryvalue ge_balance_negative_fubini_actual_sumscolumnsrowentryvalue. (((((srt_value_fubini_actual_sumscolumns) = 2 * (ge_balance_positive_fubini_actual_sumscolumnsrowentryvalue) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumscolumnsrowentryvaluedecode. (((srt_value_fubini_actual_sumscolumns) = 2 * ge_signed_half_fubini_actual_sumscolumnsrowentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumscolumnsrowentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowentryvalue) = S ge_signed_half_fubini_actual_sumscolumnsrowentryvaluedecode))) /\ ((dst_positive_fubini_actual_sumscolumnsrowentry) + ge_balance_negative_fubini_actual_sumscolumnsrowentryvalue = (dst_negative_fubini_actual_sumscolumnsrowentry) + ge_balance_positive_fubini_actual_sumscolumnsrowentryvalue))))))))) /\ (exists srs_slice_fubini_actual_sumscolumnsrowrow_sum. ((((exists dst_positive_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table dst_negative_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table. (((T) = (((((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)))) + ((((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)))))) /\ (forall dst_index_fubini_actual_sumscolumnsrowrow_sumslicesource_table. (exists pvs_le_gap_fubini_actual_sumscolumnsrowrow_sumslicesource_tabledomain. pvs_le_gap_fubini_actual_sumscolumnsrowrow_sumslicesource_tabledomain + (dst_index_fubini_actual_sumscolumnsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_fubini_actual_sumscolumnsrowrow_sumslicesource_table dst_negative_fubini_actual_sumscolumnsrowrow_sumslicesource_table dst_value_fubini_actual_sumscolumnsrowrow_sumslicesource_table. ((((exists ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentrypositive + S (dst_positive_fubini_actual_sumscolumnsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentrypositive. dst_positive_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table = ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_positive_fubini_actual_sumscolumnsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentrynegative + S (dst_negative_fubini_actual_sumscolumnsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentrynegative. dst_negative_code_fubini_actual_sumscolumnsrowrow_sumslicesource_table = ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_fubini_actual_sumscolumnsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + (dst_negative_fubini_actual_sumscolumnsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvalue ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvalue. (((((dst_value_fubini_actual_sumscolumnsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_fubini_actual_sumscolumnsrowrow_sumslicesource_table) = 2 * ge_signed_half_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvalue = (dst_negative_fubini_actual_sumscolumnsrowrow_sumslicesource_table) + ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table. (((srs_slice_fubini_actual_sumscolumnsrowrow_sum) = (((((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table. (exists pvs_le_gap_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tabledomain + (dst_index_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) = (S n)) -> exists dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table dst_value_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + (dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceoutput_table) + ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_fubini_actual_sumscolumnsrowrow_sumslice. (exists pvs_gap_fubini_actual_sumscolumnsrowrow_sumslicebound. pvs_gap_fubini_actual_sumscolumnsrowrow_sumslicebound + S (srs_index_fubini_actual_sumscolumnsrowrow_sumslice) = (S n)) -> exists srs_value_fubini_actual_sumscolumnsrowrow_sumslice. (((exists dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceentrysource dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceentrysource. (((T) = (((((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcepositive. ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcepositive + S (dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) = S ((S (((((0) + ((1) * (srt_index_fubini_actual_sumscolumns)))) + ((S n) * (srs_index_fubini_actual_sumscolumnsrowrow_sumslice))))) * dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcepositive. dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource = ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcepositive * S ((S (((((0) + ((1) * (srt_index_fubini_actual_sumscolumns)))) + ((S n) * (srs_index_fubini_actual_sumscolumnsrowrow_sumslice))))) * dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcenegative. ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcenegative + S (dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) = S ((S (((((0) + ((1) * (srt_index_fubini_actual_sumscolumns)))) + ((S n) * (srs_index_fubini_actual_sumscolumnsrowrow_sumslice))))) * dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcenegative. dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentrysource = ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcenegative * S ((S (((((0) + ((1) * (srt_index_fubini_actual_sumscolumns)))) + ((S n) * (srs_index_fubini_actual_sumscolumnsrowrow_sumslice))))) * dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + (dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevalue ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevalue. (((((srs_value_fubini_actual_sumscolumnsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_fubini_actual_sumscolumnsrowrow_sumslice) = 2 * ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevalue = (dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceentrysource) + ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput. (((srs_slice_fubini_actual_sumscolumnsrowrow_sum) = (((((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputpositive. ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputpositive + S (dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_actual_sumscolumnsrowrow_sumslice)) * dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputpositive. dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_fubini_actual_sumscolumnsrowrow_sumslice)) * dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputnegative. ff_h_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputnegative + S (dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_actual_sumscolumnsrowrow_sumslice)) * dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputnegative. dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_fubini_actual_sumscolumnsrowrow_sumslice)) * dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + (dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvalue ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvalue. (((((srs_value_fubini_actual_sumscolumnsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_fubini_actual_sumscolumnsrowrow_sumslice) = 2 * ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvalue = (dst_negative_fubini_actual_sumscolumnsrowrow_sumsliceentryoutput) + ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsum dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsum dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum dst_positive_sum_fubini_actual_sumscolumnsrowrow_sumsum dst_negative_sum_fubini_actual_sumscolumnsrowrow_sumsum. (((srs_slice_fubini_actual_sumscolumnsrowrow_sum) = (((((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)))) * S ((((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum)) * S ((dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum)) + ((dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)))) + ((((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum))) + (((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)) * S ((dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)) + ((dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum) + (dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)))))) /\ (((exists fs_u_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive. ((((exists fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_start. fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_start. fs_u_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive = fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_terminal. fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_fubini_actual_sumscolumnsrowrow_sumsum) = S ((S (S n)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_terminal. fs_u_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive = fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_terminal * S ((S (S n)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive) + (dst_positive_sum_fubini_actual_sumscolumnsrowrow_sumsum))) /\ forall fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps = S n) -> exists fs_a_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps fs_r_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps fs_s_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum)) /\ exists fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_fubini_actual_sumscolumnsrowrow_sumsum = fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_actual_sumscolumnsrowrow_sumsum) + (fs_a_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive = fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive) + (fs_r_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive = fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive) + (fs_s_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps = fs_r_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps + fs_a_dst_fubini_actual_sumscolumnsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative. ((((exists fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_start. fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_start. fs_u_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative = fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_terminal. fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_fubini_actual_sumscolumnsrowrow_sumsum) = S ((S (S n)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_terminal. fs_u_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative = fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_terminal * S ((S (S n)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative) + (dst_negative_sum_fubini_actual_sumscolumnsrowrow_sumsum))) /\ forall fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps = S n) -> exists fs_a_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps fs_r_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps fs_s_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum)) /\ exists fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_fubini_actual_sumscolumnsrowrow_sumsum = fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_actual_sumscolumnsrowrow_sumsum) + (fs_a_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative = fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative) + (fs_r_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative = fs_q_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative) + (fs_s_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps = fs_r_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps + fs_a_dst_fubini_actual_sumscolumnsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsumresult ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsumresult. (((((srt_value_fubini_actual_sumscolumns) = 2 * (ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsumresult) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsumresultdecode. (((srt_value_fubini_actual_sumscolumns) = 2 * ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsumresult) = S ge_signed_half_fubini_actual_sumscolumnsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_fubini_actual_sumscolumnsrowrow_sumsum) + ge_balance_negative_fubini_actual_sumscolumnsrowrow_sumsumresult = (dst_negative_sum_fubini_actual_sumscolumnsrowrow_sumsum) + ge_balance_positive_fubini_actual_sumscolumnsrowrow_sumsumresult)))))))))))))))))) /\ (((exists dst_positive_code_fubini_actual_sumsrow_total dst_positive_scale_fubini_actual_sumsrow_total dst_negative_code_fubini_actual_sumsrow_total dst_negative_scale_fubini_actual_sumsrow_total dst_positive_sum_fubini_actual_sumsrow_total dst_negative_sum_fubini_actual_sumsrow_total. (((R) = (((((dst_positive_code_fubini_actual_sumsrow_total) + (dst_positive_scale_fubini_actual_sumsrow_total)) * S ((dst_positive_code_fubini_actual_sumsrow_total) + (dst_positive_scale_fubini_actual_sumsrow_total)) + ((dst_positive_scale_fubini_actual_sumsrow_total) + (dst_positive_scale_fubini_actual_sumsrow_total))) + (((dst_negative_code_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)) * S ((dst_negative_code_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)) + ((dst_negative_scale_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)))) * S ((((dst_positive_code_fubini_actual_sumsrow_total) + (dst_positive_scale_fubini_actual_sumsrow_total)) * S ((dst_positive_code_fubini_actual_sumsrow_total) + (dst_positive_scale_fubini_actual_sumsrow_total)) + ((dst_positive_scale_fubini_actual_sumsrow_total) + (dst_positive_scale_fubini_actual_sumsrow_total))) + (((dst_negative_code_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)) * S ((dst_negative_code_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)) + ((dst_negative_scale_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)))) + ((((dst_negative_code_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)) * S ((dst_negative_code_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)) + ((dst_negative_scale_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total))) + (((dst_negative_code_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)) * S ((dst_negative_code_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)) + ((dst_negative_scale_fubini_actual_sumsrow_total) + (dst_negative_scale_fubini_actual_sumsrow_total)))))) /\ (((exists fs_u_dst_fubini_actual_sumsrow_totalpositive fs_v_dst_fubini_actual_sumsrow_totalpositive. ((((exists fs_h_dst_fubini_actual_sumsrow_totalpositive_body_start. fs_h_dst_fubini_actual_sumsrow_totalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_actual_sumsrow_totalpositive)) /\ exists fs_q_dst_fubini_actual_sumsrow_totalpositive_body_start. fs_u_dst_fubini_actual_sumsrow_totalpositive = fs_q_dst_fubini_actual_sumsrow_totalpositive_body_start * S ((S (0)) * fs_v_dst_fubini_actual_sumsrow_totalpositive) + (0))) /\ ((((exists fs_h_dst_fubini_actual_sumsrow_totalpositive_body_terminal. fs_h_dst_fubini_actual_sumsrow_totalpositive_body_terminal + S (dst_positive_sum_fubini_actual_sumsrow_total) = S ((S (S n)) * fs_v_dst_fubini_actual_sumsrow_totalpositive)) /\ exists fs_q_dst_fubini_actual_sumsrow_totalpositive_body_terminal. fs_u_dst_fubini_actual_sumsrow_totalpositive = fs_q_dst_fubini_actual_sumsrow_totalpositive_body_terminal * S ((S (S n)) * fs_v_dst_fubini_actual_sumsrow_totalpositive) + (dst_positive_sum_fubini_actual_sumsrow_total))) /\ forall fs_i_dst_fubini_actual_sumsrow_totalpositive_body_steps. (exists fs_lt_dst_fubini_actual_sumsrow_totalpositive_body_steps_bound. fs_lt_dst_fubini_actual_sumsrow_totalpositive_body_steps_bound + S fs_i_dst_fubini_actual_sumsrow_totalpositive_body_steps = S n) -> exists fs_a_dst_fubini_actual_sumsrow_totalpositive_body_steps fs_r_dst_fubini_actual_sumsrow_totalpositive_body_steps fs_s_dst_fubini_actual_sumsrow_totalpositive_body_steps. ((((exists fs_h_dst_fubini_actual_sumsrow_totalpositive_body_steps_summand. fs_h_dst_fubini_actual_sumsrow_totalpositive_body_steps_summand + S (fs_a_dst_fubini_actual_sumsrow_totalpositive_body_steps) = S ((S (fs_i_dst_fubini_actual_sumsrow_totalpositive_body_steps)) * dst_positive_scale_fubini_actual_sumsrow_total)) /\ exists fs_q_dst_fubini_actual_sumsrow_totalpositive_body_steps_summand. dst_positive_code_fubini_actual_sumsrow_total = fs_q_dst_fubini_actual_sumsrow_totalpositive_body_steps_summand * S ((S (fs_i_dst_fubini_actual_sumsrow_totalpositive_body_steps)) * dst_positive_scale_fubini_actual_sumsrow_total) + (fs_a_dst_fubini_actual_sumsrow_totalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumsrow_totalpositive_body_steps_partial. fs_h_dst_fubini_actual_sumsrow_totalpositive_body_steps_partial + S (fs_r_dst_fubini_actual_sumsrow_totalpositive_body_steps) = S ((S (fs_i_dst_fubini_actual_sumsrow_totalpositive_body_steps)) * fs_v_dst_fubini_actual_sumsrow_totalpositive)) /\ exists fs_q_dst_fubini_actual_sumsrow_totalpositive_body_steps_partial. fs_u_dst_fubini_actual_sumsrow_totalpositive = fs_q_dst_fubini_actual_sumsrow_totalpositive_body_steps_partial * S ((S (fs_i_dst_fubini_actual_sumsrow_totalpositive_body_steps)) * fs_v_dst_fubini_actual_sumsrow_totalpositive) + (fs_r_dst_fubini_actual_sumsrow_totalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumsrow_totalpositive_body_steps_successor. fs_h_dst_fubini_actual_sumsrow_totalpositive_body_steps_successor + S (fs_s_dst_fubini_actual_sumsrow_totalpositive_body_steps) = S ((S (S fs_i_dst_fubini_actual_sumsrow_totalpositive_body_steps)) * fs_v_dst_fubini_actual_sumsrow_totalpositive)) /\ exists fs_q_dst_fubini_actual_sumsrow_totalpositive_body_steps_successor. fs_u_dst_fubini_actual_sumsrow_totalpositive = fs_q_dst_fubini_actual_sumsrow_totalpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_actual_sumsrow_totalpositive_body_steps)) * fs_v_dst_fubini_actual_sumsrow_totalpositive) + (fs_s_dst_fubini_actual_sumsrow_totalpositive_body_steps))) /\ fs_s_dst_fubini_actual_sumsrow_totalpositive_body_steps = fs_r_dst_fubini_actual_sumsrow_totalpositive_body_steps + fs_a_dst_fubini_actual_sumsrow_totalpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_actual_sumsrow_totalnegative fs_v_dst_fubini_actual_sumsrow_totalnegative. ((((exists fs_h_dst_fubini_actual_sumsrow_totalnegative_body_start. fs_h_dst_fubini_actual_sumsrow_totalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_actual_sumsrow_totalnegative)) /\ exists fs_q_dst_fubini_actual_sumsrow_totalnegative_body_start. fs_u_dst_fubini_actual_sumsrow_totalnegative = fs_q_dst_fubini_actual_sumsrow_totalnegative_body_start * S ((S (0)) * fs_v_dst_fubini_actual_sumsrow_totalnegative) + (0))) /\ ((((exists fs_h_dst_fubini_actual_sumsrow_totalnegative_body_terminal. fs_h_dst_fubini_actual_sumsrow_totalnegative_body_terminal + S (dst_negative_sum_fubini_actual_sumsrow_total) = S ((S (S n)) * fs_v_dst_fubini_actual_sumsrow_totalnegative)) /\ exists fs_q_dst_fubini_actual_sumsrow_totalnegative_body_terminal. fs_u_dst_fubini_actual_sumsrow_totalnegative = fs_q_dst_fubini_actual_sumsrow_totalnegative_body_terminal * S ((S (S n)) * fs_v_dst_fubini_actual_sumsrow_totalnegative) + (dst_negative_sum_fubini_actual_sumsrow_total))) /\ forall fs_i_dst_fubini_actual_sumsrow_totalnegative_body_steps. (exists fs_lt_dst_fubini_actual_sumsrow_totalnegative_body_steps_bound. fs_lt_dst_fubini_actual_sumsrow_totalnegative_body_steps_bound + S fs_i_dst_fubini_actual_sumsrow_totalnegative_body_steps = S n) -> exists fs_a_dst_fubini_actual_sumsrow_totalnegative_body_steps fs_r_dst_fubini_actual_sumsrow_totalnegative_body_steps fs_s_dst_fubini_actual_sumsrow_totalnegative_body_steps. ((((exists fs_h_dst_fubini_actual_sumsrow_totalnegative_body_steps_summand. fs_h_dst_fubini_actual_sumsrow_totalnegative_body_steps_summand + S (fs_a_dst_fubini_actual_sumsrow_totalnegative_body_steps) = S ((S (fs_i_dst_fubini_actual_sumsrow_totalnegative_body_steps)) * dst_negative_scale_fubini_actual_sumsrow_total)) /\ exists fs_q_dst_fubini_actual_sumsrow_totalnegative_body_steps_summand. dst_negative_code_fubini_actual_sumsrow_total = fs_q_dst_fubini_actual_sumsrow_totalnegative_body_steps_summand * S ((S (fs_i_dst_fubini_actual_sumsrow_totalnegative_body_steps)) * dst_negative_scale_fubini_actual_sumsrow_total) + (fs_a_dst_fubini_actual_sumsrow_totalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumsrow_totalnegative_body_steps_partial. fs_h_dst_fubini_actual_sumsrow_totalnegative_body_steps_partial + S (fs_r_dst_fubini_actual_sumsrow_totalnegative_body_steps) = S ((S (fs_i_dst_fubini_actual_sumsrow_totalnegative_body_steps)) * fs_v_dst_fubini_actual_sumsrow_totalnegative)) /\ exists fs_q_dst_fubini_actual_sumsrow_totalnegative_body_steps_partial. fs_u_dst_fubini_actual_sumsrow_totalnegative = fs_q_dst_fubini_actual_sumsrow_totalnegative_body_steps_partial * S ((S (fs_i_dst_fubini_actual_sumsrow_totalnegative_body_steps)) * fs_v_dst_fubini_actual_sumsrow_totalnegative) + (fs_r_dst_fubini_actual_sumsrow_totalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumsrow_totalnegative_body_steps_successor. fs_h_dst_fubini_actual_sumsrow_totalnegative_body_steps_successor + S (fs_s_dst_fubini_actual_sumsrow_totalnegative_body_steps) = S ((S (S fs_i_dst_fubini_actual_sumsrow_totalnegative_body_steps)) * fs_v_dst_fubini_actual_sumsrow_totalnegative)) /\ exists fs_q_dst_fubini_actual_sumsrow_totalnegative_body_steps_successor. fs_u_dst_fubini_actual_sumsrow_totalnegative = fs_q_dst_fubini_actual_sumsrow_totalnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_actual_sumsrow_totalnegative_body_steps)) * fs_v_dst_fubini_actual_sumsrow_totalnegative) + (fs_s_dst_fubini_actual_sumsrow_totalnegative_body_steps))) /\ fs_s_dst_fubini_actual_sumsrow_totalnegative_body_steps = fs_r_dst_fubini_actual_sumsrow_totalnegative_body_steps + fs_a_dst_fubini_actual_sumsrow_totalnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_actual_sumsrow_totalresult ge_balance_negative_fubini_actual_sumsrow_totalresult. (((((z) = 2 * (ge_balance_positive_fubini_actual_sumsrow_totalresult) /\ (ge_balance_negative_fubini_actual_sumsrow_totalresult) = 0) \/ exists ge_signed_half_fubini_actual_sumsrow_totalresultdecode. (((z) = 2 * ge_signed_half_fubini_actual_sumsrow_totalresultdecode + 1 /\ (ge_balance_positive_fubini_actual_sumsrow_totalresult) = 0) /\ (ge_balance_negative_fubini_actual_sumsrow_totalresult) = S ge_signed_half_fubini_actual_sumsrow_totalresultdecode))) /\ ((dst_positive_sum_fubini_actual_sumsrow_total) + ge_balance_negative_fubini_actual_sumsrow_totalresult = (dst_negative_sum_fubini_actual_sumsrow_total) + ge_balance_positive_fubini_actual_sumsrow_totalresult))))))))) /\ (exists dst_positive_code_fubini_actual_sumscolumn_total dst_positive_scale_fubini_actual_sumscolumn_total dst_negative_code_fubini_actual_sumscolumn_total dst_negative_scale_fubini_actual_sumscolumn_total dst_positive_sum_fubini_actual_sumscolumn_total dst_negative_sum_fubini_actual_sumscolumn_total. (((C) = (((((dst_positive_code_fubini_actual_sumscolumn_total) + (dst_positive_scale_fubini_actual_sumscolumn_total)) * S ((dst_positive_code_fubini_actual_sumscolumn_total) + (dst_positive_scale_fubini_actual_sumscolumn_total)) + ((dst_positive_scale_fubini_actual_sumscolumn_total) + (dst_positive_scale_fubini_actual_sumscolumn_total))) + (((dst_negative_code_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)) * S ((dst_negative_code_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)) + ((dst_negative_scale_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)))) * S ((((dst_positive_code_fubini_actual_sumscolumn_total) + (dst_positive_scale_fubini_actual_sumscolumn_total)) * S ((dst_positive_code_fubini_actual_sumscolumn_total) + (dst_positive_scale_fubini_actual_sumscolumn_total)) + ((dst_positive_scale_fubini_actual_sumscolumn_total) + (dst_positive_scale_fubini_actual_sumscolumn_total))) + (((dst_negative_code_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)) * S ((dst_negative_code_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)) + ((dst_negative_scale_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)))) + ((((dst_negative_code_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)) * S ((dst_negative_code_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)) + ((dst_negative_scale_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total))) + (((dst_negative_code_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)) * S ((dst_negative_code_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)) + ((dst_negative_scale_fubini_actual_sumscolumn_total) + (dst_negative_scale_fubini_actual_sumscolumn_total)))))) /\ (((exists fs_u_dst_fubini_actual_sumscolumn_totalpositive fs_v_dst_fubini_actual_sumscolumn_totalpositive. ((((exists fs_h_dst_fubini_actual_sumscolumn_totalpositive_body_start. fs_h_dst_fubini_actual_sumscolumn_totalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_actual_sumscolumn_totalpositive)) /\ exists fs_q_dst_fubini_actual_sumscolumn_totalpositive_body_start. fs_u_dst_fubini_actual_sumscolumn_totalpositive = fs_q_dst_fubini_actual_sumscolumn_totalpositive_body_start * S ((S (0)) * fs_v_dst_fubini_actual_sumscolumn_totalpositive) + (0))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumn_totalpositive_body_terminal. fs_h_dst_fubini_actual_sumscolumn_totalpositive_body_terminal + S (dst_positive_sum_fubini_actual_sumscolumn_total) = S ((S (S n)) * fs_v_dst_fubini_actual_sumscolumn_totalpositive)) /\ exists fs_q_dst_fubini_actual_sumscolumn_totalpositive_body_terminal. fs_u_dst_fubini_actual_sumscolumn_totalpositive = fs_q_dst_fubini_actual_sumscolumn_totalpositive_body_terminal * S ((S (S n)) * fs_v_dst_fubini_actual_sumscolumn_totalpositive) + (dst_positive_sum_fubini_actual_sumscolumn_total))) /\ forall fs_i_dst_fubini_actual_sumscolumn_totalpositive_body_steps. (exists fs_lt_dst_fubini_actual_sumscolumn_totalpositive_body_steps_bound. fs_lt_dst_fubini_actual_sumscolumn_totalpositive_body_steps_bound + S fs_i_dst_fubini_actual_sumscolumn_totalpositive_body_steps = S n) -> exists fs_a_dst_fubini_actual_sumscolumn_totalpositive_body_steps fs_r_dst_fubini_actual_sumscolumn_totalpositive_body_steps fs_s_dst_fubini_actual_sumscolumn_totalpositive_body_steps. ((((exists fs_h_dst_fubini_actual_sumscolumn_totalpositive_body_steps_summand. fs_h_dst_fubini_actual_sumscolumn_totalpositive_body_steps_summand + S (fs_a_dst_fubini_actual_sumscolumn_totalpositive_body_steps) = S ((S (fs_i_dst_fubini_actual_sumscolumn_totalpositive_body_steps)) * dst_positive_scale_fubini_actual_sumscolumn_total)) /\ exists fs_q_dst_fubini_actual_sumscolumn_totalpositive_body_steps_summand. dst_positive_code_fubini_actual_sumscolumn_total = fs_q_dst_fubini_actual_sumscolumn_totalpositive_body_steps_summand * S ((S (fs_i_dst_fubini_actual_sumscolumn_totalpositive_body_steps)) * dst_positive_scale_fubini_actual_sumscolumn_total) + (fs_a_dst_fubini_actual_sumscolumn_totalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumn_totalpositive_body_steps_partial. fs_h_dst_fubini_actual_sumscolumn_totalpositive_body_steps_partial + S (fs_r_dst_fubini_actual_sumscolumn_totalpositive_body_steps) = S ((S (fs_i_dst_fubini_actual_sumscolumn_totalpositive_body_steps)) * fs_v_dst_fubini_actual_sumscolumn_totalpositive)) /\ exists fs_q_dst_fubini_actual_sumscolumn_totalpositive_body_steps_partial. fs_u_dst_fubini_actual_sumscolumn_totalpositive = fs_q_dst_fubini_actual_sumscolumn_totalpositive_body_steps_partial * S ((S (fs_i_dst_fubini_actual_sumscolumn_totalpositive_body_steps)) * fs_v_dst_fubini_actual_sumscolumn_totalpositive) + (fs_r_dst_fubini_actual_sumscolumn_totalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumn_totalpositive_body_steps_successor. fs_h_dst_fubini_actual_sumscolumn_totalpositive_body_steps_successor + S (fs_s_dst_fubini_actual_sumscolumn_totalpositive_body_steps) = S ((S (S fs_i_dst_fubini_actual_sumscolumn_totalpositive_body_steps)) * fs_v_dst_fubini_actual_sumscolumn_totalpositive)) /\ exists fs_q_dst_fubini_actual_sumscolumn_totalpositive_body_steps_successor. fs_u_dst_fubini_actual_sumscolumn_totalpositive = fs_q_dst_fubini_actual_sumscolumn_totalpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_actual_sumscolumn_totalpositive_body_steps)) * fs_v_dst_fubini_actual_sumscolumn_totalpositive) + (fs_s_dst_fubini_actual_sumscolumn_totalpositive_body_steps))) /\ fs_s_dst_fubini_actual_sumscolumn_totalpositive_body_steps = fs_r_dst_fubini_actual_sumscolumn_totalpositive_body_steps + fs_a_dst_fubini_actual_sumscolumn_totalpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_actual_sumscolumn_totalnegative fs_v_dst_fubini_actual_sumscolumn_totalnegative. ((((exists fs_h_dst_fubini_actual_sumscolumn_totalnegative_body_start. fs_h_dst_fubini_actual_sumscolumn_totalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_actual_sumscolumn_totalnegative)) /\ exists fs_q_dst_fubini_actual_sumscolumn_totalnegative_body_start. fs_u_dst_fubini_actual_sumscolumn_totalnegative = fs_q_dst_fubini_actual_sumscolumn_totalnegative_body_start * S ((S (0)) * fs_v_dst_fubini_actual_sumscolumn_totalnegative) + (0))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumn_totalnegative_body_terminal. fs_h_dst_fubini_actual_sumscolumn_totalnegative_body_terminal + S (dst_negative_sum_fubini_actual_sumscolumn_total) = S ((S (S n)) * fs_v_dst_fubini_actual_sumscolumn_totalnegative)) /\ exists fs_q_dst_fubini_actual_sumscolumn_totalnegative_body_terminal. fs_u_dst_fubini_actual_sumscolumn_totalnegative = fs_q_dst_fubini_actual_sumscolumn_totalnegative_body_terminal * S ((S (S n)) * fs_v_dst_fubini_actual_sumscolumn_totalnegative) + (dst_negative_sum_fubini_actual_sumscolumn_total))) /\ forall fs_i_dst_fubini_actual_sumscolumn_totalnegative_body_steps. (exists fs_lt_dst_fubini_actual_sumscolumn_totalnegative_body_steps_bound. fs_lt_dst_fubini_actual_sumscolumn_totalnegative_body_steps_bound + S fs_i_dst_fubini_actual_sumscolumn_totalnegative_body_steps = S n) -> exists fs_a_dst_fubini_actual_sumscolumn_totalnegative_body_steps fs_r_dst_fubini_actual_sumscolumn_totalnegative_body_steps fs_s_dst_fubini_actual_sumscolumn_totalnegative_body_steps. ((((exists fs_h_dst_fubini_actual_sumscolumn_totalnegative_body_steps_summand. fs_h_dst_fubini_actual_sumscolumn_totalnegative_body_steps_summand + S (fs_a_dst_fubini_actual_sumscolumn_totalnegative_body_steps) = S ((S (fs_i_dst_fubini_actual_sumscolumn_totalnegative_body_steps)) * dst_negative_scale_fubini_actual_sumscolumn_total)) /\ exists fs_q_dst_fubini_actual_sumscolumn_totalnegative_body_steps_summand. dst_negative_code_fubini_actual_sumscolumn_total = fs_q_dst_fubini_actual_sumscolumn_totalnegative_body_steps_summand * S ((S (fs_i_dst_fubini_actual_sumscolumn_totalnegative_body_steps)) * dst_negative_scale_fubini_actual_sumscolumn_total) + (fs_a_dst_fubini_actual_sumscolumn_totalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumn_totalnegative_body_steps_partial. fs_h_dst_fubini_actual_sumscolumn_totalnegative_body_steps_partial + S (fs_r_dst_fubini_actual_sumscolumn_totalnegative_body_steps) = S ((S (fs_i_dst_fubini_actual_sumscolumn_totalnegative_body_steps)) * fs_v_dst_fubini_actual_sumscolumn_totalnegative)) /\ exists fs_q_dst_fubini_actual_sumscolumn_totalnegative_body_steps_partial. fs_u_dst_fubini_actual_sumscolumn_totalnegative = fs_q_dst_fubini_actual_sumscolumn_totalnegative_body_steps_partial * S ((S (fs_i_dst_fubini_actual_sumscolumn_totalnegative_body_steps)) * fs_v_dst_fubini_actual_sumscolumn_totalnegative) + (fs_r_dst_fubini_actual_sumscolumn_totalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_actual_sumscolumn_totalnegative_body_steps_successor. fs_h_dst_fubini_actual_sumscolumn_totalnegative_body_steps_successor + S (fs_s_dst_fubini_actual_sumscolumn_totalnegative_body_steps) = S ((S (S fs_i_dst_fubini_actual_sumscolumn_totalnegative_body_steps)) * fs_v_dst_fubini_actual_sumscolumn_totalnegative)) /\ exists fs_q_dst_fubini_actual_sumscolumn_totalnegative_body_steps_successor. fs_u_dst_fubini_actual_sumscolumn_totalnegative = fs_q_dst_fubini_actual_sumscolumn_totalnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_actual_sumscolumn_totalnegative_body_steps)) * fs_v_dst_fubini_actual_sumscolumn_totalnegative) + (fs_s_dst_fubini_actual_sumscolumn_totalnegative_body_steps))) /\ fs_s_dst_fubini_actual_sumscolumn_totalnegative_body_steps = fs_r_dst_fubini_actual_sumscolumn_totalnegative_body_steps + fs_a_dst_fubini_actual_sumscolumn_totalnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_actual_sumscolumn_totalresult ge_balance_negative_fubini_actual_sumscolumn_totalresult. (((((z) = 2 * (ge_balance_positive_fubini_actual_sumscolumn_totalresult) /\ (ge_balance_negative_fubini_actual_sumscolumn_totalresult) = 0) \/ exists ge_signed_half_fubini_actual_sumscolumn_totalresultdecode. (((z) = 2 * ge_signed_half_fubini_actual_sumscolumn_totalresultdecode + 1 /\ (ge_balance_positive_fubini_actual_sumscolumn_totalresult) = 0) /\ (ge_balance_negative_fubini_actual_sumscolumn_totalresult) = S ge_signed_half_fubini_actual_sumscolumn_totalresultdecode))) /\ ((dst_positive_sum_fubini_actual_sumscolumn_total) + ge_balance_negative_fubini_actual_sumscolumn_totalresult = (dst_negative_sum_fubini_actual_sumscolumn_total) + ge_balance_positive_fubini_actual_sumscolumn_totalresult))))))))))))))))Complete tactic proof in conservative notation
All 34 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
34 script commands · 10 reading checkpoints · 2 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 (1)
01Fix variables and assumptionsL1–7
02Establish hgL8–16
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet grid table exists.
- L8
have hg : ∃ T. DirichletGrid(F,G,H,n,T)Definitions: DirichletGrid(F,G,H,n,T)Original native command in the exact edition - L9
specialize dirichlet_grid_table_exists (F) - L10
specialize dirichlet_grid_table_exists (G) - L11
specialize dirichlet_grid_table_exists (H) - L12
specialize dirichlet_grid_table_exists (n) - L13
apply dirichlet_grid_table_exists - L14
exact hF - L15
exact hG - L16
exact hH
03Separate the logical casesL17–17
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L17
cases hg
04Establish hfL18–22
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed rectangular row major fubini.
- L18
have hf : ∃ R. ∃ C. ∃ z. ArithRowSums(x,R,0,S n,1,S n,S n) ∧ (ArithRowSums(x,C,0,1,S n,S n,S n) ∧ (SignedPrefixSum(R,S n,z) ∧ SignedPrefixSum(C,S n,z)))Definitions: ArithRowSums(x,R,0,S n,1,S n,S n)ArithRowSums(x,C,0,1,S n,S n,S n)SignedPrefixSum(R,S n,z)SignedPrefixSum(C,S n,z)Original native command in the exact edition - L19
specialize signed_rectangular_row_major_fubini (x) - L20
specialize signed_rectangular_row_major_fubini (S n) - L21
specialize signed_rectangular_row_major_fubini (S n) - L22
apply signed_rectangular_row_major_fubini
05Separate the logical casesL23–23
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L23
cases hg_witness
06Use earlier factsL24–24
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L24
exact hg_witness_left
07Separate the logical casesL25–27
08Construct an explicit witnessL28–31
09Separate the logical casesL32–32
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L32
split
Original defined command ledger · 34 lines
- 0001
intro F - 0002
intro G - 0003
intro H - 0004
intro n - 0005
intro hF - 0006
intro hG - 0007
intro hH - 0008
have hg : ∃ T. DirichletGrid(F,G,H,n,T) - 0009
specialize dirichlet_grid_table_exists (F) - 0010
specialize dirichlet_grid_table_exists (G) - 0011
specialize dirichlet_grid_table_exists (H) - 0012
specialize dirichlet_grid_table_exists (n) - 0013
apply dirichlet_grid_table_exists - 0014
exact hF - 0015
exact hG - 0016
exact hH - 0017
cases hg - 0018
have hf : ∃ R. ∃ C. ∃ z. ArithRowSums(x,R,0,S n,1,S n,S n) ∧ (ArithRowSums(x,C,0,1,S n,S n,S n) ∧ (SignedPrefixSum(R,S n,z) ∧ SignedPrefixSum(C,S n,z))) - 0019
specialize signed_rectangular_row_major_fubini (x) - 0020
specialize signed_rectangular_row_major_fubini (S n) - 0021
specialize signed_rectangular_row_major_fubini (S n) - 0022
apply signed_rectangular_row_major_fubini - 0023
cases hg_witness - 0024
exact hg_witness_left - 0025
cases hf - 0026
cases hf_witness - 0027
cases hf_witness_witness - 0028
exists x - 0029
exists x1 - 0030
exists x2 - 0031
exists x3 - 0032
split - 0033
exact hg_witness - 0034
exact hf_witness_witness_witness