Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall F o s t m n a b. (exists srt_rows_sum_functional_first. ((((exists dst_positive_code_sum_functional_firstrowssource_table dst_positive_scale_sum_functional_firstrowssource_table dst_negative_code_sum_functional_firstrowssource_table dst_negative_scale_sum_functional_firstrowssource_table. (((F) = (((((dst_positive_code_sum_functional_firstrowssource_table) + (dst_positive_scale_sum_functional_firstrowssource_table)) * S ((dst_positive_code_sum_functional_firstrowssource_table) + (dst_positive_scale_sum_functional_firstrowssource_table)) + ((dst_positive_scale_sum_functional_firstrowssource_table) + (dst_positive_scale_sum_functional_firstrowssource_table))) + (((dst_negative_code_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)) * S ((dst_negative_code_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)) + ((dst_negative_scale_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)))) * S ((((dst_positive_code_sum_functional_firstrowssource_table) + (dst_positive_scale_sum_functional_firstrowssource_table)) * S ((dst_positive_code_sum_functional_firstrowssource_table) + (dst_positive_scale_sum_functional_firstrowssource_table)) + ((dst_positive_scale_sum_functional_firstrowssource_table) + (dst_positive_scale_sum_functional_firstrowssource_table))) + (((dst_negative_code_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)) * S ((dst_negative_code_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)) + ((dst_negative_scale_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)))) + ((((dst_negative_code_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)) * S ((dst_negative_code_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)) + ((dst_negative_scale_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table))) + (((dst_negative_code_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)) * S ((dst_negative_code_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)) + ((dst_negative_scale_sum_functional_firstrowssource_table) + (dst_negative_scale_sum_functional_firstrowssource_table)))))) /\ (forall dst_index_sum_functional_firstrowssource_table. (exists pvs_le_gap_sum_functional_firstrowssource_tabledomain. pvs_le_gap_sum_functional_firstrowssource_tabledomain + (dst_index_sum_functional_firstrowssource_table) = (0)) -> exists dst_positive_sum_functional_firstrowssource_table dst_negative_sum_functional_firstrowssource_table dst_value_sum_functional_firstrowssource_table. ((((exists ff_h_pvs_sum_functional_firstrowssource_tableentrypositive. ff_h_pvs_sum_functional_firstrowssource_tableentrypositive + S (dst_positive_sum_functional_firstrowssource_table) = S ((S (dst_index_sum_functional_firstrowssource_table)) * dst_positive_scale_sum_functional_firstrowssource_table)) /\ exists ff_q_pvs_sum_functional_firstrowssource_tableentrypositive. dst_positive_code_sum_functional_firstrowssource_table = ff_q_pvs_sum_functional_firstrowssource_tableentrypositive * S ((S (dst_index_sum_functional_firstrowssource_table)) * dst_positive_scale_sum_functional_firstrowssource_table) + (dst_positive_sum_functional_firstrowssource_table))) /\ (((((exists ff_h_pvs_sum_functional_firstrowssource_tableentrynegative. ff_h_pvs_sum_functional_firstrowssource_tableentrynegative + S (dst_negative_sum_functional_firstrowssource_table) = S ((S (dst_index_sum_functional_firstrowssource_table)) * dst_negative_scale_sum_functional_firstrowssource_table)) /\ exists ff_q_pvs_sum_functional_firstrowssource_tableentrynegative. dst_negative_code_sum_functional_firstrowssource_table = ff_q_pvs_sum_functional_firstrowssource_tableentrynegative * S ((S (dst_index_sum_functional_firstrowssource_table)) * dst_negative_scale_sum_functional_firstrowssource_table) + (dst_negative_sum_functional_firstrowssource_table))) /\ (exists ge_balance_positive_sum_functional_firstrowssource_tableentryvalue ge_balance_negative_sum_functional_firstrowssource_tableentryvalue. (((((dst_value_sum_functional_firstrowssource_table) = 2 * (ge_balance_positive_sum_functional_firstrowssource_tableentryvalue) /\ (ge_balance_negative_sum_functional_firstrowssource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_firstrowssource_tableentryvaluedecode. (((dst_value_sum_functional_firstrowssource_table) = 2 * ge_signed_half_sum_functional_firstrowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstrowssource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_firstrowssource_tableentryvalue) = S ge_signed_half_sum_functional_firstrowssource_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_firstrowssource_table) + ge_balance_negative_sum_functional_firstrowssource_tableentryvalue = (dst_negative_sum_functional_firstrowssource_table) + ge_balance_positive_sum_functional_firstrowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_functional_firstrowsrow_table dst_positive_scale_sum_functional_firstrowsrow_table dst_negative_code_sum_functional_firstrowsrow_table dst_negative_scale_sum_functional_firstrowsrow_table. (((srt_rows_sum_functional_first) = (((((dst_positive_code_sum_functional_firstrowsrow_table) + (dst_positive_scale_sum_functional_firstrowsrow_table)) * S ((dst_positive_code_sum_functional_firstrowsrow_table) + (dst_positive_scale_sum_functional_firstrowsrow_table)) + ((dst_positive_scale_sum_functional_firstrowsrow_table) + (dst_positive_scale_sum_functional_firstrowsrow_table))) + (((dst_negative_code_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)) * S ((dst_negative_code_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)) + ((dst_negative_scale_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)))) * S ((((dst_positive_code_sum_functional_firstrowsrow_table) + (dst_positive_scale_sum_functional_firstrowsrow_table)) * S ((dst_positive_code_sum_functional_firstrowsrow_table) + (dst_positive_scale_sum_functional_firstrowsrow_table)) + ((dst_positive_scale_sum_functional_firstrowsrow_table) + (dst_positive_scale_sum_functional_firstrowsrow_table))) + (((dst_negative_code_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)) * S ((dst_negative_code_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)) + ((dst_negative_scale_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)))) + ((((dst_negative_code_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)) * S ((dst_negative_code_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)) + ((dst_negative_scale_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table))) + (((dst_negative_code_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)) * S ((dst_negative_code_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)) + ((dst_negative_scale_sum_functional_firstrowsrow_table) + (dst_negative_scale_sum_functional_firstrowsrow_table)))))) /\ (forall dst_index_sum_functional_firstrowsrow_table. (exists pvs_le_gap_sum_functional_firstrowsrow_tabledomain. pvs_le_gap_sum_functional_firstrowsrow_tabledomain + (dst_index_sum_functional_firstrowsrow_table) = (m)) -> exists dst_positive_sum_functional_firstrowsrow_table dst_negative_sum_functional_firstrowsrow_table dst_value_sum_functional_firstrowsrow_table. ((((exists ff_h_pvs_sum_functional_firstrowsrow_tableentrypositive. ff_h_pvs_sum_functional_firstrowsrow_tableentrypositive + S (dst_positive_sum_functional_firstrowsrow_table) = S ((S (dst_index_sum_functional_firstrowsrow_table)) * dst_positive_scale_sum_functional_firstrowsrow_table)) /\ exists ff_q_pvs_sum_functional_firstrowsrow_tableentrypositive. dst_positive_code_sum_functional_firstrowsrow_table = ff_q_pvs_sum_functional_firstrowsrow_tableentrypositive * S ((S (dst_index_sum_functional_firstrowsrow_table)) * dst_positive_scale_sum_functional_firstrowsrow_table) + (dst_positive_sum_functional_firstrowsrow_table))) /\ (((((exists ff_h_pvs_sum_functional_firstrowsrow_tableentrynegative. ff_h_pvs_sum_functional_firstrowsrow_tableentrynegative + S (dst_negative_sum_functional_firstrowsrow_table) = S ((S (dst_index_sum_functional_firstrowsrow_table)) * dst_negative_scale_sum_functional_firstrowsrow_table)) /\ exists ff_q_pvs_sum_functional_firstrowsrow_tableentrynegative. dst_negative_code_sum_functional_firstrowsrow_table = ff_q_pvs_sum_functional_firstrowsrow_tableentrynegative * S ((S (dst_index_sum_functional_firstrowsrow_table)) * dst_negative_scale_sum_functional_firstrowsrow_table) + (dst_negative_sum_functional_firstrowsrow_table))) /\ (exists ge_balance_positive_sum_functional_firstrowsrow_tableentryvalue ge_balance_negative_sum_functional_firstrowsrow_tableentryvalue. (((((dst_value_sum_functional_firstrowsrow_table) = 2 * (ge_balance_positive_sum_functional_firstrowsrow_tableentryvalue) /\ (ge_balance_negative_sum_functional_firstrowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_firstrowsrow_tableentryvaluedecode. (((dst_value_sum_functional_firstrowsrow_table) = 2 * ge_signed_half_sum_functional_firstrowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstrowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_firstrowsrow_tableentryvalue) = S ge_signed_half_sum_functional_firstrowsrow_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_firstrowsrow_table) + ge_balance_negative_sum_functional_firstrowsrow_tableentryvalue = (dst_negative_sum_functional_firstrowsrow_table) + ge_balance_positive_sum_functional_firstrowsrow_tableentryvalue))))))))) /\ (forall srt_index_sum_functional_firstrows. (exists pvs_gap_sum_functional_firstrowsbound. pvs_gap_sum_functional_firstrowsbound + S (srt_index_sum_functional_firstrows) = (m)) -> exists srt_value_sum_functional_firstrows. (((exists dst_positive_code_sum_functional_firstrowsrowentry dst_positive_scale_sum_functional_firstrowsrowentry dst_negative_code_sum_functional_firstrowsrowentry dst_negative_scale_sum_functional_firstrowsrowentry dst_positive_sum_functional_firstrowsrowentry dst_negative_sum_functional_firstrowsrowentry. (((srt_rows_sum_functional_first) = (((((dst_positive_code_sum_functional_firstrowsrowentry) + (dst_positive_scale_sum_functional_firstrowsrowentry)) * S ((dst_positive_code_sum_functional_firstrowsrowentry) + (dst_positive_scale_sum_functional_firstrowsrowentry)) + ((dst_positive_scale_sum_functional_firstrowsrowentry) + (dst_positive_scale_sum_functional_firstrowsrowentry))) + (((dst_negative_code_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)) * S ((dst_negative_code_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)) + ((dst_negative_scale_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)))) * S ((((dst_positive_code_sum_functional_firstrowsrowentry) + (dst_positive_scale_sum_functional_firstrowsrowentry)) * S ((dst_positive_code_sum_functional_firstrowsrowentry) + (dst_positive_scale_sum_functional_firstrowsrowentry)) + ((dst_positive_scale_sum_functional_firstrowsrowentry) + (dst_positive_scale_sum_functional_firstrowsrowentry))) + (((dst_negative_code_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)) * S ((dst_negative_code_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)) + ((dst_negative_scale_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)))) + ((((dst_negative_code_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)) * S ((dst_negative_code_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)) + ((dst_negative_scale_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry))) + (((dst_negative_code_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)) * S ((dst_negative_code_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)) + ((dst_negative_scale_sum_functional_firstrowsrowentry) + (dst_negative_scale_sum_functional_firstrowsrowentry)))))) /\ (((((exists ff_h_pvs_sum_functional_firstrowsrowentrypositive. ff_h_pvs_sum_functional_firstrowsrowentrypositive + S (dst_positive_sum_functional_firstrowsrowentry) = S ((S (srt_index_sum_functional_firstrows)) * dst_positive_scale_sum_functional_firstrowsrowentry)) /\ exists ff_q_pvs_sum_functional_firstrowsrowentrypositive. dst_positive_code_sum_functional_firstrowsrowentry = ff_q_pvs_sum_functional_firstrowsrowentrypositive * S ((S (srt_index_sum_functional_firstrows)) * dst_positive_scale_sum_functional_firstrowsrowentry) + (dst_positive_sum_functional_firstrowsrowentry))) /\ (((((exists ff_h_pvs_sum_functional_firstrowsrowentrynegative. ff_h_pvs_sum_functional_firstrowsrowentrynegative + S (dst_negative_sum_functional_firstrowsrowentry) = S ((S (srt_index_sum_functional_firstrows)) * dst_negative_scale_sum_functional_firstrowsrowentry)) /\ exists ff_q_pvs_sum_functional_firstrowsrowentrynegative. dst_negative_code_sum_functional_firstrowsrowentry = ff_q_pvs_sum_functional_firstrowsrowentrynegative * S ((S (srt_index_sum_functional_firstrows)) * dst_negative_scale_sum_functional_firstrowsrowentry) + (dst_negative_sum_functional_firstrowsrowentry))) /\ (exists ge_balance_positive_sum_functional_firstrowsrowentryvalue ge_balance_negative_sum_functional_firstrowsrowentryvalue. (((((srt_value_sum_functional_firstrows) = 2 * (ge_balance_positive_sum_functional_firstrowsrowentryvalue) /\ (ge_balance_negative_sum_functional_firstrowsrowentryvalue) = 0) \/ exists ge_signed_half_sum_functional_firstrowsrowentryvaluedecode. (((srt_value_sum_functional_firstrows) = 2 * ge_signed_half_sum_functional_firstrowsrowentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstrowsrowentryvalue) = 0) /\ (ge_balance_negative_sum_functional_firstrowsrowentryvalue) = S ge_signed_half_sum_functional_firstrowsrowentryvaluedecode))) /\ ((dst_positive_sum_functional_firstrowsrowentry) + ge_balance_negative_sum_functional_firstrowsrowentryvalue = (dst_negative_sum_functional_firstrowsrowentry) + ge_balance_positive_sum_functional_firstrowsrowentryvalue))))))))) /\ (exists srs_slice_sum_functional_firstrowsrowrow_sum. ((((exists dst_positive_code_sum_functional_firstrowsrowrow_sumslicesource_table dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table dst_negative_code_sum_functional_firstrowsrowrow_sumslicesource_table dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_sum_functional_firstrowsrowrow_sumslicesource_table. (exists pvs_le_gap_sum_functional_firstrowsrowrow_sumslicesource_tabledomain. pvs_le_gap_sum_functional_firstrowsrowrow_sumslicesource_tabledomain + (dst_index_sum_functional_firstrowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_sum_functional_firstrowsrowrow_sumslicesource_table dst_negative_sum_functional_firstrowsrowrow_sumslicesource_table dst_value_sum_functional_firstrowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_sum_functional_firstrowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_sum_functional_firstrowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_sum_functional_firstrowsrowrow_sumslicesource_table) = S ((S (dst_index_sum_functional_firstrowsrowrow_sumslicesource_table)) * dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_sum_functional_firstrowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_sum_functional_firstrowsrowrow_sumslicesource_table = ff_q_pvs_sum_functional_firstrowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_sum_functional_firstrowsrowrow_sumslicesource_table)) * dst_positive_scale_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_positive_sum_functional_firstrowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_sum_functional_firstrowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_sum_functional_firstrowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_sum_functional_firstrowsrowrow_sumslicesource_table) = S ((S (dst_index_sum_functional_firstrowsrowrow_sumslicesource_table)) * dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_sum_functional_firstrowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_sum_functional_firstrowsrowrow_sumslicesource_table = ff_q_pvs_sum_functional_firstrowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_sum_functional_firstrowsrowrow_sumslicesource_table)) * dst_negative_scale_sum_functional_firstrowsrowrow_sumslicesource_table) + (dst_negative_sum_functional_firstrowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_sum_functional_firstrowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_sum_functional_firstrowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_sum_functional_firstrowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_sum_functional_firstrowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_sum_functional_firstrowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_firstrowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_sum_functional_firstrowsrowrow_sumslicesource_table) = 2 * ge_signed_half_sum_functional_firstrowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstrowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_firstrowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_sum_functional_firstrowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_firstrowsrowrow_sumslicesource_table) + ge_balance_negative_sum_functional_firstrowsrowrow_sumslicesource_tableentryvalue = (dst_negative_sum_functional_firstrowsrowrow_sumslicesource_table) + ge_balance_positive_sum_functional_firstrowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_functional_firstrowsrowrow_sumsliceoutput_table dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table dst_negative_code_sum_functional_firstrowsrowrow_sumsliceoutput_table dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table. (((srs_slice_sum_functional_firstrowsrowrow_sum) = (((((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_sum_functional_firstrowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_sum_functional_firstrowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_sum_functional_firstrowsrowrow_sumsliceoutput_tabledomain + (dst_index_sum_functional_firstrowsrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_sum_functional_firstrowsrowrow_sumsliceoutput_table dst_negative_sum_functional_firstrowsrowrow_sumsliceoutput_table dst_value_sum_functional_firstrowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_sum_functional_firstrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_sum_functional_firstrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_sum_functional_firstrowsrowrow_sumsliceoutput_table = ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_sum_functional_firstrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_positive_sum_functional_firstrowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_sum_functional_firstrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_sum_functional_firstrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_sum_functional_firstrowsrowrow_sumsliceoutput_table = ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_sum_functional_firstrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceoutput_table) + (dst_negative_sum_functional_firstrowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_sum_functional_firstrowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_sum_functional_firstrowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_firstrowsrowrow_sumsliceoutput_table) + ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_sum_functional_firstrowsrowrow_sumsliceoutput_table) + ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_functional_firstrowsrowrow_sumslice. (exists pvs_gap_sum_functional_firstrowsrowrow_sumslicebound. pvs_gap_sum_functional_firstrowsrowrow_sumslicebound + S (srs_index_sum_functional_firstrowsrowrow_sumslice) = (n)) -> exists srs_value_sum_functional_firstrowsrowrow_sumslice. (((exists dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentrysource dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentrysource dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource dst_positive_sum_functional_firstrowsrowrow_sumsliceentrysource dst_negative_sum_functional_firstrowsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceentrysourcepositive + S (dst_positive_sum_functional_firstrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_sum_functional_firstrows)))) + ((t) * (srs_index_sum_functional_firstrowsrowrow_sumslice))))) * dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceentrysourcepositive. dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentrysource = ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((s) * (srt_index_sum_functional_firstrows)))) + ((t) * (srs_index_sum_functional_firstrowsrowrow_sumslice))))) * dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_positive_sum_functional_firstrowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceentrysourcenegative + S (dst_negative_sum_functional_firstrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_sum_functional_firstrows)))) + ((t) * (srs_index_sum_functional_firstrowsrowrow_sumslice))))) * dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceentrysourcenegative. dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentrysource = ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((s) * (srt_index_sum_functional_firstrows)))) + ((t) * (srs_index_sum_functional_firstrowsrowrow_sumslice))))) * dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentrysource) + (dst_negative_sum_functional_firstrowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceentrysourcevalue ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceentrysourcevalue. (((((srs_value_sum_functional_firstrowsrowrow_sumslice) = 2 * (ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_functional_firstrowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_sum_functional_firstrowsrowrow_sumslice) = 2 * ge_signed_half_sum_functional_firstrowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_sum_functional_firstrowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_functional_firstrowsrowrow_sumsliceentrysource) + ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceentrysourcevalue = (dst_negative_sum_functional_firstrowsrowrow_sumsliceentrysource) + ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentryoutput dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentryoutput dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput dst_positive_sum_functional_firstrowsrowrow_sumsliceentryoutput dst_negative_sum_functional_firstrowsrowrow_sumsliceentryoutput. (((srs_slice_sum_functional_firstrowsrowrow_sum) = (((((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceentryoutputpositive + S (dst_positive_sum_functional_firstrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_sum_functional_firstrowsrowrow_sumslice)) * dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceentryoutputpositive. dst_positive_code_sum_functional_firstrowsrowrow_sumsliceentryoutput = ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_sum_functional_firstrowsrowrow_sumslice)) * dst_positive_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_positive_sum_functional_firstrowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_sum_functional_firstrowsrowrow_sumsliceentryoutputnegative + S (dst_negative_sum_functional_firstrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_sum_functional_firstrowsrowrow_sumslice)) * dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceentryoutputnegative. dst_negative_code_sum_functional_firstrowsrowrow_sumsliceentryoutput = ff_q_pvs_sum_functional_firstrowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_sum_functional_firstrowsrowrow_sumslice)) * dst_negative_scale_sum_functional_firstrowsrowrow_sumsliceentryoutput) + (dst_negative_sum_functional_firstrowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceentryoutputvalue ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceentryoutputvalue. (((((srs_value_sum_functional_firstrowsrowrow_sumslice) = 2 * (ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_functional_firstrowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_sum_functional_firstrowsrowrow_sumslice) = 2 * ge_signed_half_sum_functional_firstrowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_sum_functional_firstrowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_functional_firstrowsrowrow_sumsliceentryoutput) + ge_balance_negative_sum_functional_firstrowsrowrow_sumsliceentryoutputvalue = (dst_negative_sum_functional_firstrowsrowrow_sumsliceentryoutput) + ge_balance_positive_sum_functional_firstrowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_functional_firstrowsrowrow_sumsum dst_positive_scale_sum_functional_firstrowsrowrow_sumsum dst_negative_code_sum_functional_firstrowsrowrow_sumsum dst_negative_scale_sum_functional_firstrowsrowrow_sumsum dst_positive_sum_sum_functional_firstrowsrowrow_sumsum dst_negative_sum_sum_functional_firstrowsrowrow_sumsum. (((srs_slice_sum_functional_firstrowsrowrow_sum) = (((((dst_positive_code_sum_functional_firstrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsum)) * S ((dst_positive_code_sum_functional_firstrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsum)) + ((dst_positive_scale_sum_functional_firstrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsum))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)))) * S ((((dst_positive_code_sum_functional_firstrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsum)) * S ((dst_positive_code_sum_functional_firstrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsum)) + ((dst_positive_scale_sum_functional_firstrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_firstrowsrowrow_sumsum))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)))) + ((((dst_negative_code_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum))) + (((dst_negative_code_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)) * S ((dst_negative_code_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)) + ((dst_negative_scale_sum_functional_firstrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_sum_functional_firstrowsrowrow_sumsumpositive fs_v_dst_sum_functional_firstrowsrowrow_sumsumpositive. ((((exists fs_h_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_start. fs_h_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_start. fs_u_dst_sum_functional_firstrowsrowrow_sumsumpositive = fs_q_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_terminal. fs_h_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_sum_functional_firstrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_terminal. fs_u_dst_sum_functional_firstrowsrowrow_sumsumpositive = fs_q_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumpositive) + (dst_positive_sum_sum_functional_firstrowsrowrow_sumsum))) /\ forall fs_i_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps fs_r_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps fs_s_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_sum_functional_firstrowsrowrow_sumsum)) /\ exists fs_q_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_sum_functional_firstrowsrowrow_sumsum = fs_q_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_sum_functional_firstrowsrowrow_sumsum) + (fs_a_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_sum_functional_firstrowsrowrow_sumsumpositive = fs_q_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumpositive) + (fs_r_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_sum_functional_firstrowsrowrow_sumsumpositive = fs_q_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumpositive) + (fs_s_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps = fs_r_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps + fs_a_dst_sum_functional_firstrowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_functional_firstrowsrowrow_sumsumnegative fs_v_dst_sum_functional_firstrowsrowrow_sumsumnegative. ((((exists fs_h_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_start. fs_h_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_start. fs_u_dst_sum_functional_firstrowsrowrow_sumsumnegative = fs_q_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_terminal. fs_h_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_sum_functional_firstrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_terminal. fs_u_dst_sum_functional_firstrowsrowrow_sumsumnegative = fs_q_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumnegative) + (dst_negative_sum_sum_functional_firstrowsrowrow_sumsum))) /\ forall fs_i_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps fs_r_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps fs_s_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_sum_functional_firstrowsrowrow_sumsum)) /\ exists fs_q_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_sum_functional_firstrowsrowrow_sumsum = fs_q_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_sum_functional_firstrowsrowrow_sumsum) + (fs_a_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_sum_functional_firstrowsrowrow_sumsumnegative = fs_q_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumnegative) + (fs_r_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_sum_functional_firstrowsrowrow_sumsumnegative = fs_q_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_sum_functional_firstrowsrowrow_sumsumnegative) + (fs_s_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps = fs_r_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps + fs_a_dst_sum_functional_firstrowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_functional_firstrowsrowrow_sumsumresult ge_balance_negative_sum_functional_firstrowsrowrow_sumsumresult. (((((srt_value_sum_functional_firstrows) = 2 * (ge_balance_positive_sum_functional_firstrowsrowrow_sumsumresult) /\ (ge_balance_negative_sum_functional_firstrowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_sum_functional_firstrowsrowrow_sumsumresultdecode. (((srt_value_sum_functional_firstrows) = 2 * ge_signed_half_sum_functional_firstrowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_sum_functional_firstrowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_sum_functional_firstrowsrowrow_sumsumresult) = S ge_signed_half_sum_functional_firstrowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_sum_functional_firstrowsrowrow_sumsum) + ge_balance_negative_sum_functional_firstrowsrowrow_sumsumresult = (dst_negative_sum_sum_functional_firstrowsrowrow_sumsum) + ge_balance_positive_sum_functional_firstrowsrowrow_sumsumresult)))))))))))))))))) /\ (exists dst_positive_code_sum_functional_firsttotal dst_positive_scale_sum_functional_firsttotal dst_negative_code_sum_functional_firsttotal dst_negative_scale_sum_functional_firsttotal dst_positive_sum_sum_functional_firsttotal dst_negative_sum_sum_functional_firsttotal. (((srt_rows_sum_functional_first) = (((((dst_positive_code_sum_functional_firsttotal) + (dst_positive_scale_sum_functional_firsttotal)) * S ((dst_positive_code_sum_functional_firsttotal) + (dst_positive_scale_sum_functional_firsttotal)) + ((dst_positive_scale_sum_functional_firsttotal) + (dst_positive_scale_sum_functional_firsttotal))) + (((dst_negative_code_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)) * S ((dst_negative_code_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)) + ((dst_negative_scale_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)))) * S ((((dst_positive_code_sum_functional_firsttotal) + (dst_positive_scale_sum_functional_firsttotal)) * S ((dst_positive_code_sum_functional_firsttotal) + (dst_positive_scale_sum_functional_firsttotal)) + ((dst_positive_scale_sum_functional_firsttotal) + (dst_positive_scale_sum_functional_firsttotal))) + (((dst_negative_code_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)) * S ((dst_negative_code_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)) + ((dst_negative_scale_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)))) + ((((dst_negative_code_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)) * S ((dst_negative_code_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)) + ((dst_negative_scale_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal))) + (((dst_negative_code_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)) * S ((dst_negative_code_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)) + ((dst_negative_scale_sum_functional_firsttotal) + (dst_negative_scale_sum_functional_firsttotal)))))) /\ (((exists fs_u_dst_sum_functional_firsttotalpositive fs_v_dst_sum_functional_firsttotalpositive. ((((exists fs_h_dst_sum_functional_firsttotalpositive_body_start. fs_h_dst_sum_functional_firsttotalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_firsttotalpositive)) /\ exists fs_q_dst_sum_functional_firsttotalpositive_body_start. fs_u_dst_sum_functional_firsttotalpositive = fs_q_dst_sum_functional_firsttotalpositive_body_start * S ((S (0)) * fs_v_dst_sum_functional_firsttotalpositive) + (0))) /\ ((((exists fs_h_dst_sum_functional_firsttotalpositive_body_terminal. fs_h_dst_sum_functional_firsttotalpositive_body_terminal + S (dst_positive_sum_sum_functional_firsttotal) = S ((S (m)) * fs_v_dst_sum_functional_firsttotalpositive)) /\ exists fs_q_dst_sum_functional_firsttotalpositive_body_terminal. fs_u_dst_sum_functional_firsttotalpositive = fs_q_dst_sum_functional_firsttotalpositive_body_terminal * S ((S (m)) * fs_v_dst_sum_functional_firsttotalpositive) + (dst_positive_sum_sum_functional_firsttotal))) /\ forall fs_i_dst_sum_functional_firsttotalpositive_body_steps. (exists fs_lt_dst_sum_functional_firsttotalpositive_body_steps_bound. fs_lt_dst_sum_functional_firsttotalpositive_body_steps_bound + S fs_i_dst_sum_functional_firsttotalpositive_body_steps = m) -> exists fs_a_dst_sum_functional_firsttotalpositive_body_steps fs_r_dst_sum_functional_firsttotalpositive_body_steps fs_s_dst_sum_functional_firsttotalpositive_body_steps. ((((exists fs_h_dst_sum_functional_firsttotalpositive_body_steps_summand. fs_h_dst_sum_functional_firsttotalpositive_body_steps_summand + S (fs_a_dst_sum_functional_firsttotalpositive_body_steps) = S ((S (fs_i_dst_sum_functional_firsttotalpositive_body_steps)) * dst_positive_scale_sum_functional_firsttotal)) /\ exists fs_q_dst_sum_functional_firsttotalpositive_body_steps_summand. dst_positive_code_sum_functional_firsttotal = fs_q_dst_sum_functional_firsttotalpositive_body_steps_summand * S ((S (fs_i_dst_sum_functional_firsttotalpositive_body_steps)) * dst_positive_scale_sum_functional_firsttotal) + (fs_a_dst_sum_functional_firsttotalpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firsttotalpositive_body_steps_partial. fs_h_dst_sum_functional_firsttotalpositive_body_steps_partial + S (fs_r_dst_sum_functional_firsttotalpositive_body_steps) = S ((S (fs_i_dst_sum_functional_firsttotalpositive_body_steps)) * fs_v_dst_sum_functional_firsttotalpositive)) /\ exists fs_q_dst_sum_functional_firsttotalpositive_body_steps_partial. fs_u_dst_sum_functional_firsttotalpositive = fs_q_dst_sum_functional_firsttotalpositive_body_steps_partial * S ((S (fs_i_dst_sum_functional_firsttotalpositive_body_steps)) * fs_v_dst_sum_functional_firsttotalpositive) + (fs_r_dst_sum_functional_firsttotalpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firsttotalpositive_body_steps_successor. fs_h_dst_sum_functional_firsttotalpositive_body_steps_successor + S (fs_s_dst_sum_functional_firsttotalpositive_body_steps) = S ((S (S fs_i_dst_sum_functional_firsttotalpositive_body_steps)) * fs_v_dst_sum_functional_firsttotalpositive)) /\ exists fs_q_dst_sum_functional_firsttotalpositive_body_steps_successor. fs_u_dst_sum_functional_firsttotalpositive = fs_q_dst_sum_functional_firsttotalpositive_body_steps_successor * S ((S (S fs_i_dst_sum_functional_firsttotalpositive_body_steps)) * fs_v_dst_sum_functional_firsttotalpositive) + (fs_s_dst_sum_functional_firsttotalpositive_body_steps))) /\ fs_s_dst_sum_functional_firsttotalpositive_body_steps = fs_r_dst_sum_functional_firsttotalpositive_body_steps + fs_a_dst_sum_functional_firsttotalpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_functional_firsttotalnegative fs_v_dst_sum_functional_firsttotalnegative. ((((exists fs_h_dst_sum_functional_firsttotalnegative_body_start. fs_h_dst_sum_functional_firsttotalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_firsttotalnegative)) /\ exists fs_q_dst_sum_functional_firsttotalnegative_body_start. fs_u_dst_sum_functional_firsttotalnegative = fs_q_dst_sum_functional_firsttotalnegative_body_start * S ((S (0)) * fs_v_dst_sum_functional_firsttotalnegative) + (0))) /\ ((((exists fs_h_dst_sum_functional_firsttotalnegative_body_terminal. fs_h_dst_sum_functional_firsttotalnegative_body_terminal + S (dst_negative_sum_sum_functional_firsttotal) = S ((S (m)) * fs_v_dst_sum_functional_firsttotalnegative)) /\ exists fs_q_dst_sum_functional_firsttotalnegative_body_terminal. fs_u_dst_sum_functional_firsttotalnegative = fs_q_dst_sum_functional_firsttotalnegative_body_terminal * S ((S (m)) * fs_v_dst_sum_functional_firsttotalnegative) + (dst_negative_sum_sum_functional_firsttotal))) /\ forall fs_i_dst_sum_functional_firsttotalnegative_body_steps. (exists fs_lt_dst_sum_functional_firsttotalnegative_body_steps_bound. fs_lt_dst_sum_functional_firsttotalnegative_body_steps_bound + S fs_i_dst_sum_functional_firsttotalnegative_body_steps = m) -> exists fs_a_dst_sum_functional_firsttotalnegative_body_steps fs_r_dst_sum_functional_firsttotalnegative_body_steps fs_s_dst_sum_functional_firsttotalnegative_body_steps. ((((exists fs_h_dst_sum_functional_firsttotalnegative_body_steps_summand. fs_h_dst_sum_functional_firsttotalnegative_body_steps_summand + S (fs_a_dst_sum_functional_firsttotalnegative_body_steps) = S ((S (fs_i_dst_sum_functional_firsttotalnegative_body_steps)) * dst_negative_scale_sum_functional_firsttotal)) /\ exists fs_q_dst_sum_functional_firsttotalnegative_body_steps_summand. dst_negative_code_sum_functional_firsttotal = fs_q_dst_sum_functional_firsttotalnegative_body_steps_summand * S ((S (fs_i_dst_sum_functional_firsttotalnegative_body_steps)) * dst_negative_scale_sum_functional_firsttotal) + (fs_a_dst_sum_functional_firsttotalnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firsttotalnegative_body_steps_partial. fs_h_dst_sum_functional_firsttotalnegative_body_steps_partial + S (fs_r_dst_sum_functional_firsttotalnegative_body_steps) = S ((S (fs_i_dst_sum_functional_firsttotalnegative_body_steps)) * fs_v_dst_sum_functional_firsttotalnegative)) /\ exists fs_q_dst_sum_functional_firsttotalnegative_body_steps_partial. fs_u_dst_sum_functional_firsttotalnegative = fs_q_dst_sum_functional_firsttotalnegative_body_steps_partial * S ((S (fs_i_dst_sum_functional_firsttotalnegative_body_steps)) * fs_v_dst_sum_functional_firsttotalnegative) + (fs_r_dst_sum_functional_firsttotalnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_firsttotalnegative_body_steps_successor. fs_h_dst_sum_functional_firsttotalnegative_body_steps_successor + S (fs_s_dst_sum_functional_firsttotalnegative_body_steps) = S ((S (S fs_i_dst_sum_functional_firsttotalnegative_body_steps)) * fs_v_dst_sum_functional_firsttotalnegative)) /\ exists fs_q_dst_sum_functional_firsttotalnegative_body_steps_successor. fs_u_dst_sum_functional_firsttotalnegative = fs_q_dst_sum_functional_firsttotalnegative_body_steps_successor * S ((S (S fs_i_dst_sum_functional_firsttotalnegative_body_steps)) * fs_v_dst_sum_functional_firsttotalnegative) + (fs_s_dst_sum_functional_firsttotalnegative_body_steps))) /\ fs_s_dst_sum_functional_firsttotalnegative_body_steps = fs_r_dst_sum_functional_firsttotalnegative_body_steps + fs_a_dst_sum_functional_firsttotalnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_functional_firsttotalresult ge_balance_negative_sum_functional_firsttotalresult. (((((a) = 2 * (ge_balance_positive_sum_functional_firsttotalresult) /\ (ge_balance_negative_sum_functional_firsttotalresult) = 0) \/ exists ge_signed_half_sum_functional_firsttotalresultdecode. (((a) = 2 * ge_signed_half_sum_functional_firsttotalresultdecode + 1 /\ (ge_balance_positive_sum_functional_firsttotalresult) = 0) /\ (ge_balance_negative_sum_functional_firsttotalresult) = S ge_signed_half_sum_functional_firsttotalresultdecode))) /\ ((dst_positive_sum_sum_functional_firsttotal) + ge_balance_negative_sum_functional_firsttotalresult = (dst_negative_sum_sum_functional_firsttotal) + ge_balance_positive_sum_functional_firsttotalresult))))))))))) -> (exists srt_rows_sum_functional_second. ((((exists dst_positive_code_sum_functional_secondrowssource_table dst_positive_scale_sum_functional_secondrowssource_table dst_negative_code_sum_functional_secondrowssource_table dst_negative_scale_sum_functional_secondrowssource_table. (((F) = (((((dst_positive_code_sum_functional_secondrowssource_table) + (dst_positive_scale_sum_functional_secondrowssource_table)) * S ((dst_positive_code_sum_functional_secondrowssource_table) + (dst_positive_scale_sum_functional_secondrowssource_table)) + ((dst_positive_scale_sum_functional_secondrowssource_table) + (dst_positive_scale_sum_functional_secondrowssource_table))) + (((dst_negative_code_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)) * S ((dst_negative_code_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)) + ((dst_negative_scale_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)))) * S ((((dst_positive_code_sum_functional_secondrowssource_table) + (dst_positive_scale_sum_functional_secondrowssource_table)) * S ((dst_positive_code_sum_functional_secondrowssource_table) + (dst_positive_scale_sum_functional_secondrowssource_table)) + ((dst_positive_scale_sum_functional_secondrowssource_table) + (dst_positive_scale_sum_functional_secondrowssource_table))) + (((dst_negative_code_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)) * S ((dst_negative_code_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)) + ((dst_negative_scale_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)))) + ((((dst_negative_code_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)) * S ((dst_negative_code_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)) + ((dst_negative_scale_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table))) + (((dst_negative_code_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)) * S ((dst_negative_code_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)) + ((dst_negative_scale_sum_functional_secondrowssource_table) + (dst_negative_scale_sum_functional_secondrowssource_table)))))) /\ (forall dst_index_sum_functional_secondrowssource_table. (exists pvs_le_gap_sum_functional_secondrowssource_tabledomain. pvs_le_gap_sum_functional_secondrowssource_tabledomain + (dst_index_sum_functional_secondrowssource_table) = (0)) -> exists dst_positive_sum_functional_secondrowssource_table dst_negative_sum_functional_secondrowssource_table dst_value_sum_functional_secondrowssource_table. ((((exists ff_h_pvs_sum_functional_secondrowssource_tableentrypositive. ff_h_pvs_sum_functional_secondrowssource_tableentrypositive + S (dst_positive_sum_functional_secondrowssource_table) = S ((S (dst_index_sum_functional_secondrowssource_table)) * dst_positive_scale_sum_functional_secondrowssource_table)) /\ exists ff_q_pvs_sum_functional_secondrowssource_tableentrypositive. dst_positive_code_sum_functional_secondrowssource_table = ff_q_pvs_sum_functional_secondrowssource_tableentrypositive * S ((S (dst_index_sum_functional_secondrowssource_table)) * dst_positive_scale_sum_functional_secondrowssource_table) + (dst_positive_sum_functional_secondrowssource_table))) /\ (((((exists ff_h_pvs_sum_functional_secondrowssource_tableentrynegative. ff_h_pvs_sum_functional_secondrowssource_tableentrynegative + S (dst_negative_sum_functional_secondrowssource_table) = S ((S (dst_index_sum_functional_secondrowssource_table)) * dst_negative_scale_sum_functional_secondrowssource_table)) /\ exists ff_q_pvs_sum_functional_secondrowssource_tableentrynegative. dst_negative_code_sum_functional_secondrowssource_table = ff_q_pvs_sum_functional_secondrowssource_tableentrynegative * S ((S (dst_index_sum_functional_secondrowssource_table)) * dst_negative_scale_sum_functional_secondrowssource_table) + (dst_negative_sum_functional_secondrowssource_table))) /\ (exists ge_balance_positive_sum_functional_secondrowssource_tableentryvalue ge_balance_negative_sum_functional_secondrowssource_tableentryvalue. (((((dst_value_sum_functional_secondrowssource_table) = 2 * (ge_balance_positive_sum_functional_secondrowssource_tableentryvalue) /\ (ge_balance_negative_sum_functional_secondrowssource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_secondrowssource_tableentryvaluedecode. (((dst_value_sum_functional_secondrowssource_table) = 2 * ge_signed_half_sum_functional_secondrowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondrowssource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_secondrowssource_tableentryvalue) = S ge_signed_half_sum_functional_secondrowssource_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_secondrowssource_table) + ge_balance_negative_sum_functional_secondrowssource_tableentryvalue = (dst_negative_sum_functional_secondrowssource_table) + ge_balance_positive_sum_functional_secondrowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_functional_secondrowsrow_table dst_positive_scale_sum_functional_secondrowsrow_table dst_negative_code_sum_functional_secondrowsrow_table dst_negative_scale_sum_functional_secondrowsrow_table. (((srt_rows_sum_functional_second) = (((((dst_positive_code_sum_functional_secondrowsrow_table) + (dst_positive_scale_sum_functional_secondrowsrow_table)) * S ((dst_positive_code_sum_functional_secondrowsrow_table) + (dst_positive_scale_sum_functional_secondrowsrow_table)) + ((dst_positive_scale_sum_functional_secondrowsrow_table) + (dst_positive_scale_sum_functional_secondrowsrow_table))) + (((dst_negative_code_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)) * S ((dst_negative_code_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)) + ((dst_negative_scale_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)))) * S ((((dst_positive_code_sum_functional_secondrowsrow_table) + (dst_positive_scale_sum_functional_secondrowsrow_table)) * S ((dst_positive_code_sum_functional_secondrowsrow_table) + (dst_positive_scale_sum_functional_secondrowsrow_table)) + ((dst_positive_scale_sum_functional_secondrowsrow_table) + (dst_positive_scale_sum_functional_secondrowsrow_table))) + (((dst_negative_code_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)) * S ((dst_negative_code_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)) + ((dst_negative_scale_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)))) + ((((dst_negative_code_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)) * S ((dst_negative_code_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)) + ((dst_negative_scale_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table))) + (((dst_negative_code_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)) * S ((dst_negative_code_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)) + ((dst_negative_scale_sum_functional_secondrowsrow_table) + (dst_negative_scale_sum_functional_secondrowsrow_table)))))) /\ (forall dst_index_sum_functional_secondrowsrow_table. (exists pvs_le_gap_sum_functional_secondrowsrow_tabledomain. pvs_le_gap_sum_functional_secondrowsrow_tabledomain + (dst_index_sum_functional_secondrowsrow_table) = (m)) -> exists dst_positive_sum_functional_secondrowsrow_table dst_negative_sum_functional_secondrowsrow_table dst_value_sum_functional_secondrowsrow_table. ((((exists ff_h_pvs_sum_functional_secondrowsrow_tableentrypositive. ff_h_pvs_sum_functional_secondrowsrow_tableentrypositive + S (dst_positive_sum_functional_secondrowsrow_table) = S ((S (dst_index_sum_functional_secondrowsrow_table)) * dst_positive_scale_sum_functional_secondrowsrow_table)) /\ exists ff_q_pvs_sum_functional_secondrowsrow_tableentrypositive. dst_positive_code_sum_functional_secondrowsrow_table = ff_q_pvs_sum_functional_secondrowsrow_tableentrypositive * S ((S (dst_index_sum_functional_secondrowsrow_table)) * dst_positive_scale_sum_functional_secondrowsrow_table) + (dst_positive_sum_functional_secondrowsrow_table))) /\ (((((exists ff_h_pvs_sum_functional_secondrowsrow_tableentrynegative. ff_h_pvs_sum_functional_secondrowsrow_tableentrynegative + S (dst_negative_sum_functional_secondrowsrow_table) = S ((S (dst_index_sum_functional_secondrowsrow_table)) * dst_negative_scale_sum_functional_secondrowsrow_table)) /\ exists ff_q_pvs_sum_functional_secondrowsrow_tableentrynegative. dst_negative_code_sum_functional_secondrowsrow_table = ff_q_pvs_sum_functional_secondrowsrow_tableentrynegative * S ((S (dst_index_sum_functional_secondrowsrow_table)) * dst_negative_scale_sum_functional_secondrowsrow_table) + (dst_negative_sum_functional_secondrowsrow_table))) /\ (exists ge_balance_positive_sum_functional_secondrowsrow_tableentryvalue ge_balance_negative_sum_functional_secondrowsrow_tableentryvalue. (((((dst_value_sum_functional_secondrowsrow_table) = 2 * (ge_balance_positive_sum_functional_secondrowsrow_tableentryvalue) /\ (ge_balance_negative_sum_functional_secondrowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_secondrowsrow_tableentryvaluedecode. (((dst_value_sum_functional_secondrowsrow_table) = 2 * ge_signed_half_sum_functional_secondrowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondrowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_secondrowsrow_tableentryvalue) = S ge_signed_half_sum_functional_secondrowsrow_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_secondrowsrow_table) + ge_balance_negative_sum_functional_secondrowsrow_tableentryvalue = (dst_negative_sum_functional_secondrowsrow_table) + ge_balance_positive_sum_functional_secondrowsrow_tableentryvalue))))))))) /\ (forall srt_index_sum_functional_secondrows. (exists pvs_gap_sum_functional_secondrowsbound. pvs_gap_sum_functional_secondrowsbound + S (srt_index_sum_functional_secondrows) = (m)) -> exists srt_value_sum_functional_secondrows. (((exists dst_positive_code_sum_functional_secondrowsrowentry dst_positive_scale_sum_functional_secondrowsrowentry dst_negative_code_sum_functional_secondrowsrowentry dst_negative_scale_sum_functional_secondrowsrowentry dst_positive_sum_functional_secondrowsrowentry dst_negative_sum_functional_secondrowsrowentry. (((srt_rows_sum_functional_second) = (((((dst_positive_code_sum_functional_secondrowsrowentry) + (dst_positive_scale_sum_functional_secondrowsrowentry)) * S ((dst_positive_code_sum_functional_secondrowsrowentry) + (dst_positive_scale_sum_functional_secondrowsrowentry)) + ((dst_positive_scale_sum_functional_secondrowsrowentry) + (dst_positive_scale_sum_functional_secondrowsrowentry))) + (((dst_negative_code_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)) * S ((dst_negative_code_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)) + ((dst_negative_scale_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)))) * S ((((dst_positive_code_sum_functional_secondrowsrowentry) + (dst_positive_scale_sum_functional_secondrowsrowentry)) * S ((dst_positive_code_sum_functional_secondrowsrowentry) + (dst_positive_scale_sum_functional_secondrowsrowentry)) + ((dst_positive_scale_sum_functional_secondrowsrowentry) + (dst_positive_scale_sum_functional_secondrowsrowentry))) + (((dst_negative_code_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)) * S ((dst_negative_code_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)) + ((dst_negative_scale_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)))) + ((((dst_negative_code_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)) * S ((dst_negative_code_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)) + ((dst_negative_scale_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry))) + (((dst_negative_code_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)) * S ((dst_negative_code_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)) + ((dst_negative_scale_sum_functional_secondrowsrowentry) + (dst_negative_scale_sum_functional_secondrowsrowentry)))))) /\ (((((exists ff_h_pvs_sum_functional_secondrowsrowentrypositive. ff_h_pvs_sum_functional_secondrowsrowentrypositive + S (dst_positive_sum_functional_secondrowsrowentry) = S ((S (srt_index_sum_functional_secondrows)) * dst_positive_scale_sum_functional_secondrowsrowentry)) /\ exists ff_q_pvs_sum_functional_secondrowsrowentrypositive. dst_positive_code_sum_functional_secondrowsrowentry = ff_q_pvs_sum_functional_secondrowsrowentrypositive * S ((S (srt_index_sum_functional_secondrows)) * dst_positive_scale_sum_functional_secondrowsrowentry) + (dst_positive_sum_functional_secondrowsrowentry))) /\ (((((exists ff_h_pvs_sum_functional_secondrowsrowentrynegative. ff_h_pvs_sum_functional_secondrowsrowentrynegative + S (dst_negative_sum_functional_secondrowsrowentry) = S ((S (srt_index_sum_functional_secondrows)) * dst_negative_scale_sum_functional_secondrowsrowentry)) /\ exists ff_q_pvs_sum_functional_secondrowsrowentrynegative. dst_negative_code_sum_functional_secondrowsrowentry = ff_q_pvs_sum_functional_secondrowsrowentrynegative * S ((S (srt_index_sum_functional_secondrows)) * dst_negative_scale_sum_functional_secondrowsrowentry) + (dst_negative_sum_functional_secondrowsrowentry))) /\ (exists ge_balance_positive_sum_functional_secondrowsrowentryvalue ge_balance_negative_sum_functional_secondrowsrowentryvalue. (((((srt_value_sum_functional_secondrows) = 2 * (ge_balance_positive_sum_functional_secondrowsrowentryvalue) /\ (ge_balance_negative_sum_functional_secondrowsrowentryvalue) = 0) \/ exists ge_signed_half_sum_functional_secondrowsrowentryvaluedecode. (((srt_value_sum_functional_secondrows) = 2 * ge_signed_half_sum_functional_secondrowsrowentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondrowsrowentryvalue) = 0) /\ (ge_balance_negative_sum_functional_secondrowsrowentryvalue) = S ge_signed_half_sum_functional_secondrowsrowentryvaluedecode))) /\ ((dst_positive_sum_functional_secondrowsrowentry) + ge_balance_negative_sum_functional_secondrowsrowentryvalue = (dst_negative_sum_functional_secondrowsrowentry) + ge_balance_positive_sum_functional_secondrowsrowentryvalue))))))))) /\ (exists srs_slice_sum_functional_secondrowsrowrow_sum. ((((exists dst_positive_code_sum_functional_secondrowsrowrow_sumslicesource_table dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table dst_negative_code_sum_functional_secondrowsrowrow_sumslicesource_table dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_sum_functional_secondrowsrowrow_sumslicesource_table. (exists pvs_le_gap_sum_functional_secondrowsrowrow_sumslicesource_tabledomain. pvs_le_gap_sum_functional_secondrowsrowrow_sumslicesource_tabledomain + (dst_index_sum_functional_secondrowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_sum_functional_secondrowsrowrow_sumslicesource_table dst_negative_sum_functional_secondrowsrowrow_sumslicesource_table dst_value_sum_functional_secondrowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_sum_functional_secondrowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_sum_functional_secondrowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_sum_functional_secondrowsrowrow_sumslicesource_table) = S ((S (dst_index_sum_functional_secondrowsrowrow_sumslicesource_table)) * dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_sum_functional_secondrowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_sum_functional_secondrowsrowrow_sumslicesource_table = ff_q_pvs_sum_functional_secondrowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_sum_functional_secondrowsrowrow_sumslicesource_table)) * dst_positive_scale_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_positive_sum_functional_secondrowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_sum_functional_secondrowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_sum_functional_secondrowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_sum_functional_secondrowsrowrow_sumslicesource_table) = S ((S (dst_index_sum_functional_secondrowsrowrow_sumslicesource_table)) * dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_sum_functional_secondrowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_sum_functional_secondrowsrowrow_sumslicesource_table = ff_q_pvs_sum_functional_secondrowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_sum_functional_secondrowsrowrow_sumslicesource_table)) * dst_negative_scale_sum_functional_secondrowsrowrow_sumslicesource_table) + (dst_negative_sum_functional_secondrowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_sum_functional_secondrowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_sum_functional_secondrowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_sum_functional_secondrowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_sum_functional_secondrowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_sum_functional_secondrowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_secondrowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_sum_functional_secondrowsrowrow_sumslicesource_table) = 2 * ge_signed_half_sum_functional_secondrowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondrowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_secondrowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_sum_functional_secondrowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_secondrowsrowrow_sumslicesource_table) + ge_balance_negative_sum_functional_secondrowsrowrow_sumslicesource_tableentryvalue = (dst_negative_sum_functional_secondrowsrowrow_sumslicesource_table) + ge_balance_positive_sum_functional_secondrowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_functional_secondrowsrowrow_sumsliceoutput_table dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table dst_negative_code_sum_functional_secondrowsrowrow_sumsliceoutput_table dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table. (((srs_slice_sum_functional_secondrowsrowrow_sum) = (((((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_sum_functional_secondrowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_sum_functional_secondrowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_sum_functional_secondrowsrowrow_sumsliceoutput_tabledomain + (dst_index_sum_functional_secondrowsrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_sum_functional_secondrowsrowrow_sumsliceoutput_table dst_negative_sum_functional_secondrowsrowrow_sumsliceoutput_table dst_value_sum_functional_secondrowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_sum_functional_secondrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_sum_functional_secondrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_sum_functional_secondrowsrowrow_sumsliceoutput_table = ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_sum_functional_secondrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_positive_sum_functional_secondrowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_sum_functional_secondrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_sum_functional_secondrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_sum_functional_secondrowsrowrow_sumsliceoutput_table = ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_sum_functional_secondrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceoutput_table) + (dst_negative_sum_functional_secondrowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_sum_functional_secondrowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_sum_functional_secondrowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_functional_secondrowsrowrow_sumsliceoutput_table) + ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_sum_functional_secondrowsrowrow_sumsliceoutput_table) + ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_functional_secondrowsrowrow_sumslice. (exists pvs_gap_sum_functional_secondrowsrowrow_sumslicebound. pvs_gap_sum_functional_secondrowsrowrow_sumslicebound + S (srs_index_sum_functional_secondrowsrowrow_sumslice) = (n)) -> exists srs_value_sum_functional_secondrowsrowrow_sumslice. (((exists dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentrysource dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentrysource dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource dst_positive_sum_functional_secondrowsrowrow_sumsliceentrysource dst_negative_sum_functional_secondrowsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceentrysourcepositive + S (dst_positive_sum_functional_secondrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_sum_functional_secondrows)))) + ((t) * (srs_index_sum_functional_secondrowsrowrow_sumslice))))) * dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceentrysourcepositive. dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentrysource = ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((s) * (srt_index_sum_functional_secondrows)))) + ((t) * (srs_index_sum_functional_secondrowsrowrow_sumslice))))) * dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_positive_sum_functional_secondrowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceentrysourcenegative + S (dst_negative_sum_functional_secondrowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_sum_functional_secondrows)))) + ((t) * (srs_index_sum_functional_secondrowsrowrow_sumslice))))) * dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceentrysourcenegative. dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentrysource = ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((s) * (srt_index_sum_functional_secondrows)))) + ((t) * (srs_index_sum_functional_secondrowsrowrow_sumslice))))) * dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentrysource) + (dst_negative_sum_functional_secondrowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceentrysourcevalue ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceentrysourcevalue. (((((srs_value_sum_functional_secondrowsrowrow_sumslice) = 2 * (ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_functional_secondrowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_sum_functional_secondrowsrowrow_sumslice) = 2 * ge_signed_half_sum_functional_secondrowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_sum_functional_secondrowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_functional_secondrowsrowrow_sumsliceentrysource) + ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceentrysourcevalue = (dst_negative_sum_functional_secondrowsrowrow_sumsliceentrysource) + ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentryoutput dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentryoutput dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput dst_positive_sum_functional_secondrowsrowrow_sumsliceentryoutput dst_negative_sum_functional_secondrowsrowrow_sumsliceentryoutput. (((srs_slice_sum_functional_secondrowsrowrow_sum) = (((((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceentryoutputpositive + S (dst_positive_sum_functional_secondrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_sum_functional_secondrowsrowrow_sumslice)) * dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceentryoutputpositive. dst_positive_code_sum_functional_secondrowsrowrow_sumsliceentryoutput = ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_sum_functional_secondrowsrowrow_sumslice)) * dst_positive_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_positive_sum_functional_secondrowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_sum_functional_secondrowsrowrow_sumsliceentryoutputnegative + S (dst_negative_sum_functional_secondrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_sum_functional_secondrowsrowrow_sumslice)) * dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceentryoutputnegative. dst_negative_code_sum_functional_secondrowsrowrow_sumsliceentryoutput = ff_q_pvs_sum_functional_secondrowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_sum_functional_secondrowsrowrow_sumslice)) * dst_negative_scale_sum_functional_secondrowsrowrow_sumsliceentryoutput) + (dst_negative_sum_functional_secondrowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceentryoutputvalue ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceentryoutputvalue. (((((srs_value_sum_functional_secondrowsrowrow_sumslice) = 2 * (ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_functional_secondrowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_sum_functional_secondrowsrowrow_sumslice) = 2 * ge_signed_half_sum_functional_secondrowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_sum_functional_secondrowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_functional_secondrowsrowrow_sumsliceentryoutput) + ge_balance_negative_sum_functional_secondrowsrowrow_sumsliceentryoutputvalue = (dst_negative_sum_functional_secondrowsrowrow_sumsliceentryoutput) + ge_balance_positive_sum_functional_secondrowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_functional_secondrowsrowrow_sumsum dst_positive_scale_sum_functional_secondrowsrowrow_sumsum dst_negative_code_sum_functional_secondrowsrowrow_sumsum dst_negative_scale_sum_functional_secondrowsrowrow_sumsum dst_positive_sum_sum_functional_secondrowsrowrow_sumsum dst_negative_sum_sum_functional_secondrowsrowrow_sumsum. (((srs_slice_sum_functional_secondrowsrowrow_sum) = (((((dst_positive_code_sum_functional_secondrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsum)) * S ((dst_positive_code_sum_functional_secondrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsum)) + ((dst_positive_scale_sum_functional_secondrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsum))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)))) * S ((((dst_positive_code_sum_functional_secondrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsum)) * S ((dst_positive_code_sum_functional_secondrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsum)) + ((dst_positive_scale_sum_functional_secondrowsrowrow_sumsum) + (dst_positive_scale_sum_functional_secondrowsrowrow_sumsum))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)))) + ((((dst_negative_code_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum))) + (((dst_negative_code_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)) * S ((dst_negative_code_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)) + ((dst_negative_scale_sum_functional_secondrowsrowrow_sumsum) + (dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_sum_functional_secondrowsrowrow_sumsumpositive fs_v_dst_sum_functional_secondrowsrowrow_sumsumpositive. ((((exists fs_h_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_start. fs_h_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_start. fs_u_dst_sum_functional_secondrowsrowrow_sumsumpositive = fs_q_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_terminal. fs_h_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_sum_functional_secondrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_terminal. fs_u_dst_sum_functional_secondrowsrowrow_sumsumpositive = fs_q_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumpositive) + (dst_positive_sum_sum_functional_secondrowsrowrow_sumsum))) /\ forall fs_i_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps fs_r_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps fs_s_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_sum_functional_secondrowsrowrow_sumsum)) /\ exists fs_q_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_sum_functional_secondrowsrowrow_sumsum = fs_q_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_sum_functional_secondrowsrowrow_sumsum) + (fs_a_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_sum_functional_secondrowsrowrow_sumsumpositive = fs_q_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumpositive) + (fs_r_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_sum_functional_secondrowsrowrow_sumsumpositive = fs_q_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumpositive) + (fs_s_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps = fs_r_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps + fs_a_dst_sum_functional_secondrowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_functional_secondrowsrowrow_sumsumnegative fs_v_dst_sum_functional_secondrowsrowrow_sumsumnegative. ((((exists fs_h_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_start. fs_h_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_start. fs_u_dst_sum_functional_secondrowsrowrow_sumsumnegative = fs_q_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_terminal. fs_h_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_sum_functional_secondrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_terminal. fs_u_dst_sum_functional_secondrowsrowrow_sumsumnegative = fs_q_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumnegative) + (dst_negative_sum_sum_functional_secondrowsrowrow_sumsum))) /\ forall fs_i_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps fs_r_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps fs_s_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_sum_functional_secondrowsrowrow_sumsum)) /\ exists fs_q_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_sum_functional_secondrowsrowrow_sumsum = fs_q_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_sum_functional_secondrowsrowrow_sumsum) + (fs_a_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_sum_functional_secondrowsrowrow_sumsumnegative = fs_q_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumnegative) + (fs_r_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_sum_functional_secondrowsrowrow_sumsumnegative = fs_q_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_sum_functional_secondrowsrowrow_sumsumnegative) + (fs_s_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps = fs_r_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps + fs_a_dst_sum_functional_secondrowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_functional_secondrowsrowrow_sumsumresult ge_balance_negative_sum_functional_secondrowsrowrow_sumsumresult. (((((srt_value_sum_functional_secondrows) = 2 * (ge_balance_positive_sum_functional_secondrowsrowrow_sumsumresult) /\ (ge_balance_negative_sum_functional_secondrowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_sum_functional_secondrowsrowrow_sumsumresultdecode. (((srt_value_sum_functional_secondrows) = 2 * ge_signed_half_sum_functional_secondrowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_sum_functional_secondrowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_sum_functional_secondrowsrowrow_sumsumresult) = S ge_signed_half_sum_functional_secondrowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_sum_functional_secondrowsrowrow_sumsum) + ge_balance_negative_sum_functional_secondrowsrowrow_sumsumresult = (dst_negative_sum_sum_functional_secondrowsrowrow_sumsum) + ge_balance_positive_sum_functional_secondrowsrowrow_sumsumresult)))))))))))))))))) /\ (exists dst_positive_code_sum_functional_secondtotal dst_positive_scale_sum_functional_secondtotal dst_negative_code_sum_functional_secondtotal dst_negative_scale_sum_functional_secondtotal dst_positive_sum_sum_functional_secondtotal dst_negative_sum_sum_functional_secondtotal. (((srt_rows_sum_functional_second) = (((((dst_positive_code_sum_functional_secondtotal) + (dst_positive_scale_sum_functional_secondtotal)) * S ((dst_positive_code_sum_functional_secondtotal) + (dst_positive_scale_sum_functional_secondtotal)) + ((dst_positive_scale_sum_functional_secondtotal) + (dst_positive_scale_sum_functional_secondtotal))) + (((dst_negative_code_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)) * S ((dst_negative_code_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)) + ((dst_negative_scale_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)))) * S ((((dst_positive_code_sum_functional_secondtotal) + (dst_positive_scale_sum_functional_secondtotal)) * S ((dst_positive_code_sum_functional_secondtotal) + (dst_positive_scale_sum_functional_secondtotal)) + ((dst_positive_scale_sum_functional_secondtotal) + (dst_positive_scale_sum_functional_secondtotal))) + (((dst_negative_code_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)) * S ((dst_negative_code_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)) + ((dst_negative_scale_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)))) + ((((dst_negative_code_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)) * S ((dst_negative_code_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)) + ((dst_negative_scale_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal))) + (((dst_negative_code_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)) * S ((dst_negative_code_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)) + ((dst_negative_scale_sum_functional_secondtotal) + (dst_negative_scale_sum_functional_secondtotal)))))) /\ (((exists fs_u_dst_sum_functional_secondtotalpositive fs_v_dst_sum_functional_secondtotalpositive. ((((exists fs_h_dst_sum_functional_secondtotalpositive_body_start. fs_h_dst_sum_functional_secondtotalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_secondtotalpositive)) /\ exists fs_q_dst_sum_functional_secondtotalpositive_body_start. fs_u_dst_sum_functional_secondtotalpositive = fs_q_dst_sum_functional_secondtotalpositive_body_start * S ((S (0)) * fs_v_dst_sum_functional_secondtotalpositive) + (0))) /\ ((((exists fs_h_dst_sum_functional_secondtotalpositive_body_terminal. fs_h_dst_sum_functional_secondtotalpositive_body_terminal + S (dst_positive_sum_sum_functional_secondtotal) = S ((S (m)) * fs_v_dst_sum_functional_secondtotalpositive)) /\ exists fs_q_dst_sum_functional_secondtotalpositive_body_terminal. fs_u_dst_sum_functional_secondtotalpositive = fs_q_dst_sum_functional_secondtotalpositive_body_terminal * S ((S (m)) * fs_v_dst_sum_functional_secondtotalpositive) + (dst_positive_sum_sum_functional_secondtotal))) /\ forall fs_i_dst_sum_functional_secondtotalpositive_body_steps. (exists fs_lt_dst_sum_functional_secondtotalpositive_body_steps_bound. fs_lt_dst_sum_functional_secondtotalpositive_body_steps_bound + S fs_i_dst_sum_functional_secondtotalpositive_body_steps = m) -> exists fs_a_dst_sum_functional_secondtotalpositive_body_steps fs_r_dst_sum_functional_secondtotalpositive_body_steps fs_s_dst_sum_functional_secondtotalpositive_body_steps. ((((exists fs_h_dst_sum_functional_secondtotalpositive_body_steps_summand. fs_h_dst_sum_functional_secondtotalpositive_body_steps_summand + S (fs_a_dst_sum_functional_secondtotalpositive_body_steps) = S ((S (fs_i_dst_sum_functional_secondtotalpositive_body_steps)) * dst_positive_scale_sum_functional_secondtotal)) /\ exists fs_q_dst_sum_functional_secondtotalpositive_body_steps_summand. dst_positive_code_sum_functional_secondtotal = fs_q_dst_sum_functional_secondtotalpositive_body_steps_summand * S ((S (fs_i_dst_sum_functional_secondtotalpositive_body_steps)) * dst_positive_scale_sum_functional_secondtotal) + (fs_a_dst_sum_functional_secondtotalpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondtotalpositive_body_steps_partial. fs_h_dst_sum_functional_secondtotalpositive_body_steps_partial + S (fs_r_dst_sum_functional_secondtotalpositive_body_steps) = S ((S (fs_i_dst_sum_functional_secondtotalpositive_body_steps)) * fs_v_dst_sum_functional_secondtotalpositive)) /\ exists fs_q_dst_sum_functional_secondtotalpositive_body_steps_partial. fs_u_dst_sum_functional_secondtotalpositive = fs_q_dst_sum_functional_secondtotalpositive_body_steps_partial * S ((S (fs_i_dst_sum_functional_secondtotalpositive_body_steps)) * fs_v_dst_sum_functional_secondtotalpositive) + (fs_r_dst_sum_functional_secondtotalpositive_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondtotalpositive_body_steps_successor. fs_h_dst_sum_functional_secondtotalpositive_body_steps_successor + S (fs_s_dst_sum_functional_secondtotalpositive_body_steps) = S ((S (S fs_i_dst_sum_functional_secondtotalpositive_body_steps)) * fs_v_dst_sum_functional_secondtotalpositive)) /\ exists fs_q_dst_sum_functional_secondtotalpositive_body_steps_successor. fs_u_dst_sum_functional_secondtotalpositive = fs_q_dst_sum_functional_secondtotalpositive_body_steps_successor * S ((S (S fs_i_dst_sum_functional_secondtotalpositive_body_steps)) * fs_v_dst_sum_functional_secondtotalpositive) + (fs_s_dst_sum_functional_secondtotalpositive_body_steps))) /\ fs_s_dst_sum_functional_secondtotalpositive_body_steps = fs_r_dst_sum_functional_secondtotalpositive_body_steps + fs_a_dst_sum_functional_secondtotalpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_functional_secondtotalnegative fs_v_dst_sum_functional_secondtotalnegative. ((((exists fs_h_dst_sum_functional_secondtotalnegative_body_start. fs_h_dst_sum_functional_secondtotalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_functional_secondtotalnegative)) /\ exists fs_q_dst_sum_functional_secondtotalnegative_body_start. fs_u_dst_sum_functional_secondtotalnegative = fs_q_dst_sum_functional_secondtotalnegative_body_start * S ((S (0)) * fs_v_dst_sum_functional_secondtotalnegative) + (0))) /\ ((((exists fs_h_dst_sum_functional_secondtotalnegative_body_terminal. fs_h_dst_sum_functional_secondtotalnegative_body_terminal + S (dst_negative_sum_sum_functional_secondtotal) = S ((S (m)) * fs_v_dst_sum_functional_secondtotalnegative)) /\ exists fs_q_dst_sum_functional_secondtotalnegative_body_terminal. fs_u_dst_sum_functional_secondtotalnegative = fs_q_dst_sum_functional_secondtotalnegative_body_terminal * S ((S (m)) * fs_v_dst_sum_functional_secondtotalnegative) + (dst_negative_sum_sum_functional_secondtotal))) /\ forall fs_i_dst_sum_functional_secondtotalnegative_body_steps. (exists fs_lt_dst_sum_functional_secondtotalnegative_body_steps_bound. fs_lt_dst_sum_functional_secondtotalnegative_body_steps_bound + S fs_i_dst_sum_functional_secondtotalnegative_body_steps = m) -> exists fs_a_dst_sum_functional_secondtotalnegative_body_steps fs_r_dst_sum_functional_secondtotalnegative_body_steps fs_s_dst_sum_functional_secondtotalnegative_body_steps. ((((exists fs_h_dst_sum_functional_secondtotalnegative_body_steps_summand. fs_h_dst_sum_functional_secondtotalnegative_body_steps_summand + S (fs_a_dst_sum_functional_secondtotalnegative_body_steps) = S ((S (fs_i_dst_sum_functional_secondtotalnegative_body_steps)) * dst_negative_scale_sum_functional_secondtotal)) /\ exists fs_q_dst_sum_functional_secondtotalnegative_body_steps_summand. dst_negative_code_sum_functional_secondtotal = fs_q_dst_sum_functional_secondtotalnegative_body_steps_summand * S ((S (fs_i_dst_sum_functional_secondtotalnegative_body_steps)) * dst_negative_scale_sum_functional_secondtotal) + (fs_a_dst_sum_functional_secondtotalnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondtotalnegative_body_steps_partial. fs_h_dst_sum_functional_secondtotalnegative_body_steps_partial + S (fs_r_dst_sum_functional_secondtotalnegative_body_steps) = S ((S (fs_i_dst_sum_functional_secondtotalnegative_body_steps)) * fs_v_dst_sum_functional_secondtotalnegative)) /\ exists fs_q_dst_sum_functional_secondtotalnegative_body_steps_partial. fs_u_dst_sum_functional_secondtotalnegative = fs_q_dst_sum_functional_secondtotalnegative_body_steps_partial * S ((S (fs_i_dst_sum_functional_secondtotalnegative_body_steps)) * fs_v_dst_sum_functional_secondtotalnegative) + (fs_r_dst_sum_functional_secondtotalnegative_body_steps))) /\ ((((exists fs_h_dst_sum_functional_secondtotalnegative_body_steps_successor. fs_h_dst_sum_functional_secondtotalnegative_body_steps_successor + S (fs_s_dst_sum_functional_secondtotalnegative_body_steps) = S ((S (S fs_i_dst_sum_functional_secondtotalnegative_body_steps)) * fs_v_dst_sum_functional_secondtotalnegative)) /\ exists fs_q_dst_sum_functional_secondtotalnegative_body_steps_successor. fs_u_dst_sum_functional_secondtotalnegative = fs_q_dst_sum_functional_secondtotalnegative_body_steps_successor * S ((S (S fs_i_dst_sum_functional_secondtotalnegative_body_steps)) * fs_v_dst_sum_functional_secondtotalnegative) + (fs_s_dst_sum_functional_secondtotalnegative_body_steps))) /\ fs_s_dst_sum_functional_secondtotalnegative_body_steps = fs_r_dst_sum_functional_secondtotalnegative_body_steps + fs_a_dst_sum_functional_secondtotalnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_functional_secondtotalresult ge_balance_negative_sum_functional_secondtotalresult. (((((b) = 2 * (ge_balance_positive_sum_functional_secondtotalresult) /\ (ge_balance_negative_sum_functional_secondtotalresult) = 0) \/ exists ge_signed_half_sum_functional_secondtotalresultdecode. (((b) = 2 * ge_signed_half_sum_functional_secondtotalresultdecode + 1 /\ (ge_balance_positive_sum_functional_secondtotalresult) = 0) /\ (ge_balance_negative_sum_functional_secondtotalresult) = S ge_signed_half_sum_functional_secondtotalresultdecode))) /\ ((dst_positive_sum_sum_functional_secondtotal) + ge_balance_negative_sum_functional_secondtotalresult = (dst_negative_sum_sum_functional_secondtotal) + ge_balance_positive_sum_functional_secondtotalresult))))))))))) -> a=bConstructive proof overview
Generated structural guide
All actual representations of the same rectangular sum have the identical canonical signed result.
The unchanged tactic script uses 2 declared prerequisites and contains 33 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
divisor_signed_sum_extensional Alpha theorem; checked-use authorized RS0013 signed_rectangular_row_sums_extensional_uniqueDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Separate the logical casesL11–14
03Use earlier factsL15–24
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L15
specialize divisor_signed_sum_extensional (x) - L16
specialize divisor_signed_sum_extensional (x1) - L17
specialize divisor_signed_sum_extensional (m) - L18
specialize divisor_signed_sum_extensional (a) - L19
specialize divisor_signed_sum_extensional (b) - L20
apply divisor_signed_sum_extensional - L21
specialize signed_rectangular_row_sums_extensional_unique (F) - L22
specialize signed_rectangular_row_sums_extensional_unique (x) - L23
specialize signed_rectangular_row_sums_extensional_unique (x1) - L24
specialize signed_rectangular_row_sums_extensional_unique (o)
04Use earlier factsL25–33
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
specialize signed_rectangular_row_sums_extensional_unique (s) - L26
specialize signed_rectangular_row_sums_extensional_unique (t) - L27
specialize signed_rectangular_row_sums_extensional_unique (m) - L28
specialize signed_rectangular_row_sums_extensional_unique (n) - L29
apply signed_rectangular_row_sums_extensional_unique - L30
exact ha_witness_left - L31
exact hb_witness_left - L32
exact ha_witness_right - L33
exact hb_witness_right
Original exact command ledger · 33 lines
- 0001
intro F - 0002
intro o - 0003
intro s - 0004
intro t - 0005
intro m - 0006
intro n - 0007
intro a - 0008
intro b - 0009
intro ha - 0010
intro hb - 0011
cases ha - 0012
cases ha_witness - 0013
cases hb - 0014
cases hb_witness - 0015
specialize divisor_signed_sum_extensional (x) - 0016
specialize divisor_signed_sum_extensional (x1) - 0017
specialize divisor_signed_sum_extensional (m) - 0018
specialize divisor_signed_sum_extensional (a) - 0019
specialize divisor_signed_sum_extensional (b) - 0020
apply divisor_signed_sum_extensional - 0021
specialize signed_rectangular_row_sums_extensional_unique (F) - 0022
specialize signed_rectangular_row_sums_extensional_unique (x) - 0023
specialize signed_rectangular_row_sums_extensional_unique (x1) - 0024
specialize signed_rectangular_row_sums_extensional_unique (o) - 0025
specialize signed_rectangular_row_sums_extensional_unique (s) - 0026
specialize signed_rectangular_row_sums_extensional_unique (t) - 0027
specialize signed_rectangular_row_sums_extensional_unique (m) - 0028
specialize signed_rectangular_row_sums_extensional_unique (n) - 0029
apply signed_rectangular_row_sums_extensional_unique - 0030
exact ha_witness_left - 0031
exact hb_witness_left - 0032
exact ha_witness_right - 0033
exact hb_witness_right