Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Every slice, row table, column table and signed sum is an actual beta-coded witness. Entries are F((o+s*i)+t*j), for i<m and j<n. Zero dimensions and zero strides are allowed; separately certified endpoints are unused. Table uniqueness concerns values, not codes. No infinite-sum assertion is made.
Exact theorem in conservative defined notation
∀ F. ∀ R. ∀ Q. ∀ o. ∀ s. ∀ t. ∀ m. ∀ n. ∀ a. ArithRowSums(F,R,o,s,t,m,n) → ArithTable(m,Q) → ArithTableEqual(R,Q,m) → ArithAt(Q,m,a) → SignedSliceSum(F,o + s · m,t,n,a) → ArithRowSums(F,Q,o,s,t,S m,n)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order 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))))))))))))))))))Complete tactic proof in conservative notation
All 70 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
70 script commands · 19 reading checkpoints · 2 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–14
03Separate the logical casesL15–17
04Use earlier factsL18–18
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L18
exact hr_left
05Separate the logical casesL19–19
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L19
split
06Use earlier factsL20–24
07Fix variables and assumptionsL25–26
08Establish hcaseL27–31
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.
09Separate the logical casesL32–32
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L32
cases hcase
10Calculate and transport equalitiesL33–40
11Construct an explicit witnessL41–41
Supply the displayed value, then prove that it has the required property.
- L41
exists a
12Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
split
13Use earlier factsL43–44
14Establish holdL45–48
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hr right right.
- L45
have hold : ∃ z. ArithAt(R,i,z) ∧ SignedSliceSum(F,o + s · i,t,n,z)Definitions: ArithAt(R,i,z)SignedSliceSum(F,o + s · i,t,n,z)Original native command in the exact edition - L46
specialize hr_right_right (i) - L47
apply hr_right_right - L48
exact hcase_right
15Separate the logical casesL49–50
16Construct an explicit witnessL51–51
Supply the displayed value, then prove that it has the required property.
- L51
exists x
17Separate the logical casesL52–52
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L52
split
18Use earlier factsL53–62
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L53
specialize arithmetic_signed_table_equal_entry_transport (i) - L54
specialize arithmetic_signed_table_equal_entry_transport (R) - L55
specialize arithmetic_signed_table_equal_entry_transport (Q) - L56
specialize arithmetic_signed_table_equal_entry_transport (m) - L57
specialize arithmetic_signed_table_equal_entry_transport (i) - L58
specialize arithmetic_signed_table_equal_entry_transport (x) - L59
apply arithmetic_signed_table_equal_entry_transport - L60
specialize signed_table_domain_resize (m) - L61
specialize signed_table_domain_resize (i) - L62
specialize signed_table_domain_resize (Q)
Original defined command ledger · 70 lines
- 0001
intro F - 0002
intro R - 0003
intro Q - 0004
intro o - 0005
intro s - 0006
intro t - 0007
intro m - 0008
intro n - 0009
intro a - 0010
intro hr - 0011
intro hQ - 0012
intro hequal - 0013
intro hentry - 0014
intro hsum - 0015
cases hr - 0016
cases hr_right - 0017
split - 0018
exact hr_left - 0019
split - 0020
specialize signed_table_domain_resize (m) - 0021
specialize signed_table_domain_resize (S m) - 0022
specialize signed_table_domain_resize (Q) - 0023
apply signed_table_domain_resize - 0024
exact hQ - 0025
intro i - 0026
intro hi - 0027
have hcase : i = m ∨ Lt(i,m) - 0028
specialize finite_lt_succ_eq_or_lt (m) - 0029
specialize finite_lt_succ_eq_or_lt (i) - 0030
apply finite_lt_succ_eq_or_lt - 0031
exact hi - 0032
cases hcase - 0033
rewrite hcase_left - 0034
rewrite hcase_left - 0035
rewrite hcase_left - 0036
rewrite hcase_left - 0037
rewrite hcase_left - 0038
rewrite hcase_left - 0039
rewrite hcase_left - 0040
rewrite hcase_left - 0041
exists a - 0042
split - 0043
exact hentry - 0044
exact hsum - 0045
have hold : ∃ z. ArithAt(R,i,z) ∧ SignedSliceSum(F,o + s · i,t,n,z) - 0046
specialize hr_right_right (i) - 0047
apply hr_right_right - 0048
exact hcase_right - 0049
cases hold - 0050
cases hold_witness - 0051
exists x - 0052
split - 0053
specialize arithmetic_signed_table_equal_entry_transport (i) - 0054
specialize arithmetic_signed_table_equal_entry_transport (R) - 0055
specialize arithmetic_signed_table_equal_entry_transport (Q) - 0056
specialize arithmetic_signed_table_equal_entry_transport (m) - 0057
specialize arithmetic_signed_table_equal_entry_transport (i) - 0058
specialize arithmetic_signed_table_equal_entry_transport (x) - 0059
apply arithmetic_signed_table_equal_entry_transport - 0060
specialize signed_table_domain_resize (m) - 0061
specialize signed_table_domain_resize (i) - 0062
specialize signed_table_domain_resize (Q) - 0063
apply signed_table_domain_resize - 0064
exact hQ - 0065
exact hequal - 0066
specialize le_refl (i) - 0067
apply le_refl - 0068
exact hcase_right - 0069
exact hold_witness_left - 0070
exact hold_witness_right