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. ∀ C. ∀ V. ∀ D. ∀ o. ∀ s. ∀ t. ∀ m. ∀ n. ArithRowSums(F,C,o,t,s,n,m) → ArithSlice(F,V,o + s · m,t,n) → ArithRowSums(F,D,o,t,s,n,S m) → ArithAdd(C,V,D,n)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall F C V D o s t m n. (((exists dst_positive_code_column_step_beforesource_table dst_positive_scale_column_step_beforesource_table dst_negative_code_column_step_beforesource_table dst_negative_scale_column_step_beforesource_table. (((F) = (((((dst_positive_code_column_step_beforesource_table) + (dst_positive_scale_column_step_beforesource_table)) * S ((dst_positive_code_column_step_beforesource_table) + (dst_positive_scale_column_step_beforesource_table)) + ((dst_positive_scale_column_step_beforesource_table) + (dst_positive_scale_column_step_beforesource_table))) + (((dst_negative_code_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)) * S ((dst_negative_code_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)) + ((dst_negative_scale_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)))) * S ((((dst_positive_code_column_step_beforesource_table) + (dst_positive_scale_column_step_beforesource_table)) * S ((dst_positive_code_column_step_beforesource_table) + (dst_positive_scale_column_step_beforesource_table)) + ((dst_positive_scale_column_step_beforesource_table) + (dst_positive_scale_column_step_beforesource_table))) + (((dst_negative_code_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)) * S ((dst_negative_code_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)) + ((dst_negative_scale_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)))) + ((((dst_negative_code_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)) * S ((dst_negative_code_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)) + ((dst_negative_scale_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table))) + (((dst_negative_code_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)) * S ((dst_negative_code_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)) + ((dst_negative_scale_column_step_beforesource_table) + (dst_negative_scale_column_step_beforesource_table)))))) /\ (forall dst_index_column_step_beforesource_table. (exists pvs_le_gap_column_step_beforesource_tabledomain. pvs_le_gap_column_step_beforesource_tabledomain + (dst_index_column_step_beforesource_table) = (0)) -> exists dst_positive_column_step_beforesource_table dst_negative_column_step_beforesource_table dst_value_column_step_beforesource_table. ((((exists ff_h_pvs_column_step_beforesource_tableentrypositive. ff_h_pvs_column_step_beforesource_tableentrypositive + S (dst_positive_column_step_beforesource_table) = S ((S (dst_index_column_step_beforesource_table)) * dst_positive_scale_column_step_beforesource_table)) /\ exists ff_q_pvs_column_step_beforesource_tableentrypositive. dst_positive_code_column_step_beforesource_table = ff_q_pvs_column_step_beforesource_tableentrypositive * S ((S (dst_index_column_step_beforesource_table)) * dst_positive_scale_column_step_beforesource_table) + (dst_positive_column_step_beforesource_table))) /\ (((((exists ff_h_pvs_column_step_beforesource_tableentrynegative. ff_h_pvs_column_step_beforesource_tableentrynegative + S (dst_negative_column_step_beforesource_table) = S ((S (dst_index_column_step_beforesource_table)) * dst_negative_scale_column_step_beforesource_table)) /\ exists ff_q_pvs_column_step_beforesource_tableentrynegative. dst_negative_code_column_step_beforesource_table = ff_q_pvs_column_step_beforesource_tableentrynegative * S ((S (dst_index_column_step_beforesource_table)) * dst_negative_scale_column_step_beforesource_table) + (dst_negative_column_step_beforesource_table))) /\ (exists ge_balance_positive_column_step_beforesource_tableentryvalue ge_balance_negative_column_step_beforesource_tableentryvalue. (((((dst_value_column_step_beforesource_table) = 2 * (ge_balance_positive_column_step_beforesource_tableentryvalue) /\ (ge_balance_negative_column_step_beforesource_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_beforesource_tableentryvaluedecode. (((dst_value_column_step_beforesource_table) = 2 * ge_signed_half_column_step_beforesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_beforesource_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_beforesource_tableentryvalue) = S ge_signed_half_column_step_beforesource_tableentryvaluedecode))) /\ ((dst_positive_column_step_beforesource_table) + ge_balance_negative_column_step_beforesource_tableentryvalue = (dst_negative_column_step_beforesource_table) + ge_balance_positive_column_step_beforesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_step_beforerow_table dst_positive_scale_column_step_beforerow_table dst_negative_code_column_step_beforerow_table dst_negative_scale_column_step_beforerow_table. (((C) = (((((dst_positive_code_column_step_beforerow_table) + (dst_positive_scale_column_step_beforerow_table)) * S ((dst_positive_code_column_step_beforerow_table) + (dst_positive_scale_column_step_beforerow_table)) + ((dst_positive_scale_column_step_beforerow_table) + (dst_positive_scale_column_step_beforerow_table))) + (((dst_negative_code_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)) * S ((dst_negative_code_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)) + ((dst_negative_scale_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)))) * S ((((dst_positive_code_column_step_beforerow_table) + (dst_positive_scale_column_step_beforerow_table)) * S ((dst_positive_code_column_step_beforerow_table) + (dst_positive_scale_column_step_beforerow_table)) + ((dst_positive_scale_column_step_beforerow_table) + (dst_positive_scale_column_step_beforerow_table))) + (((dst_negative_code_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)) * S ((dst_negative_code_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)) + ((dst_negative_scale_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)))) + ((((dst_negative_code_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)) * S ((dst_negative_code_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)) + ((dst_negative_scale_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table))) + (((dst_negative_code_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)) * S ((dst_negative_code_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)) + ((dst_negative_scale_column_step_beforerow_table) + (dst_negative_scale_column_step_beforerow_table)))))) /\ (forall dst_index_column_step_beforerow_table. (exists pvs_le_gap_column_step_beforerow_tabledomain. pvs_le_gap_column_step_beforerow_tabledomain + (dst_index_column_step_beforerow_table) = (n)) -> exists dst_positive_column_step_beforerow_table dst_negative_column_step_beforerow_table dst_value_column_step_beforerow_table. ((((exists ff_h_pvs_column_step_beforerow_tableentrypositive. ff_h_pvs_column_step_beforerow_tableentrypositive + S (dst_positive_column_step_beforerow_table) = S ((S (dst_index_column_step_beforerow_table)) * dst_positive_scale_column_step_beforerow_table)) /\ exists ff_q_pvs_column_step_beforerow_tableentrypositive. dst_positive_code_column_step_beforerow_table = ff_q_pvs_column_step_beforerow_tableentrypositive * S ((S (dst_index_column_step_beforerow_table)) * dst_positive_scale_column_step_beforerow_table) + (dst_positive_column_step_beforerow_table))) /\ (((((exists ff_h_pvs_column_step_beforerow_tableentrynegative. ff_h_pvs_column_step_beforerow_tableentrynegative + S (dst_negative_column_step_beforerow_table) = S ((S (dst_index_column_step_beforerow_table)) * dst_negative_scale_column_step_beforerow_table)) /\ exists ff_q_pvs_column_step_beforerow_tableentrynegative. dst_negative_code_column_step_beforerow_table = ff_q_pvs_column_step_beforerow_tableentrynegative * S ((S (dst_index_column_step_beforerow_table)) * dst_negative_scale_column_step_beforerow_table) + (dst_negative_column_step_beforerow_table))) /\ (exists ge_balance_positive_column_step_beforerow_tableentryvalue ge_balance_negative_column_step_beforerow_tableentryvalue. (((((dst_value_column_step_beforerow_table) = 2 * (ge_balance_positive_column_step_beforerow_tableentryvalue) /\ (ge_balance_negative_column_step_beforerow_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_beforerow_tableentryvaluedecode. (((dst_value_column_step_beforerow_table) = 2 * ge_signed_half_column_step_beforerow_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_beforerow_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_beforerow_tableentryvalue) = S ge_signed_half_column_step_beforerow_tableentryvaluedecode))) /\ ((dst_positive_column_step_beforerow_table) + ge_balance_negative_column_step_beforerow_tableentryvalue = (dst_negative_column_step_beforerow_table) + ge_balance_positive_column_step_beforerow_tableentryvalue))))))))) /\ (forall srt_index_column_step_before. (exists pvs_gap_column_step_beforebound. pvs_gap_column_step_beforebound + S (srt_index_column_step_before) = (n)) -> exists srt_value_column_step_before. (((exists dst_positive_code_column_step_beforerowentry dst_positive_scale_column_step_beforerowentry dst_negative_code_column_step_beforerowentry dst_negative_scale_column_step_beforerowentry dst_positive_column_step_beforerowentry dst_negative_column_step_beforerowentry. (((C) = (((((dst_positive_code_column_step_beforerowentry) + (dst_positive_scale_column_step_beforerowentry)) * S ((dst_positive_code_column_step_beforerowentry) + (dst_positive_scale_column_step_beforerowentry)) + ((dst_positive_scale_column_step_beforerowentry) + (dst_positive_scale_column_step_beforerowentry))) + (((dst_negative_code_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)) * S ((dst_negative_code_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)) + ((dst_negative_scale_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)))) * S ((((dst_positive_code_column_step_beforerowentry) + (dst_positive_scale_column_step_beforerowentry)) * S ((dst_positive_code_column_step_beforerowentry) + (dst_positive_scale_column_step_beforerowentry)) + ((dst_positive_scale_column_step_beforerowentry) + (dst_positive_scale_column_step_beforerowentry))) + (((dst_negative_code_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)) * S ((dst_negative_code_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)) + ((dst_negative_scale_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)))) + ((((dst_negative_code_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)) * S ((dst_negative_code_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)) + ((dst_negative_scale_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry))) + (((dst_negative_code_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)) * S ((dst_negative_code_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)) + ((dst_negative_scale_column_step_beforerowentry) + (dst_negative_scale_column_step_beforerowentry)))))) /\ (((((exists ff_h_pvs_column_step_beforerowentrypositive. ff_h_pvs_column_step_beforerowentrypositive + S (dst_positive_column_step_beforerowentry) = S ((S (srt_index_column_step_before)) * dst_positive_scale_column_step_beforerowentry)) /\ exists ff_q_pvs_column_step_beforerowentrypositive. dst_positive_code_column_step_beforerowentry = ff_q_pvs_column_step_beforerowentrypositive * S ((S (srt_index_column_step_before)) * dst_positive_scale_column_step_beforerowentry) + (dst_positive_column_step_beforerowentry))) /\ (((((exists ff_h_pvs_column_step_beforerowentrynegative. ff_h_pvs_column_step_beforerowentrynegative + S (dst_negative_column_step_beforerowentry) = S ((S (srt_index_column_step_before)) * dst_negative_scale_column_step_beforerowentry)) /\ exists ff_q_pvs_column_step_beforerowentrynegative. dst_negative_code_column_step_beforerowentry = ff_q_pvs_column_step_beforerowentrynegative * S ((S (srt_index_column_step_before)) * dst_negative_scale_column_step_beforerowentry) + (dst_negative_column_step_beforerowentry))) /\ (exists ge_balance_positive_column_step_beforerowentryvalue ge_balance_negative_column_step_beforerowentryvalue. (((((srt_value_column_step_before) = 2 * (ge_balance_positive_column_step_beforerowentryvalue) /\ (ge_balance_negative_column_step_beforerowentryvalue) = 0) \/ exists ge_signed_half_column_step_beforerowentryvaluedecode. (((srt_value_column_step_before) = 2 * ge_signed_half_column_step_beforerowentryvaluedecode + 1 /\ (ge_balance_positive_column_step_beforerowentryvalue) = 0) /\ (ge_balance_negative_column_step_beforerowentryvalue) = S ge_signed_half_column_step_beforerowentryvaluedecode))) /\ ((dst_positive_column_step_beforerowentry) + ge_balance_negative_column_step_beforerowentryvalue = (dst_negative_column_step_beforerowentry) + ge_balance_positive_column_step_beforerowentryvalue))))))))) /\ (exists srs_slice_column_step_beforerowrow_sum. ((((exists dst_positive_code_column_step_beforerowrow_sumslicesource_table dst_positive_scale_column_step_beforerowrow_sumslicesource_table dst_negative_code_column_step_beforerowrow_sumslicesource_table dst_negative_scale_column_step_beforerowrow_sumslicesource_table. (((F) = (((((dst_positive_code_column_step_beforerowrow_sumslicesource_table) + (dst_positive_scale_column_step_beforerowrow_sumslicesource_table)) * S ((dst_positive_code_column_step_beforerowrow_sumslicesource_table) + (dst_positive_scale_column_step_beforerowrow_sumslicesource_table)) + ((dst_positive_scale_column_step_beforerowrow_sumslicesource_table) + (dst_positive_scale_column_step_beforerowrow_sumslicesource_table))) + (((dst_negative_code_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)) * S ((dst_negative_code_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)) + ((dst_negative_scale_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)))) * S ((((dst_positive_code_column_step_beforerowrow_sumslicesource_table) + (dst_positive_scale_column_step_beforerowrow_sumslicesource_table)) * S ((dst_positive_code_column_step_beforerowrow_sumslicesource_table) + (dst_positive_scale_column_step_beforerowrow_sumslicesource_table)) + ((dst_positive_scale_column_step_beforerowrow_sumslicesource_table) + (dst_positive_scale_column_step_beforerowrow_sumslicesource_table))) + (((dst_negative_code_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)) * S ((dst_negative_code_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)) + ((dst_negative_scale_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)))) + ((((dst_negative_code_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)) * S ((dst_negative_code_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)) + ((dst_negative_scale_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table))) + (((dst_negative_code_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)) * S ((dst_negative_code_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)) + ((dst_negative_scale_column_step_beforerowrow_sumslicesource_table) + (dst_negative_scale_column_step_beforerowrow_sumslicesource_table)))))) /\ (forall dst_index_column_step_beforerowrow_sumslicesource_table. (exists pvs_le_gap_column_step_beforerowrow_sumslicesource_tabledomain. pvs_le_gap_column_step_beforerowrow_sumslicesource_tabledomain + (dst_index_column_step_beforerowrow_sumslicesource_table) = (0)) -> exists dst_positive_column_step_beforerowrow_sumslicesource_table dst_negative_column_step_beforerowrow_sumslicesource_table dst_value_column_step_beforerowrow_sumslicesource_table. ((((exists ff_h_pvs_column_step_beforerowrow_sumslicesource_tableentrypositive. ff_h_pvs_column_step_beforerowrow_sumslicesource_tableentrypositive + S (dst_positive_column_step_beforerowrow_sumslicesource_table) = S ((S (dst_index_column_step_beforerowrow_sumslicesource_table)) * dst_positive_scale_column_step_beforerowrow_sumslicesource_table)) /\ exists ff_q_pvs_column_step_beforerowrow_sumslicesource_tableentrypositive. dst_positive_code_column_step_beforerowrow_sumslicesource_table = ff_q_pvs_column_step_beforerowrow_sumslicesource_tableentrypositive * S ((S (dst_index_column_step_beforerowrow_sumslicesource_table)) * dst_positive_scale_column_step_beforerowrow_sumslicesource_table) + (dst_positive_column_step_beforerowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_column_step_beforerowrow_sumslicesource_tableentrynegative. ff_h_pvs_column_step_beforerowrow_sumslicesource_tableentrynegative + S (dst_negative_column_step_beforerowrow_sumslicesource_table) = S ((S (dst_index_column_step_beforerowrow_sumslicesource_table)) * dst_negative_scale_column_step_beforerowrow_sumslicesource_table)) /\ exists ff_q_pvs_column_step_beforerowrow_sumslicesource_tableentrynegative. dst_negative_code_column_step_beforerowrow_sumslicesource_table = ff_q_pvs_column_step_beforerowrow_sumslicesource_tableentrynegative * S ((S (dst_index_column_step_beforerowrow_sumslicesource_table)) * dst_negative_scale_column_step_beforerowrow_sumslicesource_table) + (dst_negative_column_step_beforerowrow_sumslicesource_table))) /\ (exists ge_balance_positive_column_step_beforerowrow_sumslicesource_tableentryvalue ge_balance_negative_column_step_beforerowrow_sumslicesource_tableentryvalue. (((((dst_value_column_step_beforerowrow_sumslicesource_table) = 2 * (ge_balance_positive_column_step_beforerowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_column_step_beforerowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_beforerowrow_sumslicesource_tableentryvaluedecode. (((dst_value_column_step_beforerowrow_sumslicesource_table) = 2 * ge_signed_half_column_step_beforerowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_beforerowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_beforerowrow_sumslicesource_tableentryvalue) = S ge_signed_half_column_step_beforerowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_column_step_beforerowrow_sumslicesource_table) + ge_balance_negative_column_step_beforerowrow_sumslicesource_tableentryvalue = (dst_negative_column_step_beforerowrow_sumslicesource_table) + ge_balance_positive_column_step_beforerowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_step_beforerowrow_sumsliceoutput_table dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table dst_negative_code_column_step_beforerowrow_sumsliceoutput_table dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table. (((srs_slice_column_step_beforerowrow_sum) = (((((dst_positive_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table)) * S ((dst_positive_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table)) + ((dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table))) + (((dst_negative_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table)) * S ((dst_positive_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table)) + ((dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table))) + (((dst_negative_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)))) + ((((dst_negative_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table))) + (((dst_negative_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)))))) /\ (forall dst_index_column_step_beforerowrow_sumsliceoutput_table. (exists pvs_le_gap_column_step_beforerowrow_sumsliceoutput_tabledomain. pvs_le_gap_column_step_beforerowrow_sumsliceoutput_tabledomain + (dst_index_column_step_beforerowrow_sumsliceoutput_table) = (m)) -> exists dst_positive_column_step_beforerowrow_sumsliceoutput_table dst_negative_column_step_beforerowrow_sumsliceoutput_table dst_value_column_step_beforerowrow_sumsliceoutput_table. ((((exists ff_h_pvs_column_step_beforerowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_column_step_beforerowrow_sumsliceoutput_tableentrypositive + S (dst_positive_column_step_beforerowrow_sumsliceoutput_table) = S ((S (dst_index_column_step_beforerowrow_sumsliceoutput_table)) * dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_column_step_beforerowrow_sumsliceoutput_tableentrypositive. dst_positive_code_column_step_beforerowrow_sumsliceoutput_table = ff_q_pvs_column_step_beforerowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_column_step_beforerowrow_sumsliceoutput_table)) * dst_positive_scale_column_step_beforerowrow_sumsliceoutput_table) + (dst_positive_column_step_beforerowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_column_step_beforerowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_column_step_beforerowrow_sumsliceoutput_tableentrynegative + S (dst_negative_column_step_beforerowrow_sumsliceoutput_table) = S ((S (dst_index_column_step_beforerowrow_sumsliceoutput_table)) * dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_column_step_beforerowrow_sumsliceoutput_tableentrynegative. dst_negative_code_column_step_beforerowrow_sumsliceoutput_table = ff_q_pvs_column_step_beforerowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_column_step_beforerowrow_sumsliceoutput_table)) * dst_negative_scale_column_step_beforerowrow_sumsliceoutput_table) + (dst_negative_column_step_beforerowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_column_step_beforerowrow_sumsliceoutput_tableentryvalue ge_balance_negative_column_step_beforerowrow_sumsliceoutput_tableentryvalue. (((((dst_value_column_step_beforerowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_column_step_beforerowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_column_step_beforerowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_beforerowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_column_step_beforerowrow_sumsliceoutput_table) = 2 * ge_signed_half_column_step_beforerowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_beforerowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_beforerowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_column_step_beforerowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_column_step_beforerowrow_sumsliceoutput_table) + ge_balance_negative_column_step_beforerowrow_sumsliceoutput_tableentryvalue = (dst_negative_column_step_beforerowrow_sumsliceoutput_table) + ge_balance_positive_column_step_beforerowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_column_step_beforerowrow_sumslice. (exists pvs_gap_column_step_beforerowrow_sumslicebound. pvs_gap_column_step_beforerowrow_sumslicebound + S (srs_index_column_step_beforerowrow_sumslice) = (m)) -> exists srs_value_column_step_beforerowrow_sumslice. (((exists dst_positive_code_column_step_beforerowrow_sumsliceentrysource dst_positive_scale_column_step_beforerowrow_sumsliceentrysource dst_negative_code_column_step_beforerowrow_sumsliceentrysource dst_negative_scale_column_step_beforerowrow_sumsliceentrysource dst_positive_column_step_beforerowrow_sumsliceentrysource dst_negative_column_step_beforerowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_column_step_beforerowrow_sumsliceentrysource) + (dst_positive_scale_column_step_beforerowrow_sumsliceentrysource)) * S ((dst_positive_code_column_step_beforerowrow_sumsliceentrysource) + (dst_positive_scale_column_step_beforerowrow_sumsliceentrysource)) + ((dst_positive_scale_column_step_beforerowrow_sumsliceentrysource) + (dst_positive_scale_column_step_beforerowrow_sumsliceentrysource))) + (((dst_negative_code_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)))) * S ((((dst_positive_code_column_step_beforerowrow_sumsliceentrysource) + (dst_positive_scale_column_step_beforerowrow_sumsliceentrysource)) * S ((dst_positive_code_column_step_beforerowrow_sumsliceentrysource) + (dst_positive_scale_column_step_beforerowrow_sumsliceentrysource)) + ((dst_positive_scale_column_step_beforerowrow_sumsliceentrysource) + (dst_positive_scale_column_step_beforerowrow_sumsliceentrysource))) + (((dst_negative_code_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)))) + ((((dst_negative_code_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource))) + (((dst_negative_code_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_column_step_beforerowrow_sumsliceentrysourcepositive. ff_h_pvs_column_step_beforerowrow_sumsliceentrysourcepositive + S (dst_positive_column_step_beforerowrow_sumsliceentrysource) = S ((S (((((o) + ((t) * (srt_index_column_step_before)))) + ((s) * (srs_index_column_step_beforerowrow_sumslice))))) * dst_positive_scale_column_step_beforerowrow_sumsliceentrysource)) /\ exists ff_q_pvs_column_step_beforerowrow_sumsliceentrysourcepositive. dst_positive_code_column_step_beforerowrow_sumsliceentrysource = ff_q_pvs_column_step_beforerowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((t) * (srt_index_column_step_before)))) + ((s) * (srs_index_column_step_beforerowrow_sumslice))))) * dst_positive_scale_column_step_beforerowrow_sumsliceentrysource) + (dst_positive_column_step_beforerowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_column_step_beforerowrow_sumsliceentrysourcenegative. ff_h_pvs_column_step_beforerowrow_sumsliceentrysourcenegative + S (dst_negative_column_step_beforerowrow_sumsliceentrysource) = S ((S (((((o) + ((t) * (srt_index_column_step_before)))) + ((s) * (srs_index_column_step_beforerowrow_sumslice))))) * dst_negative_scale_column_step_beforerowrow_sumsliceentrysource)) /\ exists ff_q_pvs_column_step_beforerowrow_sumsliceentrysourcenegative. dst_negative_code_column_step_beforerowrow_sumsliceentrysource = ff_q_pvs_column_step_beforerowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((t) * (srt_index_column_step_before)))) + ((s) * (srs_index_column_step_beforerowrow_sumslice))))) * dst_negative_scale_column_step_beforerowrow_sumsliceentrysource) + (dst_negative_column_step_beforerowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_column_step_beforerowrow_sumsliceentrysourcevalue ge_balance_negative_column_step_beforerowrow_sumsliceentrysourcevalue. (((((srs_value_column_step_beforerowrow_sumslice) = 2 * (ge_balance_positive_column_step_beforerowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_column_step_beforerowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_column_step_beforerowrow_sumsliceentrysourcevaluedecode. (((srs_value_column_step_beforerowrow_sumslice) = 2 * ge_signed_half_column_step_beforerowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_column_step_beforerowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_column_step_beforerowrow_sumsliceentrysourcevalue) = S ge_signed_half_column_step_beforerowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_column_step_beforerowrow_sumsliceentrysource) + ge_balance_negative_column_step_beforerowrow_sumsliceentrysourcevalue = (dst_negative_column_step_beforerowrow_sumsliceentrysource) + ge_balance_positive_column_step_beforerowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_column_step_beforerowrow_sumsliceentryoutput dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput dst_negative_code_column_step_beforerowrow_sumsliceentryoutput dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput dst_positive_column_step_beforerowrow_sumsliceentryoutput dst_negative_column_step_beforerowrow_sumsliceentryoutput. (((srs_slice_column_step_beforerowrow_sum) = (((((dst_positive_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput)) * S ((dst_positive_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput)) + ((dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput))) + (((dst_negative_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput)) * S ((dst_positive_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput)) + ((dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput))) + (((dst_negative_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)))) + ((((dst_negative_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput))) + (((dst_negative_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_column_step_beforerowrow_sumsliceentryoutputpositive. ff_h_pvs_column_step_beforerowrow_sumsliceentryoutputpositive + S (dst_positive_column_step_beforerowrow_sumsliceentryoutput) = S ((S (srs_index_column_step_beforerowrow_sumslice)) * dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_column_step_beforerowrow_sumsliceentryoutputpositive. dst_positive_code_column_step_beforerowrow_sumsliceentryoutput = ff_q_pvs_column_step_beforerowrow_sumsliceentryoutputpositive * S ((S (srs_index_column_step_beforerowrow_sumslice)) * dst_positive_scale_column_step_beforerowrow_sumsliceentryoutput) + (dst_positive_column_step_beforerowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_column_step_beforerowrow_sumsliceentryoutputnegative. ff_h_pvs_column_step_beforerowrow_sumsliceentryoutputnegative + S (dst_negative_column_step_beforerowrow_sumsliceentryoutput) = S ((S (srs_index_column_step_beforerowrow_sumslice)) * dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_column_step_beforerowrow_sumsliceentryoutputnegative. dst_negative_code_column_step_beforerowrow_sumsliceentryoutput = ff_q_pvs_column_step_beforerowrow_sumsliceentryoutputnegative * S ((S (srs_index_column_step_beforerowrow_sumslice)) * dst_negative_scale_column_step_beforerowrow_sumsliceentryoutput) + (dst_negative_column_step_beforerowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_column_step_beforerowrow_sumsliceentryoutputvalue ge_balance_negative_column_step_beforerowrow_sumsliceentryoutputvalue. (((((srs_value_column_step_beforerowrow_sumslice) = 2 * (ge_balance_positive_column_step_beforerowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_column_step_beforerowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_column_step_beforerowrow_sumsliceentryoutputvaluedecode. (((srs_value_column_step_beforerowrow_sumslice) = 2 * ge_signed_half_column_step_beforerowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_column_step_beforerowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_column_step_beforerowrow_sumsliceentryoutputvalue) = S ge_signed_half_column_step_beforerowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_column_step_beforerowrow_sumsliceentryoutput) + ge_balance_negative_column_step_beforerowrow_sumsliceentryoutputvalue = (dst_negative_column_step_beforerowrow_sumsliceentryoutput) + ge_balance_positive_column_step_beforerowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_column_step_beforerowrow_sumsum dst_positive_scale_column_step_beforerowrow_sumsum dst_negative_code_column_step_beforerowrow_sumsum dst_negative_scale_column_step_beforerowrow_sumsum dst_positive_sum_column_step_beforerowrow_sumsum dst_negative_sum_column_step_beforerowrow_sumsum. (((srs_slice_column_step_beforerowrow_sum) = (((((dst_positive_code_column_step_beforerowrow_sumsum) + (dst_positive_scale_column_step_beforerowrow_sumsum)) * S ((dst_positive_code_column_step_beforerowrow_sumsum) + (dst_positive_scale_column_step_beforerowrow_sumsum)) + ((dst_positive_scale_column_step_beforerowrow_sumsum) + (dst_positive_scale_column_step_beforerowrow_sumsum))) + (((dst_negative_code_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)) * S ((dst_negative_code_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)) + ((dst_negative_scale_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)))) * S ((((dst_positive_code_column_step_beforerowrow_sumsum) + (dst_positive_scale_column_step_beforerowrow_sumsum)) * S ((dst_positive_code_column_step_beforerowrow_sumsum) + (dst_positive_scale_column_step_beforerowrow_sumsum)) + ((dst_positive_scale_column_step_beforerowrow_sumsum) + (dst_positive_scale_column_step_beforerowrow_sumsum))) + (((dst_negative_code_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)) * S ((dst_negative_code_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)) + ((dst_negative_scale_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)))) + ((((dst_negative_code_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)) * S ((dst_negative_code_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)) + ((dst_negative_scale_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum))) + (((dst_negative_code_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)) * S ((dst_negative_code_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)) + ((dst_negative_scale_column_step_beforerowrow_sumsum) + (dst_negative_scale_column_step_beforerowrow_sumsum)))))) /\ (((exists fs_u_dst_column_step_beforerowrow_sumsumpositive fs_v_dst_column_step_beforerowrow_sumsumpositive. ((((exists fs_h_dst_column_step_beforerowrow_sumsumpositive_body_start. fs_h_dst_column_step_beforerowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_column_step_beforerowrow_sumsumpositive)) /\ exists fs_q_dst_column_step_beforerowrow_sumsumpositive_body_start. fs_u_dst_column_step_beforerowrow_sumsumpositive = fs_q_dst_column_step_beforerowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_column_step_beforerowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_column_step_beforerowrow_sumsumpositive_body_terminal. fs_h_dst_column_step_beforerowrow_sumsumpositive_body_terminal + S (dst_positive_sum_column_step_beforerowrow_sumsum) = S ((S (m)) * fs_v_dst_column_step_beforerowrow_sumsumpositive)) /\ exists fs_q_dst_column_step_beforerowrow_sumsumpositive_body_terminal. fs_u_dst_column_step_beforerowrow_sumsumpositive = fs_q_dst_column_step_beforerowrow_sumsumpositive_body_terminal * S ((S (m)) * fs_v_dst_column_step_beforerowrow_sumsumpositive) + (dst_positive_sum_column_step_beforerowrow_sumsum))) /\ forall fs_i_dst_column_step_beforerowrow_sumsumpositive_body_steps. (exists fs_lt_dst_column_step_beforerowrow_sumsumpositive_body_steps_bound. fs_lt_dst_column_step_beforerowrow_sumsumpositive_body_steps_bound + S fs_i_dst_column_step_beforerowrow_sumsumpositive_body_steps = m) -> exists fs_a_dst_column_step_beforerowrow_sumsumpositive_body_steps fs_r_dst_column_step_beforerowrow_sumsumpositive_body_steps fs_s_dst_column_step_beforerowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_column_step_beforerowrow_sumsumpositive_body_steps_summand. fs_h_dst_column_step_beforerowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_column_step_beforerowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_column_step_beforerowrow_sumsumpositive_body_steps)) * dst_positive_scale_column_step_beforerowrow_sumsum)) /\ exists fs_q_dst_column_step_beforerowrow_sumsumpositive_body_steps_summand. dst_positive_code_column_step_beforerowrow_sumsum = fs_q_dst_column_step_beforerowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_column_step_beforerowrow_sumsumpositive_body_steps)) * dst_positive_scale_column_step_beforerowrow_sumsum) + (fs_a_dst_column_step_beforerowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_column_step_beforerowrow_sumsumpositive_body_steps_partial. fs_h_dst_column_step_beforerowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_column_step_beforerowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_column_step_beforerowrow_sumsumpositive_body_steps)) * fs_v_dst_column_step_beforerowrow_sumsumpositive)) /\ exists fs_q_dst_column_step_beforerowrow_sumsumpositive_body_steps_partial. fs_u_dst_column_step_beforerowrow_sumsumpositive = fs_q_dst_column_step_beforerowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_column_step_beforerowrow_sumsumpositive_body_steps)) * fs_v_dst_column_step_beforerowrow_sumsumpositive) + (fs_r_dst_column_step_beforerowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_column_step_beforerowrow_sumsumpositive_body_steps_successor. fs_h_dst_column_step_beforerowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_column_step_beforerowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_column_step_beforerowrow_sumsumpositive_body_steps)) * fs_v_dst_column_step_beforerowrow_sumsumpositive)) /\ exists fs_q_dst_column_step_beforerowrow_sumsumpositive_body_steps_successor. fs_u_dst_column_step_beforerowrow_sumsumpositive = fs_q_dst_column_step_beforerowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_column_step_beforerowrow_sumsumpositive_body_steps)) * fs_v_dst_column_step_beforerowrow_sumsumpositive) + (fs_s_dst_column_step_beforerowrow_sumsumpositive_body_steps))) /\ fs_s_dst_column_step_beforerowrow_sumsumpositive_body_steps = fs_r_dst_column_step_beforerowrow_sumsumpositive_body_steps + fs_a_dst_column_step_beforerowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_column_step_beforerowrow_sumsumnegative fs_v_dst_column_step_beforerowrow_sumsumnegative. ((((exists fs_h_dst_column_step_beforerowrow_sumsumnegative_body_start. fs_h_dst_column_step_beforerowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_column_step_beforerowrow_sumsumnegative)) /\ exists fs_q_dst_column_step_beforerowrow_sumsumnegative_body_start. fs_u_dst_column_step_beforerowrow_sumsumnegative = fs_q_dst_column_step_beforerowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_column_step_beforerowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_column_step_beforerowrow_sumsumnegative_body_terminal. fs_h_dst_column_step_beforerowrow_sumsumnegative_body_terminal + S (dst_negative_sum_column_step_beforerowrow_sumsum) = S ((S (m)) * fs_v_dst_column_step_beforerowrow_sumsumnegative)) /\ exists fs_q_dst_column_step_beforerowrow_sumsumnegative_body_terminal. fs_u_dst_column_step_beforerowrow_sumsumnegative = fs_q_dst_column_step_beforerowrow_sumsumnegative_body_terminal * S ((S (m)) * fs_v_dst_column_step_beforerowrow_sumsumnegative) + (dst_negative_sum_column_step_beforerowrow_sumsum))) /\ forall fs_i_dst_column_step_beforerowrow_sumsumnegative_body_steps. (exists fs_lt_dst_column_step_beforerowrow_sumsumnegative_body_steps_bound. fs_lt_dst_column_step_beforerowrow_sumsumnegative_body_steps_bound + S fs_i_dst_column_step_beforerowrow_sumsumnegative_body_steps = m) -> exists fs_a_dst_column_step_beforerowrow_sumsumnegative_body_steps fs_r_dst_column_step_beforerowrow_sumsumnegative_body_steps fs_s_dst_column_step_beforerowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_column_step_beforerowrow_sumsumnegative_body_steps_summand. fs_h_dst_column_step_beforerowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_column_step_beforerowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_column_step_beforerowrow_sumsumnegative_body_steps)) * dst_negative_scale_column_step_beforerowrow_sumsum)) /\ exists fs_q_dst_column_step_beforerowrow_sumsumnegative_body_steps_summand. dst_negative_code_column_step_beforerowrow_sumsum = fs_q_dst_column_step_beforerowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_column_step_beforerowrow_sumsumnegative_body_steps)) * dst_negative_scale_column_step_beforerowrow_sumsum) + (fs_a_dst_column_step_beforerowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_column_step_beforerowrow_sumsumnegative_body_steps_partial. fs_h_dst_column_step_beforerowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_column_step_beforerowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_column_step_beforerowrow_sumsumnegative_body_steps)) * fs_v_dst_column_step_beforerowrow_sumsumnegative)) /\ exists fs_q_dst_column_step_beforerowrow_sumsumnegative_body_steps_partial. fs_u_dst_column_step_beforerowrow_sumsumnegative = fs_q_dst_column_step_beforerowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_column_step_beforerowrow_sumsumnegative_body_steps)) * fs_v_dst_column_step_beforerowrow_sumsumnegative) + (fs_r_dst_column_step_beforerowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_column_step_beforerowrow_sumsumnegative_body_steps_successor. fs_h_dst_column_step_beforerowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_column_step_beforerowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_column_step_beforerowrow_sumsumnegative_body_steps)) * fs_v_dst_column_step_beforerowrow_sumsumnegative)) /\ exists fs_q_dst_column_step_beforerowrow_sumsumnegative_body_steps_successor. fs_u_dst_column_step_beforerowrow_sumsumnegative = fs_q_dst_column_step_beforerowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_column_step_beforerowrow_sumsumnegative_body_steps)) * fs_v_dst_column_step_beforerowrow_sumsumnegative) + (fs_s_dst_column_step_beforerowrow_sumsumnegative_body_steps))) /\ fs_s_dst_column_step_beforerowrow_sumsumnegative_body_steps = fs_r_dst_column_step_beforerowrow_sumsumnegative_body_steps + fs_a_dst_column_step_beforerowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_column_step_beforerowrow_sumsumresult ge_balance_negative_column_step_beforerowrow_sumsumresult. (((((srt_value_column_step_before) = 2 * (ge_balance_positive_column_step_beforerowrow_sumsumresult) /\ (ge_balance_negative_column_step_beforerowrow_sumsumresult) = 0) \/ exists ge_signed_half_column_step_beforerowrow_sumsumresultdecode. (((srt_value_column_step_before) = 2 * ge_signed_half_column_step_beforerowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_column_step_beforerowrow_sumsumresult) = 0) /\ (ge_balance_negative_column_step_beforerowrow_sumsumresult) = S ge_signed_half_column_step_beforerowrow_sumsumresultdecode))) /\ ((dst_positive_sum_column_step_beforerowrow_sumsum) + ge_balance_negative_column_step_beforerowrow_sumsumresult = (dst_negative_sum_column_step_beforerowrow_sumsum) + ge_balance_positive_column_step_beforerowrow_sumsumresult)))))))))))))))))) -> (((exists dst_positive_code_column_step_rowsource_table dst_positive_scale_column_step_rowsource_table dst_negative_code_column_step_rowsource_table dst_negative_scale_column_step_rowsource_table. (((F) = (((((dst_positive_code_column_step_rowsource_table) + (dst_positive_scale_column_step_rowsource_table)) * S ((dst_positive_code_column_step_rowsource_table) + (dst_positive_scale_column_step_rowsource_table)) + ((dst_positive_scale_column_step_rowsource_table) + (dst_positive_scale_column_step_rowsource_table))) + (((dst_negative_code_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)) * S ((dst_negative_code_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)) + ((dst_negative_scale_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)))) * S ((((dst_positive_code_column_step_rowsource_table) + (dst_positive_scale_column_step_rowsource_table)) * S ((dst_positive_code_column_step_rowsource_table) + (dst_positive_scale_column_step_rowsource_table)) + ((dst_positive_scale_column_step_rowsource_table) + (dst_positive_scale_column_step_rowsource_table))) + (((dst_negative_code_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)) * S ((dst_negative_code_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)) + ((dst_negative_scale_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)))) + ((((dst_negative_code_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)) * S ((dst_negative_code_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)) + ((dst_negative_scale_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table))) + (((dst_negative_code_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)) * S ((dst_negative_code_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)) + ((dst_negative_scale_column_step_rowsource_table) + (dst_negative_scale_column_step_rowsource_table)))))) /\ (forall dst_index_column_step_rowsource_table. (exists pvs_le_gap_column_step_rowsource_tabledomain. pvs_le_gap_column_step_rowsource_tabledomain + (dst_index_column_step_rowsource_table) = (0)) -> exists dst_positive_column_step_rowsource_table dst_negative_column_step_rowsource_table dst_value_column_step_rowsource_table. ((((exists ff_h_pvs_column_step_rowsource_tableentrypositive. ff_h_pvs_column_step_rowsource_tableentrypositive + S (dst_positive_column_step_rowsource_table) = S ((S (dst_index_column_step_rowsource_table)) * dst_positive_scale_column_step_rowsource_table)) /\ exists ff_q_pvs_column_step_rowsource_tableentrypositive. dst_positive_code_column_step_rowsource_table = ff_q_pvs_column_step_rowsource_tableentrypositive * S ((S (dst_index_column_step_rowsource_table)) * dst_positive_scale_column_step_rowsource_table) + (dst_positive_column_step_rowsource_table))) /\ (((((exists ff_h_pvs_column_step_rowsource_tableentrynegative. ff_h_pvs_column_step_rowsource_tableentrynegative + S (dst_negative_column_step_rowsource_table) = S ((S (dst_index_column_step_rowsource_table)) * dst_negative_scale_column_step_rowsource_table)) /\ exists ff_q_pvs_column_step_rowsource_tableentrynegative. dst_negative_code_column_step_rowsource_table = ff_q_pvs_column_step_rowsource_tableentrynegative * S ((S (dst_index_column_step_rowsource_table)) * dst_negative_scale_column_step_rowsource_table) + (dst_negative_column_step_rowsource_table))) /\ (exists ge_balance_positive_column_step_rowsource_tableentryvalue ge_balance_negative_column_step_rowsource_tableentryvalue. (((((dst_value_column_step_rowsource_table) = 2 * (ge_balance_positive_column_step_rowsource_tableentryvalue) /\ (ge_balance_negative_column_step_rowsource_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_rowsource_tableentryvaluedecode. (((dst_value_column_step_rowsource_table) = 2 * ge_signed_half_column_step_rowsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_rowsource_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_rowsource_tableentryvalue) = S ge_signed_half_column_step_rowsource_tableentryvaluedecode))) /\ ((dst_positive_column_step_rowsource_table) + ge_balance_negative_column_step_rowsource_tableentryvalue = (dst_negative_column_step_rowsource_table) + ge_balance_positive_column_step_rowsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_step_rowoutput_table dst_positive_scale_column_step_rowoutput_table dst_negative_code_column_step_rowoutput_table dst_negative_scale_column_step_rowoutput_table. (((V) = (((((dst_positive_code_column_step_rowoutput_table) + (dst_positive_scale_column_step_rowoutput_table)) * S ((dst_positive_code_column_step_rowoutput_table) + (dst_positive_scale_column_step_rowoutput_table)) + ((dst_positive_scale_column_step_rowoutput_table) + (dst_positive_scale_column_step_rowoutput_table))) + (((dst_negative_code_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)) * S ((dst_negative_code_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)) + ((dst_negative_scale_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)))) * S ((((dst_positive_code_column_step_rowoutput_table) + (dst_positive_scale_column_step_rowoutput_table)) * S ((dst_positive_code_column_step_rowoutput_table) + (dst_positive_scale_column_step_rowoutput_table)) + ((dst_positive_scale_column_step_rowoutput_table) + (dst_positive_scale_column_step_rowoutput_table))) + (((dst_negative_code_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)) * S ((dst_negative_code_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)) + ((dst_negative_scale_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)))) + ((((dst_negative_code_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)) * S ((dst_negative_code_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)) + ((dst_negative_scale_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table))) + (((dst_negative_code_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)) * S ((dst_negative_code_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)) + ((dst_negative_scale_column_step_rowoutput_table) + (dst_negative_scale_column_step_rowoutput_table)))))) /\ (forall dst_index_column_step_rowoutput_table. (exists pvs_le_gap_column_step_rowoutput_tabledomain. pvs_le_gap_column_step_rowoutput_tabledomain + (dst_index_column_step_rowoutput_table) = (n)) -> exists dst_positive_column_step_rowoutput_table dst_negative_column_step_rowoutput_table dst_value_column_step_rowoutput_table. ((((exists ff_h_pvs_column_step_rowoutput_tableentrypositive. ff_h_pvs_column_step_rowoutput_tableentrypositive + S (dst_positive_column_step_rowoutput_table) = S ((S (dst_index_column_step_rowoutput_table)) * dst_positive_scale_column_step_rowoutput_table)) /\ exists ff_q_pvs_column_step_rowoutput_tableentrypositive. dst_positive_code_column_step_rowoutput_table = ff_q_pvs_column_step_rowoutput_tableentrypositive * S ((S (dst_index_column_step_rowoutput_table)) * dst_positive_scale_column_step_rowoutput_table) + (dst_positive_column_step_rowoutput_table))) /\ (((((exists ff_h_pvs_column_step_rowoutput_tableentrynegative. ff_h_pvs_column_step_rowoutput_tableentrynegative + S (dst_negative_column_step_rowoutput_table) = S ((S (dst_index_column_step_rowoutput_table)) * dst_negative_scale_column_step_rowoutput_table)) /\ exists ff_q_pvs_column_step_rowoutput_tableentrynegative. dst_negative_code_column_step_rowoutput_table = ff_q_pvs_column_step_rowoutput_tableentrynegative * S ((S (dst_index_column_step_rowoutput_table)) * dst_negative_scale_column_step_rowoutput_table) + (dst_negative_column_step_rowoutput_table))) /\ (exists ge_balance_positive_column_step_rowoutput_tableentryvalue ge_balance_negative_column_step_rowoutput_tableentryvalue. (((((dst_value_column_step_rowoutput_table) = 2 * (ge_balance_positive_column_step_rowoutput_tableentryvalue) /\ (ge_balance_negative_column_step_rowoutput_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_rowoutput_tableentryvaluedecode. (((dst_value_column_step_rowoutput_table) = 2 * ge_signed_half_column_step_rowoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_rowoutput_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_rowoutput_tableentryvalue) = S ge_signed_half_column_step_rowoutput_tableentryvaluedecode))) /\ ((dst_positive_column_step_rowoutput_table) + ge_balance_negative_column_step_rowoutput_tableentryvalue = (dst_negative_column_step_rowoutput_table) + ge_balance_positive_column_step_rowoutput_tableentryvalue))))))))) /\ (forall srs_index_column_step_row. (exists pvs_gap_column_step_rowbound. pvs_gap_column_step_rowbound + S (srs_index_column_step_row) = (n)) -> exists srs_value_column_step_row. (((exists dst_positive_code_column_step_rowentrysource dst_positive_scale_column_step_rowentrysource dst_negative_code_column_step_rowentrysource dst_negative_scale_column_step_rowentrysource dst_positive_column_step_rowentrysource dst_negative_column_step_rowentrysource. (((F) = (((((dst_positive_code_column_step_rowentrysource) + (dst_positive_scale_column_step_rowentrysource)) * S ((dst_positive_code_column_step_rowentrysource) + (dst_positive_scale_column_step_rowentrysource)) + ((dst_positive_scale_column_step_rowentrysource) + (dst_positive_scale_column_step_rowentrysource))) + (((dst_negative_code_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)) * S ((dst_negative_code_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)) + ((dst_negative_scale_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)))) * S ((((dst_positive_code_column_step_rowentrysource) + (dst_positive_scale_column_step_rowentrysource)) * S ((dst_positive_code_column_step_rowentrysource) + (dst_positive_scale_column_step_rowentrysource)) + ((dst_positive_scale_column_step_rowentrysource) + (dst_positive_scale_column_step_rowentrysource))) + (((dst_negative_code_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)) * S ((dst_negative_code_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)) + ((dst_negative_scale_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)))) + ((((dst_negative_code_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)) * S ((dst_negative_code_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)) + ((dst_negative_scale_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource))) + (((dst_negative_code_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)) * S ((dst_negative_code_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)) + ((dst_negative_scale_column_step_rowentrysource) + (dst_negative_scale_column_step_rowentrysource)))))) /\ (((((exists ff_h_pvs_column_step_rowentrysourcepositive. ff_h_pvs_column_step_rowentrysourcepositive + S (dst_positive_column_step_rowentrysource) = S ((S (((((o) + ((s) * (m)))) + ((t) * (srs_index_column_step_row))))) * dst_positive_scale_column_step_rowentrysource)) /\ exists ff_q_pvs_column_step_rowentrysourcepositive. dst_positive_code_column_step_rowentrysource = ff_q_pvs_column_step_rowentrysourcepositive * S ((S (((((o) + ((s) * (m)))) + ((t) * (srs_index_column_step_row))))) * dst_positive_scale_column_step_rowentrysource) + (dst_positive_column_step_rowentrysource))) /\ (((((exists ff_h_pvs_column_step_rowentrysourcenegative. ff_h_pvs_column_step_rowentrysourcenegative + S (dst_negative_column_step_rowentrysource) = S ((S (((((o) + ((s) * (m)))) + ((t) * (srs_index_column_step_row))))) * dst_negative_scale_column_step_rowentrysource)) /\ exists ff_q_pvs_column_step_rowentrysourcenegative. dst_negative_code_column_step_rowentrysource = ff_q_pvs_column_step_rowentrysourcenegative * S ((S (((((o) + ((s) * (m)))) + ((t) * (srs_index_column_step_row))))) * dst_negative_scale_column_step_rowentrysource) + (dst_negative_column_step_rowentrysource))) /\ (exists ge_balance_positive_column_step_rowentrysourcevalue ge_balance_negative_column_step_rowentrysourcevalue. (((((srs_value_column_step_row) = 2 * (ge_balance_positive_column_step_rowentrysourcevalue) /\ (ge_balance_negative_column_step_rowentrysourcevalue) = 0) \/ exists ge_signed_half_column_step_rowentrysourcevaluedecode. (((srs_value_column_step_row) = 2 * ge_signed_half_column_step_rowentrysourcevaluedecode + 1 /\ (ge_balance_positive_column_step_rowentrysourcevalue) = 0) /\ (ge_balance_negative_column_step_rowentrysourcevalue) = S ge_signed_half_column_step_rowentrysourcevaluedecode))) /\ ((dst_positive_column_step_rowentrysource) + ge_balance_negative_column_step_rowentrysourcevalue = (dst_negative_column_step_rowentrysource) + ge_balance_positive_column_step_rowentrysourcevalue))))))))) /\ (exists dst_positive_code_column_step_rowentryoutput dst_positive_scale_column_step_rowentryoutput dst_negative_code_column_step_rowentryoutput dst_negative_scale_column_step_rowentryoutput dst_positive_column_step_rowentryoutput dst_negative_column_step_rowentryoutput. (((V) = (((((dst_positive_code_column_step_rowentryoutput) + (dst_positive_scale_column_step_rowentryoutput)) * S ((dst_positive_code_column_step_rowentryoutput) + (dst_positive_scale_column_step_rowentryoutput)) + ((dst_positive_scale_column_step_rowentryoutput) + (dst_positive_scale_column_step_rowentryoutput))) + (((dst_negative_code_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)) * S ((dst_negative_code_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)) + ((dst_negative_scale_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)))) * S ((((dst_positive_code_column_step_rowentryoutput) + (dst_positive_scale_column_step_rowentryoutput)) * S ((dst_positive_code_column_step_rowentryoutput) + (dst_positive_scale_column_step_rowentryoutput)) + ((dst_positive_scale_column_step_rowentryoutput) + (dst_positive_scale_column_step_rowentryoutput))) + (((dst_negative_code_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)) * S ((dst_negative_code_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)) + ((dst_negative_scale_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)))) + ((((dst_negative_code_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)) * S ((dst_negative_code_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)) + ((dst_negative_scale_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput))) + (((dst_negative_code_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)) * S ((dst_negative_code_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)) + ((dst_negative_scale_column_step_rowentryoutput) + (dst_negative_scale_column_step_rowentryoutput)))))) /\ (((((exists ff_h_pvs_column_step_rowentryoutputpositive. ff_h_pvs_column_step_rowentryoutputpositive + S (dst_positive_column_step_rowentryoutput) = S ((S (srs_index_column_step_row)) * dst_positive_scale_column_step_rowentryoutput)) /\ exists ff_q_pvs_column_step_rowentryoutputpositive. dst_positive_code_column_step_rowentryoutput = ff_q_pvs_column_step_rowentryoutputpositive * S ((S (srs_index_column_step_row)) * dst_positive_scale_column_step_rowentryoutput) + (dst_positive_column_step_rowentryoutput))) /\ (((((exists ff_h_pvs_column_step_rowentryoutputnegative. ff_h_pvs_column_step_rowentryoutputnegative + S (dst_negative_column_step_rowentryoutput) = S ((S (srs_index_column_step_row)) * dst_negative_scale_column_step_rowentryoutput)) /\ exists ff_q_pvs_column_step_rowentryoutputnegative. dst_negative_code_column_step_rowentryoutput = ff_q_pvs_column_step_rowentryoutputnegative * S ((S (srs_index_column_step_row)) * dst_negative_scale_column_step_rowentryoutput) + (dst_negative_column_step_rowentryoutput))) /\ (exists ge_balance_positive_column_step_rowentryoutputvalue ge_balance_negative_column_step_rowentryoutputvalue. (((((srs_value_column_step_row) = 2 * (ge_balance_positive_column_step_rowentryoutputvalue) /\ (ge_balance_negative_column_step_rowentryoutputvalue) = 0) \/ exists ge_signed_half_column_step_rowentryoutputvaluedecode. (((srs_value_column_step_row) = 2 * ge_signed_half_column_step_rowentryoutputvaluedecode + 1 /\ (ge_balance_positive_column_step_rowentryoutputvalue) = 0) /\ (ge_balance_negative_column_step_rowentryoutputvalue) = S ge_signed_half_column_step_rowentryoutputvaluedecode))) /\ ((dst_positive_column_step_rowentryoutput) + ge_balance_negative_column_step_rowentryoutputvalue = (dst_negative_column_step_rowentryoutput) + ge_balance_positive_column_step_rowentryoutputvalue)))))))))))))))) -> (((exists dst_positive_code_column_step_aftersource_table dst_positive_scale_column_step_aftersource_table dst_negative_code_column_step_aftersource_table dst_negative_scale_column_step_aftersource_table. (((F) = (((((dst_positive_code_column_step_aftersource_table) + (dst_positive_scale_column_step_aftersource_table)) * S ((dst_positive_code_column_step_aftersource_table) + (dst_positive_scale_column_step_aftersource_table)) + ((dst_positive_scale_column_step_aftersource_table) + (dst_positive_scale_column_step_aftersource_table))) + (((dst_negative_code_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)) * S ((dst_negative_code_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)) + ((dst_negative_scale_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)))) * S ((((dst_positive_code_column_step_aftersource_table) + (dst_positive_scale_column_step_aftersource_table)) * S ((dst_positive_code_column_step_aftersource_table) + (dst_positive_scale_column_step_aftersource_table)) + ((dst_positive_scale_column_step_aftersource_table) + (dst_positive_scale_column_step_aftersource_table))) + (((dst_negative_code_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)) * S ((dst_negative_code_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)) + ((dst_negative_scale_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)))) + ((((dst_negative_code_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)) * S ((dst_negative_code_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)) + ((dst_negative_scale_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table))) + (((dst_negative_code_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)) * S ((dst_negative_code_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)) + ((dst_negative_scale_column_step_aftersource_table) + (dst_negative_scale_column_step_aftersource_table)))))) /\ (forall dst_index_column_step_aftersource_table. (exists pvs_le_gap_column_step_aftersource_tabledomain. pvs_le_gap_column_step_aftersource_tabledomain + (dst_index_column_step_aftersource_table) = (0)) -> exists dst_positive_column_step_aftersource_table dst_negative_column_step_aftersource_table dst_value_column_step_aftersource_table. ((((exists ff_h_pvs_column_step_aftersource_tableentrypositive. ff_h_pvs_column_step_aftersource_tableentrypositive + S (dst_positive_column_step_aftersource_table) = S ((S (dst_index_column_step_aftersource_table)) * dst_positive_scale_column_step_aftersource_table)) /\ exists ff_q_pvs_column_step_aftersource_tableentrypositive. dst_positive_code_column_step_aftersource_table = ff_q_pvs_column_step_aftersource_tableentrypositive * S ((S (dst_index_column_step_aftersource_table)) * dst_positive_scale_column_step_aftersource_table) + (dst_positive_column_step_aftersource_table))) /\ (((((exists ff_h_pvs_column_step_aftersource_tableentrynegative. ff_h_pvs_column_step_aftersource_tableentrynegative + S (dst_negative_column_step_aftersource_table) = S ((S (dst_index_column_step_aftersource_table)) * dst_negative_scale_column_step_aftersource_table)) /\ exists ff_q_pvs_column_step_aftersource_tableentrynegative. dst_negative_code_column_step_aftersource_table = ff_q_pvs_column_step_aftersource_tableentrynegative * S ((S (dst_index_column_step_aftersource_table)) * dst_negative_scale_column_step_aftersource_table) + (dst_negative_column_step_aftersource_table))) /\ (exists ge_balance_positive_column_step_aftersource_tableentryvalue ge_balance_negative_column_step_aftersource_tableentryvalue. (((((dst_value_column_step_aftersource_table) = 2 * (ge_balance_positive_column_step_aftersource_tableentryvalue) /\ (ge_balance_negative_column_step_aftersource_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_aftersource_tableentryvaluedecode. (((dst_value_column_step_aftersource_table) = 2 * ge_signed_half_column_step_aftersource_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_aftersource_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_aftersource_tableentryvalue) = S ge_signed_half_column_step_aftersource_tableentryvaluedecode))) /\ ((dst_positive_column_step_aftersource_table) + ge_balance_negative_column_step_aftersource_tableentryvalue = (dst_negative_column_step_aftersource_table) + ge_balance_positive_column_step_aftersource_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_step_afterrow_table dst_positive_scale_column_step_afterrow_table dst_negative_code_column_step_afterrow_table dst_negative_scale_column_step_afterrow_table. (((D) = (((((dst_positive_code_column_step_afterrow_table) + (dst_positive_scale_column_step_afterrow_table)) * S ((dst_positive_code_column_step_afterrow_table) + (dst_positive_scale_column_step_afterrow_table)) + ((dst_positive_scale_column_step_afterrow_table) + (dst_positive_scale_column_step_afterrow_table))) + (((dst_negative_code_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)) * S ((dst_negative_code_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)) + ((dst_negative_scale_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)))) * S ((((dst_positive_code_column_step_afterrow_table) + (dst_positive_scale_column_step_afterrow_table)) * S ((dst_positive_code_column_step_afterrow_table) + (dst_positive_scale_column_step_afterrow_table)) + ((dst_positive_scale_column_step_afterrow_table) + (dst_positive_scale_column_step_afterrow_table))) + (((dst_negative_code_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)) * S ((dst_negative_code_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)) + ((dst_negative_scale_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)))) + ((((dst_negative_code_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)) * S ((dst_negative_code_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)) + ((dst_negative_scale_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table))) + (((dst_negative_code_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)) * S ((dst_negative_code_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)) + ((dst_negative_scale_column_step_afterrow_table) + (dst_negative_scale_column_step_afterrow_table)))))) /\ (forall dst_index_column_step_afterrow_table. (exists pvs_le_gap_column_step_afterrow_tabledomain. pvs_le_gap_column_step_afterrow_tabledomain + (dst_index_column_step_afterrow_table) = (n)) -> exists dst_positive_column_step_afterrow_table dst_negative_column_step_afterrow_table dst_value_column_step_afterrow_table. ((((exists ff_h_pvs_column_step_afterrow_tableentrypositive. ff_h_pvs_column_step_afterrow_tableentrypositive + S (dst_positive_column_step_afterrow_table) = S ((S (dst_index_column_step_afterrow_table)) * dst_positive_scale_column_step_afterrow_table)) /\ exists ff_q_pvs_column_step_afterrow_tableentrypositive. dst_positive_code_column_step_afterrow_table = ff_q_pvs_column_step_afterrow_tableentrypositive * S ((S (dst_index_column_step_afterrow_table)) * dst_positive_scale_column_step_afterrow_table) + (dst_positive_column_step_afterrow_table))) /\ (((((exists ff_h_pvs_column_step_afterrow_tableentrynegative. ff_h_pvs_column_step_afterrow_tableentrynegative + S (dst_negative_column_step_afterrow_table) = S ((S (dst_index_column_step_afterrow_table)) * dst_negative_scale_column_step_afterrow_table)) /\ exists ff_q_pvs_column_step_afterrow_tableentrynegative. dst_negative_code_column_step_afterrow_table = ff_q_pvs_column_step_afterrow_tableentrynegative * S ((S (dst_index_column_step_afterrow_table)) * dst_negative_scale_column_step_afterrow_table) + (dst_negative_column_step_afterrow_table))) /\ (exists ge_balance_positive_column_step_afterrow_tableentryvalue ge_balance_negative_column_step_afterrow_tableentryvalue. (((((dst_value_column_step_afterrow_table) = 2 * (ge_balance_positive_column_step_afterrow_tableentryvalue) /\ (ge_balance_negative_column_step_afterrow_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_afterrow_tableentryvaluedecode. (((dst_value_column_step_afterrow_table) = 2 * ge_signed_half_column_step_afterrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_afterrow_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_afterrow_tableentryvalue) = S ge_signed_half_column_step_afterrow_tableentryvaluedecode))) /\ ((dst_positive_column_step_afterrow_table) + ge_balance_negative_column_step_afterrow_tableentryvalue = (dst_negative_column_step_afterrow_table) + ge_balance_positive_column_step_afterrow_tableentryvalue))))))))) /\ (forall srt_index_column_step_after. (exists pvs_gap_column_step_afterbound. pvs_gap_column_step_afterbound + S (srt_index_column_step_after) = (n)) -> exists srt_value_column_step_after. (((exists dst_positive_code_column_step_afterrowentry dst_positive_scale_column_step_afterrowentry dst_negative_code_column_step_afterrowentry dst_negative_scale_column_step_afterrowentry dst_positive_column_step_afterrowentry dst_negative_column_step_afterrowentry. (((D) = (((((dst_positive_code_column_step_afterrowentry) + (dst_positive_scale_column_step_afterrowentry)) * S ((dst_positive_code_column_step_afterrowentry) + (dst_positive_scale_column_step_afterrowentry)) + ((dst_positive_scale_column_step_afterrowentry) + (dst_positive_scale_column_step_afterrowentry))) + (((dst_negative_code_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)) * S ((dst_negative_code_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)) + ((dst_negative_scale_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)))) * S ((((dst_positive_code_column_step_afterrowentry) + (dst_positive_scale_column_step_afterrowentry)) * S ((dst_positive_code_column_step_afterrowentry) + (dst_positive_scale_column_step_afterrowentry)) + ((dst_positive_scale_column_step_afterrowentry) + (dst_positive_scale_column_step_afterrowentry))) + (((dst_negative_code_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)) * S ((dst_negative_code_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)) + ((dst_negative_scale_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)))) + ((((dst_negative_code_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)) * S ((dst_negative_code_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)) + ((dst_negative_scale_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry))) + (((dst_negative_code_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)) * S ((dst_negative_code_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)) + ((dst_negative_scale_column_step_afterrowentry) + (dst_negative_scale_column_step_afterrowentry)))))) /\ (((((exists ff_h_pvs_column_step_afterrowentrypositive. ff_h_pvs_column_step_afterrowentrypositive + S (dst_positive_column_step_afterrowentry) = S ((S (srt_index_column_step_after)) * dst_positive_scale_column_step_afterrowentry)) /\ exists ff_q_pvs_column_step_afterrowentrypositive. dst_positive_code_column_step_afterrowentry = ff_q_pvs_column_step_afterrowentrypositive * S ((S (srt_index_column_step_after)) * dst_positive_scale_column_step_afterrowentry) + (dst_positive_column_step_afterrowentry))) /\ (((((exists ff_h_pvs_column_step_afterrowentrynegative. ff_h_pvs_column_step_afterrowentrynegative + S (dst_negative_column_step_afterrowentry) = S ((S (srt_index_column_step_after)) * dst_negative_scale_column_step_afterrowentry)) /\ exists ff_q_pvs_column_step_afterrowentrynegative. dst_negative_code_column_step_afterrowentry = ff_q_pvs_column_step_afterrowentrynegative * S ((S (srt_index_column_step_after)) * dst_negative_scale_column_step_afterrowentry) + (dst_negative_column_step_afterrowentry))) /\ (exists ge_balance_positive_column_step_afterrowentryvalue ge_balance_negative_column_step_afterrowentryvalue. (((((srt_value_column_step_after) = 2 * (ge_balance_positive_column_step_afterrowentryvalue) /\ (ge_balance_negative_column_step_afterrowentryvalue) = 0) \/ exists ge_signed_half_column_step_afterrowentryvaluedecode. (((srt_value_column_step_after) = 2 * ge_signed_half_column_step_afterrowentryvaluedecode + 1 /\ (ge_balance_positive_column_step_afterrowentryvalue) = 0) /\ (ge_balance_negative_column_step_afterrowentryvalue) = S ge_signed_half_column_step_afterrowentryvaluedecode))) /\ ((dst_positive_column_step_afterrowentry) + ge_balance_negative_column_step_afterrowentryvalue = (dst_negative_column_step_afterrowentry) + ge_balance_positive_column_step_afterrowentryvalue))))))))) /\ (exists srs_slice_column_step_afterrowrow_sum. ((((exists dst_positive_code_column_step_afterrowrow_sumslicesource_table dst_positive_scale_column_step_afterrowrow_sumslicesource_table dst_negative_code_column_step_afterrowrow_sumslicesource_table dst_negative_scale_column_step_afterrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_column_step_afterrowrow_sumslicesource_table) + (dst_positive_scale_column_step_afterrowrow_sumslicesource_table)) * S ((dst_positive_code_column_step_afterrowrow_sumslicesource_table) + (dst_positive_scale_column_step_afterrowrow_sumslicesource_table)) + ((dst_positive_scale_column_step_afterrowrow_sumslicesource_table) + (dst_positive_scale_column_step_afterrowrow_sumslicesource_table))) + (((dst_negative_code_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)) * S ((dst_negative_code_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)) + ((dst_negative_scale_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)))) * S ((((dst_positive_code_column_step_afterrowrow_sumslicesource_table) + (dst_positive_scale_column_step_afterrowrow_sumslicesource_table)) * S ((dst_positive_code_column_step_afterrowrow_sumslicesource_table) + (dst_positive_scale_column_step_afterrowrow_sumslicesource_table)) + ((dst_positive_scale_column_step_afterrowrow_sumslicesource_table) + (dst_positive_scale_column_step_afterrowrow_sumslicesource_table))) + (((dst_negative_code_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)) * S ((dst_negative_code_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)) + ((dst_negative_scale_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)))) + ((((dst_negative_code_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)) * S ((dst_negative_code_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)) + ((dst_negative_scale_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table))) + (((dst_negative_code_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)) * S ((dst_negative_code_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)) + ((dst_negative_scale_column_step_afterrowrow_sumslicesource_table) + (dst_negative_scale_column_step_afterrowrow_sumslicesource_table)))))) /\ (forall dst_index_column_step_afterrowrow_sumslicesource_table. (exists pvs_le_gap_column_step_afterrowrow_sumslicesource_tabledomain. pvs_le_gap_column_step_afterrowrow_sumslicesource_tabledomain + (dst_index_column_step_afterrowrow_sumslicesource_table) = (0)) -> exists dst_positive_column_step_afterrowrow_sumslicesource_table dst_negative_column_step_afterrowrow_sumslicesource_table dst_value_column_step_afterrowrow_sumslicesource_table. ((((exists ff_h_pvs_column_step_afterrowrow_sumslicesource_tableentrypositive. ff_h_pvs_column_step_afterrowrow_sumslicesource_tableentrypositive + S (dst_positive_column_step_afterrowrow_sumslicesource_table) = S ((S (dst_index_column_step_afterrowrow_sumslicesource_table)) * dst_positive_scale_column_step_afterrowrow_sumslicesource_table)) /\ exists ff_q_pvs_column_step_afterrowrow_sumslicesource_tableentrypositive. dst_positive_code_column_step_afterrowrow_sumslicesource_table = ff_q_pvs_column_step_afterrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_column_step_afterrowrow_sumslicesource_table)) * dst_positive_scale_column_step_afterrowrow_sumslicesource_table) + (dst_positive_column_step_afterrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_column_step_afterrowrow_sumslicesource_tableentrynegative. ff_h_pvs_column_step_afterrowrow_sumslicesource_tableentrynegative + S (dst_negative_column_step_afterrowrow_sumslicesource_table) = S ((S (dst_index_column_step_afterrowrow_sumslicesource_table)) * dst_negative_scale_column_step_afterrowrow_sumslicesource_table)) /\ exists ff_q_pvs_column_step_afterrowrow_sumslicesource_tableentrynegative. dst_negative_code_column_step_afterrowrow_sumslicesource_table = ff_q_pvs_column_step_afterrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_column_step_afterrowrow_sumslicesource_table)) * dst_negative_scale_column_step_afterrowrow_sumslicesource_table) + (dst_negative_column_step_afterrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_column_step_afterrowrow_sumslicesource_tableentryvalue ge_balance_negative_column_step_afterrowrow_sumslicesource_tableentryvalue. (((((dst_value_column_step_afterrowrow_sumslicesource_table) = 2 * (ge_balance_positive_column_step_afterrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_column_step_afterrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_afterrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_column_step_afterrowrow_sumslicesource_table) = 2 * ge_signed_half_column_step_afterrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_afterrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_afterrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_column_step_afterrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_column_step_afterrowrow_sumslicesource_table) + ge_balance_negative_column_step_afterrowrow_sumslicesource_tableentryvalue = (dst_negative_column_step_afterrowrow_sumslicesource_table) + ge_balance_positive_column_step_afterrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_step_afterrowrow_sumsliceoutput_table dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table dst_negative_code_column_step_afterrowrow_sumsliceoutput_table dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table. (((srs_slice_column_step_afterrowrow_sum) = (((((dst_positive_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table)) * S ((dst_positive_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table)) + ((dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table))) + (((dst_negative_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table)) * S ((dst_positive_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table)) + ((dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table) + (dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table))) + (((dst_negative_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table))) + (((dst_negative_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_column_step_afterrowrow_sumsliceoutput_table. (exists pvs_le_gap_column_step_afterrowrow_sumsliceoutput_tabledomain. pvs_le_gap_column_step_afterrowrow_sumsliceoutput_tabledomain + (dst_index_column_step_afterrowrow_sumsliceoutput_table) = (S m)) -> exists dst_positive_column_step_afterrowrow_sumsliceoutput_table dst_negative_column_step_afterrowrow_sumsliceoutput_table dst_value_column_step_afterrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_column_step_afterrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_column_step_afterrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_column_step_afterrowrow_sumsliceoutput_table) = S ((S (dst_index_column_step_afterrowrow_sumsliceoutput_table)) * dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_column_step_afterrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_column_step_afterrowrow_sumsliceoutput_table = ff_q_pvs_column_step_afterrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_column_step_afterrowrow_sumsliceoutput_table)) * dst_positive_scale_column_step_afterrowrow_sumsliceoutput_table) + (dst_positive_column_step_afterrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_column_step_afterrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_column_step_afterrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_column_step_afterrowrow_sumsliceoutput_table) = S ((S (dst_index_column_step_afterrowrow_sumsliceoutput_table)) * dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_column_step_afterrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_column_step_afterrowrow_sumsliceoutput_table = ff_q_pvs_column_step_afterrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_column_step_afterrowrow_sumsliceoutput_table)) * dst_negative_scale_column_step_afterrowrow_sumsliceoutput_table) + (dst_negative_column_step_afterrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_column_step_afterrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_column_step_afterrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_column_step_afterrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_column_step_afterrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_column_step_afterrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_afterrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_column_step_afterrowrow_sumsliceoutput_table) = 2 * ge_signed_half_column_step_afterrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_afterrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_afterrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_column_step_afterrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_column_step_afterrowrow_sumsliceoutput_table) + ge_balance_negative_column_step_afterrowrow_sumsliceoutput_tableentryvalue = (dst_negative_column_step_afterrowrow_sumsliceoutput_table) + ge_balance_positive_column_step_afterrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_column_step_afterrowrow_sumslice. (exists pvs_gap_column_step_afterrowrow_sumslicebound. pvs_gap_column_step_afterrowrow_sumslicebound + S (srs_index_column_step_afterrowrow_sumslice) = (S m)) -> exists srs_value_column_step_afterrowrow_sumslice. (((exists dst_positive_code_column_step_afterrowrow_sumsliceentrysource dst_positive_scale_column_step_afterrowrow_sumsliceentrysource dst_negative_code_column_step_afterrowrow_sumsliceentrysource dst_negative_scale_column_step_afterrowrow_sumsliceentrysource dst_positive_column_step_afterrowrow_sumsliceentrysource dst_negative_column_step_afterrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_column_step_afterrowrow_sumsliceentrysource) + (dst_positive_scale_column_step_afterrowrow_sumsliceentrysource)) * S ((dst_positive_code_column_step_afterrowrow_sumsliceentrysource) + (dst_positive_scale_column_step_afterrowrow_sumsliceentrysource)) + ((dst_positive_scale_column_step_afterrowrow_sumsliceentrysource) + (dst_positive_scale_column_step_afterrowrow_sumsliceentrysource))) + (((dst_negative_code_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_column_step_afterrowrow_sumsliceentrysource) + (dst_positive_scale_column_step_afterrowrow_sumsliceentrysource)) * S ((dst_positive_code_column_step_afterrowrow_sumsliceentrysource) + (dst_positive_scale_column_step_afterrowrow_sumsliceentrysource)) + ((dst_positive_scale_column_step_afterrowrow_sumsliceentrysource) + (dst_positive_scale_column_step_afterrowrow_sumsliceentrysource))) + (((dst_negative_code_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)))) + ((((dst_negative_code_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource))) + (((dst_negative_code_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_column_step_afterrowrow_sumsliceentrysourcepositive. ff_h_pvs_column_step_afterrowrow_sumsliceentrysourcepositive + S (dst_positive_column_step_afterrowrow_sumsliceentrysource) = S ((S (((((o) + ((t) * (srt_index_column_step_after)))) + ((s) * (srs_index_column_step_afterrowrow_sumslice))))) * dst_positive_scale_column_step_afterrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_column_step_afterrowrow_sumsliceentrysourcepositive. dst_positive_code_column_step_afterrowrow_sumsliceentrysource = ff_q_pvs_column_step_afterrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((t) * (srt_index_column_step_after)))) + ((s) * (srs_index_column_step_afterrowrow_sumslice))))) * dst_positive_scale_column_step_afterrowrow_sumsliceentrysource) + (dst_positive_column_step_afterrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_column_step_afterrowrow_sumsliceentrysourcenegative. ff_h_pvs_column_step_afterrowrow_sumsliceentrysourcenegative + S (dst_negative_column_step_afterrowrow_sumsliceentrysource) = S ((S (((((o) + ((t) * (srt_index_column_step_after)))) + ((s) * (srs_index_column_step_afterrowrow_sumslice))))) * dst_negative_scale_column_step_afterrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_column_step_afterrowrow_sumsliceentrysourcenegative. dst_negative_code_column_step_afterrowrow_sumsliceentrysource = ff_q_pvs_column_step_afterrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((t) * (srt_index_column_step_after)))) + ((s) * (srs_index_column_step_afterrowrow_sumslice))))) * dst_negative_scale_column_step_afterrowrow_sumsliceentrysource) + (dst_negative_column_step_afterrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_column_step_afterrowrow_sumsliceentrysourcevalue ge_balance_negative_column_step_afterrowrow_sumsliceentrysourcevalue. (((((srs_value_column_step_afterrowrow_sumslice) = 2 * (ge_balance_positive_column_step_afterrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_column_step_afterrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_column_step_afterrowrow_sumsliceentrysourcevaluedecode. (((srs_value_column_step_afterrowrow_sumslice) = 2 * ge_signed_half_column_step_afterrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_column_step_afterrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_column_step_afterrowrow_sumsliceentrysourcevalue) = S ge_signed_half_column_step_afterrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_column_step_afterrowrow_sumsliceentrysource) + ge_balance_negative_column_step_afterrowrow_sumsliceentrysourcevalue = (dst_negative_column_step_afterrowrow_sumsliceentrysource) + ge_balance_positive_column_step_afterrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_column_step_afterrowrow_sumsliceentryoutput dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput dst_negative_code_column_step_afterrowrow_sumsliceentryoutput dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput dst_positive_column_step_afterrowrow_sumsliceentryoutput dst_negative_column_step_afterrowrow_sumsliceentryoutput. (((srs_slice_column_step_afterrowrow_sum) = (((((dst_positive_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput)) * S ((dst_positive_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput)) + ((dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput))) + (((dst_negative_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput)) * S ((dst_positive_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput)) + ((dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput) + (dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput))) + (((dst_negative_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput))) + (((dst_negative_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_column_step_afterrowrow_sumsliceentryoutputpositive. ff_h_pvs_column_step_afterrowrow_sumsliceentryoutputpositive + S (dst_positive_column_step_afterrowrow_sumsliceentryoutput) = S ((S (srs_index_column_step_afterrowrow_sumslice)) * dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_column_step_afterrowrow_sumsliceentryoutputpositive. dst_positive_code_column_step_afterrowrow_sumsliceentryoutput = ff_q_pvs_column_step_afterrowrow_sumsliceentryoutputpositive * S ((S (srs_index_column_step_afterrowrow_sumslice)) * dst_positive_scale_column_step_afterrowrow_sumsliceentryoutput) + (dst_positive_column_step_afterrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_column_step_afterrowrow_sumsliceentryoutputnegative. ff_h_pvs_column_step_afterrowrow_sumsliceentryoutputnegative + S (dst_negative_column_step_afterrowrow_sumsliceentryoutput) = S ((S (srs_index_column_step_afterrowrow_sumslice)) * dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_column_step_afterrowrow_sumsliceentryoutputnegative. dst_negative_code_column_step_afterrowrow_sumsliceentryoutput = ff_q_pvs_column_step_afterrowrow_sumsliceentryoutputnegative * S ((S (srs_index_column_step_afterrowrow_sumslice)) * dst_negative_scale_column_step_afterrowrow_sumsliceentryoutput) + (dst_negative_column_step_afterrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_column_step_afterrowrow_sumsliceentryoutputvalue ge_balance_negative_column_step_afterrowrow_sumsliceentryoutputvalue. (((((srs_value_column_step_afterrowrow_sumslice) = 2 * (ge_balance_positive_column_step_afterrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_column_step_afterrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_column_step_afterrowrow_sumsliceentryoutputvaluedecode. (((srs_value_column_step_afterrowrow_sumslice) = 2 * ge_signed_half_column_step_afterrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_column_step_afterrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_column_step_afterrowrow_sumsliceentryoutputvalue) = S ge_signed_half_column_step_afterrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_column_step_afterrowrow_sumsliceentryoutput) + ge_balance_negative_column_step_afterrowrow_sumsliceentryoutputvalue = (dst_negative_column_step_afterrowrow_sumsliceentryoutput) + ge_balance_positive_column_step_afterrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_column_step_afterrowrow_sumsum dst_positive_scale_column_step_afterrowrow_sumsum dst_negative_code_column_step_afterrowrow_sumsum dst_negative_scale_column_step_afterrowrow_sumsum dst_positive_sum_column_step_afterrowrow_sumsum dst_negative_sum_column_step_afterrowrow_sumsum. (((srs_slice_column_step_afterrowrow_sum) = (((((dst_positive_code_column_step_afterrowrow_sumsum) + (dst_positive_scale_column_step_afterrowrow_sumsum)) * S ((dst_positive_code_column_step_afterrowrow_sumsum) + (dst_positive_scale_column_step_afterrowrow_sumsum)) + ((dst_positive_scale_column_step_afterrowrow_sumsum) + (dst_positive_scale_column_step_afterrowrow_sumsum))) + (((dst_negative_code_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)) * S ((dst_negative_code_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)) + ((dst_negative_scale_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)))) * S ((((dst_positive_code_column_step_afterrowrow_sumsum) + (dst_positive_scale_column_step_afterrowrow_sumsum)) * S ((dst_positive_code_column_step_afterrowrow_sumsum) + (dst_positive_scale_column_step_afterrowrow_sumsum)) + ((dst_positive_scale_column_step_afterrowrow_sumsum) + (dst_positive_scale_column_step_afterrowrow_sumsum))) + (((dst_negative_code_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)) * S ((dst_negative_code_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)) + ((dst_negative_scale_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)))) + ((((dst_negative_code_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)) * S ((dst_negative_code_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)) + ((dst_negative_scale_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum))) + (((dst_negative_code_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)) * S ((dst_negative_code_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)) + ((dst_negative_scale_column_step_afterrowrow_sumsum) + (dst_negative_scale_column_step_afterrowrow_sumsum)))))) /\ (((exists fs_u_dst_column_step_afterrowrow_sumsumpositive fs_v_dst_column_step_afterrowrow_sumsumpositive. ((((exists fs_h_dst_column_step_afterrowrow_sumsumpositive_body_start. fs_h_dst_column_step_afterrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_column_step_afterrowrow_sumsumpositive)) /\ exists fs_q_dst_column_step_afterrowrow_sumsumpositive_body_start. fs_u_dst_column_step_afterrowrow_sumsumpositive = fs_q_dst_column_step_afterrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_column_step_afterrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_column_step_afterrowrow_sumsumpositive_body_terminal. fs_h_dst_column_step_afterrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_column_step_afterrowrow_sumsum) = S ((S (S m)) * fs_v_dst_column_step_afterrowrow_sumsumpositive)) /\ exists fs_q_dst_column_step_afterrowrow_sumsumpositive_body_terminal. fs_u_dst_column_step_afterrowrow_sumsumpositive = fs_q_dst_column_step_afterrowrow_sumsumpositive_body_terminal * S ((S (S m)) * fs_v_dst_column_step_afterrowrow_sumsumpositive) + (dst_positive_sum_column_step_afterrowrow_sumsum))) /\ forall fs_i_dst_column_step_afterrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_column_step_afterrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_column_step_afterrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_column_step_afterrowrow_sumsumpositive_body_steps = S m) -> exists fs_a_dst_column_step_afterrowrow_sumsumpositive_body_steps fs_r_dst_column_step_afterrowrow_sumsumpositive_body_steps fs_s_dst_column_step_afterrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_column_step_afterrowrow_sumsumpositive_body_steps_summand. fs_h_dst_column_step_afterrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_column_step_afterrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_column_step_afterrowrow_sumsumpositive_body_steps)) * dst_positive_scale_column_step_afterrowrow_sumsum)) /\ exists fs_q_dst_column_step_afterrowrow_sumsumpositive_body_steps_summand. dst_positive_code_column_step_afterrowrow_sumsum = fs_q_dst_column_step_afterrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_column_step_afterrowrow_sumsumpositive_body_steps)) * dst_positive_scale_column_step_afterrowrow_sumsum) + (fs_a_dst_column_step_afterrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_column_step_afterrowrow_sumsumpositive_body_steps_partial. fs_h_dst_column_step_afterrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_column_step_afterrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_column_step_afterrowrow_sumsumpositive_body_steps)) * fs_v_dst_column_step_afterrowrow_sumsumpositive)) /\ exists fs_q_dst_column_step_afterrowrow_sumsumpositive_body_steps_partial. fs_u_dst_column_step_afterrowrow_sumsumpositive = fs_q_dst_column_step_afterrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_column_step_afterrowrow_sumsumpositive_body_steps)) * fs_v_dst_column_step_afterrowrow_sumsumpositive) + (fs_r_dst_column_step_afterrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_column_step_afterrowrow_sumsumpositive_body_steps_successor. fs_h_dst_column_step_afterrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_column_step_afterrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_column_step_afterrowrow_sumsumpositive_body_steps)) * fs_v_dst_column_step_afterrowrow_sumsumpositive)) /\ exists fs_q_dst_column_step_afterrowrow_sumsumpositive_body_steps_successor. fs_u_dst_column_step_afterrowrow_sumsumpositive = fs_q_dst_column_step_afterrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_column_step_afterrowrow_sumsumpositive_body_steps)) * fs_v_dst_column_step_afterrowrow_sumsumpositive) + (fs_s_dst_column_step_afterrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_column_step_afterrowrow_sumsumpositive_body_steps = fs_r_dst_column_step_afterrowrow_sumsumpositive_body_steps + fs_a_dst_column_step_afterrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_column_step_afterrowrow_sumsumnegative fs_v_dst_column_step_afterrowrow_sumsumnegative. ((((exists fs_h_dst_column_step_afterrowrow_sumsumnegative_body_start. fs_h_dst_column_step_afterrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_column_step_afterrowrow_sumsumnegative)) /\ exists fs_q_dst_column_step_afterrowrow_sumsumnegative_body_start. fs_u_dst_column_step_afterrowrow_sumsumnegative = fs_q_dst_column_step_afterrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_column_step_afterrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_column_step_afterrowrow_sumsumnegative_body_terminal. fs_h_dst_column_step_afterrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_column_step_afterrowrow_sumsum) = S ((S (S m)) * fs_v_dst_column_step_afterrowrow_sumsumnegative)) /\ exists fs_q_dst_column_step_afterrowrow_sumsumnegative_body_terminal. fs_u_dst_column_step_afterrowrow_sumsumnegative = fs_q_dst_column_step_afterrowrow_sumsumnegative_body_terminal * S ((S (S m)) * fs_v_dst_column_step_afterrowrow_sumsumnegative) + (dst_negative_sum_column_step_afterrowrow_sumsum))) /\ forall fs_i_dst_column_step_afterrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_column_step_afterrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_column_step_afterrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_column_step_afterrowrow_sumsumnegative_body_steps = S m) -> exists fs_a_dst_column_step_afterrowrow_sumsumnegative_body_steps fs_r_dst_column_step_afterrowrow_sumsumnegative_body_steps fs_s_dst_column_step_afterrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_column_step_afterrowrow_sumsumnegative_body_steps_summand. fs_h_dst_column_step_afterrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_column_step_afterrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_column_step_afterrowrow_sumsumnegative_body_steps)) * dst_negative_scale_column_step_afterrowrow_sumsum)) /\ exists fs_q_dst_column_step_afterrowrow_sumsumnegative_body_steps_summand. dst_negative_code_column_step_afterrowrow_sumsum = fs_q_dst_column_step_afterrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_column_step_afterrowrow_sumsumnegative_body_steps)) * dst_negative_scale_column_step_afterrowrow_sumsum) + (fs_a_dst_column_step_afterrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_column_step_afterrowrow_sumsumnegative_body_steps_partial. fs_h_dst_column_step_afterrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_column_step_afterrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_column_step_afterrowrow_sumsumnegative_body_steps)) * fs_v_dst_column_step_afterrowrow_sumsumnegative)) /\ exists fs_q_dst_column_step_afterrowrow_sumsumnegative_body_steps_partial. fs_u_dst_column_step_afterrowrow_sumsumnegative = fs_q_dst_column_step_afterrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_column_step_afterrowrow_sumsumnegative_body_steps)) * fs_v_dst_column_step_afterrowrow_sumsumnegative) + (fs_r_dst_column_step_afterrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_column_step_afterrowrow_sumsumnegative_body_steps_successor. fs_h_dst_column_step_afterrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_column_step_afterrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_column_step_afterrowrow_sumsumnegative_body_steps)) * fs_v_dst_column_step_afterrowrow_sumsumnegative)) /\ exists fs_q_dst_column_step_afterrowrow_sumsumnegative_body_steps_successor. fs_u_dst_column_step_afterrowrow_sumsumnegative = fs_q_dst_column_step_afterrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_column_step_afterrowrow_sumsumnegative_body_steps)) * fs_v_dst_column_step_afterrowrow_sumsumnegative) + (fs_s_dst_column_step_afterrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_column_step_afterrowrow_sumsumnegative_body_steps = fs_r_dst_column_step_afterrowrow_sumsumnegative_body_steps + fs_a_dst_column_step_afterrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_column_step_afterrowrow_sumsumresult ge_balance_negative_column_step_afterrowrow_sumsumresult. (((((srt_value_column_step_after) = 2 * (ge_balance_positive_column_step_afterrowrow_sumsumresult) /\ (ge_balance_negative_column_step_afterrowrow_sumsumresult) = 0) \/ exists ge_signed_half_column_step_afterrowrow_sumsumresultdecode. (((srt_value_column_step_after) = 2 * ge_signed_half_column_step_afterrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_column_step_afterrowrow_sumsumresult) = 0) /\ (ge_balance_negative_column_step_afterrowrow_sumsumresult) = S ge_signed_half_column_step_afterrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_column_step_afterrowrow_sumsum) + ge_balance_negative_column_step_afterrowrow_sumsumresult = (dst_negative_sum_column_step_afterrowrow_sumsum) + ge_balance_positive_column_step_afterrowrow_sumsumresult)))))))))))))))))) -> (((exists dst_positive_code_column_step_addleft_table dst_positive_scale_column_step_addleft_table dst_negative_code_column_step_addleft_table dst_negative_scale_column_step_addleft_table. (((C) = (((((dst_positive_code_column_step_addleft_table) + (dst_positive_scale_column_step_addleft_table)) * S ((dst_positive_code_column_step_addleft_table) + (dst_positive_scale_column_step_addleft_table)) + ((dst_positive_scale_column_step_addleft_table) + (dst_positive_scale_column_step_addleft_table))) + (((dst_negative_code_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)) * S ((dst_negative_code_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)) + ((dst_negative_scale_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)))) * S ((((dst_positive_code_column_step_addleft_table) + (dst_positive_scale_column_step_addleft_table)) * S ((dst_positive_code_column_step_addleft_table) + (dst_positive_scale_column_step_addleft_table)) + ((dst_positive_scale_column_step_addleft_table) + (dst_positive_scale_column_step_addleft_table))) + (((dst_negative_code_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)) * S ((dst_negative_code_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)) + ((dst_negative_scale_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)))) + ((((dst_negative_code_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)) * S ((dst_negative_code_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)) + ((dst_negative_scale_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table))) + (((dst_negative_code_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)) * S ((dst_negative_code_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)) + ((dst_negative_scale_column_step_addleft_table) + (dst_negative_scale_column_step_addleft_table)))))) /\ (forall dst_index_column_step_addleft_table. (exists pvs_le_gap_column_step_addleft_tabledomain. pvs_le_gap_column_step_addleft_tabledomain + (dst_index_column_step_addleft_table) = (n)) -> exists dst_positive_column_step_addleft_table dst_negative_column_step_addleft_table dst_value_column_step_addleft_table. ((((exists ff_h_pvs_column_step_addleft_tableentrypositive. ff_h_pvs_column_step_addleft_tableentrypositive + S (dst_positive_column_step_addleft_table) = S ((S (dst_index_column_step_addleft_table)) * dst_positive_scale_column_step_addleft_table)) /\ exists ff_q_pvs_column_step_addleft_tableentrypositive. dst_positive_code_column_step_addleft_table = ff_q_pvs_column_step_addleft_tableentrypositive * S ((S (dst_index_column_step_addleft_table)) * dst_positive_scale_column_step_addleft_table) + (dst_positive_column_step_addleft_table))) /\ (((((exists ff_h_pvs_column_step_addleft_tableentrynegative. ff_h_pvs_column_step_addleft_tableentrynegative + S (dst_negative_column_step_addleft_table) = S ((S (dst_index_column_step_addleft_table)) * dst_negative_scale_column_step_addleft_table)) /\ exists ff_q_pvs_column_step_addleft_tableentrynegative. dst_negative_code_column_step_addleft_table = ff_q_pvs_column_step_addleft_tableentrynegative * S ((S (dst_index_column_step_addleft_table)) * dst_negative_scale_column_step_addleft_table) + (dst_negative_column_step_addleft_table))) /\ (exists ge_balance_positive_column_step_addleft_tableentryvalue ge_balance_negative_column_step_addleft_tableentryvalue. (((((dst_value_column_step_addleft_table) = 2 * (ge_balance_positive_column_step_addleft_tableentryvalue) /\ (ge_balance_negative_column_step_addleft_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_addleft_tableentryvaluedecode. (((dst_value_column_step_addleft_table) = 2 * ge_signed_half_column_step_addleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_addleft_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_addleft_tableentryvalue) = S ge_signed_half_column_step_addleft_tableentryvaluedecode))) /\ ((dst_positive_column_step_addleft_table) + ge_balance_negative_column_step_addleft_tableentryvalue = (dst_negative_column_step_addleft_table) + ge_balance_positive_column_step_addleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_step_addright_table dst_positive_scale_column_step_addright_table dst_negative_code_column_step_addright_table dst_negative_scale_column_step_addright_table. (((V) = (((((dst_positive_code_column_step_addright_table) + (dst_positive_scale_column_step_addright_table)) * S ((dst_positive_code_column_step_addright_table) + (dst_positive_scale_column_step_addright_table)) + ((dst_positive_scale_column_step_addright_table) + (dst_positive_scale_column_step_addright_table))) + (((dst_negative_code_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)) * S ((dst_negative_code_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)) + ((dst_negative_scale_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)))) * S ((((dst_positive_code_column_step_addright_table) + (dst_positive_scale_column_step_addright_table)) * S ((dst_positive_code_column_step_addright_table) + (dst_positive_scale_column_step_addright_table)) + ((dst_positive_scale_column_step_addright_table) + (dst_positive_scale_column_step_addright_table))) + (((dst_negative_code_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)) * S ((dst_negative_code_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)) + ((dst_negative_scale_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)))) + ((((dst_negative_code_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)) * S ((dst_negative_code_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)) + ((dst_negative_scale_column_step_addright_table) + (dst_negative_scale_column_step_addright_table))) + (((dst_negative_code_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)) * S ((dst_negative_code_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)) + ((dst_negative_scale_column_step_addright_table) + (dst_negative_scale_column_step_addright_table)))))) /\ (forall dst_index_column_step_addright_table. (exists pvs_le_gap_column_step_addright_tabledomain. pvs_le_gap_column_step_addright_tabledomain + (dst_index_column_step_addright_table) = (n)) -> exists dst_positive_column_step_addright_table dst_negative_column_step_addright_table dst_value_column_step_addright_table. ((((exists ff_h_pvs_column_step_addright_tableentrypositive. ff_h_pvs_column_step_addright_tableentrypositive + S (dst_positive_column_step_addright_table) = S ((S (dst_index_column_step_addright_table)) * dst_positive_scale_column_step_addright_table)) /\ exists ff_q_pvs_column_step_addright_tableentrypositive. dst_positive_code_column_step_addright_table = ff_q_pvs_column_step_addright_tableentrypositive * S ((S (dst_index_column_step_addright_table)) * dst_positive_scale_column_step_addright_table) + (dst_positive_column_step_addright_table))) /\ (((((exists ff_h_pvs_column_step_addright_tableentrynegative. ff_h_pvs_column_step_addright_tableentrynegative + S (dst_negative_column_step_addright_table) = S ((S (dst_index_column_step_addright_table)) * dst_negative_scale_column_step_addright_table)) /\ exists ff_q_pvs_column_step_addright_tableentrynegative. dst_negative_code_column_step_addright_table = ff_q_pvs_column_step_addright_tableentrynegative * S ((S (dst_index_column_step_addright_table)) * dst_negative_scale_column_step_addright_table) + (dst_negative_column_step_addright_table))) /\ (exists ge_balance_positive_column_step_addright_tableentryvalue ge_balance_negative_column_step_addright_tableentryvalue. (((((dst_value_column_step_addright_table) = 2 * (ge_balance_positive_column_step_addright_tableentryvalue) /\ (ge_balance_negative_column_step_addright_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_addright_tableentryvaluedecode. (((dst_value_column_step_addright_table) = 2 * ge_signed_half_column_step_addright_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_addright_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_addright_tableentryvalue) = S ge_signed_half_column_step_addright_tableentryvaluedecode))) /\ ((dst_positive_column_step_addright_table) + ge_balance_negative_column_step_addright_tableentryvalue = (dst_negative_column_step_addright_table) + ge_balance_positive_column_step_addright_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_step_addoutput_table dst_positive_scale_column_step_addoutput_table dst_negative_code_column_step_addoutput_table dst_negative_scale_column_step_addoutput_table. (((D) = (((((dst_positive_code_column_step_addoutput_table) + (dst_positive_scale_column_step_addoutput_table)) * S ((dst_positive_code_column_step_addoutput_table) + (dst_positive_scale_column_step_addoutput_table)) + ((dst_positive_scale_column_step_addoutput_table) + (dst_positive_scale_column_step_addoutput_table))) + (((dst_negative_code_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)) * S ((dst_negative_code_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)) + ((dst_negative_scale_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)))) * S ((((dst_positive_code_column_step_addoutput_table) + (dst_positive_scale_column_step_addoutput_table)) * S ((dst_positive_code_column_step_addoutput_table) + (dst_positive_scale_column_step_addoutput_table)) + ((dst_positive_scale_column_step_addoutput_table) + (dst_positive_scale_column_step_addoutput_table))) + (((dst_negative_code_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)) * S ((dst_negative_code_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)) + ((dst_negative_scale_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)))) + ((((dst_negative_code_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)) * S ((dst_negative_code_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)) + ((dst_negative_scale_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table))) + (((dst_negative_code_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)) * S ((dst_negative_code_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)) + ((dst_negative_scale_column_step_addoutput_table) + (dst_negative_scale_column_step_addoutput_table)))))) /\ (forall dst_index_column_step_addoutput_table. (exists pvs_le_gap_column_step_addoutput_tabledomain. pvs_le_gap_column_step_addoutput_tabledomain + (dst_index_column_step_addoutput_table) = (n)) -> exists dst_positive_column_step_addoutput_table dst_negative_column_step_addoutput_table dst_value_column_step_addoutput_table. ((((exists ff_h_pvs_column_step_addoutput_tableentrypositive. ff_h_pvs_column_step_addoutput_tableentrypositive + S (dst_positive_column_step_addoutput_table) = S ((S (dst_index_column_step_addoutput_table)) * dst_positive_scale_column_step_addoutput_table)) /\ exists ff_q_pvs_column_step_addoutput_tableentrypositive. dst_positive_code_column_step_addoutput_table = ff_q_pvs_column_step_addoutput_tableentrypositive * S ((S (dst_index_column_step_addoutput_table)) * dst_positive_scale_column_step_addoutput_table) + (dst_positive_column_step_addoutput_table))) /\ (((((exists ff_h_pvs_column_step_addoutput_tableentrynegative. ff_h_pvs_column_step_addoutput_tableentrynegative + S (dst_negative_column_step_addoutput_table) = S ((S (dst_index_column_step_addoutput_table)) * dst_negative_scale_column_step_addoutput_table)) /\ exists ff_q_pvs_column_step_addoutput_tableentrynegative. dst_negative_code_column_step_addoutput_table = ff_q_pvs_column_step_addoutput_tableentrynegative * S ((S (dst_index_column_step_addoutput_table)) * dst_negative_scale_column_step_addoutput_table) + (dst_negative_column_step_addoutput_table))) /\ (exists ge_balance_positive_column_step_addoutput_tableentryvalue ge_balance_negative_column_step_addoutput_tableentryvalue. (((((dst_value_column_step_addoutput_table) = 2 * (ge_balance_positive_column_step_addoutput_tableentryvalue) /\ (ge_balance_negative_column_step_addoutput_tableentryvalue) = 0) \/ exists ge_signed_half_column_step_addoutput_tableentryvaluedecode. (((dst_value_column_step_addoutput_table) = 2 * ge_signed_half_column_step_addoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_step_addoutput_tableentryvalue) = 0) /\ (ge_balance_negative_column_step_addoutput_tableentryvalue) = S ge_signed_half_column_step_addoutput_tableentryvaluedecode))) /\ ((dst_positive_column_step_addoutput_table) + ge_balance_negative_column_step_addoutput_tableentryvalue = (dst_negative_column_step_addoutput_table) + ge_balance_positive_column_step_addoutput_tableentryvalue))))))))) /\ (forall sto_index_column_step_addentries. (exists pvs_gap_column_step_addentriesbound. pvs_gap_column_step_addentriesbound + S (sto_index_column_step_addentries) = (n)) -> exists sto_left_column_step_addentries sto_right_column_step_addentries sto_output_column_step_addentries. ((exists dst_positive_code_column_step_addentriesentryleft dst_positive_scale_column_step_addentriesentryleft dst_negative_code_column_step_addentriesentryleft dst_negative_scale_column_step_addentriesentryleft dst_positive_column_step_addentriesentryleft dst_negative_column_step_addentriesentryleft. (((C) = (((((dst_positive_code_column_step_addentriesentryleft) + (dst_positive_scale_column_step_addentriesentryleft)) * S ((dst_positive_code_column_step_addentriesentryleft) + (dst_positive_scale_column_step_addentriesentryleft)) + ((dst_positive_scale_column_step_addentriesentryleft) + (dst_positive_scale_column_step_addentriesentryleft))) + (((dst_negative_code_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)) * S ((dst_negative_code_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)) + ((dst_negative_scale_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)))) * S ((((dst_positive_code_column_step_addentriesentryleft) + (dst_positive_scale_column_step_addentriesentryleft)) * S ((dst_positive_code_column_step_addentriesentryleft) + (dst_positive_scale_column_step_addentriesentryleft)) + ((dst_positive_scale_column_step_addentriesentryleft) + (dst_positive_scale_column_step_addentriesentryleft))) + (((dst_negative_code_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)) * S ((dst_negative_code_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)) + ((dst_negative_scale_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)))) + ((((dst_negative_code_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)) * S ((dst_negative_code_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)) + ((dst_negative_scale_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft))) + (((dst_negative_code_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)) * S ((dst_negative_code_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)) + ((dst_negative_scale_column_step_addentriesentryleft) + (dst_negative_scale_column_step_addentriesentryleft)))))) /\ (((((exists ff_h_pvs_column_step_addentriesentryleftpositive. ff_h_pvs_column_step_addentriesentryleftpositive + S (dst_positive_column_step_addentriesentryleft) = S ((S (sto_index_column_step_addentries)) * dst_positive_scale_column_step_addentriesentryleft)) /\ exists ff_q_pvs_column_step_addentriesentryleftpositive. dst_positive_code_column_step_addentriesentryleft = ff_q_pvs_column_step_addentriesentryleftpositive * S ((S (sto_index_column_step_addentries)) * dst_positive_scale_column_step_addentriesentryleft) + (dst_positive_column_step_addentriesentryleft))) /\ (((((exists ff_h_pvs_column_step_addentriesentryleftnegative. ff_h_pvs_column_step_addentriesentryleftnegative + S (dst_negative_column_step_addentriesentryleft) = S ((S (sto_index_column_step_addentries)) * dst_negative_scale_column_step_addentriesentryleft)) /\ exists ff_q_pvs_column_step_addentriesentryleftnegative. dst_negative_code_column_step_addentriesentryleft = ff_q_pvs_column_step_addentriesentryleftnegative * S ((S (sto_index_column_step_addentries)) * dst_negative_scale_column_step_addentriesentryleft) + (dst_negative_column_step_addentriesentryleft))) /\ (exists ge_balance_positive_column_step_addentriesentryleftvalue ge_balance_negative_column_step_addentriesentryleftvalue. (((((sto_left_column_step_addentries) = 2 * (ge_balance_positive_column_step_addentriesentryleftvalue) /\ (ge_balance_negative_column_step_addentriesentryleftvalue) = 0) \/ exists ge_signed_half_column_step_addentriesentryleftvaluedecode. (((sto_left_column_step_addentries) = 2 * ge_signed_half_column_step_addentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_column_step_addentriesentryleftvalue) = 0) /\ (ge_balance_negative_column_step_addentriesentryleftvalue) = S ge_signed_half_column_step_addentriesentryleftvaluedecode))) /\ ((dst_positive_column_step_addentriesentryleft) + ge_balance_negative_column_step_addentriesentryleftvalue = (dst_negative_column_step_addentriesentryleft) + ge_balance_positive_column_step_addentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_column_step_addentriesentryright dst_positive_scale_column_step_addentriesentryright dst_negative_code_column_step_addentriesentryright dst_negative_scale_column_step_addentriesentryright dst_positive_column_step_addentriesentryright dst_negative_column_step_addentriesentryright. (((V) = (((((dst_positive_code_column_step_addentriesentryright) + (dst_positive_scale_column_step_addentriesentryright)) * S ((dst_positive_code_column_step_addentriesentryright) + (dst_positive_scale_column_step_addentriesentryright)) + ((dst_positive_scale_column_step_addentriesentryright) + (dst_positive_scale_column_step_addentriesentryright))) + (((dst_negative_code_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)) * S ((dst_negative_code_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)) + ((dst_negative_scale_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)))) * S ((((dst_positive_code_column_step_addentriesentryright) + (dst_positive_scale_column_step_addentriesentryright)) * S ((dst_positive_code_column_step_addentriesentryright) + (dst_positive_scale_column_step_addentriesentryright)) + ((dst_positive_scale_column_step_addentriesentryright) + (dst_positive_scale_column_step_addentriesentryright))) + (((dst_negative_code_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)) * S ((dst_negative_code_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)) + ((dst_negative_scale_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)))) + ((((dst_negative_code_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)) * S ((dst_negative_code_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)) + ((dst_negative_scale_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright))) + (((dst_negative_code_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)) * S ((dst_negative_code_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)) + ((dst_negative_scale_column_step_addentriesentryright) + (dst_negative_scale_column_step_addentriesentryright)))))) /\ (((((exists ff_h_pvs_column_step_addentriesentryrightpositive. ff_h_pvs_column_step_addentriesentryrightpositive + S (dst_positive_column_step_addentriesentryright) = S ((S (sto_index_column_step_addentries)) * dst_positive_scale_column_step_addentriesentryright)) /\ exists ff_q_pvs_column_step_addentriesentryrightpositive. dst_positive_code_column_step_addentriesentryright = ff_q_pvs_column_step_addentriesentryrightpositive * S ((S (sto_index_column_step_addentries)) * dst_positive_scale_column_step_addentriesentryright) + (dst_positive_column_step_addentriesentryright))) /\ (((((exists ff_h_pvs_column_step_addentriesentryrightnegative. ff_h_pvs_column_step_addentriesentryrightnegative + S (dst_negative_column_step_addentriesentryright) = S ((S (sto_index_column_step_addentries)) * dst_negative_scale_column_step_addentriesentryright)) /\ exists ff_q_pvs_column_step_addentriesentryrightnegative. dst_negative_code_column_step_addentriesentryright = ff_q_pvs_column_step_addentriesentryrightnegative * S ((S (sto_index_column_step_addentries)) * dst_negative_scale_column_step_addentriesentryright) + (dst_negative_column_step_addentriesentryright))) /\ (exists ge_balance_positive_column_step_addentriesentryrightvalue ge_balance_negative_column_step_addentriesentryrightvalue. (((((sto_right_column_step_addentries) = 2 * (ge_balance_positive_column_step_addentriesentryrightvalue) /\ (ge_balance_negative_column_step_addentriesentryrightvalue) = 0) \/ exists ge_signed_half_column_step_addentriesentryrightvaluedecode. (((sto_right_column_step_addentries) = 2 * ge_signed_half_column_step_addentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_column_step_addentriesentryrightvalue) = 0) /\ (ge_balance_negative_column_step_addentriesentryrightvalue) = S ge_signed_half_column_step_addentriesentryrightvaluedecode))) /\ ((dst_positive_column_step_addentriesentryright) + ge_balance_negative_column_step_addentriesentryrightvalue = (dst_negative_column_step_addentriesentryright) + ge_balance_positive_column_step_addentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_column_step_addentriesentryoutput dst_positive_scale_column_step_addentriesentryoutput dst_negative_code_column_step_addentriesentryoutput dst_negative_scale_column_step_addentriesentryoutput dst_positive_column_step_addentriesentryoutput dst_negative_column_step_addentriesentryoutput. (((D) = (((((dst_positive_code_column_step_addentriesentryoutput) + (dst_positive_scale_column_step_addentriesentryoutput)) * S ((dst_positive_code_column_step_addentriesentryoutput) + (dst_positive_scale_column_step_addentriesentryoutput)) + ((dst_positive_scale_column_step_addentriesentryoutput) + (dst_positive_scale_column_step_addentriesentryoutput))) + (((dst_negative_code_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)) * S ((dst_negative_code_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)) + ((dst_negative_scale_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)))) * S ((((dst_positive_code_column_step_addentriesentryoutput) + (dst_positive_scale_column_step_addentriesentryoutput)) * S ((dst_positive_code_column_step_addentriesentryoutput) + (dst_positive_scale_column_step_addentriesentryoutput)) + ((dst_positive_scale_column_step_addentriesentryoutput) + (dst_positive_scale_column_step_addentriesentryoutput))) + (((dst_negative_code_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)) * S ((dst_negative_code_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)) + ((dst_negative_scale_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)))) + ((((dst_negative_code_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)) * S ((dst_negative_code_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)) + ((dst_negative_scale_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput))) + (((dst_negative_code_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)) * S ((dst_negative_code_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)) + ((dst_negative_scale_column_step_addentriesentryoutput) + (dst_negative_scale_column_step_addentriesentryoutput)))))) /\ (((((exists ff_h_pvs_column_step_addentriesentryoutputpositive. ff_h_pvs_column_step_addentriesentryoutputpositive + S (dst_positive_column_step_addentriesentryoutput) = S ((S (sto_index_column_step_addentries)) * dst_positive_scale_column_step_addentriesentryoutput)) /\ exists ff_q_pvs_column_step_addentriesentryoutputpositive. dst_positive_code_column_step_addentriesentryoutput = ff_q_pvs_column_step_addentriesentryoutputpositive * S ((S (sto_index_column_step_addentries)) * dst_positive_scale_column_step_addentriesentryoutput) + (dst_positive_column_step_addentriesentryoutput))) /\ (((((exists ff_h_pvs_column_step_addentriesentryoutputnegative. ff_h_pvs_column_step_addentriesentryoutputnegative + S (dst_negative_column_step_addentriesentryoutput) = S ((S (sto_index_column_step_addentries)) * dst_negative_scale_column_step_addentriesentryoutput)) /\ exists ff_q_pvs_column_step_addentriesentryoutputnegative. dst_negative_code_column_step_addentriesentryoutput = ff_q_pvs_column_step_addentriesentryoutputnegative * S ((S (sto_index_column_step_addentries)) * dst_negative_scale_column_step_addentriesentryoutput) + (dst_negative_column_step_addentriesentryoutput))) /\ (exists ge_balance_positive_column_step_addentriesentryoutputvalue ge_balance_negative_column_step_addentriesentryoutputvalue. (((((sto_output_column_step_addentries) = 2 * (ge_balance_positive_column_step_addentriesentryoutputvalue) /\ (ge_balance_negative_column_step_addentriesentryoutputvalue) = 0) \/ exists ge_signed_half_column_step_addentriesentryoutputvaluedecode. (((sto_output_column_step_addentries) = 2 * ge_signed_half_column_step_addentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_column_step_addentriesentryoutputvalue) = 0) /\ (ge_balance_negative_column_step_addentriesentryoutputvalue) = S ge_signed_half_column_step_addentriesentryoutputvaluedecode))) /\ ((dst_positive_column_step_addentriesentryoutput) + ge_balance_negative_column_step_addentriesentryoutputvalue = (dst_negative_column_step_addentriesentryoutput) + ge_balance_positive_column_step_addentriesentryoutputvalue))))))))) /\ (exists dsa_ap_column_step_addentriesentryoperation dsa_an_column_step_addentriesentryoperation dsa_bp_column_step_addentriesentryoperation dsa_bn_column_step_addentriesentryoperation dsa_cp_column_step_addentriesentryoperation dsa_cn_column_step_addentriesentryoperation. (((((sto_left_column_step_addentries) = 2 * (dsa_ap_column_step_addentriesentryoperation) /\ (dsa_an_column_step_addentriesentryoperation) = 0) \/ exists ge_signed_half_column_step_addentriesentryoperationleft. (((sto_left_column_step_addentries) = 2 * ge_signed_half_column_step_addentriesentryoperationleft + 1 /\ (dsa_ap_column_step_addentriesentryoperation) = 0) /\ (dsa_an_column_step_addentriesentryoperation) = S ge_signed_half_column_step_addentriesentryoperationleft))) /\ ((((((sto_right_column_step_addentries) = 2 * (dsa_bp_column_step_addentriesentryoperation) /\ (dsa_bn_column_step_addentriesentryoperation) = 0) \/ exists ge_signed_half_column_step_addentriesentryoperationright. (((sto_right_column_step_addentries) = 2 * ge_signed_half_column_step_addentriesentryoperationright + 1 /\ (dsa_bp_column_step_addentriesentryoperation) = 0) /\ (dsa_bn_column_step_addentriesentryoperation) = S ge_signed_half_column_step_addentriesentryoperationright))) /\ ((((((sto_output_column_step_addentries) = 2 * (dsa_cp_column_step_addentriesentryoperation) /\ (dsa_cn_column_step_addentriesentryoperation) = 0) \/ exists ge_signed_half_column_step_addentriesentryoperationoutput. (((sto_output_column_step_addentries) = 2 * ge_signed_half_column_step_addentriesentryoperationoutput + 1 /\ (dsa_cp_column_step_addentriesentryoperation) = 0) /\ (dsa_cn_column_step_addentriesentryoperation) = S ge_signed_half_column_step_addentriesentryoperationoutput))) /\ ((dsa_ap_column_step_addentriesentryoperation + dsa_bp_column_step_addentriesentryoperation) + dsa_cn_column_step_addentriesentryoperation = (dsa_an_column_step_addentriesentryoperation + dsa_bn_column_step_addentriesentryoperation) + dsa_cp_column_step_addentriesentryoperation)))))))))))))))))))Complete tactic proof in conservative notation
All 112 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
112 script commands · 30 reading checkpoints · 5 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.
Named ingredients (3)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–12
03Separate the logical casesL13–19
04Use earlier factsL20–20
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L20
exact hC_right_left
05Separate the logical casesL21–21
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L21
split
06Use earlier factsL22–22
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L22
exact hV_right_left
07Separate the logical casesL23–23
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L23
split
08Use earlier factsL24–24
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L24
exact hD_right_left
09Fix variables and assumptionsL25–26
10Establish heCL27–32
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.
- L27
have heC : ∃ z. ArithAt(C,j,z)Definitions: ArithAt(C,j,z)Original native command in the exact edition - L28
specialize signed_table_lookup_any (n) - L29
specialize signed_table_lookup_any (C) - L30
specialize signed_table_lookup_any (j) - L31
apply signed_table_lookup_any - L32
exact hC_right_left
11Separate the logical casesL33–33
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L33
cases heC
12Establish heVL34–39
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.
- L34
have heV : ∃ z. ArithAt(V,j,z)Definitions: ArithAt(V,j,z)Original native command in the exact edition - L35
specialize signed_table_lookup_any (n) - L36
specialize signed_table_lookup_any (V) - L37
specialize signed_table_lookup_any (j) - L38
apply signed_table_lookup_any - L39
exact hV_right_left
13Separate the logical casesL40–40
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L40
cases heV
14Establish heDL41–46
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.
- L41
have heD : ∃ z. ArithAt(D,j,z)Definitions: ArithAt(D,j,z)Original native command in the exact edition - L42
specialize signed_table_lookup_any (n) - L43
specialize signed_table_lookup_any (D) - L44
specialize signed_table_lookup_any (j) - L45
apply signed_table_lookup_any - L46
exact hD_right_left
15Separate the logical casesL47–47
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L47
cases heD
16Construct an explicit witnessL48–50
17Separate the logical casesL51–51
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L51
split
18Use earlier factsL52–52
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L52
exact heC_witness
19Separate the logical casesL53–53
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L53
split
20Use earlier factsL54–54
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L54
exact heV_witness
21Separate the logical casesL55–55
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L55
split
22Use earlier factsL56–56
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L56
exact heD_witness
23Establish hindexL57–61
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square euler add swap last.
24Establish hentryL62–71
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed rectangular slice lookup.
- L62
have hentry : ArithAt(F,o + s · m + t · j,x1)Definitions: ArithAt(F,o + s · m + t · j,x1)Original native command in the exact edition - L63
specialize signed_rectangular_slice_lookup (F) - L64
specialize signed_rectangular_slice_lookup (V) - L65
specialize signed_rectangular_slice_lookup (((o) + ((s) * (m)))) - L66
specialize signed_rectangular_slice_lookup (t) - L67
specialize signed_rectangular_slice_lookup (n) - L68
specialize signed_rectangular_slice_lookup (j) - L69
specialize signed_rectangular_slice_lookup (x1) - L70
apply signed_rectangular_slice_lookup - L71
exact hV
25Use earlier factsL72–73
26Calculate and transport equalitiesL74–77
27Use earlier factsL78–87
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L78
specialize signed_rectangular_slice_sum_successor_add (F) - L79
specialize signed_rectangular_slice_sum_successor_add (((o) + ((t) * (j)))) - L80
specialize signed_rectangular_slice_sum_successor_add (s) - L81
specialize signed_rectangular_slice_sum_successor_add (m) - L82
specialize signed_rectangular_slice_sum_successor_add (x) - L83
specialize signed_rectangular_slice_sum_successor_add (x1) - L84
specialize signed_rectangular_slice_sum_successor_add (x2) - L85
apply signed_rectangular_slice_sum_successor_add - L86
specialize signed_rectangular_row_sums_lookup (F) - L87
specialize signed_rectangular_row_sums_lookup (C)
28Use earlier factsL88–97
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L88
specialize signed_rectangular_row_sums_lookup (o) - L89
specialize signed_rectangular_row_sums_lookup (t) - L90
specialize signed_rectangular_row_sums_lookup (s) - L91
specialize signed_rectangular_row_sums_lookup (n) - L92
specialize signed_rectangular_row_sums_lookup (m) - L93
specialize signed_rectangular_row_sums_lookup (j) - L94
specialize signed_rectangular_row_sums_lookup (x) - L95
apply signed_rectangular_row_sums_lookup - L96
exact hC - L97
exact hj
29Use earlier factsL98–107
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L98
exact heC_witness - L99
exact hentry - L100
specialize signed_rectangular_row_sums_lookup (F) - L101
specialize signed_rectangular_row_sums_lookup (D) - L102
specialize signed_rectangular_row_sums_lookup (o) - L103
specialize signed_rectangular_row_sums_lookup (t) - L104
specialize signed_rectangular_row_sums_lookup (s) - L105
specialize signed_rectangular_row_sums_lookup (n) - L106
specialize signed_rectangular_row_sums_lookup (S m) - L107
specialize signed_rectangular_row_sums_lookup (j)
Original defined command ledger · 112 lines
- 0001
intro F - 0002
intro C - 0003
intro V - 0004
intro D - 0005
intro o - 0006
intro s - 0007
intro t - 0008
intro m - 0009
intro n - 0010
intro hC - 0011
intro hV - 0012
intro hD - 0013
cases hC - 0014
cases hC_right - 0015
cases hV - 0016
cases hV_right - 0017
cases hD - 0018
cases hD_right - 0019
split - 0020
exact hC_right_left - 0021
split - 0022
exact hV_right_left - 0023
split - 0024
exact hD_right_left - 0025
intro j - 0026
intro hj - 0027
have heC : ∃ z. ArithAt(C,j,z) - 0028
specialize signed_table_lookup_any (n) - 0029
specialize signed_table_lookup_any (C) - 0030
specialize signed_table_lookup_any (j) - 0031
apply signed_table_lookup_any - 0032
exact hC_right_left - 0033
cases heC - 0034
have heV : ∃ z. ArithAt(V,j,z) - 0035
specialize signed_table_lookup_any (n) - 0036
specialize signed_table_lookup_any (V) - 0037
specialize signed_table_lookup_any (j) - 0038
apply signed_table_lookup_any - 0039
exact hV_right_left - 0040
cases heV - 0041
have heD : ∃ z. ArithAt(D,j,z) - 0042
specialize signed_table_lookup_any (n) - 0043
specialize signed_table_lookup_any (D) - 0044
specialize signed_table_lookup_any (j) - 0045
apply signed_table_lookup_any - 0046
exact hD_right_left - 0047
cases heD - 0048
exists x - 0049
exists x1 - 0050
exists x2 - 0051
split - 0052
exact heC_witness - 0053
split - 0054
exact heV_witness - 0055
split - 0056
exact heD_witness - 0057
have hindex : ((((o) + ((s) * (m)))) + ((t) * (j))) = ((((o) + ((t) * (j)))) + ((s) * (m))) - 0058
specialize four_square_euler_add_swap_last (o) - 0059
specialize four_square_euler_add_swap_last (s*m) - 0060
specialize four_square_euler_add_swap_last (t*j) - 0061
apply four_square_euler_add_swap_last - 0062
have hentry : ArithAt(F,o + s · m + t · j,x1) - 0063
specialize signed_rectangular_slice_lookup (F) - 0064
specialize signed_rectangular_slice_lookup (V) - 0065
specialize signed_rectangular_slice_lookup (((o) + ((s) * (m)))) - 0066
specialize signed_rectangular_slice_lookup (t) - 0067
specialize signed_rectangular_slice_lookup (n) - 0068
specialize signed_rectangular_slice_lookup (j) - 0069
specialize signed_rectangular_slice_lookup (x1) - 0070
apply signed_rectangular_slice_lookup - 0071
exact hV - 0072
exact hj - 0073
exact heV_witness - 0074
rewrite hindex at hentry - 0075
rewrite hindex at hentry - 0076
rewrite hindex at hentry - 0077
rewrite hindex at hentry - 0078
specialize signed_rectangular_slice_sum_successor_add (F) - 0079
specialize signed_rectangular_slice_sum_successor_add (((o) + ((t) * (j)))) - 0080
specialize signed_rectangular_slice_sum_successor_add (s) - 0081
specialize signed_rectangular_slice_sum_successor_add (m) - 0082
specialize signed_rectangular_slice_sum_successor_add (x) - 0083
specialize signed_rectangular_slice_sum_successor_add (x1) - 0084
specialize signed_rectangular_slice_sum_successor_add (x2) - 0085
apply signed_rectangular_slice_sum_successor_add - 0086
specialize signed_rectangular_row_sums_lookup (F) - 0087
specialize signed_rectangular_row_sums_lookup (C) - 0088
specialize signed_rectangular_row_sums_lookup (o) - 0089
specialize signed_rectangular_row_sums_lookup (t) - 0090
specialize signed_rectangular_row_sums_lookup (s) - 0091
specialize signed_rectangular_row_sums_lookup (n) - 0092
specialize signed_rectangular_row_sums_lookup (m) - 0093
specialize signed_rectangular_row_sums_lookup (j) - 0094
specialize signed_rectangular_row_sums_lookup (x) - 0095
apply signed_rectangular_row_sums_lookup - 0096
exact hC - 0097
exact hj - 0098
exact heC_witness - 0099
exact hentry - 0100
specialize signed_rectangular_row_sums_lookup (F) - 0101
specialize signed_rectangular_row_sums_lookup (D) - 0102
specialize signed_rectangular_row_sums_lookup (o) - 0103
specialize signed_rectangular_row_sums_lookup (t) - 0104
specialize signed_rectangular_row_sums_lookup (s) - 0105
specialize signed_rectangular_row_sums_lookup (n) - 0106
specialize signed_rectangular_row_sums_lookup (S m) - 0107
specialize signed_rectangular_row_sums_lookup (j) - 0108
specialize signed_rectangular_row_sums_lookup (x2) - 0109
apply signed_rectangular_row_sums_lookup - 0110
exact hD - 0111
exact hj - 0112
exact heD_witness