signed_rectangular_fubini_exists

forall F o s t m n. (exists dst_positive_code_fubini_exists_source dst_positive_scale_fubini_exists_source dst_negative_code_fubini_exists_source dst_negative_scale_fubini_exists_source. (((F) = (((((dst_positive_code_fubini_exists_source) + (dst_positive_scale_fubini_exists_source)) * S ((dst_positive_code_fubini_exists_source) + (dst_positive_scale_fubini_exists_source)) + ((dst_positive_scale_fubini_exists_source) + (dst_positive_scale_fubini_exists_source))) + (((dst_negative_code_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)) * S ((dst_negative_code_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)) + ((dst_negative_scale_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)))) * S ((((dst_positive_code_fubini_exists_source) + (dst_positive_scale_fubini_exists_source)) * S ((dst_positive_code_fubini_exists_source) + (dst_positive_scale_fubini_exists_source)) + ((dst_positive_scale_fubini_exists_source) + (dst_positive_scale_fubini_exists_source))) + (((dst_negative_code_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)) * S ((dst_negative_code_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)) + ((dst_negative_scale_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)))) + ((((dst_negative_code_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)) * S ((dst_negative_code_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)) + ((dst_negative_scale_fubini_exists_source) + (dst_negative_scale_fubini_exists_source))) + (((dst_negative_code_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)) * S ((dst_negative_code_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)) + ((dst_negative_scale_fubini_exists_source) + (dst_negative_scale_fubini_exists_source)))))) /\ (forall dst_index_fubini_exists_source. (exists pvs_le_gap_fubini_exists_sourcedomain. pvs_le_gap_fubini_exists_sourcedomain + (dst_index_fubini_exists_source) = (0)) -> exists dst_positive_fubini_exists_source dst_negative_fubini_exists_source dst_value_fubini_exists_source. ((((exists ff_h_pvs_fubini_exists_sourceentrypositive. ff_h_pvs_fubini_exists_sourceentrypositive + S (dst_positive_fubini_exists_source) = S ((S (dst_index_fubini_exists_source)) * dst_positive_scale_fubini_exists_source)) /\ exists ff_q_pvs_fubini_exists_sourceentrypositive. dst_positive_code_fubini_exists_source = ff_q_pvs_fubini_exists_sourceentrypositive * S ((S (dst_index_fubini_exists_source)) * dst_positive_scale_fubini_exists_source) + (dst_positive_fubini_exists_source))) /\ (((((exists ff_h_pvs_fubini_exists_sourceentrynegative. ff_h_pvs_fubini_exists_sourceentrynegative + S (dst_negative_fubini_exists_source) = S ((S (dst_index_fubini_exists_source)) * dst_negative_scale_fubini_exists_source)) /\ exists ff_q_pvs_fubini_exists_sourceentrynegative. dst_negative_code_fubini_exists_source = ff_q_pvs_fubini_exists_sourceentrynegative * S ((S (dst_index_fubini_exists_source)) * dst_negative_scale_fubini_exists_source) + (dst_negative_fubini_exists_source))) /\ (exists ge_balance_positive_fubini_exists_sourceentryvalue ge_balance_negative_fubini_exists_sourceentryvalue. (((((dst_value_fubini_exists_source) = 2 * (ge_balance_positive_fubini_exists_sourceentryvalue) /\ (ge_balance_negative_fubini_exists_sourceentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_sourceentryvaluedecode. (((dst_value_fubini_exists_source) = 2 * ge_signed_half_fubini_exists_sourceentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_sourceentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_sourceentryvalue) = S ge_signed_half_fubini_exists_sourceentryvaluedecode))) /\ ((dst_positive_fubini_exists_source) + ge_balance_negative_fubini_exists_sourceentryvalue = (dst_negative_fubini_exists_source) + ge_balance_positive_fubini_exists_sourceentryvalue))))))))) -> exists R C z. (((((exists dst_positive_code_fubini_exists_resultrowssource_table dst_positive_scale_fubini_exists_resultrowssource_table dst_negative_code_fubini_exists_resultrowssource_table dst_negative_scale_fubini_exists_resultrowssource_table. (((F) = (((((dst_positive_code_fubini_exists_resultrowssource_table) + (dst_positive_scale_fubini_exists_resultrowssource_table)) * S ((dst_positive_code_fubini_exists_resultrowssource_table) + (dst_positive_scale_fubini_exists_resultrowssource_table)) + ((dst_positive_scale_fubini_exists_resultrowssource_table) + (dst_positive_scale_fubini_exists_resultrowssource_table))) + (((dst_negative_code_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)) * S ((dst_negative_code_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)) + ((dst_negative_scale_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)))) * S ((((dst_positive_code_fubini_exists_resultrowssource_table) + (dst_positive_scale_fubini_exists_resultrowssource_table)) * S ((dst_positive_code_fubini_exists_resultrowssource_table) + (dst_positive_scale_fubini_exists_resultrowssource_table)) + ((dst_positive_scale_fubini_exists_resultrowssource_table) + (dst_positive_scale_fubini_exists_resultrowssource_table))) + (((dst_negative_code_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)) * S ((dst_negative_code_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)) + ((dst_negative_scale_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)))) + ((((dst_negative_code_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)) * S ((dst_negative_code_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)) + ((dst_negative_scale_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table))) + (((dst_negative_code_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)) * S ((dst_negative_code_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)) + ((dst_negative_scale_fubini_exists_resultrowssource_table) + (dst_negative_scale_fubini_exists_resultrowssource_table)))))) /\ (forall dst_index_fubini_exists_resultrowssource_table. (exists pvs_le_gap_fubini_exists_resultrowssource_tabledomain. pvs_le_gap_fubini_exists_resultrowssource_tabledomain + (dst_index_fubini_exists_resultrowssource_table) = (0)) -> exists dst_positive_fubini_exists_resultrowssource_table dst_negative_fubini_exists_resultrowssource_table dst_value_fubini_exists_resultrowssource_table. ((((exists ff_h_pvs_fubini_exists_resultrowssource_tableentrypositive. ff_h_pvs_fubini_exists_resultrowssource_tableentrypositive + S (dst_positive_fubini_exists_resultrowssource_table) = S ((S (dst_index_fubini_exists_resultrowssource_table)) * dst_positive_scale_fubini_exists_resultrowssource_table)) /\ exists ff_q_pvs_fubini_exists_resultrowssource_tableentrypositive. dst_positive_code_fubini_exists_resultrowssource_table = ff_q_pvs_fubini_exists_resultrowssource_tableentrypositive * S ((S (dst_index_fubini_exists_resultrowssource_table)) * dst_positive_scale_fubini_exists_resultrowssource_table) + (dst_positive_fubini_exists_resultrowssource_table))) /\ (((((exists ff_h_pvs_fubini_exists_resultrowssource_tableentrynegative. ff_h_pvs_fubini_exists_resultrowssource_tableentrynegative + S (dst_negative_fubini_exists_resultrowssource_table) = S ((S (dst_index_fubini_exists_resultrowssource_table)) * dst_negative_scale_fubini_exists_resultrowssource_table)) /\ exists ff_q_pvs_fubini_exists_resultrowssource_tableentrynegative. dst_negative_code_fubini_exists_resultrowssource_table = ff_q_pvs_fubini_exists_resultrowssource_tableentrynegative * S ((S (dst_index_fubini_exists_resultrowssource_table)) * dst_negative_scale_fubini_exists_resultrowssource_table) + (dst_negative_fubini_exists_resultrowssource_table))) /\ (exists ge_balance_positive_fubini_exists_resultrowssource_tableentryvalue ge_balance_negative_fubini_exists_resultrowssource_tableentryvalue. (((((dst_value_fubini_exists_resultrowssource_table) = 2 * (ge_balance_positive_fubini_exists_resultrowssource_tableentryvalue) /\ (ge_balance_negative_fubini_exists_resultrowssource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultrowssource_tableentryvaluedecode. (((dst_value_fubini_exists_resultrowssource_table) = 2 * ge_signed_half_fubini_exists_resultrowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultrowssource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultrowssource_tableentryvalue) = S ge_signed_half_fubini_exists_resultrowssource_tableentryvaluedecode))) /\ ((dst_positive_fubini_exists_resultrowssource_table) + ge_balance_negative_fubini_exists_resultrowssource_tableentryvalue = (dst_negative_fubini_exists_resultrowssource_table) + ge_balance_positive_fubini_exists_resultrowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_exists_resultrowsrow_table dst_positive_scale_fubini_exists_resultrowsrow_table dst_negative_code_fubini_exists_resultrowsrow_table dst_negative_scale_fubini_exists_resultrowsrow_table. (((R) = (((((dst_positive_code_fubini_exists_resultrowsrow_table) + (dst_positive_scale_fubini_exists_resultrowsrow_table)) * S ((dst_positive_code_fubini_exists_resultrowsrow_table) + (dst_positive_scale_fubini_exists_resultrowsrow_table)) + ((dst_positive_scale_fubini_exists_resultrowsrow_table) + (dst_positive_scale_fubini_exists_resultrowsrow_table))) + (((dst_negative_code_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)) * S ((dst_negative_code_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)) + ((dst_negative_scale_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)))) * S ((((dst_positive_code_fubini_exists_resultrowsrow_table) + (dst_positive_scale_fubini_exists_resultrowsrow_table)) * S ((dst_positive_code_fubini_exists_resultrowsrow_table) + (dst_positive_scale_fubini_exists_resultrowsrow_table)) + ((dst_positive_scale_fubini_exists_resultrowsrow_table) + (dst_positive_scale_fubini_exists_resultrowsrow_table))) + (((dst_negative_code_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)) * S ((dst_negative_code_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)) + ((dst_negative_scale_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)))) + ((((dst_negative_code_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)) * S ((dst_negative_code_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)) + ((dst_negative_scale_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table))) + (((dst_negative_code_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)) * S ((dst_negative_code_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)) + ((dst_negative_scale_fubini_exists_resultrowsrow_table) + (dst_negative_scale_fubini_exists_resultrowsrow_table)))))) /\ (forall dst_index_fubini_exists_resultrowsrow_table. (exists pvs_le_gap_fubini_exists_resultrowsrow_tabledomain. pvs_le_gap_fubini_exists_resultrowsrow_tabledomain + (dst_index_fubini_exists_resultrowsrow_table) = (m)) -> exists dst_positive_fubini_exists_resultrowsrow_table dst_negative_fubini_exists_resultrowsrow_table dst_value_fubini_exists_resultrowsrow_table. ((((exists ff_h_pvs_fubini_exists_resultrowsrow_tableentrypositive. ff_h_pvs_fubini_exists_resultrowsrow_tableentrypositive + S (dst_positive_fubini_exists_resultrowsrow_table) = S ((S (dst_index_fubini_exists_resultrowsrow_table)) * dst_positive_scale_fubini_exists_resultrowsrow_table)) /\ exists ff_q_pvs_fubini_exists_resultrowsrow_tableentrypositive. dst_positive_code_fubini_exists_resultrowsrow_table = ff_q_pvs_fubini_exists_resultrowsrow_tableentrypositive * S ((S (dst_index_fubini_exists_resultrowsrow_table)) * dst_positive_scale_fubini_exists_resultrowsrow_table) + (dst_positive_fubini_exists_resultrowsrow_table))) /\ (((((exists ff_h_pvs_fubini_exists_resultrowsrow_tableentrynegative. ff_h_pvs_fubini_exists_resultrowsrow_tableentrynegative + S (dst_negative_fubini_exists_resultrowsrow_table) = S ((S (dst_index_fubini_exists_resultrowsrow_table)) * dst_negative_scale_fubini_exists_resultrowsrow_table)) /\ exists ff_q_pvs_fubini_exists_resultrowsrow_tableentrynegative. dst_negative_code_fubini_exists_resultrowsrow_table = ff_q_pvs_fubini_exists_resultrowsrow_tableentrynegative * S ((S (dst_index_fubini_exists_resultrowsrow_table)) * dst_negative_scale_fubini_exists_resultrowsrow_table) + (dst_negative_fubini_exists_resultrowsrow_table))) /\ (exists ge_balance_positive_fubini_exists_resultrowsrow_tableentryvalue ge_balance_negative_fubini_exists_resultrowsrow_tableentryvalue. (((((dst_value_fubini_exists_resultrowsrow_table) = 2 * (ge_balance_positive_fubini_exists_resultrowsrow_tableentryvalue) /\ (ge_balance_negative_fubini_exists_resultrowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultrowsrow_tableentryvaluedecode. (((dst_value_fubini_exists_resultrowsrow_table) = 2 * ge_signed_half_fubini_exists_resultrowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultrowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultrowsrow_tableentryvalue) = S ge_signed_half_fubini_exists_resultrowsrow_tableentryvaluedecode))) /\ ((dst_positive_fubini_exists_resultrowsrow_table) + ge_balance_negative_fubini_exists_resultrowsrow_tableentryvalue = (dst_negative_fubini_exists_resultrowsrow_table) + ge_balance_positive_fubini_exists_resultrowsrow_tableentryvalue))))))))) /\ (forall srt_index_fubini_exists_resultrows. (exists pvs_gap_fubini_exists_resultrowsbound. pvs_gap_fubini_exists_resultrowsbound + S (srt_index_fubini_exists_resultrows) = (m)) -> exists srt_value_fubini_exists_resultrows. (((exists dst_positive_code_fubini_exists_resultrowsrowentry dst_positive_scale_fubini_exists_resultrowsrowentry dst_negative_code_fubini_exists_resultrowsrowentry dst_negative_scale_fubini_exists_resultrowsrowentry dst_positive_fubini_exists_resultrowsrowentry dst_negative_fubini_exists_resultrowsrowentry. (((R) = (((((dst_positive_code_fubini_exists_resultrowsrowentry) + (dst_positive_scale_fubini_exists_resultrowsrowentry)) * S ((dst_positive_code_fubini_exists_resultrowsrowentry) + (dst_positive_scale_fubini_exists_resultrowsrowentry)) + ((dst_positive_scale_fubini_exists_resultrowsrowentry) + (dst_positive_scale_fubini_exists_resultrowsrowentry))) + (((dst_negative_code_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)) * S ((dst_negative_code_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)) + ((dst_negative_scale_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)))) * S ((((dst_positive_code_fubini_exists_resultrowsrowentry) + (dst_positive_scale_fubini_exists_resultrowsrowentry)) * S ((dst_positive_code_fubini_exists_resultrowsrowentry) + (dst_positive_scale_fubini_exists_resultrowsrowentry)) + ((dst_positive_scale_fubini_exists_resultrowsrowentry) + (dst_positive_scale_fubini_exists_resultrowsrowentry))) + (((dst_negative_code_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)) * S ((dst_negative_code_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)) + ((dst_negative_scale_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)))) + ((((dst_negative_code_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)) * S ((dst_negative_code_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)) + ((dst_negative_scale_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry))) + (((dst_negative_code_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)) * S ((dst_negative_code_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)) + ((dst_negative_scale_fubini_exists_resultrowsrowentry) + (dst_negative_scale_fubini_exists_resultrowsrowentry)))))) /\ (((((exists ff_h_pvs_fubini_exists_resultrowsrowentrypositive. ff_h_pvs_fubini_exists_resultrowsrowentrypositive + S (dst_positive_fubini_exists_resultrowsrowentry) = S ((S (srt_index_fubini_exists_resultrows)) * dst_positive_scale_fubini_exists_resultrowsrowentry)) /\ exists ff_q_pvs_fubini_exists_resultrowsrowentrypositive. dst_positive_code_fubini_exists_resultrowsrowentry = ff_q_pvs_fubini_exists_resultrowsrowentrypositive * S ((S (srt_index_fubini_exists_resultrows)) * dst_positive_scale_fubini_exists_resultrowsrowentry) + (dst_positive_fubini_exists_resultrowsrowentry))) /\ (((((exists ff_h_pvs_fubini_exists_resultrowsrowentrynegative. ff_h_pvs_fubini_exists_resultrowsrowentrynegative + S (dst_negative_fubini_exists_resultrowsrowentry) = S ((S (srt_index_fubini_exists_resultrows)) * dst_negative_scale_fubini_exists_resultrowsrowentry)) /\ exists ff_q_pvs_fubini_exists_resultrowsrowentrynegative. dst_negative_code_fubini_exists_resultrowsrowentry = ff_q_pvs_fubini_exists_resultrowsrowentrynegative * S ((S (srt_index_fubini_exists_resultrows)) * dst_negative_scale_fubini_exists_resultrowsrowentry) + (dst_negative_fubini_exists_resultrowsrowentry))) /\ (exists ge_balance_positive_fubini_exists_resultrowsrowentryvalue ge_balance_negative_fubini_exists_resultrowsrowentryvalue. (((((srt_value_fubini_exists_resultrows) = 2 * (ge_balance_positive_fubini_exists_resultrowsrowentryvalue) /\ (ge_balance_negative_fubini_exists_resultrowsrowentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultrowsrowentryvaluedecode. (((srt_value_fubini_exists_resultrows) = 2 * ge_signed_half_fubini_exists_resultrowsrowentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultrowsrowentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultrowsrowentryvalue) = S ge_signed_half_fubini_exists_resultrowsrowentryvaluedecode))) /\ ((dst_positive_fubini_exists_resultrowsrowentry) + ge_balance_negative_fubini_exists_resultrowsrowentryvalue = (dst_negative_fubini_exists_resultrowsrowentry) + ge_balance_positive_fubini_exists_resultrowsrowentryvalue))))))))) /\ (exists srs_slice_fubini_exists_resultrowsrowrow_sum. ((((exists dst_positive_code_fubini_exists_resultrowsrowrow_sumslicesource_table dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table dst_negative_code_fubini_exists_resultrowsrowrow_sumslicesource_table dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_fubini_exists_resultrowsrowrow_sumslicesource_table. (exists pvs_le_gap_fubini_exists_resultrowsrowrow_sumslicesource_tabledomain. pvs_le_gap_fubini_exists_resultrowsrowrow_sumslicesource_tabledomain + (dst_index_fubini_exists_resultrowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_fubini_exists_resultrowsrowrow_sumslicesource_table dst_negative_fubini_exists_resultrowsrowrow_sumslicesource_table dst_value_fubini_exists_resultrowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_fubini_exists_resultrowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_fubini_exists_resultrowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_fubini_exists_resultrowsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_exists_resultrowsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_exists_resultrowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_fubini_exists_resultrowsrowrow_sumslicesource_table = ff_q_pvs_fubini_exists_resultrowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_fubini_exists_resultrowsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_positive_fubini_exists_resultrowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_fubini_exists_resultrowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_fubini_exists_resultrowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_fubini_exists_resultrowsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_exists_resultrowsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_exists_resultrowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_fubini_exists_resultrowsrowrow_sumslicesource_table = ff_q_pvs_fubini_exists_resultrowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_fubini_exists_resultrowsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_exists_resultrowsrowrow_sumslicesource_table) + (dst_negative_fubini_exists_resultrowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_fubini_exists_resultrowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_fubini_exists_resultrowsrowrow_sumslicesource_table) = 2 * ge_signed_half_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_fubini_exists_resultrowsrowrow_sumslicesource_table) + ge_balance_negative_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvalue = (dst_negative_fubini_exists_resultrowsrowrow_sumslicesource_table) + ge_balance_positive_fubini_exists_resultrowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table. (((srs_slice_fubini_exists_resultrowsrowrow_sum) = (((((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_fubini_exists_resultrowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_fubini_exists_resultrowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_fubini_exists_resultrowsrowrow_sumsliceoutput_tabledomain + (dst_index_fubini_exists_resultrowsrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_fubini_exists_resultrowsrowrow_sumsliceoutput_table dst_negative_fubini_exists_resultrowsrowrow_sumsliceoutput_table dst_value_fubini_exists_resultrowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_fubini_exists_resultrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_positive_fubini_exists_resultrowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_fubini_exists_resultrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_fubini_exists_resultrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + (dst_negative_fubini_exists_resultrowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_fubini_exists_resultrowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_fubini_exists_resultrowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_fubini_exists_resultrowsrowrow_sumsliceoutput_table) + ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_fubini_exists_resultrowsrowrow_sumslice. (exists pvs_gap_fubini_exists_resultrowsrowrow_sumslicebound. pvs_gap_fubini_exists_resultrowsrowrow_sumslicebound + S (srs_index_fubini_exists_resultrowsrowrow_sumslice) = (n)) -> exists srs_value_fubini_exists_resultrowsrowrow_sumslice. (((exists dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentrysource dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentrysource dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource dst_positive_fubini_exists_resultrowsrowrow_sumsliceentrysource dst_negative_fubini_exists_resultrowsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceentrysourcepositive + S (dst_positive_fubini_exists_resultrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_fubini_exists_resultrows)))) + ((t) * (srs_index_fubini_exists_resultrowsrowrow_sumslice))))) * dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceentrysourcepositive. dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentrysource = ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((s) * (srt_index_fubini_exists_resultrows)))) + ((t) * (srs_index_fubini_exists_resultrowsrowrow_sumslice))))) * dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_positive_fubini_exists_resultrowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceentrysourcenegative + S (dst_negative_fubini_exists_resultrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_fubini_exists_resultrows)))) + ((t) * (srs_index_fubini_exists_resultrowsrowrow_sumslice))))) * dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceentrysourcenegative. dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentrysource = ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((s) * (srt_index_fubini_exists_resultrows)))) + ((t) * (srs_index_fubini_exists_resultrowsrowrow_sumslice))))) * dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentrysource) + (dst_negative_fubini_exists_resultrowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceentrysourcevalue ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceentrysourcevalue. (((((srs_value_fubini_exists_resultrowsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_fubini_exists_resultrowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_fubini_exists_resultrowsrowrow_sumslice) = 2 * ge_signed_half_fubini_exists_resultrowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_fubini_exists_resultrowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_fubini_exists_resultrowsrowrow_sumsliceentrysource) + ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceentrysourcevalue = (dst_negative_fubini_exists_resultrowsrowrow_sumsliceentrysource) + ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput dst_positive_fubini_exists_resultrowsrowrow_sumsliceentryoutput dst_negative_fubini_exists_resultrowsrowrow_sumsliceentryoutput. (((srs_slice_fubini_exists_resultrowsrowrow_sum) = (((((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceentryoutputpositive + S (dst_positive_fubini_exists_resultrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_exists_resultrowsrowrow_sumslice)) * dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceentryoutputpositive. dst_positive_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_fubini_exists_resultrowsrowrow_sumslice)) * dst_positive_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_positive_fubini_exists_resultrowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_fubini_exists_resultrowsrowrow_sumsliceentryoutputnegative + S (dst_negative_fubini_exists_resultrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_exists_resultrowsrowrow_sumslice)) * dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceentryoutputnegative. dst_negative_code_fubini_exists_resultrowsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_exists_resultrowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_fubini_exists_resultrowsrowrow_sumslice)) * dst_negative_scale_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + (dst_negative_fubini_exists_resultrowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceentryoutputvalue ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceentryoutputvalue. (((((srs_value_fubini_exists_resultrowsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultrowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_fubini_exists_resultrowsrowrow_sumslice) = 2 * ge_signed_half_fubini_exists_resultrowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_fubini_exists_resultrowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + ge_balance_negative_fubini_exists_resultrowsrowrow_sumsliceentryoutputvalue = (dst_negative_fubini_exists_resultrowsrowrow_sumsliceentryoutput) + ge_balance_positive_fubini_exists_resultrowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_fubini_exists_resultrowsrowrow_sumsum dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum dst_negative_code_fubini_exists_resultrowsrowrow_sumsum dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum dst_positive_sum_fubini_exists_resultrowsrowrow_sumsum dst_negative_sum_fubini_exists_resultrowsrowrow_sumsum. (((srs_slice_fubini_exists_resultrowsrowrow_sum) = (((((dst_positive_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum)) * S ((dst_positive_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum)) + ((dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)))) * S ((((dst_positive_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum)) * S ((dst_positive_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum)) + ((dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)))) + ((((dst_negative_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum))) + (((dst_negative_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)) * S ((dst_negative_code_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)) + ((dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_fubini_exists_resultrowsrowrow_sumsumpositive fs_v_dst_fubini_exists_resultrowsrowrow_sumsumpositive. ((((exists fs_h_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_start. fs_h_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_start. fs_u_dst_fubini_exists_resultrowsrowrow_sumsumpositive = fs_q_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_terminal. fs_h_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_fubini_exists_resultrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_terminal. fs_u_dst_fubini_exists_resultrowsrowrow_sumsumpositive = fs_q_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumpositive) + (dst_positive_sum_fubini_exists_resultrowsrowrow_sumsum))) /\ forall fs_i_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps fs_r_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps fs_s_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum)) /\ exists fs_q_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_fubini_exists_resultrowsrowrow_sumsum = fs_q_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_exists_resultrowsrowrow_sumsum) + (fs_a_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_fubini_exists_resultrowsrowrow_sumsumpositive = fs_q_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumpositive) + (fs_r_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_fubini_exists_resultrowsrowrow_sumsumpositive = fs_q_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumpositive) + (fs_s_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps = fs_r_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps + fs_a_dst_fubini_exists_resultrowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_exists_resultrowsrowrow_sumsumnegative fs_v_dst_fubini_exists_resultrowsrowrow_sumsumnegative. ((((exists fs_h_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_start. fs_h_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_start. fs_u_dst_fubini_exists_resultrowsrowrow_sumsumnegative = fs_q_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_terminal. fs_h_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_fubini_exists_resultrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_terminal. fs_u_dst_fubini_exists_resultrowsrowrow_sumsumnegative = fs_q_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumnegative) + (dst_negative_sum_fubini_exists_resultrowsrowrow_sumsum))) /\ forall fs_i_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps fs_r_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps fs_s_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum)) /\ exists fs_q_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_fubini_exists_resultrowsrowrow_sumsum = fs_q_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_exists_resultrowsrowrow_sumsum) + (fs_a_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_fubini_exists_resultrowsrowrow_sumsumnegative = fs_q_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumnegative) + (fs_r_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_fubini_exists_resultrowsrowrow_sumsumnegative = fs_q_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_exists_resultrowsrowrow_sumsumnegative) + (fs_s_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps = fs_r_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps + fs_a_dst_fubini_exists_resultrowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_exists_resultrowsrowrow_sumsumresult ge_balance_negative_fubini_exists_resultrowsrowrow_sumsumresult. (((((srt_value_fubini_exists_resultrows) = 2 * (ge_balance_positive_fubini_exists_resultrowsrowrow_sumsumresult) /\ (ge_balance_negative_fubini_exists_resultrowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_fubini_exists_resultrowsrowrow_sumsumresultdecode. (((srt_value_fubini_exists_resultrows) = 2 * ge_signed_half_fubini_exists_resultrowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_fubini_exists_resultrowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_fubini_exists_resultrowsrowrow_sumsumresult) = S ge_signed_half_fubini_exists_resultrowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_fubini_exists_resultrowsrowrow_sumsum) + ge_balance_negative_fubini_exists_resultrowsrowrow_sumsumresult = (dst_negative_sum_fubini_exists_resultrowsrowrow_sumsum) + ge_balance_positive_fubini_exists_resultrowsrowrow_sumsumresult)))))))))))))))))) /\ (((((exists dst_positive_code_fubini_exists_resultcolumnssource_table dst_positive_scale_fubini_exists_resultcolumnssource_table dst_negative_code_fubini_exists_resultcolumnssource_table dst_negative_scale_fubini_exists_resultcolumnssource_table. (((F) = (((((dst_positive_code_fubini_exists_resultcolumnssource_table) + (dst_positive_scale_fubini_exists_resultcolumnssource_table)) * S ((dst_positive_code_fubini_exists_resultcolumnssource_table) + (dst_positive_scale_fubini_exists_resultcolumnssource_table)) + ((dst_positive_scale_fubini_exists_resultcolumnssource_table) + (dst_positive_scale_fubini_exists_resultcolumnssource_table))) + (((dst_negative_code_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)) * S ((dst_negative_code_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)) + ((dst_negative_scale_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)))) * S ((((dst_positive_code_fubini_exists_resultcolumnssource_table) + (dst_positive_scale_fubini_exists_resultcolumnssource_table)) * S ((dst_positive_code_fubini_exists_resultcolumnssource_table) + (dst_positive_scale_fubini_exists_resultcolumnssource_table)) + ((dst_positive_scale_fubini_exists_resultcolumnssource_table) + (dst_positive_scale_fubini_exists_resultcolumnssource_table))) + (((dst_negative_code_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)) * S ((dst_negative_code_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)) + ((dst_negative_scale_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)))) + ((((dst_negative_code_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)) * S ((dst_negative_code_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)) + ((dst_negative_scale_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table))) + (((dst_negative_code_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)) * S ((dst_negative_code_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)) + ((dst_negative_scale_fubini_exists_resultcolumnssource_table) + (dst_negative_scale_fubini_exists_resultcolumnssource_table)))))) /\ (forall dst_index_fubini_exists_resultcolumnssource_table. (exists pvs_le_gap_fubini_exists_resultcolumnssource_tabledomain. pvs_le_gap_fubini_exists_resultcolumnssource_tabledomain + (dst_index_fubini_exists_resultcolumnssource_table) = (0)) -> exists dst_positive_fubini_exists_resultcolumnssource_table dst_negative_fubini_exists_resultcolumnssource_table dst_value_fubini_exists_resultcolumnssource_table. ((((exists ff_h_pvs_fubini_exists_resultcolumnssource_tableentrypositive. ff_h_pvs_fubini_exists_resultcolumnssource_tableentrypositive + S (dst_positive_fubini_exists_resultcolumnssource_table) = S ((S (dst_index_fubini_exists_resultcolumnssource_table)) * dst_positive_scale_fubini_exists_resultcolumnssource_table)) /\ exists ff_q_pvs_fubini_exists_resultcolumnssource_tableentrypositive. dst_positive_code_fubini_exists_resultcolumnssource_table = ff_q_pvs_fubini_exists_resultcolumnssource_tableentrypositive * S ((S (dst_index_fubini_exists_resultcolumnssource_table)) * dst_positive_scale_fubini_exists_resultcolumnssource_table) + (dst_positive_fubini_exists_resultcolumnssource_table))) /\ (((((exists ff_h_pvs_fubini_exists_resultcolumnssource_tableentrynegative. ff_h_pvs_fubini_exists_resultcolumnssource_tableentrynegative + S (dst_negative_fubini_exists_resultcolumnssource_table) = S ((S (dst_index_fubini_exists_resultcolumnssource_table)) * dst_negative_scale_fubini_exists_resultcolumnssource_table)) /\ exists ff_q_pvs_fubini_exists_resultcolumnssource_tableentrynegative. dst_negative_code_fubini_exists_resultcolumnssource_table = ff_q_pvs_fubini_exists_resultcolumnssource_tableentrynegative * S ((S (dst_index_fubini_exists_resultcolumnssource_table)) * dst_negative_scale_fubini_exists_resultcolumnssource_table) + (dst_negative_fubini_exists_resultcolumnssource_table))) /\ (exists ge_balance_positive_fubini_exists_resultcolumnssource_tableentryvalue ge_balance_negative_fubini_exists_resultcolumnssource_tableentryvalue. (((((dst_value_fubini_exists_resultcolumnssource_table) = 2 * (ge_balance_positive_fubini_exists_resultcolumnssource_tableentryvalue) /\ (ge_balance_negative_fubini_exists_resultcolumnssource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultcolumnssource_tableentryvaluedecode. (((dst_value_fubini_exists_resultcolumnssource_table) = 2 * ge_signed_half_fubini_exists_resultcolumnssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultcolumnssource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultcolumnssource_tableentryvalue) = S ge_signed_half_fubini_exists_resultcolumnssource_tableentryvaluedecode))) /\ ((dst_positive_fubini_exists_resultcolumnssource_table) + ge_balance_negative_fubini_exists_resultcolumnssource_tableentryvalue = (dst_negative_fubini_exists_resultcolumnssource_table) + ge_balance_positive_fubini_exists_resultcolumnssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_exists_resultcolumnsrow_table dst_positive_scale_fubini_exists_resultcolumnsrow_table dst_negative_code_fubini_exists_resultcolumnsrow_table dst_negative_scale_fubini_exists_resultcolumnsrow_table. (((C) = (((((dst_positive_code_fubini_exists_resultcolumnsrow_table) + (dst_positive_scale_fubini_exists_resultcolumnsrow_table)) * S ((dst_positive_code_fubini_exists_resultcolumnsrow_table) + (dst_positive_scale_fubini_exists_resultcolumnsrow_table)) + ((dst_positive_scale_fubini_exists_resultcolumnsrow_table) + (dst_positive_scale_fubini_exists_resultcolumnsrow_table))) + (((dst_negative_code_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)))) * S ((((dst_positive_code_fubini_exists_resultcolumnsrow_table) + (dst_positive_scale_fubini_exists_resultcolumnsrow_table)) * S ((dst_positive_code_fubini_exists_resultcolumnsrow_table) + (dst_positive_scale_fubini_exists_resultcolumnsrow_table)) + ((dst_positive_scale_fubini_exists_resultcolumnsrow_table) + (dst_positive_scale_fubini_exists_resultcolumnsrow_table))) + (((dst_negative_code_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)))) + ((((dst_negative_code_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table))) + (((dst_negative_code_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrow_table) + (dst_negative_scale_fubini_exists_resultcolumnsrow_table)))))) /\ (forall dst_index_fubini_exists_resultcolumnsrow_table. (exists pvs_le_gap_fubini_exists_resultcolumnsrow_tabledomain. pvs_le_gap_fubini_exists_resultcolumnsrow_tabledomain + (dst_index_fubini_exists_resultcolumnsrow_table) = (n)) -> exists dst_positive_fubini_exists_resultcolumnsrow_table dst_negative_fubini_exists_resultcolumnsrow_table dst_value_fubini_exists_resultcolumnsrow_table. ((((exists ff_h_pvs_fubini_exists_resultcolumnsrow_tableentrypositive. ff_h_pvs_fubini_exists_resultcolumnsrow_tableentrypositive + S (dst_positive_fubini_exists_resultcolumnsrow_table) = S ((S (dst_index_fubini_exists_resultcolumnsrow_table)) * dst_positive_scale_fubini_exists_resultcolumnsrow_table)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrow_tableentrypositive. dst_positive_code_fubini_exists_resultcolumnsrow_table = ff_q_pvs_fubini_exists_resultcolumnsrow_tableentrypositive * S ((S (dst_index_fubini_exists_resultcolumnsrow_table)) * dst_positive_scale_fubini_exists_resultcolumnsrow_table) + (dst_positive_fubini_exists_resultcolumnsrow_table))) /\ (((((exists ff_h_pvs_fubini_exists_resultcolumnsrow_tableentrynegative. ff_h_pvs_fubini_exists_resultcolumnsrow_tableentrynegative + S (dst_negative_fubini_exists_resultcolumnsrow_table) = S ((S (dst_index_fubini_exists_resultcolumnsrow_table)) * dst_negative_scale_fubini_exists_resultcolumnsrow_table)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrow_tableentrynegative. dst_negative_code_fubini_exists_resultcolumnsrow_table = ff_q_pvs_fubini_exists_resultcolumnsrow_tableentrynegative * S ((S (dst_index_fubini_exists_resultcolumnsrow_table)) * dst_negative_scale_fubini_exists_resultcolumnsrow_table) + (dst_negative_fubini_exists_resultcolumnsrow_table))) /\ (exists ge_balance_positive_fubini_exists_resultcolumnsrow_tableentryvalue ge_balance_negative_fubini_exists_resultcolumnsrow_tableentryvalue. (((((dst_value_fubini_exists_resultcolumnsrow_table) = 2 * (ge_balance_positive_fubini_exists_resultcolumnsrow_tableentryvalue) /\ (ge_balance_negative_fubini_exists_resultcolumnsrow_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultcolumnsrow_tableentryvaluedecode. (((dst_value_fubini_exists_resultcolumnsrow_table) = 2 * ge_signed_half_fubini_exists_resultcolumnsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultcolumnsrow_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultcolumnsrow_tableentryvalue) = S ge_signed_half_fubini_exists_resultcolumnsrow_tableentryvaluedecode))) /\ ((dst_positive_fubini_exists_resultcolumnsrow_table) + ge_balance_negative_fubini_exists_resultcolumnsrow_tableentryvalue = (dst_negative_fubini_exists_resultcolumnsrow_table) + ge_balance_positive_fubini_exists_resultcolumnsrow_tableentryvalue))))))))) /\ (forall srt_index_fubini_exists_resultcolumns. (exists pvs_gap_fubini_exists_resultcolumnsbound. pvs_gap_fubini_exists_resultcolumnsbound + S (srt_index_fubini_exists_resultcolumns) = (n)) -> exists srt_value_fubini_exists_resultcolumns. (((exists dst_positive_code_fubini_exists_resultcolumnsrowentry dst_positive_scale_fubini_exists_resultcolumnsrowentry dst_negative_code_fubini_exists_resultcolumnsrowentry dst_negative_scale_fubini_exists_resultcolumnsrowentry dst_positive_fubini_exists_resultcolumnsrowentry dst_negative_fubini_exists_resultcolumnsrowentry. (((C) = (((((dst_positive_code_fubini_exists_resultcolumnsrowentry) + (dst_positive_scale_fubini_exists_resultcolumnsrowentry)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowentry) + (dst_positive_scale_fubini_exists_resultcolumnsrowentry)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowentry) + (dst_positive_scale_fubini_exists_resultcolumnsrowentry))) + (((dst_negative_code_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)))) * S ((((dst_positive_code_fubini_exists_resultcolumnsrowentry) + (dst_positive_scale_fubini_exists_resultcolumnsrowentry)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowentry) + (dst_positive_scale_fubini_exists_resultcolumnsrowentry)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowentry) + (dst_positive_scale_fubini_exists_resultcolumnsrowentry))) + (((dst_negative_code_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)))) + ((((dst_negative_code_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry))) + (((dst_negative_code_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowentry) + (dst_negative_scale_fubini_exists_resultcolumnsrowentry)))))) /\ (((((exists ff_h_pvs_fubini_exists_resultcolumnsrowentrypositive. ff_h_pvs_fubini_exists_resultcolumnsrowentrypositive + S (dst_positive_fubini_exists_resultcolumnsrowentry) = S ((S (srt_index_fubini_exists_resultcolumns)) * dst_positive_scale_fubini_exists_resultcolumnsrowentry)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrowentrypositive. dst_positive_code_fubini_exists_resultcolumnsrowentry = ff_q_pvs_fubini_exists_resultcolumnsrowentrypositive * S ((S (srt_index_fubini_exists_resultcolumns)) * dst_positive_scale_fubini_exists_resultcolumnsrowentry) + (dst_positive_fubini_exists_resultcolumnsrowentry))) /\ (((((exists ff_h_pvs_fubini_exists_resultcolumnsrowentrynegative. ff_h_pvs_fubini_exists_resultcolumnsrowentrynegative + S (dst_negative_fubini_exists_resultcolumnsrowentry) = S ((S (srt_index_fubini_exists_resultcolumns)) * dst_negative_scale_fubini_exists_resultcolumnsrowentry)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrowentrynegative. dst_negative_code_fubini_exists_resultcolumnsrowentry = ff_q_pvs_fubini_exists_resultcolumnsrowentrynegative * S ((S (srt_index_fubini_exists_resultcolumns)) * dst_negative_scale_fubini_exists_resultcolumnsrowentry) + (dst_negative_fubini_exists_resultcolumnsrowentry))) /\ (exists ge_balance_positive_fubini_exists_resultcolumnsrowentryvalue ge_balance_negative_fubini_exists_resultcolumnsrowentryvalue. (((((srt_value_fubini_exists_resultcolumns) = 2 * (ge_balance_positive_fubini_exists_resultcolumnsrowentryvalue) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultcolumnsrowentryvaluedecode. (((srt_value_fubini_exists_resultcolumns) = 2 * ge_signed_half_fubini_exists_resultcolumnsrowentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultcolumnsrowentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowentryvalue) = S ge_signed_half_fubini_exists_resultcolumnsrowentryvaluedecode))) /\ ((dst_positive_fubini_exists_resultcolumnsrowentry) + ge_balance_negative_fubini_exists_resultcolumnsrowentryvalue = (dst_negative_fubini_exists_resultcolumnsrowentry) + ge_balance_positive_fubini_exists_resultcolumnsrowentryvalue))))))))) /\ (exists srs_slice_fubini_exists_resultcolumnsrowrow_sum. ((((exists dst_positive_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table dst_negative_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)))) + ((((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)))))) /\ (forall dst_index_fubini_exists_resultcolumnsrowrow_sumslicesource_table. (exists pvs_le_gap_fubini_exists_resultcolumnsrowrow_sumslicesource_tabledomain. pvs_le_gap_fubini_exists_resultcolumnsrowrow_sumslicesource_tabledomain + (dst_index_fubini_exists_resultcolumnsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_fubini_exists_resultcolumnsrowrow_sumslicesource_table dst_negative_fubini_exists_resultcolumnsrowrow_sumslicesource_table dst_value_fubini_exists_resultcolumnsrowrow_sumslicesource_table. ((((exists ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentrypositive + S (dst_positive_fubini_exists_resultcolumnsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentrypositive. dst_positive_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table = ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) * dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_positive_fubini_exists_resultcolumnsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentrynegative + S (dst_negative_fubini_exists_resultcolumnsrowrow_sumslicesource_table) = S ((S (dst_index_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentrynegative. dst_negative_code_fubini_exists_resultcolumnsrowrow_sumslicesource_table = ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_fubini_exists_resultcolumnsrowrow_sumslicesource_table)) * dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + (dst_negative_fubini_exists_resultcolumnsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvalue ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvalue. (((((dst_value_fubini_exists_resultcolumnsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_fubini_exists_resultcolumnsrowrow_sumslicesource_table) = 2 * ge_signed_half_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvalue = (dst_negative_fubini_exists_resultcolumnsrowrow_sumslicesource_table) + ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table. (((srs_slice_fubini_exists_resultcolumnsrowrow_sum) = (((((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table. (exists pvs_le_gap_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tabledomain + (dst_index_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) = (m)) -> exists dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table dst_value_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) * dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) = S ((S (dst_index_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table = ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table)) * dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + (dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceoutput_table) + ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_fubini_exists_resultcolumnsrowrow_sumslice. (exists pvs_gap_fubini_exists_resultcolumnsrowrow_sumslicebound. pvs_gap_fubini_exists_resultcolumnsrowrow_sumslicebound + S (srs_index_fubini_exists_resultcolumnsrowrow_sumslice) = (m)) -> exists srs_value_fubini_exists_resultcolumnsrowrow_sumslice. (((exists dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceentrysource dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcepositive. ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcepositive + S (dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) = S ((S (((((o) + ((t) * (srt_index_fubini_exists_resultcolumns)))) + ((s) * (srs_index_fubini_exists_resultcolumnsrowrow_sumslice))))) * dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcepositive. dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource = ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((t) * (srt_index_fubini_exists_resultcolumns)))) + ((s) * (srs_index_fubini_exists_resultcolumnsrowrow_sumslice))))) * dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcenegative. ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcenegative + S (dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) = S ((S (((((o) + ((t) * (srt_index_fubini_exists_resultcolumns)))) + ((s) * (srs_index_fubini_exists_resultcolumnsrowrow_sumslice))))) * dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcenegative. dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentrysource = ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((t) * (srt_index_fubini_exists_resultcolumns)))) + ((s) * (srs_index_fubini_exists_resultcolumnsrowrow_sumslice))))) * dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + (dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevalue ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevalue. (((((srs_value_fubini_exists_resultcolumnsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_fubini_exists_resultcolumnsrowrow_sumslice) = 2 * ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevalue = (dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceentrysource) + ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput. (((srs_slice_fubini_exists_resultcolumnsrowrow_sum) = (((((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputpositive. ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputpositive + S (dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_exists_resultcolumnsrowrow_sumslice)) * dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputpositive. dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_fubini_exists_resultcolumnsrowrow_sumslice)) * dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputnegative. ff_h_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputnegative + S (dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) = S ((S (srs_index_fubini_exists_resultcolumnsrowrow_sumslice)) * dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputnegative. dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput = ff_q_pvs_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_fubini_exists_resultcolumnsrowrow_sumslice)) * dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + (dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvalue ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvalue. (((((srs_value_fubini_exists_resultcolumnsrowrow_sumslice) = 2 * (ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_fubini_exists_resultcolumnsrowrow_sumslice) = 2 * ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvalue = (dst_negative_fubini_exists_resultcolumnsrowrow_sumsliceentryoutput) + ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsum dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsum dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum dst_positive_sum_fubini_exists_resultcolumnsrowrow_sumsum dst_negative_sum_fubini_exists_resultcolumnsrowrow_sumsum. (((srs_slice_fubini_exists_resultcolumnsrowrow_sum) = (((((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)))) * S ((((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum)) * S ((dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum)) + ((dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)))) + ((((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum))) + (((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)) * S ((dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)) + ((dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum) + (dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)))))) /\ (((exists fs_u_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive. ((((exists fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_start. fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_start. fs_u_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive = fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_terminal. fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_fubini_exists_resultcolumnsrowrow_sumsum) = S ((S (m)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_terminal. fs_u_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive = fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_terminal * S ((S (m)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive) + (dst_positive_sum_fubini_exists_resultcolumnsrowrow_sumsum))) /\ forall fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps = m) -> exists fs_a_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps fs_r_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps fs_s_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum)) /\ exists fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_fubini_exists_resultcolumnsrowrow_sumsum = fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_fubini_exists_resultcolumnsrowrow_sumsum) + (fs_a_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive = fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive) + (fs_r_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive)) /\ exists fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive = fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive) + (fs_s_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps = fs_r_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps + fs_a_dst_fubini_exists_resultcolumnsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative. ((((exists fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_start. fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_start. fs_u_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative = fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_terminal. fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_fubini_exists_resultcolumnsrowrow_sumsum) = S ((S (m)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_terminal. fs_u_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative = fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_terminal * S ((S (m)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative) + (dst_negative_sum_fubini_exists_resultcolumnsrowrow_sumsum))) /\ forall fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps = m) -> exists fs_a_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps fs_r_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps fs_s_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum)) /\ exists fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_fubini_exists_resultcolumnsrowrow_sumsum = fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_fubini_exists_resultcolumnsrowrow_sumsum) + (fs_a_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative = fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative) + (fs_r_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative)) /\ exists fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative = fs_q_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps)) * fs_v_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative) + (fs_s_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps = fs_r_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps + fs_a_dst_fubini_exists_resultcolumnsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsumresult ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsumresult. (((((srt_value_fubini_exists_resultcolumns) = 2 * (ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsumresult) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsumresultdecode. (((srt_value_fubini_exists_resultcolumns) = 2 * ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsumresult) = S ge_signed_half_fubini_exists_resultcolumnsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_fubini_exists_resultcolumnsrowrow_sumsum) + ge_balance_negative_fubini_exists_resultcolumnsrowrow_sumsumresult = (dst_negative_sum_fubini_exists_resultcolumnsrowrow_sumsum) + ge_balance_positive_fubini_exists_resultcolumnsrowrow_sumsumresult)))))))))))))))))) /\ (((exists dst_positive_code_fubini_exists_resultrow_total dst_positive_scale_fubini_exists_resultrow_total dst_negative_code_fubini_exists_resultrow_total dst_negative_scale_fubini_exists_resultrow_total dst_positive_sum_fubini_exists_resultrow_total dst_negative_sum_fubini_exists_resultrow_total. (((R) = (((((dst_positive_code_fubini_exists_resultrow_total) + (dst_positive_scale_fubini_exists_resultrow_total)) * S ((dst_positive_code_fubini_exists_resultrow_total) + (dst_positive_scale_fubini_exists_resultrow_total)) + ((dst_positive_scale_fubini_exists_resultrow_total) + (dst_positive_scale_fubini_exists_resultrow_total))) + (((dst_negative_code_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)) * S ((dst_negative_code_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)) + ((dst_negative_scale_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)))) * S ((((dst_positive_code_fubini_exists_resultrow_total) + (dst_positive_scale_fubini_exists_resultrow_total)) * S ((dst_positive_code_fubini_exists_resultrow_total) + (dst_positive_scale_fubini_exists_resultrow_total)) + ((dst_positive_scale_fubini_exists_resultrow_total) + (dst_positive_scale_fubini_exists_resultrow_total))) + (((dst_negative_code_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)) * S ((dst_negative_code_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)) + ((dst_negative_scale_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)))) + ((((dst_negative_code_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)) * S ((dst_negative_code_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)) + ((dst_negative_scale_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total))) + (((dst_negative_code_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)) * S ((dst_negative_code_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)) + ((dst_negative_scale_fubini_exists_resultrow_total) + (dst_negative_scale_fubini_exists_resultrow_total)))))) /\ (((exists fs_u_dst_fubini_exists_resultrow_totalpositive fs_v_dst_fubini_exists_resultrow_totalpositive. ((((exists fs_h_dst_fubini_exists_resultrow_totalpositive_body_start. fs_h_dst_fubini_exists_resultrow_totalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_exists_resultrow_totalpositive)) /\ exists fs_q_dst_fubini_exists_resultrow_totalpositive_body_start. fs_u_dst_fubini_exists_resultrow_totalpositive = fs_q_dst_fubini_exists_resultrow_totalpositive_body_start * S ((S (0)) * fs_v_dst_fubini_exists_resultrow_totalpositive) + (0))) /\ ((((exists fs_h_dst_fubini_exists_resultrow_totalpositive_body_terminal. fs_h_dst_fubini_exists_resultrow_totalpositive_body_terminal + S (dst_positive_sum_fubini_exists_resultrow_total) = S ((S (m)) * fs_v_dst_fubini_exists_resultrow_totalpositive)) /\ exists fs_q_dst_fubini_exists_resultrow_totalpositive_body_terminal. fs_u_dst_fubini_exists_resultrow_totalpositive = fs_q_dst_fubini_exists_resultrow_totalpositive_body_terminal * S ((S (m)) * fs_v_dst_fubini_exists_resultrow_totalpositive) + (dst_positive_sum_fubini_exists_resultrow_total))) /\ forall fs_i_dst_fubini_exists_resultrow_totalpositive_body_steps. (exists fs_lt_dst_fubini_exists_resultrow_totalpositive_body_steps_bound. fs_lt_dst_fubini_exists_resultrow_totalpositive_body_steps_bound + S fs_i_dst_fubini_exists_resultrow_totalpositive_body_steps = m) -> exists fs_a_dst_fubini_exists_resultrow_totalpositive_body_steps fs_r_dst_fubini_exists_resultrow_totalpositive_body_steps fs_s_dst_fubini_exists_resultrow_totalpositive_body_steps. ((((exists fs_h_dst_fubini_exists_resultrow_totalpositive_body_steps_summand. fs_h_dst_fubini_exists_resultrow_totalpositive_body_steps_summand + S (fs_a_dst_fubini_exists_resultrow_totalpositive_body_steps) = S ((S (fs_i_dst_fubini_exists_resultrow_totalpositive_body_steps)) * dst_positive_scale_fubini_exists_resultrow_total)) /\ exists fs_q_dst_fubini_exists_resultrow_totalpositive_body_steps_summand. dst_positive_code_fubini_exists_resultrow_total = fs_q_dst_fubini_exists_resultrow_totalpositive_body_steps_summand * S ((S (fs_i_dst_fubini_exists_resultrow_totalpositive_body_steps)) * dst_positive_scale_fubini_exists_resultrow_total) + (fs_a_dst_fubini_exists_resultrow_totalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultrow_totalpositive_body_steps_partial. fs_h_dst_fubini_exists_resultrow_totalpositive_body_steps_partial + S (fs_r_dst_fubini_exists_resultrow_totalpositive_body_steps) = S ((S (fs_i_dst_fubini_exists_resultrow_totalpositive_body_steps)) * fs_v_dst_fubini_exists_resultrow_totalpositive)) /\ exists fs_q_dst_fubini_exists_resultrow_totalpositive_body_steps_partial. fs_u_dst_fubini_exists_resultrow_totalpositive = fs_q_dst_fubini_exists_resultrow_totalpositive_body_steps_partial * S ((S (fs_i_dst_fubini_exists_resultrow_totalpositive_body_steps)) * fs_v_dst_fubini_exists_resultrow_totalpositive) + (fs_r_dst_fubini_exists_resultrow_totalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultrow_totalpositive_body_steps_successor. fs_h_dst_fubini_exists_resultrow_totalpositive_body_steps_successor + S (fs_s_dst_fubini_exists_resultrow_totalpositive_body_steps) = S ((S (S fs_i_dst_fubini_exists_resultrow_totalpositive_body_steps)) * fs_v_dst_fubini_exists_resultrow_totalpositive)) /\ exists fs_q_dst_fubini_exists_resultrow_totalpositive_body_steps_successor. fs_u_dst_fubini_exists_resultrow_totalpositive = fs_q_dst_fubini_exists_resultrow_totalpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_exists_resultrow_totalpositive_body_steps)) * fs_v_dst_fubini_exists_resultrow_totalpositive) + (fs_s_dst_fubini_exists_resultrow_totalpositive_body_steps))) /\ fs_s_dst_fubini_exists_resultrow_totalpositive_body_steps = fs_r_dst_fubini_exists_resultrow_totalpositive_body_steps + fs_a_dst_fubini_exists_resultrow_totalpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_exists_resultrow_totalnegative fs_v_dst_fubini_exists_resultrow_totalnegative. ((((exists fs_h_dst_fubini_exists_resultrow_totalnegative_body_start. fs_h_dst_fubini_exists_resultrow_totalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_exists_resultrow_totalnegative)) /\ exists fs_q_dst_fubini_exists_resultrow_totalnegative_body_start. fs_u_dst_fubini_exists_resultrow_totalnegative = fs_q_dst_fubini_exists_resultrow_totalnegative_body_start * S ((S (0)) * fs_v_dst_fubini_exists_resultrow_totalnegative) + (0))) /\ ((((exists fs_h_dst_fubini_exists_resultrow_totalnegative_body_terminal. fs_h_dst_fubini_exists_resultrow_totalnegative_body_terminal + S (dst_negative_sum_fubini_exists_resultrow_total) = S ((S (m)) * fs_v_dst_fubini_exists_resultrow_totalnegative)) /\ exists fs_q_dst_fubini_exists_resultrow_totalnegative_body_terminal. fs_u_dst_fubini_exists_resultrow_totalnegative = fs_q_dst_fubini_exists_resultrow_totalnegative_body_terminal * S ((S (m)) * fs_v_dst_fubini_exists_resultrow_totalnegative) + (dst_negative_sum_fubini_exists_resultrow_total))) /\ forall fs_i_dst_fubini_exists_resultrow_totalnegative_body_steps. (exists fs_lt_dst_fubini_exists_resultrow_totalnegative_body_steps_bound. fs_lt_dst_fubini_exists_resultrow_totalnegative_body_steps_bound + S fs_i_dst_fubini_exists_resultrow_totalnegative_body_steps = m) -> exists fs_a_dst_fubini_exists_resultrow_totalnegative_body_steps fs_r_dst_fubini_exists_resultrow_totalnegative_body_steps fs_s_dst_fubini_exists_resultrow_totalnegative_body_steps. ((((exists fs_h_dst_fubini_exists_resultrow_totalnegative_body_steps_summand. fs_h_dst_fubini_exists_resultrow_totalnegative_body_steps_summand + S (fs_a_dst_fubini_exists_resultrow_totalnegative_body_steps) = S ((S (fs_i_dst_fubini_exists_resultrow_totalnegative_body_steps)) * dst_negative_scale_fubini_exists_resultrow_total)) /\ exists fs_q_dst_fubini_exists_resultrow_totalnegative_body_steps_summand. dst_negative_code_fubini_exists_resultrow_total = fs_q_dst_fubini_exists_resultrow_totalnegative_body_steps_summand * S ((S (fs_i_dst_fubini_exists_resultrow_totalnegative_body_steps)) * dst_negative_scale_fubini_exists_resultrow_total) + (fs_a_dst_fubini_exists_resultrow_totalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultrow_totalnegative_body_steps_partial. fs_h_dst_fubini_exists_resultrow_totalnegative_body_steps_partial + S (fs_r_dst_fubini_exists_resultrow_totalnegative_body_steps) = S ((S (fs_i_dst_fubini_exists_resultrow_totalnegative_body_steps)) * fs_v_dst_fubini_exists_resultrow_totalnegative)) /\ exists fs_q_dst_fubini_exists_resultrow_totalnegative_body_steps_partial. fs_u_dst_fubini_exists_resultrow_totalnegative = fs_q_dst_fubini_exists_resultrow_totalnegative_body_steps_partial * S ((S (fs_i_dst_fubini_exists_resultrow_totalnegative_body_steps)) * fs_v_dst_fubini_exists_resultrow_totalnegative) + (fs_r_dst_fubini_exists_resultrow_totalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultrow_totalnegative_body_steps_successor. fs_h_dst_fubini_exists_resultrow_totalnegative_body_steps_successor + S (fs_s_dst_fubini_exists_resultrow_totalnegative_body_steps) = S ((S (S fs_i_dst_fubini_exists_resultrow_totalnegative_body_steps)) * fs_v_dst_fubini_exists_resultrow_totalnegative)) /\ exists fs_q_dst_fubini_exists_resultrow_totalnegative_body_steps_successor. fs_u_dst_fubini_exists_resultrow_totalnegative = fs_q_dst_fubini_exists_resultrow_totalnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_exists_resultrow_totalnegative_body_steps)) * fs_v_dst_fubini_exists_resultrow_totalnegative) + (fs_s_dst_fubini_exists_resultrow_totalnegative_body_steps))) /\ fs_s_dst_fubini_exists_resultrow_totalnegative_body_steps = fs_r_dst_fubini_exists_resultrow_totalnegative_body_steps + fs_a_dst_fubini_exists_resultrow_totalnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_exists_resultrow_totalresult ge_balance_negative_fubini_exists_resultrow_totalresult. (((((z) = 2 * (ge_balance_positive_fubini_exists_resultrow_totalresult) /\ (ge_balance_negative_fubini_exists_resultrow_totalresult) = 0) \/ exists ge_signed_half_fubini_exists_resultrow_totalresultdecode. (((z) = 2 * ge_signed_half_fubini_exists_resultrow_totalresultdecode + 1 /\ (ge_balance_positive_fubini_exists_resultrow_totalresult) = 0) /\ (ge_balance_negative_fubini_exists_resultrow_totalresult) = S ge_signed_half_fubini_exists_resultrow_totalresultdecode))) /\ ((dst_positive_sum_fubini_exists_resultrow_total) + ge_balance_negative_fubini_exists_resultrow_totalresult = (dst_negative_sum_fubini_exists_resultrow_total) + ge_balance_positive_fubini_exists_resultrow_totalresult))))))))) /\ (exists dst_positive_code_fubini_exists_resultcolumn_total dst_positive_scale_fubini_exists_resultcolumn_total dst_negative_code_fubini_exists_resultcolumn_total dst_negative_scale_fubini_exists_resultcolumn_total dst_positive_sum_fubini_exists_resultcolumn_total dst_negative_sum_fubini_exists_resultcolumn_total. (((C) = (((((dst_positive_code_fubini_exists_resultcolumn_total) + (dst_positive_scale_fubini_exists_resultcolumn_total)) * S ((dst_positive_code_fubini_exists_resultcolumn_total) + (dst_positive_scale_fubini_exists_resultcolumn_total)) + ((dst_positive_scale_fubini_exists_resultcolumn_total) + (dst_positive_scale_fubini_exists_resultcolumn_total))) + (((dst_negative_code_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)) * S ((dst_negative_code_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)) + ((dst_negative_scale_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)))) * S ((((dst_positive_code_fubini_exists_resultcolumn_total) + (dst_positive_scale_fubini_exists_resultcolumn_total)) * S ((dst_positive_code_fubini_exists_resultcolumn_total) + (dst_positive_scale_fubini_exists_resultcolumn_total)) + ((dst_positive_scale_fubini_exists_resultcolumn_total) + (dst_positive_scale_fubini_exists_resultcolumn_total))) + (((dst_negative_code_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)) * S ((dst_negative_code_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)) + ((dst_negative_scale_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)))) + ((((dst_negative_code_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)) * S ((dst_negative_code_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)) + ((dst_negative_scale_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total))) + (((dst_negative_code_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)) * S ((dst_negative_code_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)) + ((dst_negative_scale_fubini_exists_resultcolumn_total) + (dst_negative_scale_fubini_exists_resultcolumn_total)))))) /\ (((exists fs_u_dst_fubini_exists_resultcolumn_totalpositive fs_v_dst_fubini_exists_resultcolumn_totalpositive. ((((exists fs_h_dst_fubini_exists_resultcolumn_totalpositive_body_start. fs_h_dst_fubini_exists_resultcolumn_totalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_exists_resultcolumn_totalpositive)) /\ exists fs_q_dst_fubini_exists_resultcolumn_totalpositive_body_start. fs_u_dst_fubini_exists_resultcolumn_totalpositive = fs_q_dst_fubini_exists_resultcolumn_totalpositive_body_start * S ((S (0)) * fs_v_dst_fubini_exists_resultcolumn_totalpositive) + (0))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumn_totalpositive_body_terminal. fs_h_dst_fubini_exists_resultcolumn_totalpositive_body_terminal + S (dst_positive_sum_fubini_exists_resultcolumn_total) = S ((S (n)) * fs_v_dst_fubini_exists_resultcolumn_totalpositive)) /\ exists fs_q_dst_fubini_exists_resultcolumn_totalpositive_body_terminal. fs_u_dst_fubini_exists_resultcolumn_totalpositive = fs_q_dst_fubini_exists_resultcolumn_totalpositive_body_terminal * S ((S (n)) * fs_v_dst_fubini_exists_resultcolumn_totalpositive) + (dst_positive_sum_fubini_exists_resultcolumn_total))) /\ forall fs_i_dst_fubini_exists_resultcolumn_totalpositive_body_steps. (exists fs_lt_dst_fubini_exists_resultcolumn_totalpositive_body_steps_bound. fs_lt_dst_fubini_exists_resultcolumn_totalpositive_body_steps_bound + S fs_i_dst_fubini_exists_resultcolumn_totalpositive_body_steps = n) -> exists fs_a_dst_fubini_exists_resultcolumn_totalpositive_body_steps fs_r_dst_fubini_exists_resultcolumn_totalpositive_body_steps fs_s_dst_fubini_exists_resultcolumn_totalpositive_body_steps. ((((exists fs_h_dst_fubini_exists_resultcolumn_totalpositive_body_steps_summand. fs_h_dst_fubini_exists_resultcolumn_totalpositive_body_steps_summand + S (fs_a_dst_fubini_exists_resultcolumn_totalpositive_body_steps) = S ((S (fs_i_dst_fubini_exists_resultcolumn_totalpositive_body_steps)) * dst_positive_scale_fubini_exists_resultcolumn_total)) /\ exists fs_q_dst_fubini_exists_resultcolumn_totalpositive_body_steps_summand. dst_positive_code_fubini_exists_resultcolumn_total = fs_q_dst_fubini_exists_resultcolumn_totalpositive_body_steps_summand * S ((S (fs_i_dst_fubini_exists_resultcolumn_totalpositive_body_steps)) * dst_positive_scale_fubini_exists_resultcolumn_total) + (fs_a_dst_fubini_exists_resultcolumn_totalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumn_totalpositive_body_steps_partial. fs_h_dst_fubini_exists_resultcolumn_totalpositive_body_steps_partial + S (fs_r_dst_fubini_exists_resultcolumn_totalpositive_body_steps) = S ((S (fs_i_dst_fubini_exists_resultcolumn_totalpositive_body_steps)) * fs_v_dst_fubini_exists_resultcolumn_totalpositive)) /\ exists fs_q_dst_fubini_exists_resultcolumn_totalpositive_body_steps_partial. fs_u_dst_fubini_exists_resultcolumn_totalpositive = fs_q_dst_fubini_exists_resultcolumn_totalpositive_body_steps_partial * S ((S (fs_i_dst_fubini_exists_resultcolumn_totalpositive_body_steps)) * fs_v_dst_fubini_exists_resultcolumn_totalpositive) + (fs_r_dst_fubini_exists_resultcolumn_totalpositive_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumn_totalpositive_body_steps_successor. fs_h_dst_fubini_exists_resultcolumn_totalpositive_body_steps_successor + S (fs_s_dst_fubini_exists_resultcolumn_totalpositive_body_steps) = S ((S (S fs_i_dst_fubini_exists_resultcolumn_totalpositive_body_steps)) * fs_v_dst_fubini_exists_resultcolumn_totalpositive)) /\ exists fs_q_dst_fubini_exists_resultcolumn_totalpositive_body_steps_successor. fs_u_dst_fubini_exists_resultcolumn_totalpositive = fs_q_dst_fubini_exists_resultcolumn_totalpositive_body_steps_successor * S ((S (S fs_i_dst_fubini_exists_resultcolumn_totalpositive_body_steps)) * fs_v_dst_fubini_exists_resultcolumn_totalpositive) + (fs_s_dst_fubini_exists_resultcolumn_totalpositive_body_steps))) /\ fs_s_dst_fubini_exists_resultcolumn_totalpositive_body_steps = fs_r_dst_fubini_exists_resultcolumn_totalpositive_body_steps + fs_a_dst_fubini_exists_resultcolumn_totalpositive_body_steps)))))) /\ (((exists fs_u_dst_fubini_exists_resultcolumn_totalnegative fs_v_dst_fubini_exists_resultcolumn_totalnegative. ((((exists fs_h_dst_fubini_exists_resultcolumn_totalnegative_body_start. fs_h_dst_fubini_exists_resultcolumn_totalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_fubini_exists_resultcolumn_totalnegative)) /\ exists fs_q_dst_fubini_exists_resultcolumn_totalnegative_body_start. fs_u_dst_fubini_exists_resultcolumn_totalnegative = fs_q_dst_fubini_exists_resultcolumn_totalnegative_body_start * S ((S (0)) * fs_v_dst_fubini_exists_resultcolumn_totalnegative) + (0))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumn_totalnegative_body_terminal. fs_h_dst_fubini_exists_resultcolumn_totalnegative_body_terminal + S (dst_negative_sum_fubini_exists_resultcolumn_total) = S ((S (n)) * fs_v_dst_fubini_exists_resultcolumn_totalnegative)) /\ exists fs_q_dst_fubini_exists_resultcolumn_totalnegative_body_terminal. fs_u_dst_fubini_exists_resultcolumn_totalnegative = fs_q_dst_fubini_exists_resultcolumn_totalnegative_body_terminal * S ((S (n)) * fs_v_dst_fubini_exists_resultcolumn_totalnegative) + (dst_negative_sum_fubini_exists_resultcolumn_total))) /\ forall fs_i_dst_fubini_exists_resultcolumn_totalnegative_body_steps. (exists fs_lt_dst_fubini_exists_resultcolumn_totalnegative_body_steps_bound. fs_lt_dst_fubini_exists_resultcolumn_totalnegative_body_steps_bound + S fs_i_dst_fubini_exists_resultcolumn_totalnegative_body_steps = n) -> exists fs_a_dst_fubini_exists_resultcolumn_totalnegative_body_steps fs_r_dst_fubini_exists_resultcolumn_totalnegative_body_steps fs_s_dst_fubini_exists_resultcolumn_totalnegative_body_steps. ((((exists fs_h_dst_fubini_exists_resultcolumn_totalnegative_body_steps_summand. fs_h_dst_fubini_exists_resultcolumn_totalnegative_body_steps_summand + S (fs_a_dst_fubini_exists_resultcolumn_totalnegative_body_steps) = S ((S (fs_i_dst_fubini_exists_resultcolumn_totalnegative_body_steps)) * dst_negative_scale_fubini_exists_resultcolumn_total)) /\ exists fs_q_dst_fubini_exists_resultcolumn_totalnegative_body_steps_summand. dst_negative_code_fubini_exists_resultcolumn_total = fs_q_dst_fubini_exists_resultcolumn_totalnegative_body_steps_summand * S ((S (fs_i_dst_fubini_exists_resultcolumn_totalnegative_body_steps)) * dst_negative_scale_fubini_exists_resultcolumn_total) + (fs_a_dst_fubini_exists_resultcolumn_totalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumn_totalnegative_body_steps_partial. fs_h_dst_fubini_exists_resultcolumn_totalnegative_body_steps_partial + S (fs_r_dst_fubini_exists_resultcolumn_totalnegative_body_steps) = S ((S (fs_i_dst_fubini_exists_resultcolumn_totalnegative_body_steps)) * fs_v_dst_fubini_exists_resultcolumn_totalnegative)) /\ exists fs_q_dst_fubini_exists_resultcolumn_totalnegative_body_steps_partial. fs_u_dst_fubini_exists_resultcolumn_totalnegative = fs_q_dst_fubini_exists_resultcolumn_totalnegative_body_steps_partial * S ((S (fs_i_dst_fubini_exists_resultcolumn_totalnegative_body_steps)) * fs_v_dst_fubini_exists_resultcolumn_totalnegative) + (fs_r_dst_fubini_exists_resultcolumn_totalnegative_body_steps))) /\ ((((exists fs_h_dst_fubini_exists_resultcolumn_totalnegative_body_steps_successor. fs_h_dst_fubini_exists_resultcolumn_totalnegative_body_steps_successor + S (fs_s_dst_fubini_exists_resultcolumn_totalnegative_body_steps) = S ((S (S fs_i_dst_fubini_exists_resultcolumn_totalnegative_body_steps)) * fs_v_dst_fubini_exists_resultcolumn_totalnegative)) /\ exists fs_q_dst_fubini_exists_resultcolumn_totalnegative_body_steps_successor. fs_u_dst_fubini_exists_resultcolumn_totalnegative = fs_q_dst_fubini_exists_resultcolumn_totalnegative_body_steps_successor * S ((S (S fs_i_dst_fubini_exists_resultcolumn_totalnegative_body_steps)) * fs_v_dst_fubini_exists_resultcolumn_totalnegative) + (fs_s_dst_fubini_exists_resultcolumn_totalnegative_body_steps))) /\ fs_s_dst_fubini_exists_resultcolumn_totalnegative_body_steps = fs_r_dst_fubini_exists_resultcolumn_totalnegative_body_steps + fs_a_dst_fubini_exists_resultcolumn_totalnegative_body_steps)))))) /\ (exists ge_balance_positive_fubini_exists_resultcolumn_totalresult ge_balance_negative_fubini_exists_resultcolumn_totalresult. (((((z) = 2 * (ge_balance_positive_fubini_exists_resultcolumn_totalresult) /\ (ge_balance_negative_fubini_exists_resultcolumn_totalresult) = 0) \/ exists ge_signed_half_fubini_exists_resultcolumn_totalresultdecode. (((z) = 2 * ge_signed_half_fubini_exists_resultcolumn_totalresultdecode + 1 /\ (ge_balance_positive_fubini_exists_resultcolumn_totalresult) = 0) /\ (ge_balance_negative_fubini_exists_resultcolumn_totalresult) = S ge_signed_half_fubini_exists_resultcolumn_totalresultdecode))) /\ ((dst_positive_sum_fubini_exists_resultcolumn_total) + ge_balance_negative_fubini_exists_resultcolumn_totalresult = (dst_negative_sum_fubini_exists_resultcolumn_total) + ge_balance_positive_fubini_exists_resultcolumn_totalresult)))))))))))))))