signed_rectangular_row_sums_extend

Exact expanded first-order arithmetic statement

forall F R Q o s t m n a. (((exists dst_positive_code_extend_prefixsource_table dst_positive_scale_extend_prefixsource_table dst_negative_code_extend_prefixsource_table dst_negative_scale_extend_prefixsource_table. (((F) = (((((dst_positive_code_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table)) * S ((dst_positive_code_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table)) + ((dst_positive_scale_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table))) + (((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) * S ((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) + ((dst_negative_scale_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)))) * S ((((dst_positive_code_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table)) * S ((dst_positive_code_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table)) + ((dst_positive_scale_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table))) + (((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) * S ((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) + ((dst_negative_scale_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)))) + ((((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) * S ((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) + ((dst_negative_scale_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table))) + (((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) * S ((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) + ((dst_negative_scale_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)))))) /\ (forall dst_index_extend_prefixsource_table. (exists pvs_le_gap_extend_prefixsource_tabledomain. pvs_le_gap_extend_prefixsource_tabledomain + (dst_index_extend_prefixsource_table) = (0)) -> exists dst_positive_extend_prefixsource_table dst_negative_extend_prefixsource_table dst_value_extend_prefixsource_table. ((((exists ff_h_pvs_extend_prefixsource_tableentrypositive. ff_h_pvs_extend_prefixsource_tableentrypositive + S (dst_positive_extend_prefixsource_table) = S ((S (dst_index_extend_prefixsource_table)) * dst_positive_scale_extend_prefixsource_table)) /\ exists ff_q_pvs_extend_prefixsource_tableentrypositive. dst_positive_code_extend_prefixsource_table = ff_q_pvs_extend_prefixsource_tableentrypositive * S ((S (dst_index_extend_prefixsource_table)) * dst_positive_scale_extend_prefixsource_table) + (dst_positive_extend_prefixsource_table))) /\ (((((exists ff_h_pvs_extend_prefixsource_tableentrynegative. ff_h_pvs_extend_prefixsource_tableentrynegative + S (dst_negative_extend_prefixsource_table) = S ((S (dst_index_extend_prefixsource_table)) * dst_negative_scale_extend_prefixsource_table)) /\ exists ff_q_pvs_extend_prefixsource_tableentrynegative. dst_negative_code_extend_prefixsource_table = ff_q_pvs_extend_prefixsource_tableentrynegative * S ((S (dst_index_extend_prefixsource_table)) * dst_negative_scale_extend_prefixsource_table) + (dst_negative_extend_prefixsource_table))) /\ (exists ge_balance_positive_extend_prefixsource_tableentryvalue ge_balance_negative_extend_prefixsource_tableentryvalue. (((((dst_value_extend_prefixsource_table) = 2 * (ge_balance_positive_extend_prefixsource_tableentryvalue) /\ (ge_balance_negative_extend_prefixsource_tableentryvalue) = 0) \/ exists ge_signed_half_extend_prefixsource_tableentryvaluedecode. (((dst_value_extend_prefixsource_table) = 2 * ge_signed_half_extend_prefixsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_prefixsource_tableentryvalue) = 0) /\ (ge_balance_negative_extend_prefixsource_tableentryvalue) = S ge_signed_half_extend_prefixsource_tableentryvaluedecode))) /\ ((dst_positive_extend_prefixsource_table) + ge_balance_negative_extend_prefixsource_tableentryvalue = (dst_negative_extend_prefixsource_table) + ge_balance_positive_extend_prefixsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_extend_prefixrow_table dst_positive_scale_extend_prefixrow_table dst_negative_code_extend_prefixrow_table dst_negative_scale_extend_prefixrow_table. (((R) = (((((dst_positive_code_extend_prefixrow_table) + (dst_positive_scale_extend_prefixrow_table)) * S ((dst_positive_code_extend_prefixrow_table) + (dst_positive_scale_extend_prefixrow_table)) + ((dst_positive_scale_extend_prefixrow_table) + (dst_positive_scale_extend_prefixrow_table))) + (((dst_negative_code_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)) * S ((dst_negative_code_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)) + ((dst_negative_scale_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)))) * S ((((dst_positive_code_extend_prefixrow_table) + (dst_positive_scale_extend_prefixrow_table)) * S ((dst_positive_code_extend_prefixrow_table) + (dst_positive_scale_extend_prefixrow_table)) + ((dst_positive_scale_extend_prefixrow_table) + (dst_positive_scale_extend_prefixrow_table))) + (((dst_negative_code_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)) * S ((dst_negative_code_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)) + ((dst_negative_scale_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)))) + ((((dst_negative_code_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)) * S ((dst_negative_code_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)) + ((dst_negative_scale_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table))) + (((dst_negative_code_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)) * S ((dst_negative_code_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)) + ((dst_negative_scale_extend_prefixrow_table) + (dst_negative_scale_extend_prefixrow_table)))))) /\ (forall dst_index_extend_prefixrow_table. (exists pvs_le_gap_extend_prefixrow_tabledomain. pvs_le_gap_extend_prefixrow_tabledomain + (dst_index_extend_prefixrow_table) = (m)) -> exists dst_positive_extend_prefixrow_table dst_negative_extend_prefixrow_table dst_value_extend_prefixrow_table. ((((exists ff_h_pvs_extend_prefixrow_tableentrypositive. ff_h_pvs_extend_prefixrow_tableentrypositive + S (dst_positive_extend_prefixrow_table) = S ((S (dst_index_extend_prefixrow_table)) * dst_positive_scale_extend_prefixrow_table)) /\ exists ff_q_pvs_extend_prefixrow_tableentrypositive. dst_positive_code_extend_prefixrow_table = ff_q_pvs_extend_prefixrow_tableentrypositive * S ((S (dst_index_extend_prefixrow_table)) * dst_positive_scale_extend_prefixrow_table) + (dst_positive_extend_prefixrow_table))) /\ (((((exists ff_h_pvs_extend_prefixrow_tableentrynegative. ff_h_pvs_extend_prefixrow_tableentrynegative + S (dst_negative_extend_prefixrow_table) = S ((S (dst_index_extend_prefixrow_table)) * dst_negative_scale_extend_prefixrow_table)) /\ exists ff_q_pvs_extend_prefixrow_tableentrynegative. dst_negative_code_extend_prefixrow_table = ff_q_pvs_extend_prefixrow_tableentrynegative * S ((S (dst_index_extend_prefixrow_table)) * dst_negative_scale_extend_prefixrow_table) + (dst_negative_extend_prefixrow_table))) /\ (exists ge_balance_positive_extend_prefixrow_tableentryvalue ge_balance_negative_extend_prefixrow_tableentryvalue. (((((dst_value_extend_prefixrow_table) = 2 * (ge_balance_positive_extend_prefixrow_tableentryvalue) /\ (ge_balance_negative_extend_prefixrow_tableentryvalue) = 0) \/ exists ge_signed_half_extend_prefixrow_tableentryvaluedecode. (((dst_value_extend_prefixrow_table) = 2 * ge_signed_half_extend_prefixrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_prefixrow_tableentryvalue) = 0) /\ (ge_balance_negative_extend_prefixrow_tableentryvalue) = S ge_signed_half_extend_prefixrow_tableentryvaluedecode))) /\ ((dst_positive_extend_prefixrow_table) + ge_balance_negative_extend_prefixrow_tableentryvalue = (dst_negative_extend_prefixrow_table) + ge_balance_positive_extend_prefixrow_tableentryvalue))))))))) /\ (forall srt_index_extend_prefix. (exists pvs_gap_extend_prefixbound. pvs_gap_extend_prefixbound + S (srt_index_extend_prefix) = (m)) -> exists srt_value_extend_prefix. (((exists dst_positive_code_extend_prefixrowentry dst_positive_scale_extend_prefixrowentry dst_negative_code_extend_prefixrowentry dst_negative_scale_extend_prefixrowentry dst_positive_extend_prefixrowentry dst_negative_extend_prefixrowentry. (((R) = (((((dst_positive_code_extend_prefixrowentry) + (dst_positive_scale_extend_prefixrowentry)) * S ((dst_positive_code_extend_prefixrowentry) + (dst_positive_scale_extend_prefixrowentry)) + ((dst_positive_scale_extend_prefixrowentry) + (dst_positive_scale_extend_prefixrowentry))) + (((dst_negative_code_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)) * S ((dst_negative_code_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)) + ((dst_negative_scale_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)))) * S ((((dst_positive_code_extend_prefixrowentry) + (dst_positive_scale_extend_prefixrowentry)) * S ((dst_positive_code_extend_prefixrowentry) + (dst_positive_scale_extend_prefixrowentry)) + ((dst_positive_scale_extend_prefixrowentry) + (dst_positive_scale_extend_prefixrowentry))) + (((dst_negative_code_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)) * S ((dst_negative_code_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)) + ((dst_negative_scale_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)))) + ((((dst_negative_code_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)) * S ((dst_negative_code_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)) + ((dst_negative_scale_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry))) + (((dst_negative_code_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)) * S ((dst_negative_code_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)) + ((dst_negative_scale_extend_prefixrowentry) + (dst_negative_scale_extend_prefixrowentry)))))) /\ (((((exists ff_h_pvs_extend_prefixrowentrypositive. ff_h_pvs_extend_prefixrowentrypositive + S (dst_positive_extend_prefixrowentry) = S ((S (srt_index_extend_prefix)) * dst_positive_scale_extend_prefixrowentry)) /\ exists ff_q_pvs_extend_prefixrowentrypositive. dst_positive_code_extend_prefixrowentry = ff_q_pvs_extend_prefixrowentrypositive * S ((S (srt_index_extend_prefix)) * dst_positive_scale_extend_prefixrowentry) + (dst_positive_extend_prefixrowentry))) /\ (((((exists ff_h_pvs_extend_prefixrowentrynegative. ff_h_pvs_extend_prefixrowentrynegative + S (dst_negative_extend_prefixrowentry) = S ((S (srt_index_extend_prefix)) * dst_negative_scale_extend_prefixrowentry)) /\ exists ff_q_pvs_extend_prefixrowentrynegative. dst_negative_code_extend_prefixrowentry = ff_q_pvs_extend_prefixrowentrynegative * S ((S (srt_index_extend_prefix)) * dst_negative_scale_extend_prefixrowentry) + (dst_negative_extend_prefixrowentry))) /\ (exists ge_balance_positive_extend_prefixrowentryvalue ge_balance_negative_extend_prefixrowentryvalue. (((((srt_value_extend_prefix) = 2 * (ge_balance_positive_extend_prefixrowentryvalue) /\ (ge_balance_negative_extend_prefixrowentryvalue) = 0) \/ exists ge_signed_half_extend_prefixrowentryvaluedecode. (((srt_value_extend_prefix) = 2 * ge_signed_half_extend_prefixrowentryvaluedecode + 1 /\ (ge_balance_positive_extend_prefixrowentryvalue) = 0) /\ (ge_balance_negative_extend_prefixrowentryvalue) = S ge_signed_half_extend_prefixrowentryvaluedecode))) /\ ((dst_positive_extend_prefixrowentry) + ge_balance_negative_extend_prefixrowentryvalue = (dst_negative_extend_prefixrowentry) + ge_balance_positive_extend_prefixrowentryvalue))))))))) /\ (exists srs_slice_extend_prefixrowrow_sum. ((((exists dst_positive_code_extend_prefixrowrow_sumslicesource_table dst_positive_scale_extend_prefixrowrow_sumslicesource_table dst_negative_code_extend_prefixrowrow_sumslicesource_table dst_negative_scale_extend_prefixrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_extend_prefixrowrow_sumslicesource_table) + (dst_positive_scale_extend_prefixrowrow_sumslicesource_table)) * S ((dst_positive_code_extend_prefixrowrow_sumslicesource_table) + (dst_positive_scale_extend_prefixrowrow_sumslicesource_table)) + ((dst_positive_scale_extend_prefixrowrow_sumslicesource_table) + (dst_positive_scale_extend_prefixrowrow_sumslicesource_table))) + (((dst_negative_code_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)) * S ((dst_negative_code_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)) + ((dst_negative_scale_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)))) * S ((((dst_positive_code_extend_prefixrowrow_sumslicesource_table) + (dst_positive_scale_extend_prefixrowrow_sumslicesource_table)) * S ((dst_positive_code_extend_prefixrowrow_sumslicesource_table) + (dst_positive_scale_extend_prefixrowrow_sumslicesource_table)) + ((dst_positive_scale_extend_prefixrowrow_sumslicesource_table) + (dst_positive_scale_extend_prefixrowrow_sumslicesource_table))) + (((dst_negative_code_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)) * S ((dst_negative_code_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)) + ((dst_negative_scale_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)))) + ((((dst_negative_code_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)) * S ((dst_negative_code_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)) + ((dst_negative_scale_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table))) + (((dst_negative_code_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)) * S ((dst_negative_code_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)) + ((dst_negative_scale_extend_prefixrowrow_sumslicesource_table) + (dst_negative_scale_extend_prefixrowrow_sumslicesource_table)))))) /\ (forall dst_index_extend_prefixrowrow_sumslicesource_table. (exists pvs_le_gap_extend_prefixrowrow_sumslicesource_tabledomain. pvs_le_gap_extend_prefixrowrow_sumslicesource_tabledomain + (dst_index_extend_prefixrowrow_sumslicesource_table) = (0)) -> exists dst_positive_extend_prefixrowrow_sumslicesource_table dst_negative_extend_prefixrowrow_sumslicesource_table dst_value_extend_prefixrowrow_sumslicesource_table. ((((exists ff_h_pvs_extend_prefixrowrow_sumslicesource_tableentrypositive. ff_h_pvs_extend_prefixrowrow_sumslicesource_tableentrypositive + S (dst_positive_extend_prefixrowrow_sumslicesource_table) = S ((S (dst_index_extend_prefixrowrow_sumslicesource_table)) * dst_positive_scale_extend_prefixrowrow_sumslicesource_table)) /\ exists ff_q_pvs_extend_prefixrowrow_sumslicesource_tableentrypositive. dst_positive_code_extend_prefixrowrow_sumslicesource_table = ff_q_pvs_extend_prefixrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_extend_prefixrowrow_sumslicesource_table)) * dst_positive_scale_extend_prefixrowrow_sumslicesource_table) + (dst_positive_extend_prefixrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_extend_prefixrowrow_sumslicesource_tableentrynegative. ff_h_pvs_extend_prefixrowrow_sumslicesource_tableentrynegative + S (dst_negative_extend_prefixrowrow_sumslicesource_table) = S ((S (dst_index_extend_prefixrowrow_sumslicesource_table)) * dst_negative_scale_extend_prefixrowrow_sumslicesource_table)) /\ exists ff_q_pvs_extend_prefixrowrow_sumslicesource_tableentrynegative. dst_negative_code_extend_prefixrowrow_sumslicesource_table = ff_q_pvs_extend_prefixrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_extend_prefixrowrow_sumslicesource_table)) * dst_negative_scale_extend_prefixrowrow_sumslicesource_table) + (dst_negative_extend_prefixrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_extend_prefixrowrow_sumslicesource_tableentryvalue ge_balance_negative_extend_prefixrowrow_sumslicesource_tableentryvalue. (((((dst_value_extend_prefixrowrow_sumslicesource_table) = 2 * (ge_balance_positive_extend_prefixrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_extend_prefixrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_extend_prefixrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_extend_prefixrowrow_sumslicesource_table) = 2 * ge_signed_half_extend_prefixrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_prefixrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_extend_prefixrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_extend_prefixrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_extend_prefixrowrow_sumslicesource_table) + ge_balance_negative_extend_prefixrowrow_sumslicesource_tableentryvalue = (dst_negative_extend_prefixrowrow_sumslicesource_table) + ge_balance_positive_extend_prefixrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_extend_prefixrowrow_sumsliceoutput_table dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table dst_negative_code_extend_prefixrowrow_sumsliceoutput_table dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table. (((srs_slice_extend_prefixrowrow_sum) = (((((dst_positive_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table)) * S ((dst_positive_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table)) + ((dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table))) + (((dst_negative_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table)) * S ((dst_positive_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table)) + ((dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table))) + (((dst_negative_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table))) + (((dst_negative_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_extend_prefixrowrow_sumsliceoutput_table. (exists pvs_le_gap_extend_prefixrowrow_sumsliceoutput_tabledomain. pvs_le_gap_extend_prefixrowrow_sumsliceoutput_tabledomain + (dst_index_extend_prefixrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_extend_prefixrowrow_sumsliceoutput_table dst_negative_extend_prefixrowrow_sumsliceoutput_table dst_value_extend_prefixrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_extend_prefixrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_extend_prefixrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_extend_prefixrowrow_sumsliceoutput_table) = S ((S (dst_index_extend_prefixrowrow_sumsliceoutput_table)) * dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_extend_prefixrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_extend_prefixrowrow_sumsliceoutput_table = ff_q_pvs_extend_prefixrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_extend_prefixrowrow_sumsliceoutput_table)) * dst_positive_scale_extend_prefixrowrow_sumsliceoutput_table) + (dst_positive_extend_prefixrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_extend_prefixrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_extend_prefixrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_extend_prefixrowrow_sumsliceoutput_table) = S ((S (dst_index_extend_prefixrowrow_sumsliceoutput_table)) * dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_extend_prefixrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_extend_prefixrowrow_sumsliceoutput_table = ff_q_pvs_extend_prefixrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_extend_prefixrowrow_sumsliceoutput_table)) * dst_negative_scale_extend_prefixrowrow_sumsliceoutput_table) + (dst_negative_extend_prefixrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_extend_prefixrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_extend_prefixrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_extend_prefixrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_extend_prefixrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_extend_prefixrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_extend_prefixrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_extend_prefixrowrow_sumsliceoutput_table) = 2 * ge_signed_half_extend_prefixrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_prefixrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_extend_prefixrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_extend_prefixrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_extend_prefixrowrow_sumsliceoutput_table) + ge_balance_negative_extend_prefixrowrow_sumsliceoutput_tableentryvalue = (dst_negative_extend_prefixrowrow_sumsliceoutput_table) + ge_balance_positive_extend_prefixrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_extend_prefixrowrow_sumslice. (exists pvs_gap_extend_prefixrowrow_sumslicebound. pvs_gap_extend_prefixrowrow_sumslicebound + S (srs_index_extend_prefixrowrow_sumslice) = (n)) -> exists srs_value_extend_prefixrowrow_sumslice. (((exists dst_positive_code_extend_prefixrowrow_sumsliceentrysource dst_positive_scale_extend_prefixrowrow_sumsliceentrysource dst_negative_code_extend_prefixrowrow_sumsliceentrysource dst_negative_scale_extend_prefixrowrow_sumsliceentrysource dst_positive_extend_prefixrowrow_sumsliceentrysource dst_negative_extend_prefixrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_extend_prefixrowrow_sumsliceentrysource) + (dst_positive_scale_extend_prefixrowrow_sumsliceentrysource)) * S ((dst_positive_code_extend_prefixrowrow_sumsliceentrysource) + (dst_positive_scale_extend_prefixrowrow_sumsliceentrysource)) + ((dst_positive_scale_extend_prefixrowrow_sumsliceentrysource) + (dst_positive_scale_extend_prefixrowrow_sumsliceentrysource))) + (((dst_negative_code_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_extend_prefixrowrow_sumsliceentrysource) + (dst_positive_scale_extend_prefixrowrow_sumsliceentrysource)) * S ((dst_positive_code_extend_prefixrowrow_sumsliceentrysource) + (dst_positive_scale_extend_prefixrowrow_sumsliceentrysource)) + ((dst_positive_scale_extend_prefixrowrow_sumsliceentrysource) + (dst_positive_scale_extend_prefixrowrow_sumsliceentrysource))) + (((dst_negative_code_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)))) + ((((dst_negative_code_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource))) + (((dst_negative_code_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_extend_prefixrowrow_sumsliceentrysourcepositive. ff_h_pvs_extend_prefixrowrow_sumsliceentrysourcepositive + S (dst_positive_extend_prefixrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_extend_prefix)))) + ((t) * (srs_index_extend_prefixrowrow_sumslice))))) * dst_positive_scale_extend_prefixrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_extend_prefixrowrow_sumsliceentrysourcepositive. dst_positive_code_extend_prefixrowrow_sumsliceentrysource = ff_q_pvs_extend_prefixrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((s) * (srt_index_extend_prefix)))) + ((t) * (srs_index_extend_prefixrowrow_sumslice))))) * dst_positive_scale_extend_prefixrowrow_sumsliceentrysource) + (dst_positive_extend_prefixrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_extend_prefixrowrow_sumsliceentrysourcenegative. ff_h_pvs_extend_prefixrowrow_sumsliceentrysourcenegative + S (dst_negative_extend_prefixrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_extend_prefix)))) + ((t) * (srs_index_extend_prefixrowrow_sumslice))))) * dst_negative_scale_extend_prefixrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_extend_prefixrowrow_sumsliceentrysourcenegative. dst_negative_code_extend_prefixrowrow_sumsliceentrysource = ff_q_pvs_extend_prefixrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((s) * (srt_index_extend_prefix)))) + ((t) * (srs_index_extend_prefixrowrow_sumslice))))) * dst_negative_scale_extend_prefixrowrow_sumsliceentrysource) + (dst_negative_extend_prefixrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_extend_prefixrowrow_sumsliceentrysourcevalue ge_balance_negative_extend_prefixrowrow_sumsliceentrysourcevalue. (((((srs_value_extend_prefixrowrow_sumslice) = 2 * (ge_balance_positive_extend_prefixrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_extend_prefixrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_extend_prefixrowrow_sumsliceentrysourcevaluedecode. (((srs_value_extend_prefixrowrow_sumslice) = 2 * ge_signed_half_extend_prefixrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_extend_prefixrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_extend_prefixrowrow_sumsliceentrysourcevalue) = S ge_signed_half_extend_prefixrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_extend_prefixrowrow_sumsliceentrysource) + ge_balance_negative_extend_prefixrowrow_sumsliceentrysourcevalue = (dst_negative_extend_prefixrowrow_sumsliceentrysource) + ge_balance_positive_extend_prefixrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_extend_prefixrowrow_sumsliceentryoutput dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput dst_negative_code_extend_prefixrowrow_sumsliceentryoutput dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput dst_positive_extend_prefixrowrow_sumsliceentryoutput dst_negative_extend_prefixrowrow_sumsliceentryoutput. (((srs_slice_extend_prefixrowrow_sum) = (((((dst_positive_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput)) * S ((dst_positive_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput)) + ((dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput))) + (((dst_negative_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput)) * S ((dst_positive_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput)) + ((dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput))) + (((dst_negative_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput))) + (((dst_negative_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)) * S ((dst_negative_code_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)) + ((dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_extend_prefixrowrow_sumsliceentryoutputpositive. ff_h_pvs_extend_prefixrowrow_sumsliceentryoutputpositive + S (dst_positive_extend_prefixrowrow_sumsliceentryoutput) = S ((S (srs_index_extend_prefixrowrow_sumslice)) * dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_extend_prefixrowrow_sumsliceentryoutputpositive. dst_positive_code_extend_prefixrowrow_sumsliceentryoutput = ff_q_pvs_extend_prefixrowrow_sumsliceentryoutputpositive * S ((S (srs_index_extend_prefixrowrow_sumslice)) * dst_positive_scale_extend_prefixrowrow_sumsliceentryoutput) + (dst_positive_extend_prefixrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_extend_prefixrowrow_sumsliceentryoutputnegative. ff_h_pvs_extend_prefixrowrow_sumsliceentryoutputnegative + S (dst_negative_extend_prefixrowrow_sumsliceentryoutput) = S ((S (srs_index_extend_prefixrowrow_sumslice)) * dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_extend_prefixrowrow_sumsliceentryoutputnegative. dst_negative_code_extend_prefixrowrow_sumsliceentryoutput = ff_q_pvs_extend_prefixrowrow_sumsliceentryoutputnegative * S ((S (srs_index_extend_prefixrowrow_sumslice)) * dst_negative_scale_extend_prefixrowrow_sumsliceentryoutput) + (dst_negative_extend_prefixrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_extend_prefixrowrow_sumsliceentryoutputvalue ge_balance_negative_extend_prefixrowrow_sumsliceentryoutputvalue. (((((srs_value_extend_prefixrowrow_sumslice) = 2 * (ge_balance_positive_extend_prefixrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_extend_prefixrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_extend_prefixrowrow_sumsliceentryoutputvaluedecode. (((srs_value_extend_prefixrowrow_sumslice) = 2 * ge_signed_half_extend_prefixrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_extend_prefixrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_extend_prefixrowrow_sumsliceentryoutputvalue) = S ge_signed_half_extend_prefixrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_extend_prefixrowrow_sumsliceentryoutput) + ge_balance_negative_extend_prefixrowrow_sumsliceentryoutputvalue = (dst_negative_extend_prefixrowrow_sumsliceentryoutput) + ge_balance_positive_extend_prefixrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_extend_prefixrowrow_sumsum dst_positive_scale_extend_prefixrowrow_sumsum dst_negative_code_extend_prefixrowrow_sumsum dst_negative_scale_extend_prefixrowrow_sumsum dst_positive_sum_extend_prefixrowrow_sumsum dst_negative_sum_extend_prefixrowrow_sumsum. (((srs_slice_extend_prefixrowrow_sum) = (((((dst_positive_code_extend_prefixrowrow_sumsum) + (dst_positive_scale_extend_prefixrowrow_sumsum)) * S ((dst_positive_code_extend_prefixrowrow_sumsum) + (dst_positive_scale_extend_prefixrowrow_sumsum)) + ((dst_positive_scale_extend_prefixrowrow_sumsum) + (dst_positive_scale_extend_prefixrowrow_sumsum))) + (((dst_negative_code_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)) * S ((dst_negative_code_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)) + ((dst_negative_scale_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)))) * S ((((dst_positive_code_extend_prefixrowrow_sumsum) + (dst_positive_scale_extend_prefixrowrow_sumsum)) * S ((dst_positive_code_extend_prefixrowrow_sumsum) + (dst_positive_scale_extend_prefixrowrow_sumsum)) + ((dst_positive_scale_extend_prefixrowrow_sumsum) + (dst_positive_scale_extend_prefixrowrow_sumsum))) + (((dst_negative_code_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)) * S ((dst_negative_code_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)) + ((dst_negative_scale_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)))) + ((((dst_negative_code_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)) * S ((dst_negative_code_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)) + ((dst_negative_scale_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum))) + (((dst_negative_code_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)) * S ((dst_negative_code_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)) + ((dst_negative_scale_extend_prefixrowrow_sumsum) + (dst_negative_scale_extend_prefixrowrow_sumsum)))))) /\ (((exists fs_u_dst_extend_prefixrowrow_sumsumpositive fs_v_dst_extend_prefixrowrow_sumsumpositive. ((((exists fs_h_dst_extend_prefixrowrow_sumsumpositive_body_start. fs_h_dst_extend_prefixrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_extend_prefixrowrow_sumsumpositive)) /\ exists fs_q_dst_extend_prefixrowrow_sumsumpositive_body_start. fs_u_dst_extend_prefixrowrow_sumsumpositive = fs_q_dst_extend_prefixrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_extend_prefixrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_extend_prefixrowrow_sumsumpositive_body_terminal. fs_h_dst_extend_prefixrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_extend_prefixrowrow_sumsum) = S ((S (n)) * fs_v_dst_extend_prefixrowrow_sumsumpositive)) /\ exists fs_q_dst_extend_prefixrowrow_sumsumpositive_body_terminal. fs_u_dst_extend_prefixrowrow_sumsumpositive = fs_q_dst_extend_prefixrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_extend_prefixrowrow_sumsumpositive) + (dst_positive_sum_extend_prefixrowrow_sumsum))) /\ forall fs_i_dst_extend_prefixrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_extend_prefixrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_extend_prefixrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_extend_prefixrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_extend_prefixrowrow_sumsumpositive_body_steps fs_r_dst_extend_prefixrowrow_sumsumpositive_body_steps fs_s_dst_extend_prefixrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_extend_prefixrowrow_sumsumpositive_body_steps_summand. fs_h_dst_extend_prefixrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_extend_prefixrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_extend_prefixrowrow_sumsumpositive_body_steps)) * dst_positive_scale_extend_prefixrowrow_sumsum)) /\ exists fs_q_dst_extend_prefixrowrow_sumsumpositive_body_steps_summand. dst_positive_code_extend_prefixrowrow_sumsum = fs_q_dst_extend_prefixrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_extend_prefixrowrow_sumsumpositive_body_steps)) * dst_positive_scale_extend_prefixrowrow_sumsum) + (fs_a_dst_extend_prefixrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_extend_prefixrowrow_sumsumpositive_body_steps_partial. fs_h_dst_extend_prefixrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_extend_prefixrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_extend_prefixrowrow_sumsumpositive_body_steps)) * fs_v_dst_extend_prefixrowrow_sumsumpositive)) /\ exists fs_q_dst_extend_prefixrowrow_sumsumpositive_body_steps_partial. fs_u_dst_extend_prefixrowrow_sumsumpositive = fs_q_dst_extend_prefixrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_extend_prefixrowrow_sumsumpositive_body_steps)) * fs_v_dst_extend_prefixrowrow_sumsumpositive) + (fs_r_dst_extend_prefixrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_extend_prefixrowrow_sumsumpositive_body_steps_successor. fs_h_dst_extend_prefixrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_extend_prefixrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_extend_prefixrowrow_sumsumpositive_body_steps)) * fs_v_dst_extend_prefixrowrow_sumsumpositive)) /\ exists fs_q_dst_extend_prefixrowrow_sumsumpositive_body_steps_successor. fs_u_dst_extend_prefixrowrow_sumsumpositive = fs_q_dst_extend_prefixrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_extend_prefixrowrow_sumsumpositive_body_steps)) * fs_v_dst_extend_prefixrowrow_sumsumpositive) + (fs_s_dst_extend_prefixrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_extend_prefixrowrow_sumsumpositive_body_steps = fs_r_dst_extend_prefixrowrow_sumsumpositive_body_steps + fs_a_dst_extend_prefixrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_extend_prefixrowrow_sumsumnegative fs_v_dst_extend_prefixrowrow_sumsumnegative. ((((exists fs_h_dst_extend_prefixrowrow_sumsumnegative_body_start. fs_h_dst_extend_prefixrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_extend_prefixrowrow_sumsumnegative)) /\ exists fs_q_dst_extend_prefixrowrow_sumsumnegative_body_start. fs_u_dst_extend_prefixrowrow_sumsumnegative = fs_q_dst_extend_prefixrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_extend_prefixrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_extend_prefixrowrow_sumsumnegative_body_terminal. fs_h_dst_extend_prefixrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_extend_prefixrowrow_sumsum) = S ((S (n)) * fs_v_dst_extend_prefixrowrow_sumsumnegative)) /\ exists fs_q_dst_extend_prefixrowrow_sumsumnegative_body_terminal. fs_u_dst_extend_prefixrowrow_sumsumnegative = fs_q_dst_extend_prefixrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_extend_prefixrowrow_sumsumnegative) + (dst_negative_sum_extend_prefixrowrow_sumsum))) /\ forall fs_i_dst_extend_prefixrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_extend_prefixrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_extend_prefixrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_extend_prefixrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_extend_prefixrowrow_sumsumnegative_body_steps fs_r_dst_extend_prefixrowrow_sumsumnegative_body_steps fs_s_dst_extend_prefixrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_extend_prefixrowrow_sumsumnegative_body_steps_summand. fs_h_dst_extend_prefixrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_extend_prefixrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_extend_prefixrowrow_sumsumnegative_body_steps)) * dst_negative_scale_extend_prefixrowrow_sumsum)) /\ exists fs_q_dst_extend_prefixrowrow_sumsumnegative_body_steps_summand. dst_negative_code_extend_prefixrowrow_sumsum = fs_q_dst_extend_prefixrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_extend_prefixrowrow_sumsumnegative_body_steps)) * dst_negative_scale_extend_prefixrowrow_sumsum) + (fs_a_dst_extend_prefixrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_extend_prefixrowrow_sumsumnegative_body_steps_partial. fs_h_dst_extend_prefixrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_extend_prefixrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_extend_prefixrowrow_sumsumnegative_body_steps)) * fs_v_dst_extend_prefixrowrow_sumsumnegative)) /\ exists fs_q_dst_extend_prefixrowrow_sumsumnegative_body_steps_partial. fs_u_dst_extend_prefixrowrow_sumsumnegative = fs_q_dst_extend_prefixrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_extend_prefixrowrow_sumsumnegative_body_steps)) * fs_v_dst_extend_prefixrowrow_sumsumnegative) + (fs_r_dst_extend_prefixrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_extend_prefixrowrow_sumsumnegative_body_steps_successor. fs_h_dst_extend_prefixrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_extend_prefixrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_extend_prefixrowrow_sumsumnegative_body_steps)) * fs_v_dst_extend_prefixrowrow_sumsumnegative)) /\ exists fs_q_dst_extend_prefixrowrow_sumsumnegative_body_steps_successor. fs_u_dst_extend_prefixrowrow_sumsumnegative = fs_q_dst_extend_prefixrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_extend_prefixrowrow_sumsumnegative_body_steps)) * fs_v_dst_extend_prefixrowrow_sumsumnegative) + (fs_s_dst_extend_prefixrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_extend_prefixrowrow_sumsumnegative_body_steps = fs_r_dst_extend_prefixrowrow_sumsumnegative_body_steps + fs_a_dst_extend_prefixrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_extend_prefixrowrow_sumsumresult ge_balance_negative_extend_prefixrowrow_sumsumresult. (((((srt_value_extend_prefix) = 2 * (ge_balance_positive_extend_prefixrowrow_sumsumresult) /\ (ge_balance_negative_extend_prefixrowrow_sumsumresult) = 0) \/ exists ge_signed_half_extend_prefixrowrow_sumsumresultdecode. (((srt_value_extend_prefix) = 2 * ge_signed_half_extend_prefixrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_extend_prefixrowrow_sumsumresult) = 0) /\ (ge_balance_negative_extend_prefixrowrow_sumsumresult) = S ge_signed_half_extend_prefixrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_extend_prefixrowrow_sumsum) + ge_balance_negative_extend_prefixrowrow_sumsumresult = (dst_negative_sum_extend_prefixrowrow_sumsum) + ge_balance_positive_extend_prefixrowrow_sumsumresult)))))))))))))))))) -> (exists dst_positive_code_extend_table dst_positive_scale_extend_table dst_negative_code_extend_table dst_negative_scale_extend_table. (((Q) = (((((dst_positive_code_extend_table) + (dst_positive_scale_extend_table)) * S ((dst_positive_code_extend_table) + (dst_positive_scale_extend_table)) + ((dst_positive_scale_extend_table) + (dst_positive_scale_extend_table))) + (((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) * S ((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) + ((dst_negative_scale_extend_table) + (dst_negative_scale_extend_table)))) * S ((((dst_positive_code_extend_table) + (dst_positive_scale_extend_table)) * S ((dst_positive_code_extend_table) + (dst_positive_scale_extend_table)) + ((dst_positive_scale_extend_table) + (dst_positive_scale_extend_table))) + (((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) * S ((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) + ((dst_negative_scale_extend_table) + (dst_negative_scale_extend_table)))) + ((((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) * S ((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) + ((dst_negative_scale_extend_table) + (dst_negative_scale_extend_table))) + (((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) * S ((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) + ((dst_negative_scale_extend_table) + (dst_negative_scale_extend_table)))))) /\ (forall dst_index_extend_table. (exists pvs_le_gap_extend_tabledomain. pvs_le_gap_extend_tabledomain + (dst_index_extend_table) = (m)) -> exists dst_positive_extend_table dst_negative_extend_table dst_value_extend_table. ((((exists ff_h_pvs_extend_tableentrypositive. ff_h_pvs_extend_tableentrypositive + S (dst_positive_extend_table) = S ((S (dst_index_extend_table)) * dst_positive_scale_extend_table)) /\ exists ff_q_pvs_extend_tableentrypositive. dst_positive_code_extend_table = ff_q_pvs_extend_tableentrypositive * S ((S (dst_index_extend_table)) * dst_positive_scale_extend_table) + (dst_positive_extend_table))) /\ (((((exists ff_h_pvs_extend_tableentrynegative. ff_h_pvs_extend_tableentrynegative + S (dst_negative_extend_table) = S ((S (dst_index_extend_table)) * dst_negative_scale_extend_table)) /\ exists ff_q_pvs_extend_tableentrynegative. dst_negative_code_extend_table = ff_q_pvs_extend_tableentrynegative * S ((S (dst_index_extend_table)) * dst_negative_scale_extend_table) + (dst_negative_extend_table))) /\ (exists ge_balance_positive_extend_tableentryvalue ge_balance_negative_extend_tableentryvalue. (((((dst_value_extend_table) = 2 * (ge_balance_positive_extend_tableentryvalue) /\ (ge_balance_negative_extend_tableentryvalue) = 0) \/ exists ge_signed_half_extend_tableentryvaluedecode. (((dst_value_extend_table) = 2 * ge_signed_half_extend_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_tableentryvalue) = 0) /\ (ge_balance_negative_extend_tableentryvalue) = S ge_signed_half_extend_tableentryvaluedecode))) /\ ((dst_positive_extend_table) + ge_balance_negative_extend_tableentryvalue = (dst_negative_extend_table) + ge_balance_positive_extend_tableentryvalue))))))))) -> (forall dst_index_extend_equal dst_first_extend_equal dst_second_extend_equal. (exists pvs_gap_extend_equalbound. pvs_gap_extend_equalbound + S (dst_index_extend_equal) = (m)) -> (exists dst_positive_code_extend_equalfirst dst_positive_scale_extend_equalfirst dst_negative_code_extend_equalfirst dst_negative_scale_extend_equalfirst dst_positive_extend_equalfirst dst_negative_extend_equalfirst. (((R) = (((((dst_positive_code_extend_equalfirst) + (dst_positive_scale_extend_equalfirst)) * S ((dst_positive_code_extend_equalfirst) + (dst_positive_scale_extend_equalfirst)) + ((dst_positive_scale_extend_equalfirst) + (dst_positive_scale_extend_equalfirst))) + (((dst_negative_code_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)) * S ((dst_negative_code_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)) + ((dst_negative_scale_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)))) * S ((((dst_positive_code_extend_equalfirst) + (dst_positive_scale_extend_equalfirst)) * S ((dst_positive_code_extend_equalfirst) + (dst_positive_scale_extend_equalfirst)) + ((dst_positive_scale_extend_equalfirst) + (dst_positive_scale_extend_equalfirst))) + (((dst_negative_code_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)) * S ((dst_negative_code_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)) + ((dst_negative_scale_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)))) + ((((dst_negative_code_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)) * S ((dst_negative_code_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)) + ((dst_negative_scale_extend_equalfirst) + (dst_negative_scale_extend_equalfirst))) + (((dst_negative_code_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)) * S ((dst_negative_code_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)) + ((dst_negative_scale_extend_equalfirst) + (dst_negative_scale_extend_equalfirst)))))) /\ (((((exists ff_h_pvs_extend_equalfirstpositive. ff_h_pvs_extend_equalfirstpositive + S (dst_positive_extend_equalfirst) = S ((S (dst_index_extend_equal)) * dst_positive_scale_extend_equalfirst)) /\ exists ff_q_pvs_extend_equalfirstpositive. dst_positive_code_extend_equalfirst = ff_q_pvs_extend_equalfirstpositive * S ((S (dst_index_extend_equal)) * dst_positive_scale_extend_equalfirst) + (dst_positive_extend_equalfirst))) /\ (((((exists ff_h_pvs_extend_equalfirstnegative. ff_h_pvs_extend_equalfirstnegative + S (dst_negative_extend_equalfirst) = S ((S (dst_index_extend_equal)) * dst_negative_scale_extend_equalfirst)) /\ exists ff_q_pvs_extend_equalfirstnegative. dst_negative_code_extend_equalfirst = ff_q_pvs_extend_equalfirstnegative * S ((S (dst_index_extend_equal)) * dst_negative_scale_extend_equalfirst) + (dst_negative_extend_equalfirst))) /\ (exists ge_balance_positive_extend_equalfirstvalue ge_balance_negative_extend_equalfirstvalue. (((((dst_first_extend_equal) = 2 * (ge_balance_positive_extend_equalfirstvalue) /\ (ge_balance_negative_extend_equalfirstvalue) = 0) \/ exists ge_signed_half_extend_equalfirstvaluedecode. (((dst_first_extend_equal) = 2 * ge_signed_half_extend_equalfirstvaluedecode + 1 /\ (ge_balance_positive_extend_equalfirstvalue) = 0) /\ (ge_balance_negative_extend_equalfirstvalue) = S ge_signed_half_extend_equalfirstvaluedecode))) /\ ((dst_positive_extend_equalfirst) + ge_balance_negative_extend_equalfirstvalue = (dst_negative_extend_equalfirst) + ge_balance_positive_extend_equalfirstvalue))))))))) -> (exists dst_positive_code_extend_equalsecond dst_positive_scale_extend_equalsecond dst_negative_code_extend_equalsecond dst_negative_scale_extend_equalsecond dst_positive_extend_equalsecond dst_negative_extend_equalsecond. (((Q) = (((((dst_positive_code_extend_equalsecond) + (dst_positive_scale_extend_equalsecond)) * S ((dst_positive_code_extend_equalsecond) + (dst_positive_scale_extend_equalsecond)) + ((dst_positive_scale_extend_equalsecond) + (dst_positive_scale_extend_equalsecond))) + (((dst_negative_code_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)) * S ((dst_negative_code_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)) + ((dst_negative_scale_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)))) * S ((((dst_positive_code_extend_equalsecond) + (dst_positive_scale_extend_equalsecond)) * S ((dst_positive_code_extend_equalsecond) + (dst_positive_scale_extend_equalsecond)) + ((dst_positive_scale_extend_equalsecond) + (dst_positive_scale_extend_equalsecond))) + (((dst_negative_code_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)) * S ((dst_negative_code_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)) + ((dst_negative_scale_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)))) + ((((dst_negative_code_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)) * S ((dst_negative_code_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)) + ((dst_negative_scale_extend_equalsecond) + (dst_negative_scale_extend_equalsecond))) + (((dst_negative_code_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)) * S ((dst_negative_code_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)) + ((dst_negative_scale_extend_equalsecond) + (dst_negative_scale_extend_equalsecond)))))) /\ (((((exists ff_h_pvs_extend_equalsecondpositive. ff_h_pvs_extend_equalsecondpositive + S (dst_positive_extend_equalsecond) = S ((S (dst_index_extend_equal)) * dst_positive_scale_extend_equalsecond)) /\ exists ff_q_pvs_extend_equalsecondpositive. dst_positive_code_extend_equalsecond = ff_q_pvs_extend_equalsecondpositive * S ((S (dst_index_extend_equal)) * dst_positive_scale_extend_equalsecond) + (dst_positive_extend_equalsecond))) /\ (((((exists ff_h_pvs_extend_equalsecondnegative. ff_h_pvs_extend_equalsecondnegative + S (dst_negative_extend_equalsecond) = S ((S (dst_index_extend_equal)) * dst_negative_scale_extend_equalsecond)) /\ exists ff_q_pvs_extend_equalsecondnegative. dst_negative_code_extend_equalsecond = ff_q_pvs_extend_equalsecondnegative * S ((S (dst_index_extend_equal)) * dst_negative_scale_extend_equalsecond) + (dst_negative_extend_equalsecond))) /\ (exists ge_balance_positive_extend_equalsecondvalue ge_balance_negative_extend_equalsecondvalue. (((((dst_second_extend_equal) = 2 * (ge_balance_positive_extend_equalsecondvalue) /\ (ge_balance_negative_extend_equalsecondvalue) = 0) \/ exists ge_signed_half_extend_equalsecondvaluedecode. (((dst_second_extend_equal) = 2 * ge_signed_half_extend_equalsecondvaluedecode + 1 /\ (ge_balance_positive_extend_equalsecondvalue) = 0) /\ (ge_balance_negative_extend_equalsecondvalue) = S ge_signed_half_extend_equalsecondvaluedecode))) /\ ((dst_positive_extend_equalsecond) + ge_balance_negative_extend_equalsecondvalue = (dst_negative_extend_equalsecond) + ge_balance_positive_extend_equalsecondvalue))))))))) -> dst_first_extend_equal = dst_second_extend_equal) -> (exists dst_positive_code_extend_entry dst_positive_scale_extend_entry dst_negative_code_extend_entry dst_negative_scale_extend_entry dst_positive_extend_entry dst_negative_extend_entry. (((Q) = (((((dst_positive_code_extend_entry) + (dst_positive_scale_extend_entry)) * S ((dst_positive_code_extend_entry) + (dst_positive_scale_extend_entry)) + ((dst_positive_scale_extend_entry) + (dst_positive_scale_extend_entry))) + (((dst_negative_code_extend_entry) + (dst_negative_scale_extend_entry)) * S ((dst_negative_code_extend_entry) + (dst_negative_scale_extend_entry)) + ((dst_negative_scale_extend_entry) + (dst_negative_scale_extend_entry)))) * S ((((dst_positive_code_extend_entry) + (dst_positive_scale_extend_entry)) * S ((dst_positive_code_extend_entry) + (dst_positive_scale_extend_entry)) + ((dst_positive_scale_extend_entry) + (dst_positive_scale_extend_entry))) + (((dst_negative_code_extend_entry) + (dst_negative_scale_extend_entry)) * S ((dst_negative_code_extend_entry) + (dst_negative_scale_extend_entry)) + ((dst_negative_scale_extend_entry) + (dst_negative_scale_extend_entry)))) + ((((dst_negative_code_extend_entry) + (dst_negative_scale_extend_entry)) * S ((dst_negative_code_extend_entry) + (dst_negative_scale_extend_entry)) + ((dst_negative_scale_extend_entry) + (dst_negative_scale_extend_entry))) + (((dst_negative_code_extend_entry) + (dst_negative_scale_extend_entry)) * S ((dst_negative_code_extend_entry) + (dst_negative_scale_extend_entry)) + ((dst_negative_scale_extend_entry) + (dst_negative_scale_extend_entry)))))) /\ (((((exists ff_h_pvs_extend_entrypositive. ff_h_pvs_extend_entrypositive + S (dst_positive_extend_entry) = S ((S (m)) * dst_positive_scale_extend_entry)) /\ exists ff_q_pvs_extend_entrypositive. dst_positive_code_extend_entry = ff_q_pvs_extend_entrypositive * S ((S (m)) * dst_positive_scale_extend_entry) + (dst_positive_extend_entry))) /\ (((((exists ff_h_pvs_extend_entrynegative. ff_h_pvs_extend_entrynegative + S (dst_negative_extend_entry) = S ((S (m)) * dst_negative_scale_extend_entry)) /\ exists ff_q_pvs_extend_entrynegative. dst_negative_code_extend_entry = ff_q_pvs_extend_entrynegative * S ((S (m)) * dst_negative_scale_extend_entry) + (dst_negative_extend_entry))) /\ (exists ge_balance_positive_extend_entryvalue ge_balance_negative_extend_entryvalue. (((((a) = 2 * (ge_balance_positive_extend_entryvalue) /\ (ge_balance_negative_extend_entryvalue) = 0) \/ exists ge_signed_half_extend_entryvaluedecode. (((a) = 2 * ge_signed_half_extend_entryvaluedecode + 1 /\ (ge_balance_positive_extend_entryvalue) = 0) /\ (ge_balance_negative_extend_entryvalue) = S ge_signed_half_extend_entryvaluedecode))) /\ ((dst_positive_extend_entry) + ge_balance_negative_extend_entryvalue = (dst_negative_extend_entry) + ge_balance_positive_extend_entryvalue))))))))) -> (exists srs_slice_extend_sum. ((((exists dst_positive_code_extend_sumslicesource_table dst_positive_scale_extend_sumslicesource_table dst_negative_code_extend_sumslicesource_table dst_negative_scale_extend_sumslicesource_table. (((F) = (((((dst_positive_code_extend_sumslicesource_table) + (dst_positive_scale_extend_sumslicesource_table)) * S ((dst_positive_code_extend_sumslicesource_table) + (dst_positive_scale_extend_sumslicesource_table)) + ((dst_positive_scale_extend_sumslicesource_table) + (dst_positive_scale_extend_sumslicesource_table))) + (((dst_negative_code_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)) * S ((dst_negative_code_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)) + ((dst_negative_scale_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)))) * S ((((dst_positive_code_extend_sumslicesource_table) + (dst_positive_scale_extend_sumslicesource_table)) * S ((dst_positive_code_extend_sumslicesource_table) + (dst_positive_scale_extend_sumslicesource_table)) + ((dst_positive_scale_extend_sumslicesource_table) + (dst_positive_scale_extend_sumslicesource_table))) + (((dst_negative_code_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)) * S ((dst_negative_code_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)) + ((dst_negative_scale_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)))) + ((((dst_negative_code_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)) * S ((dst_negative_code_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)) + ((dst_negative_scale_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table))) + (((dst_negative_code_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)) * S ((dst_negative_code_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)) + ((dst_negative_scale_extend_sumslicesource_table) + (dst_negative_scale_extend_sumslicesource_table)))))) /\ (forall dst_index_extend_sumslicesource_table. (exists pvs_le_gap_extend_sumslicesource_tabledomain. pvs_le_gap_extend_sumslicesource_tabledomain + (dst_index_extend_sumslicesource_table) = (0)) -> exists dst_positive_extend_sumslicesource_table dst_negative_extend_sumslicesource_table dst_value_extend_sumslicesource_table. ((((exists ff_h_pvs_extend_sumslicesource_tableentrypositive. ff_h_pvs_extend_sumslicesource_tableentrypositive + S (dst_positive_extend_sumslicesource_table) = S ((S (dst_index_extend_sumslicesource_table)) * dst_positive_scale_extend_sumslicesource_table)) /\ exists ff_q_pvs_extend_sumslicesource_tableentrypositive. dst_positive_code_extend_sumslicesource_table = ff_q_pvs_extend_sumslicesource_tableentrypositive * S ((S (dst_index_extend_sumslicesource_table)) * dst_positive_scale_extend_sumslicesource_table) + (dst_positive_extend_sumslicesource_table))) /\ (((((exists ff_h_pvs_extend_sumslicesource_tableentrynegative. ff_h_pvs_extend_sumslicesource_tableentrynegative + S (dst_negative_extend_sumslicesource_table) = S ((S (dst_index_extend_sumslicesource_table)) * dst_negative_scale_extend_sumslicesource_table)) /\ exists ff_q_pvs_extend_sumslicesource_tableentrynegative. dst_negative_code_extend_sumslicesource_table = ff_q_pvs_extend_sumslicesource_tableentrynegative * S ((S (dst_index_extend_sumslicesource_table)) * dst_negative_scale_extend_sumslicesource_table) + (dst_negative_extend_sumslicesource_table))) /\ (exists ge_balance_positive_extend_sumslicesource_tableentryvalue ge_balance_negative_extend_sumslicesource_tableentryvalue. (((((dst_value_extend_sumslicesource_table) = 2 * (ge_balance_positive_extend_sumslicesource_tableentryvalue) /\ (ge_balance_negative_extend_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_extend_sumslicesource_tableentryvaluedecode. (((dst_value_extend_sumslicesource_table) = 2 * ge_signed_half_extend_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_extend_sumslicesource_tableentryvalue) = S ge_signed_half_extend_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_extend_sumslicesource_table) + ge_balance_negative_extend_sumslicesource_tableentryvalue = (dst_negative_extend_sumslicesource_table) + ge_balance_positive_extend_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_extend_sumsliceoutput_table dst_positive_scale_extend_sumsliceoutput_table dst_negative_code_extend_sumsliceoutput_table dst_negative_scale_extend_sumsliceoutput_table. (((srs_slice_extend_sum) = (((((dst_positive_code_extend_sumsliceoutput_table) + (dst_positive_scale_extend_sumsliceoutput_table)) * S ((dst_positive_code_extend_sumsliceoutput_table) + (dst_positive_scale_extend_sumsliceoutput_table)) + ((dst_positive_scale_extend_sumsliceoutput_table) + (dst_positive_scale_extend_sumsliceoutput_table))) + (((dst_negative_code_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)) * S ((dst_negative_code_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)) + ((dst_negative_scale_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)))) * S ((((dst_positive_code_extend_sumsliceoutput_table) + (dst_positive_scale_extend_sumsliceoutput_table)) * S ((dst_positive_code_extend_sumsliceoutput_table) + (dst_positive_scale_extend_sumsliceoutput_table)) + ((dst_positive_scale_extend_sumsliceoutput_table) + (dst_positive_scale_extend_sumsliceoutput_table))) + (((dst_negative_code_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)) * S ((dst_negative_code_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)) + ((dst_negative_scale_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)))) + ((((dst_negative_code_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)) * S ((dst_negative_code_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)) + ((dst_negative_scale_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table))) + (((dst_negative_code_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)) * S ((dst_negative_code_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)) + ((dst_negative_scale_extend_sumsliceoutput_table) + (dst_negative_scale_extend_sumsliceoutput_table)))))) /\ (forall dst_index_extend_sumsliceoutput_table. (exists pvs_le_gap_extend_sumsliceoutput_tabledomain. pvs_le_gap_extend_sumsliceoutput_tabledomain + (dst_index_extend_sumsliceoutput_table) = (n)) -> exists dst_positive_extend_sumsliceoutput_table dst_negative_extend_sumsliceoutput_table dst_value_extend_sumsliceoutput_table. ((((exists ff_h_pvs_extend_sumsliceoutput_tableentrypositive. ff_h_pvs_extend_sumsliceoutput_tableentrypositive + S (dst_positive_extend_sumsliceoutput_table) = S ((S (dst_index_extend_sumsliceoutput_table)) * dst_positive_scale_extend_sumsliceoutput_table)) /\ exists ff_q_pvs_extend_sumsliceoutput_tableentrypositive. dst_positive_code_extend_sumsliceoutput_table = ff_q_pvs_extend_sumsliceoutput_tableentrypositive * S ((S (dst_index_extend_sumsliceoutput_table)) * dst_positive_scale_extend_sumsliceoutput_table) + (dst_positive_extend_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_extend_sumsliceoutput_tableentrynegative. ff_h_pvs_extend_sumsliceoutput_tableentrynegative + S (dst_negative_extend_sumsliceoutput_table) = S ((S (dst_index_extend_sumsliceoutput_table)) * dst_negative_scale_extend_sumsliceoutput_table)) /\ exists ff_q_pvs_extend_sumsliceoutput_tableentrynegative. dst_negative_code_extend_sumsliceoutput_table = ff_q_pvs_extend_sumsliceoutput_tableentrynegative * S ((S (dst_index_extend_sumsliceoutput_table)) * dst_negative_scale_extend_sumsliceoutput_table) + (dst_negative_extend_sumsliceoutput_table))) /\ (exists ge_balance_positive_extend_sumsliceoutput_tableentryvalue ge_balance_negative_extend_sumsliceoutput_tableentryvalue. (((((dst_value_extend_sumsliceoutput_table) = 2 * (ge_balance_positive_extend_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_extend_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_extend_sumsliceoutput_tableentryvaluedecode. (((dst_value_extend_sumsliceoutput_table) = 2 * ge_signed_half_extend_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_extend_sumsliceoutput_tableentryvalue) = S ge_signed_half_extend_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_extend_sumsliceoutput_table) + ge_balance_negative_extend_sumsliceoutput_tableentryvalue = (dst_negative_extend_sumsliceoutput_table) + ge_balance_positive_extend_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_extend_sumslice. (exists pvs_gap_extend_sumslicebound. pvs_gap_extend_sumslicebound + S (srs_index_extend_sumslice) = (n)) -> exists srs_value_extend_sumslice. (((exists dst_positive_code_extend_sumsliceentrysource dst_positive_scale_extend_sumsliceentrysource dst_negative_code_extend_sumsliceentrysource dst_negative_scale_extend_sumsliceentrysource dst_positive_extend_sumsliceentrysource dst_negative_extend_sumsliceentrysource. (((F) = (((((dst_positive_code_extend_sumsliceentrysource) + (dst_positive_scale_extend_sumsliceentrysource)) * S ((dst_positive_code_extend_sumsliceentrysource) + (dst_positive_scale_extend_sumsliceentrysource)) + ((dst_positive_scale_extend_sumsliceentrysource) + (dst_positive_scale_extend_sumsliceentrysource))) + (((dst_negative_code_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)) * S ((dst_negative_code_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)) + ((dst_negative_scale_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)))) * S ((((dst_positive_code_extend_sumsliceentrysource) + (dst_positive_scale_extend_sumsliceentrysource)) * S ((dst_positive_code_extend_sumsliceentrysource) + (dst_positive_scale_extend_sumsliceentrysource)) + ((dst_positive_scale_extend_sumsliceentrysource) + (dst_positive_scale_extend_sumsliceentrysource))) + (((dst_negative_code_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)) * S ((dst_negative_code_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)) + ((dst_negative_scale_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)))) + ((((dst_negative_code_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)) * S ((dst_negative_code_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)) + ((dst_negative_scale_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource))) + (((dst_negative_code_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)) * S ((dst_negative_code_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)) + ((dst_negative_scale_extend_sumsliceentrysource) + (dst_negative_scale_extend_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_extend_sumsliceentrysourcepositive. ff_h_pvs_extend_sumsliceentrysourcepositive + S (dst_positive_extend_sumsliceentrysource) = S ((S (((((o) + ((s) * (m)))) + ((t) * (srs_index_extend_sumslice))))) * dst_positive_scale_extend_sumsliceentrysource)) /\ exists ff_q_pvs_extend_sumsliceentrysourcepositive. dst_positive_code_extend_sumsliceentrysource = ff_q_pvs_extend_sumsliceentrysourcepositive * S ((S (((((o) + ((s) * (m)))) + ((t) * (srs_index_extend_sumslice))))) * dst_positive_scale_extend_sumsliceentrysource) + (dst_positive_extend_sumsliceentrysource))) /\ (((((exists ff_h_pvs_extend_sumsliceentrysourcenegative. ff_h_pvs_extend_sumsliceentrysourcenegative + S (dst_negative_extend_sumsliceentrysource) = S ((S (((((o) + ((s) * (m)))) + ((t) * (srs_index_extend_sumslice))))) * dst_negative_scale_extend_sumsliceentrysource)) /\ exists ff_q_pvs_extend_sumsliceentrysourcenegative. dst_negative_code_extend_sumsliceentrysource = ff_q_pvs_extend_sumsliceentrysourcenegative * S ((S (((((o) + ((s) * (m)))) + ((t) * (srs_index_extend_sumslice))))) * dst_negative_scale_extend_sumsliceentrysource) + (dst_negative_extend_sumsliceentrysource))) /\ (exists ge_balance_positive_extend_sumsliceentrysourcevalue ge_balance_negative_extend_sumsliceentrysourcevalue. (((((srs_value_extend_sumslice) = 2 * (ge_balance_positive_extend_sumsliceentrysourcevalue) /\ (ge_balance_negative_extend_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_extend_sumsliceentrysourcevaluedecode. (((srs_value_extend_sumslice) = 2 * ge_signed_half_extend_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_extend_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_extend_sumsliceentrysourcevalue) = S ge_signed_half_extend_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_extend_sumsliceentrysource) + ge_balance_negative_extend_sumsliceentrysourcevalue = (dst_negative_extend_sumsliceentrysource) + ge_balance_positive_extend_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_extend_sumsliceentryoutput dst_positive_scale_extend_sumsliceentryoutput dst_negative_code_extend_sumsliceentryoutput dst_negative_scale_extend_sumsliceentryoutput dst_positive_extend_sumsliceentryoutput dst_negative_extend_sumsliceentryoutput. (((srs_slice_extend_sum) = (((((dst_positive_code_extend_sumsliceentryoutput) + (dst_positive_scale_extend_sumsliceentryoutput)) * S ((dst_positive_code_extend_sumsliceentryoutput) + (dst_positive_scale_extend_sumsliceentryoutput)) + ((dst_positive_scale_extend_sumsliceentryoutput) + (dst_positive_scale_extend_sumsliceentryoutput))) + (((dst_negative_code_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)) * S ((dst_negative_code_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)) + ((dst_negative_scale_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)))) * S ((((dst_positive_code_extend_sumsliceentryoutput) + (dst_positive_scale_extend_sumsliceentryoutput)) * S ((dst_positive_code_extend_sumsliceentryoutput) + (dst_positive_scale_extend_sumsliceentryoutput)) + ((dst_positive_scale_extend_sumsliceentryoutput) + (dst_positive_scale_extend_sumsliceentryoutput))) + (((dst_negative_code_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)) * S ((dst_negative_code_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)) + ((dst_negative_scale_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)))) + ((((dst_negative_code_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)) * S ((dst_negative_code_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)) + ((dst_negative_scale_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput))) + (((dst_negative_code_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)) * S ((dst_negative_code_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)) + ((dst_negative_scale_extend_sumsliceentryoutput) + (dst_negative_scale_extend_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_extend_sumsliceentryoutputpositive. ff_h_pvs_extend_sumsliceentryoutputpositive + S (dst_positive_extend_sumsliceentryoutput) = S ((S (srs_index_extend_sumslice)) * dst_positive_scale_extend_sumsliceentryoutput)) /\ exists ff_q_pvs_extend_sumsliceentryoutputpositive. dst_positive_code_extend_sumsliceentryoutput = ff_q_pvs_extend_sumsliceentryoutputpositive * S ((S (srs_index_extend_sumslice)) * dst_positive_scale_extend_sumsliceentryoutput) + (dst_positive_extend_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_extend_sumsliceentryoutputnegative. ff_h_pvs_extend_sumsliceentryoutputnegative + S (dst_negative_extend_sumsliceentryoutput) = S ((S (srs_index_extend_sumslice)) * dst_negative_scale_extend_sumsliceentryoutput)) /\ exists ff_q_pvs_extend_sumsliceentryoutputnegative. dst_negative_code_extend_sumsliceentryoutput = ff_q_pvs_extend_sumsliceentryoutputnegative * S ((S (srs_index_extend_sumslice)) * dst_negative_scale_extend_sumsliceentryoutput) + (dst_negative_extend_sumsliceentryoutput))) /\ (exists ge_balance_positive_extend_sumsliceentryoutputvalue ge_balance_negative_extend_sumsliceentryoutputvalue. (((((srs_value_extend_sumslice) = 2 * (ge_balance_positive_extend_sumsliceentryoutputvalue) /\ (ge_balance_negative_extend_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_extend_sumsliceentryoutputvaluedecode. (((srs_value_extend_sumslice) = 2 * ge_signed_half_extend_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_extend_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_extend_sumsliceentryoutputvalue) = S ge_signed_half_extend_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_extend_sumsliceentryoutput) + ge_balance_negative_extend_sumsliceentryoutputvalue = (dst_negative_extend_sumsliceentryoutput) + ge_balance_positive_extend_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_extend_sumsum dst_positive_scale_extend_sumsum dst_negative_code_extend_sumsum dst_negative_scale_extend_sumsum dst_positive_sum_extend_sumsum dst_negative_sum_extend_sumsum. (((srs_slice_extend_sum) = (((((dst_positive_code_extend_sumsum) + (dst_positive_scale_extend_sumsum)) * S ((dst_positive_code_extend_sumsum) + (dst_positive_scale_extend_sumsum)) + ((dst_positive_scale_extend_sumsum) + (dst_positive_scale_extend_sumsum))) + (((dst_negative_code_extend_sumsum) + (dst_negative_scale_extend_sumsum)) * S ((dst_negative_code_extend_sumsum) + (dst_negative_scale_extend_sumsum)) + ((dst_negative_scale_extend_sumsum) + (dst_negative_scale_extend_sumsum)))) * S ((((dst_positive_code_extend_sumsum) + (dst_positive_scale_extend_sumsum)) * S ((dst_positive_code_extend_sumsum) + (dst_positive_scale_extend_sumsum)) + ((dst_positive_scale_extend_sumsum) + (dst_positive_scale_extend_sumsum))) + (((dst_negative_code_extend_sumsum) + (dst_negative_scale_extend_sumsum)) * S ((dst_negative_code_extend_sumsum) + (dst_negative_scale_extend_sumsum)) + ((dst_negative_scale_extend_sumsum) + (dst_negative_scale_extend_sumsum)))) + ((((dst_negative_code_extend_sumsum) + (dst_negative_scale_extend_sumsum)) * S ((dst_negative_code_extend_sumsum) + (dst_negative_scale_extend_sumsum)) + ((dst_negative_scale_extend_sumsum) + (dst_negative_scale_extend_sumsum))) + (((dst_negative_code_extend_sumsum) + (dst_negative_scale_extend_sumsum)) * S ((dst_negative_code_extend_sumsum) + (dst_negative_scale_extend_sumsum)) + ((dst_negative_scale_extend_sumsum) + (dst_negative_scale_extend_sumsum)))))) /\ (((exists fs_u_dst_extend_sumsumpositive fs_v_dst_extend_sumsumpositive. ((((exists fs_h_dst_extend_sumsumpositive_body_start. fs_h_dst_extend_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_extend_sumsumpositive)) /\ exists fs_q_dst_extend_sumsumpositive_body_start. fs_u_dst_extend_sumsumpositive = fs_q_dst_extend_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_extend_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_extend_sumsumpositive_body_terminal. fs_h_dst_extend_sumsumpositive_body_terminal + S (dst_positive_sum_extend_sumsum) = S ((S (n)) * fs_v_dst_extend_sumsumpositive)) /\ exists fs_q_dst_extend_sumsumpositive_body_terminal. fs_u_dst_extend_sumsumpositive = fs_q_dst_extend_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_extend_sumsumpositive) + (dst_positive_sum_extend_sumsum))) /\ forall fs_i_dst_extend_sumsumpositive_body_steps. (exists fs_lt_dst_extend_sumsumpositive_body_steps_bound. fs_lt_dst_extend_sumsumpositive_body_steps_bound + S fs_i_dst_extend_sumsumpositive_body_steps = n) -> exists fs_a_dst_extend_sumsumpositive_body_steps fs_r_dst_extend_sumsumpositive_body_steps fs_s_dst_extend_sumsumpositive_body_steps. ((((exists fs_h_dst_extend_sumsumpositive_body_steps_summand. fs_h_dst_extend_sumsumpositive_body_steps_summand + S (fs_a_dst_extend_sumsumpositive_body_steps) = S ((S (fs_i_dst_extend_sumsumpositive_body_steps)) * dst_positive_scale_extend_sumsum)) /\ exists fs_q_dst_extend_sumsumpositive_body_steps_summand. dst_positive_code_extend_sumsum = fs_q_dst_extend_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_extend_sumsumpositive_body_steps)) * dst_positive_scale_extend_sumsum) + (fs_a_dst_extend_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_extend_sumsumpositive_body_steps_partial. fs_h_dst_extend_sumsumpositive_body_steps_partial + S (fs_r_dst_extend_sumsumpositive_body_steps) = S ((S (fs_i_dst_extend_sumsumpositive_body_steps)) * fs_v_dst_extend_sumsumpositive)) /\ exists fs_q_dst_extend_sumsumpositive_body_steps_partial. fs_u_dst_extend_sumsumpositive = fs_q_dst_extend_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_extend_sumsumpositive_body_steps)) * fs_v_dst_extend_sumsumpositive) + (fs_r_dst_extend_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_extend_sumsumpositive_body_steps_successor. fs_h_dst_extend_sumsumpositive_body_steps_successor + S (fs_s_dst_extend_sumsumpositive_body_steps) = S ((S (S fs_i_dst_extend_sumsumpositive_body_steps)) * fs_v_dst_extend_sumsumpositive)) /\ exists fs_q_dst_extend_sumsumpositive_body_steps_successor. fs_u_dst_extend_sumsumpositive = fs_q_dst_extend_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_extend_sumsumpositive_body_steps)) * fs_v_dst_extend_sumsumpositive) + (fs_s_dst_extend_sumsumpositive_body_steps))) /\ fs_s_dst_extend_sumsumpositive_body_steps = fs_r_dst_extend_sumsumpositive_body_steps + fs_a_dst_extend_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_extend_sumsumnegative fs_v_dst_extend_sumsumnegative. ((((exists fs_h_dst_extend_sumsumnegative_body_start. fs_h_dst_extend_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_extend_sumsumnegative)) /\ exists fs_q_dst_extend_sumsumnegative_body_start. fs_u_dst_extend_sumsumnegative = fs_q_dst_extend_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_extend_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_extend_sumsumnegative_body_terminal. fs_h_dst_extend_sumsumnegative_body_terminal + S (dst_negative_sum_extend_sumsum) = S ((S (n)) * fs_v_dst_extend_sumsumnegative)) /\ exists fs_q_dst_extend_sumsumnegative_body_terminal. fs_u_dst_extend_sumsumnegative = fs_q_dst_extend_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_extend_sumsumnegative) + (dst_negative_sum_extend_sumsum))) /\ forall fs_i_dst_extend_sumsumnegative_body_steps. (exists fs_lt_dst_extend_sumsumnegative_body_steps_bound. fs_lt_dst_extend_sumsumnegative_body_steps_bound + S fs_i_dst_extend_sumsumnegative_body_steps = n) -> exists fs_a_dst_extend_sumsumnegative_body_steps fs_r_dst_extend_sumsumnegative_body_steps fs_s_dst_extend_sumsumnegative_body_steps. ((((exists fs_h_dst_extend_sumsumnegative_body_steps_summand. fs_h_dst_extend_sumsumnegative_body_steps_summand + S (fs_a_dst_extend_sumsumnegative_body_steps) = S ((S (fs_i_dst_extend_sumsumnegative_body_steps)) * dst_negative_scale_extend_sumsum)) /\ exists fs_q_dst_extend_sumsumnegative_body_steps_summand. dst_negative_code_extend_sumsum = fs_q_dst_extend_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_extend_sumsumnegative_body_steps)) * dst_negative_scale_extend_sumsum) + (fs_a_dst_extend_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_extend_sumsumnegative_body_steps_partial. fs_h_dst_extend_sumsumnegative_body_steps_partial + S (fs_r_dst_extend_sumsumnegative_body_steps) = S ((S (fs_i_dst_extend_sumsumnegative_body_steps)) * fs_v_dst_extend_sumsumnegative)) /\ exists fs_q_dst_extend_sumsumnegative_body_steps_partial. fs_u_dst_extend_sumsumnegative = fs_q_dst_extend_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_extend_sumsumnegative_body_steps)) * fs_v_dst_extend_sumsumnegative) + (fs_r_dst_extend_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_extend_sumsumnegative_body_steps_successor. fs_h_dst_extend_sumsumnegative_body_steps_successor + S (fs_s_dst_extend_sumsumnegative_body_steps) = S ((S (S fs_i_dst_extend_sumsumnegative_body_steps)) * fs_v_dst_extend_sumsumnegative)) /\ exists fs_q_dst_extend_sumsumnegative_body_steps_successor. fs_u_dst_extend_sumsumnegative = fs_q_dst_extend_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_extend_sumsumnegative_body_steps)) * fs_v_dst_extend_sumsumnegative) + (fs_s_dst_extend_sumsumnegative_body_steps))) /\ fs_s_dst_extend_sumsumnegative_body_steps = fs_r_dst_extend_sumsumnegative_body_steps + fs_a_dst_extend_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_extend_sumsumresult ge_balance_negative_extend_sumsumresult. (((((a) = 2 * (ge_balance_positive_extend_sumsumresult) /\ (ge_balance_negative_extend_sumsumresult) = 0) \/ exists ge_signed_half_extend_sumsumresultdecode. (((a) = 2 * ge_signed_half_extend_sumsumresultdecode + 1 /\ (ge_balance_positive_extend_sumsumresult) = 0) /\ (ge_balance_negative_extend_sumsumresult) = S ge_signed_half_extend_sumsumresultdecode))) /\ ((dst_positive_sum_extend_sumsum) + ge_balance_negative_extend_sumsumresult = (dst_negative_sum_extend_sumsum) + ge_balance_positive_extend_sumsumresult))))))))))) -> (((exists dst_positive_code_extend_resultsource_table dst_positive_scale_extend_resultsource_table dst_negative_code_extend_resultsource_table dst_negative_scale_extend_resultsource_table. (((F) = (((((dst_positive_code_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table)) * S ((dst_positive_code_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table)) + ((dst_positive_scale_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table))) + (((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) * S ((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) + ((dst_negative_scale_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)))) * S ((((dst_positive_code_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table)) * S ((dst_positive_code_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table)) + ((dst_positive_scale_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table))) + (((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) * S ((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) + ((dst_negative_scale_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)))) + ((((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) * S ((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) + ((dst_negative_scale_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table))) + (((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) * S ((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) + ((dst_negative_scale_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)))))) /\ (forall dst_index_extend_resultsource_table. (exists pvs_le_gap_extend_resultsource_tabledomain. pvs_le_gap_extend_resultsource_tabledomain + (dst_index_extend_resultsource_table) = (0)) -> exists dst_positive_extend_resultsource_table dst_negative_extend_resultsource_table dst_value_extend_resultsource_table. ((((exists ff_h_pvs_extend_resultsource_tableentrypositive. ff_h_pvs_extend_resultsource_tableentrypositive + S (dst_positive_extend_resultsource_table) = S ((S (dst_index_extend_resultsource_table)) * dst_positive_scale_extend_resultsource_table)) /\ exists ff_q_pvs_extend_resultsource_tableentrypositive. dst_positive_code_extend_resultsource_table = ff_q_pvs_extend_resultsource_tableentrypositive * S ((S (dst_index_extend_resultsource_table)) * dst_positive_scale_extend_resultsource_table) + (dst_positive_extend_resultsource_table))) /\ (((((exists ff_h_pvs_extend_resultsource_tableentrynegative. ff_h_pvs_extend_resultsource_tableentrynegative + S (dst_negative_extend_resultsource_table) = S ((S (dst_index_extend_resultsource_table)) * dst_negative_scale_extend_resultsource_table)) /\ exists ff_q_pvs_extend_resultsource_tableentrynegative. dst_negative_code_extend_resultsource_table = ff_q_pvs_extend_resultsource_tableentrynegative * S ((S (dst_index_extend_resultsource_table)) * dst_negative_scale_extend_resultsource_table) + (dst_negative_extend_resultsource_table))) /\ (exists ge_balance_positive_extend_resultsource_tableentryvalue ge_balance_negative_extend_resultsource_tableentryvalue. (((((dst_value_extend_resultsource_table) = 2 * (ge_balance_positive_extend_resultsource_tableentryvalue) /\ (ge_balance_negative_extend_resultsource_tableentryvalue) = 0) \/ exists ge_signed_half_extend_resultsource_tableentryvaluedecode. (((dst_value_extend_resultsource_table) = 2 * ge_signed_half_extend_resultsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_resultsource_tableentryvalue) = 0) /\ (ge_balance_negative_extend_resultsource_tableentryvalue) = S ge_signed_half_extend_resultsource_tableentryvaluedecode))) /\ ((dst_positive_extend_resultsource_table) + ge_balance_negative_extend_resultsource_tableentryvalue = (dst_negative_extend_resultsource_table) + ge_balance_positive_extend_resultsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_extend_resultrow_table dst_positive_scale_extend_resultrow_table dst_negative_code_extend_resultrow_table dst_negative_scale_extend_resultrow_table. (((Q) = (((((dst_positive_code_extend_resultrow_table) + (dst_positive_scale_extend_resultrow_table)) * S ((dst_positive_code_extend_resultrow_table) + (dst_positive_scale_extend_resultrow_table)) + ((dst_positive_scale_extend_resultrow_table) + (dst_positive_scale_extend_resultrow_table))) + (((dst_negative_code_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)) * S ((dst_negative_code_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)) + ((dst_negative_scale_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)))) * S ((((dst_positive_code_extend_resultrow_table) + (dst_positive_scale_extend_resultrow_table)) * S ((dst_positive_code_extend_resultrow_table) + (dst_positive_scale_extend_resultrow_table)) + ((dst_positive_scale_extend_resultrow_table) + (dst_positive_scale_extend_resultrow_table))) + (((dst_negative_code_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)) * S ((dst_negative_code_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)) + ((dst_negative_scale_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)))) + ((((dst_negative_code_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)) * S ((dst_negative_code_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)) + ((dst_negative_scale_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table))) + (((dst_negative_code_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)) * S ((dst_negative_code_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)) + ((dst_negative_scale_extend_resultrow_table) + (dst_negative_scale_extend_resultrow_table)))))) /\ (forall dst_index_extend_resultrow_table. (exists pvs_le_gap_extend_resultrow_tabledomain. pvs_le_gap_extend_resultrow_tabledomain + (dst_index_extend_resultrow_table) = (S m)) -> exists dst_positive_extend_resultrow_table dst_negative_extend_resultrow_table dst_value_extend_resultrow_table. ((((exists ff_h_pvs_extend_resultrow_tableentrypositive. ff_h_pvs_extend_resultrow_tableentrypositive + S (dst_positive_extend_resultrow_table) = S ((S (dst_index_extend_resultrow_table)) * dst_positive_scale_extend_resultrow_table)) /\ exists ff_q_pvs_extend_resultrow_tableentrypositive. dst_positive_code_extend_resultrow_table = ff_q_pvs_extend_resultrow_tableentrypositive * S ((S (dst_index_extend_resultrow_table)) * dst_positive_scale_extend_resultrow_table) + (dst_positive_extend_resultrow_table))) /\ (((((exists ff_h_pvs_extend_resultrow_tableentrynegative. ff_h_pvs_extend_resultrow_tableentrynegative + S (dst_negative_extend_resultrow_table) = S ((S (dst_index_extend_resultrow_table)) * dst_negative_scale_extend_resultrow_table)) /\ exists ff_q_pvs_extend_resultrow_tableentrynegative. dst_negative_code_extend_resultrow_table = ff_q_pvs_extend_resultrow_tableentrynegative * S ((S (dst_index_extend_resultrow_table)) * dst_negative_scale_extend_resultrow_table) + (dst_negative_extend_resultrow_table))) /\ (exists ge_balance_positive_extend_resultrow_tableentryvalue ge_balance_negative_extend_resultrow_tableentryvalue. (((((dst_value_extend_resultrow_table) = 2 * (ge_balance_positive_extend_resultrow_tableentryvalue) /\ (ge_balance_negative_extend_resultrow_tableentryvalue) = 0) \/ exists ge_signed_half_extend_resultrow_tableentryvaluedecode. (((dst_value_extend_resultrow_table) = 2 * ge_signed_half_extend_resultrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_resultrow_tableentryvalue) = 0) /\ (ge_balance_negative_extend_resultrow_tableentryvalue) = S ge_signed_half_extend_resultrow_tableentryvaluedecode))) /\ ((dst_positive_extend_resultrow_table) + ge_balance_negative_extend_resultrow_tableentryvalue = (dst_negative_extend_resultrow_table) + ge_balance_positive_extend_resultrow_tableentryvalue))))))))) /\ (forall srt_index_extend_result. (exists pvs_gap_extend_resultbound. pvs_gap_extend_resultbound + S (srt_index_extend_result) = (S m)) -> exists srt_value_extend_result. (((exists dst_positive_code_extend_resultrowentry dst_positive_scale_extend_resultrowentry dst_negative_code_extend_resultrowentry dst_negative_scale_extend_resultrowentry dst_positive_extend_resultrowentry dst_negative_extend_resultrowentry. (((Q) = (((((dst_positive_code_extend_resultrowentry) + (dst_positive_scale_extend_resultrowentry)) * S ((dst_positive_code_extend_resultrowentry) + (dst_positive_scale_extend_resultrowentry)) + ((dst_positive_scale_extend_resultrowentry) + (dst_positive_scale_extend_resultrowentry))) + (((dst_negative_code_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)) * S ((dst_negative_code_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)) + ((dst_negative_scale_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)))) * S ((((dst_positive_code_extend_resultrowentry) + (dst_positive_scale_extend_resultrowentry)) * S ((dst_positive_code_extend_resultrowentry) + (dst_positive_scale_extend_resultrowentry)) + ((dst_positive_scale_extend_resultrowentry) + (dst_positive_scale_extend_resultrowentry))) + (((dst_negative_code_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)) * S ((dst_negative_code_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)) + ((dst_negative_scale_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)))) + ((((dst_negative_code_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)) * S ((dst_negative_code_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)) + ((dst_negative_scale_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry))) + (((dst_negative_code_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)) * S ((dst_negative_code_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)) + ((dst_negative_scale_extend_resultrowentry) + (dst_negative_scale_extend_resultrowentry)))))) /\ (((((exists ff_h_pvs_extend_resultrowentrypositive. ff_h_pvs_extend_resultrowentrypositive + S (dst_positive_extend_resultrowentry) = S ((S (srt_index_extend_result)) * dst_positive_scale_extend_resultrowentry)) /\ exists ff_q_pvs_extend_resultrowentrypositive. dst_positive_code_extend_resultrowentry = ff_q_pvs_extend_resultrowentrypositive * S ((S (srt_index_extend_result)) * dst_positive_scale_extend_resultrowentry) + (dst_positive_extend_resultrowentry))) /\ (((((exists ff_h_pvs_extend_resultrowentrynegative. ff_h_pvs_extend_resultrowentrynegative + S (dst_negative_extend_resultrowentry) = S ((S (srt_index_extend_result)) * dst_negative_scale_extend_resultrowentry)) /\ exists ff_q_pvs_extend_resultrowentrynegative. dst_negative_code_extend_resultrowentry = ff_q_pvs_extend_resultrowentrynegative * S ((S (srt_index_extend_result)) * dst_negative_scale_extend_resultrowentry) + (dst_negative_extend_resultrowentry))) /\ (exists ge_balance_positive_extend_resultrowentryvalue ge_balance_negative_extend_resultrowentryvalue. (((((srt_value_extend_result) = 2 * (ge_balance_positive_extend_resultrowentryvalue) /\ (ge_balance_negative_extend_resultrowentryvalue) = 0) \/ exists ge_signed_half_extend_resultrowentryvaluedecode. (((srt_value_extend_result) = 2 * ge_signed_half_extend_resultrowentryvaluedecode + 1 /\ (ge_balance_positive_extend_resultrowentryvalue) = 0) /\ (ge_balance_negative_extend_resultrowentryvalue) = S ge_signed_half_extend_resultrowentryvaluedecode))) /\ ((dst_positive_extend_resultrowentry) + ge_balance_negative_extend_resultrowentryvalue = (dst_negative_extend_resultrowentry) + ge_balance_positive_extend_resultrowentryvalue))))))))) /\ (exists srs_slice_extend_resultrowrow_sum. ((((exists dst_positive_code_extend_resultrowrow_sumslicesource_table dst_positive_scale_extend_resultrowrow_sumslicesource_table dst_negative_code_extend_resultrowrow_sumslicesource_table dst_negative_scale_extend_resultrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_extend_resultrowrow_sumslicesource_table) + (dst_positive_scale_extend_resultrowrow_sumslicesource_table)) * S ((dst_positive_code_extend_resultrowrow_sumslicesource_table) + (dst_positive_scale_extend_resultrowrow_sumslicesource_table)) + ((dst_positive_scale_extend_resultrowrow_sumslicesource_table) + (dst_positive_scale_extend_resultrowrow_sumslicesource_table))) + (((dst_negative_code_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)) * S ((dst_negative_code_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)) + ((dst_negative_scale_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)))) * S ((((dst_positive_code_extend_resultrowrow_sumslicesource_table) + (dst_positive_scale_extend_resultrowrow_sumslicesource_table)) * S ((dst_positive_code_extend_resultrowrow_sumslicesource_table) + (dst_positive_scale_extend_resultrowrow_sumslicesource_table)) + ((dst_positive_scale_extend_resultrowrow_sumslicesource_table) + (dst_positive_scale_extend_resultrowrow_sumslicesource_table))) + (((dst_negative_code_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)) * S ((dst_negative_code_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)) + ((dst_negative_scale_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)))) + ((((dst_negative_code_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)) * S ((dst_negative_code_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)) + ((dst_negative_scale_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table))) + (((dst_negative_code_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)) * S ((dst_negative_code_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)) + ((dst_negative_scale_extend_resultrowrow_sumslicesource_table) + (dst_negative_scale_extend_resultrowrow_sumslicesource_table)))))) /\ (forall dst_index_extend_resultrowrow_sumslicesource_table. (exists pvs_le_gap_extend_resultrowrow_sumslicesource_tabledomain. pvs_le_gap_extend_resultrowrow_sumslicesource_tabledomain + (dst_index_extend_resultrowrow_sumslicesource_table) = (0)) -> exists dst_positive_extend_resultrowrow_sumslicesource_table dst_negative_extend_resultrowrow_sumslicesource_table dst_value_extend_resultrowrow_sumslicesource_table. ((((exists ff_h_pvs_extend_resultrowrow_sumslicesource_tableentrypositive. ff_h_pvs_extend_resultrowrow_sumslicesource_tableentrypositive + S (dst_positive_extend_resultrowrow_sumslicesource_table) = S ((S (dst_index_extend_resultrowrow_sumslicesource_table)) * dst_positive_scale_extend_resultrowrow_sumslicesource_table)) /\ exists ff_q_pvs_extend_resultrowrow_sumslicesource_tableentrypositive. dst_positive_code_extend_resultrowrow_sumslicesource_table = ff_q_pvs_extend_resultrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_extend_resultrowrow_sumslicesource_table)) * dst_positive_scale_extend_resultrowrow_sumslicesource_table) + (dst_positive_extend_resultrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_extend_resultrowrow_sumslicesource_tableentrynegative. ff_h_pvs_extend_resultrowrow_sumslicesource_tableentrynegative + S (dst_negative_extend_resultrowrow_sumslicesource_table) = S ((S (dst_index_extend_resultrowrow_sumslicesource_table)) * dst_negative_scale_extend_resultrowrow_sumslicesource_table)) /\ exists ff_q_pvs_extend_resultrowrow_sumslicesource_tableentrynegative. dst_negative_code_extend_resultrowrow_sumslicesource_table = ff_q_pvs_extend_resultrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_extend_resultrowrow_sumslicesource_table)) * dst_negative_scale_extend_resultrowrow_sumslicesource_table) + (dst_negative_extend_resultrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_extend_resultrowrow_sumslicesource_tableentryvalue ge_balance_negative_extend_resultrowrow_sumslicesource_tableentryvalue. (((((dst_value_extend_resultrowrow_sumslicesource_table) = 2 * (ge_balance_positive_extend_resultrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_extend_resultrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_extend_resultrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_extend_resultrowrow_sumslicesource_table) = 2 * ge_signed_half_extend_resultrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_resultrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_extend_resultrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_extend_resultrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_extend_resultrowrow_sumslicesource_table) + ge_balance_negative_extend_resultrowrow_sumslicesource_tableentryvalue = (dst_negative_extend_resultrowrow_sumslicesource_table) + ge_balance_positive_extend_resultrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_extend_resultrowrow_sumsliceoutput_table dst_positive_scale_extend_resultrowrow_sumsliceoutput_table dst_negative_code_extend_resultrowrow_sumsliceoutput_table dst_negative_scale_extend_resultrowrow_sumsliceoutput_table. (((srs_slice_extend_resultrowrow_sum) = (((((dst_positive_code_extend_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_resultrowrow_sumsliceoutput_table)) * S ((dst_positive_code_extend_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_resultrowrow_sumsliceoutput_table)) + ((dst_positive_scale_extend_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_resultrowrow_sumsliceoutput_table))) + (((dst_negative_code_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)) * S ((dst_negative_code_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)) + ((dst_negative_scale_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_extend_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_resultrowrow_sumsliceoutput_table)) * S ((dst_positive_code_extend_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_resultrowrow_sumsliceoutput_table)) + ((dst_positive_scale_extend_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_extend_resultrowrow_sumsliceoutput_table))) + (((dst_negative_code_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)) * S ((dst_negative_code_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)) + ((dst_negative_scale_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)) * S ((dst_negative_code_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)) + ((dst_negative_scale_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table))) + (((dst_negative_code_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)) * S ((dst_negative_code_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)) + ((dst_negative_scale_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_extend_resultrowrow_sumsliceoutput_table. (exists pvs_le_gap_extend_resultrowrow_sumsliceoutput_tabledomain. pvs_le_gap_extend_resultrowrow_sumsliceoutput_tabledomain + (dst_index_extend_resultrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_extend_resultrowrow_sumsliceoutput_table dst_negative_extend_resultrowrow_sumsliceoutput_table dst_value_extend_resultrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_extend_resultrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_extend_resultrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_extend_resultrowrow_sumsliceoutput_table) = S ((S (dst_index_extend_resultrowrow_sumsliceoutput_table)) * dst_positive_scale_extend_resultrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_extend_resultrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_extend_resultrowrow_sumsliceoutput_table = ff_q_pvs_extend_resultrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_extend_resultrowrow_sumsliceoutput_table)) * dst_positive_scale_extend_resultrowrow_sumsliceoutput_table) + (dst_positive_extend_resultrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_extend_resultrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_extend_resultrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_extend_resultrowrow_sumsliceoutput_table) = S ((S (dst_index_extend_resultrowrow_sumsliceoutput_table)) * dst_negative_scale_extend_resultrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_extend_resultrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_extend_resultrowrow_sumsliceoutput_table = ff_q_pvs_extend_resultrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_extend_resultrowrow_sumsliceoutput_table)) * dst_negative_scale_extend_resultrowrow_sumsliceoutput_table) + (dst_negative_extend_resultrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_extend_resultrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_extend_resultrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_extend_resultrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_extend_resultrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_extend_resultrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_extend_resultrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_extend_resultrowrow_sumsliceoutput_table) = 2 * ge_signed_half_extend_resultrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_resultrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_extend_resultrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_extend_resultrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_extend_resultrowrow_sumsliceoutput_table) + ge_balance_negative_extend_resultrowrow_sumsliceoutput_tableentryvalue = (dst_negative_extend_resultrowrow_sumsliceoutput_table) + ge_balance_positive_extend_resultrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_extend_resultrowrow_sumslice. (exists pvs_gap_extend_resultrowrow_sumslicebound. pvs_gap_extend_resultrowrow_sumslicebound + S (srs_index_extend_resultrowrow_sumslice) = (n)) -> exists srs_value_extend_resultrowrow_sumslice. (((exists dst_positive_code_extend_resultrowrow_sumsliceentrysource dst_positive_scale_extend_resultrowrow_sumsliceentrysource dst_negative_code_extend_resultrowrow_sumsliceentrysource dst_negative_scale_extend_resultrowrow_sumsliceentrysource dst_positive_extend_resultrowrow_sumsliceentrysource dst_negative_extend_resultrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_extend_resultrowrow_sumsliceentrysource) + (dst_positive_scale_extend_resultrowrow_sumsliceentrysource)) * S ((dst_positive_code_extend_resultrowrow_sumsliceentrysource) + (dst_positive_scale_extend_resultrowrow_sumsliceentrysource)) + ((dst_positive_scale_extend_resultrowrow_sumsliceentrysource) + (dst_positive_scale_extend_resultrowrow_sumsliceentrysource))) + (((dst_negative_code_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)) * S ((dst_negative_code_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)) + ((dst_negative_scale_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_extend_resultrowrow_sumsliceentrysource) + (dst_positive_scale_extend_resultrowrow_sumsliceentrysource)) * S ((dst_positive_code_extend_resultrowrow_sumsliceentrysource) + (dst_positive_scale_extend_resultrowrow_sumsliceentrysource)) + ((dst_positive_scale_extend_resultrowrow_sumsliceentrysource) + (dst_positive_scale_extend_resultrowrow_sumsliceentrysource))) + (((dst_negative_code_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)) * S ((dst_negative_code_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)) + ((dst_negative_scale_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)))) + ((((dst_negative_code_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)) * S ((dst_negative_code_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)) + ((dst_negative_scale_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource))) + (((dst_negative_code_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)) * S ((dst_negative_code_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)) + ((dst_negative_scale_extend_resultrowrow_sumsliceentrysource) + (dst_negative_scale_extend_resultrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_extend_resultrowrow_sumsliceentrysourcepositive. ff_h_pvs_extend_resultrowrow_sumsliceentrysourcepositive + S (dst_positive_extend_resultrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_extend_result)))) + ((t) * (srs_index_extend_resultrowrow_sumslice))))) * dst_positive_scale_extend_resultrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_extend_resultrowrow_sumsliceentrysourcepositive. dst_positive_code_extend_resultrowrow_sumsliceentrysource = ff_q_pvs_extend_resultrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((s) * (srt_index_extend_result)))) + ((t) * (srs_index_extend_resultrowrow_sumslice))))) * dst_positive_scale_extend_resultrowrow_sumsliceentrysource) + (dst_positive_extend_resultrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_extend_resultrowrow_sumsliceentrysourcenegative. ff_h_pvs_extend_resultrowrow_sumsliceentrysourcenegative + S (dst_negative_extend_resultrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_extend_result)))) + ((t) * (srs_index_extend_resultrowrow_sumslice))))) * dst_negative_scale_extend_resultrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_extend_resultrowrow_sumsliceentrysourcenegative. dst_negative_code_extend_resultrowrow_sumsliceentrysource = ff_q_pvs_extend_resultrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((s) * (srt_index_extend_result)))) + ((t) * (srs_index_extend_resultrowrow_sumslice))))) * dst_negative_scale_extend_resultrowrow_sumsliceentrysource) + (dst_negative_extend_resultrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_extend_resultrowrow_sumsliceentrysourcevalue ge_balance_negative_extend_resultrowrow_sumsliceentrysourcevalue. (((((srs_value_extend_resultrowrow_sumslice) = 2 * (ge_balance_positive_extend_resultrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_extend_resultrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_extend_resultrowrow_sumsliceentrysourcevaluedecode. (((srs_value_extend_resultrowrow_sumslice) = 2 * ge_signed_half_extend_resultrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_extend_resultrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_extend_resultrowrow_sumsliceentrysourcevalue) = S ge_signed_half_extend_resultrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_extend_resultrowrow_sumsliceentrysource) + ge_balance_negative_extend_resultrowrow_sumsliceentrysourcevalue = (dst_negative_extend_resultrowrow_sumsliceentrysource) + ge_balance_positive_extend_resultrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_extend_resultrowrow_sumsliceentryoutput dst_positive_scale_extend_resultrowrow_sumsliceentryoutput dst_negative_code_extend_resultrowrow_sumsliceentryoutput dst_negative_scale_extend_resultrowrow_sumsliceentryoutput dst_positive_extend_resultrowrow_sumsliceentryoutput dst_negative_extend_resultrowrow_sumsliceentryoutput. (((srs_slice_extend_resultrowrow_sum) = (((((dst_positive_code_extend_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_resultrowrow_sumsliceentryoutput)) * S ((dst_positive_code_extend_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_resultrowrow_sumsliceentryoutput)) + ((dst_positive_scale_extend_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_resultrowrow_sumsliceentryoutput))) + (((dst_negative_code_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)) * S ((dst_negative_code_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)) + ((dst_negative_scale_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_extend_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_resultrowrow_sumsliceentryoutput)) * S ((dst_positive_code_extend_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_resultrowrow_sumsliceentryoutput)) + ((dst_positive_scale_extend_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_extend_resultrowrow_sumsliceentryoutput))) + (((dst_negative_code_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)) * S ((dst_negative_code_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)) + ((dst_negative_scale_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)) * S ((dst_negative_code_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)) + ((dst_negative_scale_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput))) + (((dst_negative_code_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)) * S ((dst_negative_code_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)) + ((dst_negative_scale_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_extend_resultrowrow_sumsliceentryoutputpositive. ff_h_pvs_extend_resultrowrow_sumsliceentryoutputpositive + S (dst_positive_extend_resultrowrow_sumsliceentryoutput) = S ((S (srs_index_extend_resultrowrow_sumslice)) * dst_positive_scale_extend_resultrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_extend_resultrowrow_sumsliceentryoutputpositive. dst_positive_code_extend_resultrowrow_sumsliceentryoutput = ff_q_pvs_extend_resultrowrow_sumsliceentryoutputpositive * S ((S (srs_index_extend_resultrowrow_sumslice)) * dst_positive_scale_extend_resultrowrow_sumsliceentryoutput) + (dst_positive_extend_resultrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_extend_resultrowrow_sumsliceentryoutputnegative. ff_h_pvs_extend_resultrowrow_sumsliceentryoutputnegative + S (dst_negative_extend_resultrowrow_sumsliceentryoutput) = S ((S (srs_index_extend_resultrowrow_sumslice)) * dst_negative_scale_extend_resultrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_extend_resultrowrow_sumsliceentryoutputnegative. dst_negative_code_extend_resultrowrow_sumsliceentryoutput = ff_q_pvs_extend_resultrowrow_sumsliceentryoutputnegative * S ((S (srs_index_extend_resultrowrow_sumslice)) * dst_negative_scale_extend_resultrowrow_sumsliceentryoutput) + (dst_negative_extend_resultrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_extend_resultrowrow_sumsliceentryoutputvalue ge_balance_negative_extend_resultrowrow_sumsliceentryoutputvalue. (((((srs_value_extend_resultrowrow_sumslice) = 2 * (ge_balance_positive_extend_resultrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_extend_resultrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_extend_resultrowrow_sumsliceentryoutputvaluedecode. (((srs_value_extend_resultrowrow_sumslice) = 2 * ge_signed_half_extend_resultrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_extend_resultrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_extend_resultrowrow_sumsliceentryoutputvalue) = S ge_signed_half_extend_resultrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_extend_resultrowrow_sumsliceentryoutput) + ge_balance_negative_extend_resultrowrow_sumsliceentryoutputvalue = (dst_negative_extend_resultrowrow_sumsliceentryoutput) + ge_balance_positive_extend_resultrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_extend_resultrowrow_sumsum dst_positive_scale_extend_resultrowrow_sumsum dst_negative_code_extend_resultrowrow_sumsum dst_negative_scale_extend_resultrowrow_sumsum dst_positive_sum_extend_resultrowrow_sumsum dst_negative_sum_extend_resultrowrow_sumsum. (((srs_slice_extend_resultrowrow_sum) = (((((dst_positive_code_extend_resultrowrow_sumsum) + (dst_positive_scale_extend_resultrowrow_sumsum)) * S ((dst_positive_code_extend_resultrowrow_sumsum) + (dst_positive_scale_extend_resultrowrow_sumsum)) + ((dst_positive_scale_extend_resultrowrow_sumsum) + (dst_positive_scale_extend_resultrowrow_sumsum))) + (((dst_negative_code_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)) * S ((dst_negative_code_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)) + ((dst_negative_scale_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)))) * S ((((dst_positive_code_extend_resultrowrow_sumsum) + (dst_positive_scale_extend_resultrowrow_sumsum)) * S ((dst_positive_code_extend_resultrowrow_sumsum) + (dst_positive_scale_extend_resultrowrow_sumsum)) + ((dst_positive_scale_extend_resultrowrow_sumsum) + (dst_positive_scale_extend_resultrowrow_sumsum))) + (((dst_negative_code_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)) * S ((dst_negative_code_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)) + ((dst_negative_scale_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)))) + ((((dst_negative_code_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)) * S ((dst_negative_code_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)) + ((dst_negative_scale_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum))) + (((dst_negative_code_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)) * S ((dst_negative_code_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)) + ((dst_negative_scale_extend_resultrowrow_sumsum) + (dst_negative_scale_extend_resultrowrow_sumsum)))))) /\ (((exists fs_u_dst_extend_resultrowrow_sumsumpositive fs_v_dst_extend_resultrowrow_sumsumpositive. ((((exists fs_h_dst_extend_resultrowrow_sumsumpositive_body_start. fs_h_dst_extend_resultrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_extend_resultrowrow_sumsumpositive)) /\ exists fs_q_dst_extend_resultrowrow_sumsumpositive_body_start. fs_u_dst_extend_resultrowrow_sumsumpositive = fs_q_dst_extend_resultrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_extend_resultrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_extend_resultrowrow_sumsumpositive_body_terminal. fs_h_dst_extend_resultrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_extend_resultrowrow_sumsum) = S ((S (n)) * fs_v_dst_extend_resultrowrow_sumsumpositive)) /\ exists fs_q_dst_extend_resultrowrow_sumsumpositive_body_terminal. fs_u_dst_extend_resultrowrow_sumsumpositive = fs_q_dst_extend_resultrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_extend_resultrowrow_sumsumpositive) + (dst_positive_sum_extend_resultrowrow_sumsum))) /\ forall fs_i_dst_extend_resultrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_extend_resultrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_extend_resultrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_extend_resultrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_extend_resultrowrow_sumsumpositive_body_steps fs_r_dst_extend_resultrowrow_sumsumpositive_body_steps fs_s_dst_extend_resultrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_extend_resultrowrow_sumsumpositive_body_steps_summand. fs_h_dst_extend_resultrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_extend_resultrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_extend_resultrowrow_sumsumpositive_body_steps)) * dst_positive_scale_extend_resultrowrow_sumsum)) /\ exists fs_q_dst_extend_resultrowrow_sumsumpositive_body_steps_summand. dst_positive_code_extend_resultrowrow_sumsum = fs_q_dst_extend_resultrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_extend_resultrowrow_sumsumpositive_body_steps)) * dst_positive_scale_extend_resultrowrow_sumsum) + (fs_a_dst_extend_resultrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_extend_resultrowrow_sumsumpositive_body_steps_partial. fs_h_dst_extend_resultrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_extend_resultrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_extend_resultrowrow_sumsumpositive_body_steps)) * fs_v_dst_extend_resultrowrow_sumsumpositive)) /\ exists fs_q_dst_extend_resultrowrow_sumsumpositive_body_steps_partial. fs_u_dst_extend_resultrowrow_sumsumpositive = fs_q_dst_extend_resultrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_extend_resultrowrow_sumsumpositive_body_steps)) * fs_v_dst_extend_resultrowrow_sumsumpositive) + (fs_r_dst_extend_resultrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_extend_resultrowrow_sumsumpositive_body_steps_successor. fs_h_dst_extend_resultrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_extend_resultrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_extend_resultrowrow_sumsumpositive_body_steps)) * fs_v_dst_extend_resultrowrow_sumsumpositive)) /\ exists fs_q_dst_extend_resultrowrow_sumsumpositive_body_steps_successor. fs_u_dst_extend_resultrowrow_sumsumpositive = fs_q_dst_extend_resultrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_extend_resultrowrow_sumsumpositive_body_steps)) * fs_v_dst_extend_resultrowrow_sumsumpositive) + (fs_s_dst_extend_resultrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_extend_resultrowrow_sumsumpositive_body_steps = fs_r_dst_extend_resultrowrow_sumsumpositive_body_steps + fs_a_dst_extend_resultrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_extend_resultrowrow_sumsumnegative fs_v_dst_extend_resultrowrow_sumsumnegative. ((((exists fs_h_dst_extend_resultrowrow_sumsumnegative_body_start. fs_h_dst_extend_resultrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_extend_resultrowrow_sumsumnegative)) /\ exists fs_q_dst_extend_resultrowrow_sumsumnegative_body_start. fs_u_dst_extend_resultrowrow_sumsumnegative = fs_q_dst_extend_resultrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_extend_resultrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_extend_resultrowrow_sumsumnegative_body_terminal. fs_h_dst_extend_resultrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_extend_resultrowrow_sumsum) = S ((S (n)) * fs_v_dst_extend_resultrowrow_sumsumnegative)) /\ exists fs_q_dst_extend_resultrowrow_sumsumnegative_body_terminal. fs_u_dst_extend_resultrowrow_sumsumnegative = fs_q_dst_extend_resultrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_extend_resultrowrow_sumsumnegative) + (dst_negative_sum_extend_resultrowrow_sumsum))) /\ forall fs_i_dst_extend_resultrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_extend_resultrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_extend_resultrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_extend_resultrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_extend_resultrowrow_sumsumnegative_body_steps fs_r_dst_extend_resultrowrow_sumsumnegative_body_steps fs_s_dst_extend_resultrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_extend_resultrowrow_sumsumnegative_body_steps_summand. fs_h_dst_extend_resultrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_extend_resultrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_extend_resultrowrow_sumsumnegative_body_steps)) * dst_negative_scale_extend_resultrowrow_sumsum)) /\ exists fs_q_dst_extend_resultrowrow_sumsumnegative_body_steps_summand. dst_negative_code_extend_resultrowrow_sumsum = fs_q_dst_extend_resultrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_extend_resultrowrow_sumsumnegative_body_steps)) * dst_negative_scale_extend_resultrowrow_sumsum) + (fs_a_dst_extend_resultrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_extend_resultrowrow_sumsumnegative_body_steps_partial. fs_h_dst_extend_resultrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_extend_resultrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_extend_resultrowrow_sumsumnegative_body_steps)) * fs_v_dst_extend_resultrowrow_sumsumnegative)) /\ exists fs_q_dst_extend_resultrowrow_sumsumnegative_body_steps_partial. fs_u_dst_extend_resultrowrow_sumsumnegative = fs_q_dst_extend_resultrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_extend_resultrowrow_sumsumnegative_body_steps)) * fs_v_dst_extend_resultrowrow_sumsumnegative) + (fs_r_dst_extend_resultrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_extend_resultrowrow_sumsumnegative_body_steps_successor. fs_h_dst_extend_resultrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_extend_resultrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_extend_resultrowrow_sumsumnegative_body_steps)) * fs_v_dst_extend_resultrowrow_sumsumnegative)) /\ exists fs_q_dst_extend_resultrowrow_sumsumnegative_body_steps_successor. fs_u_dst_extend_resultrowrow_sumsumnegative = fs_q_dst_extend_resultrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_extend_resultrowrow_sumsumnegative_body_steps)) * fs_v_dst_extend_resultrowrow_sumsumnegative) + (fs_s_dst_extend_resultrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_extend_resultrowrow_sumsumnegative_body_steps = fs_r_dst_extend_resultrowrow_sumsumnegative_body_steps + fs_a_dst_extend_resultrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_extend_resultrowrow_sumsumresult ge_balance_negative_extend_resultrowrow_sumsumresult. (((((srt_value_extend_result) = 2 * (ge_balance_positive_extend_resultrowrow_sumsumresult) /\ (ge_balance_negative_extend_resultrowrow_sumsumresult) = 0) \/ exists ge_signed_half_extend_resultrowrow_sumsumresultdecode. (((srt_value_extend_result) = 2 * ge_signed_half_extend_resultrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_extend_resultrowrow_sumsumresult) = 0) /\ (ge_balance_negative_extend_resultrowrow_sumsumresult) = S ge_signed_half_extend_resultrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_extend_resultrowrow_sumsum) + ge_balance_negative_extend_resultrowrow_sumsumresult = (dst_negative_sum_extend_resultrowrow_sumsum) + ge_balance_positive_extend_resultrowrow_sumsumresult))))))))))))))))))