dirichlet_grid_fubini_exists

Exact expanded first-order arithmetic 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))))))))))))))))