RS0015

signed_rectangular_row_sums_exists

Ordinary induction computes each finite slice sum and appends its actual signed value to construct the entire row-sum table.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

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

∀ m. ∀ F. ∀ o. ∀ s. ∀ t. ∀ n. ArithTable(0,F) → ∃ x. ArithRowSums(F,x,o,s,t,m,n)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ArithTable(N,F) · 1ArithExtend(F,G,l,z) · 1SignedSliceSum(F,o,s,l,z) · 1ArithRowSums(F,R,o,s,t,m,n) · 2

Actual proof prerequisites

signed_rectangular_row_sums_emptydivisor_signed_table_from_components · checked external prerequisitesigned_rectangular_slice_sum_existsarithmetic_signed_table_extend_at · checked external prerequisitesigned_rectangular_row_sums_extend
Original expanded first-order statement 
forall m F o s t n. (exists dst_positive_code_exists_source dst_positive_scale_exists_source dst_negative_code_exists_source dst_negative_scale_exists_source. (((F) = (((((dst_positive_code_exists_source) + (dst_positive_scale_exists_source)) * S ((dst_positive_code_exists_source) + (dst_positive_scale_exists_source)) + ((dst_positive_scale_exists_source) + (dst_positive_scale_exists_source))) + (((dst_negative_code_exists_source) + (dst_negative_scale_exists_source)) * S ((dst_negative_code_exists_source) + (dst_negative_scale_exists_source)) + ((dst_negative_scale_exists_source) + (dst_negative_scale_exists_source)))) * S ((((dst_positive_code_exists_source) + (dst_positive_scale_exists_source)) * S ((dst_positive_code_exists_source) + (dst_positive_scale_exists_source)) + ((dst_positive_scale_exists_source) + (dst_positive_scale_exists_source))) + (((dst_negative_code_exists_source) + (dst_negative_scale_exists_source)) * S ((dst_negative_code_exists_source) + (dst_negative_scale_exists_source)) + ((dst_negative_scale_exists_source) + (dst_negative_scale_exists_source)))) + ((((dst_negative_code_exists_source) + (dst_negative_scale_exists_source)) * S ((dst_negative_code_exists_source) + (dst_negative_scale_exists_source)) + ((dst_negative_scale_exists_source) + (dst_negative_scale_exists_source))) + (((dst_negative_code_exists_source) + (dst_negative_scale_exists_source)) * S ((dst_negative_code_exists_source) + (dst_negative_scale_exists_source)) + ((dst_negative_scale_exists_source) + (dst_negative_scale_exists_source)))))) /\ (forall dst_index_exists_source. (exists pvs_le_gap_exists_sourcedomain. pvs_le_gap_exists_sourcedomain + (dst_index_exists_source) = (0)) -> exists dst_positive_exists_source dst_negative_exists_source dst_value_exists_source. ((((exists ff_h_pvs_exists_sourceentrypositive. ff_h_pvs_exists_sourceentrypositive + S (dst_positive_exists_source) = S ((S (dst_index_exists_source)) * dst_positive_scale_exists_source)) /\ exists ff_q_pvs_exists_sourceentrypositive. dst_positive_code_exists_source = ff_q_pvs_exists_sourceentrypositive * S ((S (dst_index_exists_source)) * dst_positive_scale_exists_source) + (dst_positive_exists_source))) /\ (((((exists ff_h_pvs_exists_sourceentrynegative. ff_h_pvs_exists_sourceentrynegative + S (dst_negative_exists_source) = S ((S (dst_index_exists_source)) * dst_negative_scale_exists_source)) /\ exists ff_q_pvs_exists_sourceentrynegative. dst_negative_code_exists_source = ff_q_pvs_exists_sourceentrynegative * S ((S (dst_index_exists_source)) * dst_negative_scale_exists_source) + (dst_negative_exists_source))) /\ (exists ge_balance_positive_exists_sourceentryvalue ge_balance_negative_exists_sourceentryvalue. (((((dst_value_exists_source) = 2 * (ge_balance_positive_exists_sourceentryvalue) /\ (ge_balance_negative_exists_sourceentryvalue) = 0) \/ exists ge_signed_half_exists_sourceentryvaluedecode. (((dst_value_exists_source) = 2 * ge_signed_half_exists_sourceentryvaluedecode + 1 /\ (ge_balance_positive_exists_sourceentryvalue) = 0) /\ (ge_balance_negative_exists_sourceentryvalue) = S ge_signed_half_exists_sourceentryvaluedecode))) /\ ((dst_positive_exists_source) + ge_balance_negative_exists_sourceentryvalue = (dst_negative_exists_source) + ge_balance_positive_exists_sourceentryvalue))))))))) -> exists R. (((exists dst_positive_code_exists_resultsource_table dst_positive_scale_exists_resultsource_table dst_negative_code_exists_resultsource_table dst_negative_scale_exists_resultsource_table. (((F) = (((((dst_positive_code_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table)) * S ((dst_positive_code_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table)) + ((dst_positive_scale_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table))) + (((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) * S ((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) + ((dst_negative_scale_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)))) * S ((((dst_positive_code_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table)) * S ((dst_positive_code_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table)) + ((dst_positive_scale_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table))) + (((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) * S ((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) + ((dst_negative_scale_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)))) + ((((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) * S ((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) + ((dst_negative_scale_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table))) + (((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) * S ((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) + ((dst_negative_scale_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)))))) /\ (forall dst_index_exists_resultsource_table. (exists pvs_le_gap_exists_resultsource_tabledomain. pvs_le_gap_exists_resultsource_tabledomain + (dst_index_exists_resultsource_table) = (0)) -> exists dst_positive_exists_resultsource_table dst_negative_exists_resultsource_table dst_value_exists_resultsource_table. ((((exists ff_h_pvs_exists_resultsource_tableentrypositive. ff_h_pvs_exists_resultsource_tableentrypositive + S (dst_positive_exists_resultsource_table) = S ((S (dst_index_exists_resultsource_table)) * dst_positive_scale_exists_resultsource_table)) /\ exists ff_q_pvs_exists_resultsource_tableentrypositive. dst_positive_code_exists_resultsource_table = ff_q_pvs_exists_resultsource_tableentrypositive * S ((S (dst_index_exists_resultsource_table)) * dst_positive_scale_exists_resultsource_table) + (dst_positive_exists_resultsource_table))) /\ (((((exists ff_h_pvs_exists_resultsource_tableentrynegative. ff_h_pvs_exists_resultsource_tableentrynegative + S (dst_negative_exists_resultsource_table) = S ((S (dst_index_exists_resultsource_table)) * dst_negative_scale_exists_resultsource_table)) /\ exists ff_q_pvs_exists_resultsource_tableentrynegative. dst_negative_code_exists_resultsource_table = ff_q_pvs_exists_resultsource_tableentrynegative * S ((S (dst_index_exists_resultsource_table)) * dst_negative_scale_exists_resultsource_table) + (dst_negative_exists_resultsource_table))) /\ (exists ge_balance_positive_exists_resultsource_tableentryvalue ge_balance_negative_exists_resultsource_tableentryvalue. (((((dst_value_exists_resultsource_table) = 2 * (ge_balance_positive_exists_resultsource_tableentryvalue) /\ (ge_balance_negative_exists_resultsource_tableentryvalue) = 0) \/ exists ge_signed_half_exists_resultsource_tableentryvaluedecode. (((dst_value_exists_resultsource_table) = 2 * ge_signed_half_exists_resultsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_resultsource_tableentryvalue) = 0) /\ (ge_balance_negative_exists_resultsource_tableentryvalue) = S ge_signed_half_exists_resultsource_tableentryvaluedecode))) /\ ((dst_positive_exists_resultsource_table) + ge_balance_negative_exists_resultsource_tableentryvalue = (dst_negative_exists_resultsource_table) + ge_balance_positive_exists_resultsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_exists_resultrow_table dst_positive_scale_exists_resultrow_table dst_negative_code_exists_resultrow_table dst_negative_scale_exists_resultrow_table. (((R) = (((((dst_positive_code_exists_resultrow_table) + (dst_positive_scale_exists_resultrow_table)) * S ((dst_positive_code_exists_resultrow_table) + (dst_positive_scale_exists_resultrow_table)) + ((dst_positive_scale_exists_resultrow_table) + (dst_positive_scale_exists_resultrow_table))) + (((dst_negative_code_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)) * S ((dst_negative_code_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)) + ((dst_negative_scale_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)))) * S ((((dst_positive_code_exists_resultrow_table) + (dst_positive_scale_exists_resultrow_table)) * S ((dst_positive_code_exists_resultrow_table) + (dst_positive_scale_exists_resultrow_table)) + ((dst_positive_scale_exists_resultrow_table) + (dst_positive_scale_exists_resultrow_table))) + (((dst_negative_code_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)) * S ((dst_negative_code_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)) + ((dst_negative_scale_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)))) + ((((dst_negative_code_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)) * S ((dst_negative_code_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)) + ((dst_negative_scale_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table))) + (((dst_negative_code_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)) * S ((dst_negative_code_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)) + ((dst_negative_scale_exists_resultrow_table) + (dst_negative_scale_exists_resultrow_table)))))) /\ (forall dst_index_exists_resultrow_table. (exists pvs_le_gap_exists_resultrow_tabledomain. pvs_le_gap_exists_resultrow_tabledomain + (dst_index_exists_resultrow_table) = (m)) -> exists dst_positive_exists_resultrow_table dst_negative_exists_resultrow_table dst_value_exists_resultrow_table. ((((exists ff_h_pvs_exists_resultrow_tableentrypositive. ff_h_pvs_exists_resultrow_tableentrypositive + S (dst_positive_exists_resultrow_table) = S ((S (dst_index_exists_resultrow_table)) * dst_positive_scale_exists_resultrow_table)) /\ exists ff_q_pvs_exists_resultrow_tableentrypositive. dst_positive_code_exists_resultrow_table = ff_q_pvs_exists_resultrow_tableentrypositive * S ((S (dst_index_exists_resultrow_table)) * dst_positive_scale_exists_resultrow_table) + (dst_positive_exists_resultrow_table))) /\ (((((exists ff_h_pvs_exists_resultrow_tableentrynegative. ff_h_pvs_exists_resultrow_tableentrynegative + S (dst_negative_exists_resultrow_table) = S ((S (dst_index_exists_resultrow_table)) * dst_negative_scale_exists_resultrow_table)) /\ exists ff_q_pvs_exists_resultrow_tableentrynegative. dst_negative_code_exists_resultrow_table = ff_q_pvs_exists_resultrow_tableentrynegative * S ((S (dst_index_exists_resultrow_table)) * dst_negative_scale_exists_resultrow_table) + (dst_negative_exists_resultrow_table))) /\ (exists ge_balance_positive_exists_resultrow_tableentryvalue ge_balance_negative_exists_resultrow_tableentryvalue. (((((dst_value_exists_resultrow_table) = 2 * (ge_balance_positive_exists_resultrow_tableentryvalue) /\ (ge_balance_negative_exists_resultrow_tableentryvalue) = 0) \/ exists ge_signed_half_exists_resultrow_tableentryvaluedecode. (((dst_value_exists_resultrow_table) = 2 * ge_signed_half_exists_resultrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_resultrow_tableentryvalue) = 0) /\ (ge_balance_negative_exists_resultrow_tableentryvalue) = S ge_signed_half_exists_resultrow_tableentryvaluedecode))) /\ ((dst_positive_exists_resultrow_table) + ge_balance_negative_exists_resultrow_tableentryvalue = (dst_negative_exists_resultrow_table) + ge_balance_positive_exists_resultrow_tableentryvalue))))))))) /\ (forall srt_index_exists_result. (exists pvs_gap_exists_resultbound. pvs_gap_exists_resultbound + S (srt_index_exists_result) = (m)) -> exists srt_value_exists_result. (((exists dst_positive_code_exists_resultrowentry dst_positive_scale_exists_resultrowentry dst_negative_code_exists_resultrowentry dst_negative_scale_exists_resultrowentry dst_positive_exists_resultrowentry dst_negative_exists_resultrowentry. (((R) = (((((dst_positive_code_exists_resultrowentry) + (dst_positive_scale_exists_resultrowentry)) * S ((dst_positive_code_exists_resultrowentry) + (dst_positive_scale_exists_resultrowentry)) + ((dst_positive_scale_exists_resultrowentry) + (dst_positive_scale_exists_resultrowentry))) + (((dst_negative_code_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)) * S ((dst_negative_code_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)) + ((dst_negative_scale_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)))) * S ((((dst_positive_code_exists_resultrowentry) + (dst_positive_scale_exists_resultrowentry)) * S ((dst_positive_code_exists_resultrowentry) + (dst_positive_scale_exists_resultrowentry)) + ((dst_positive_scale_exists_resultrowentry) + (dst_positive_scale_exists_resultrowentry))) + (((dst_negative_code_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)) * S ((dst_negative_code_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)) + ((dst_negative_scale_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)))) + ((((dst_negative_code_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)) * S ((dst_negative_code_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)) + ((dst_negative_scale_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry))) + (((dst_negative_code_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)) * S ((dst_negative_code_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)) + ((dst_negative_scale_exists_resultrowentry) + (dst_negative_scale_exists_resultrowentry)))))) /\ (((((exists ff_h_pvs_exists_resultrowentrypositive. ff_h_pvs_exists_resultrowentrypositive + S (dst_positive_exists_resultrowentry) = S ((S (srt_index_exists_result)) * dst_positive_scale_exists_resultrowentry)) /\ exists ff_q_pvs_exists_resultrowentrypositive. dst_positive_code_exists_resultrowentry = ff_q_pvs_exists_resultrowentrypositive * S ((S (srt_index_exists_result)) * dst_positive_scale_exists_resultrowentry) + (dst_positive_exists_resultrowentry))) /\ (((((exists ff_h_pvs_exists_resultrowentrynegative. ff_h_pvs_exists_resultrowentrynegative + S (dst_negative_exists_resultrowentry) = S ((S (srt_index_exists_result)) * dst_negative_scale_exists_resultrowentry)) /\ exists ff_q_pvs_exists_resultrowentrynegative. dst_negative_code_exists_resultrowentry = ff_q_pvs_exists_resultrowentrynegative * S ((S (srt_index_exists_result)) * dst_negative_scale_exists_resultrowentry) + (dst_negative_exists_resultrowentry))) /\ (exists ge_balance_positive_exists_resultrowentryvalue ge_balance_negative_exists_resultrowentryvalue. (((((srt_value_exists_result) = 2 * (ge_balance_positive_exists_resultrowentryvalue) /\ (ge_balance_negative_exists_resultrowentryvalue) = 0) \/ exists ge_signed_half_exists_resultrowentryvaluedecode. (((srt_value_exists_result) = 2 * ge_signed_half_exists_resultrowentryvaluedecode + 1 /\ (ge_balance_positive_exists_resultrowentryvalue) = 0) /\ (ge_balance_negative_exists_resultrowentryvalue) = S ge_signed_half_exists_resultrowentryvaluedecode))) /\ ((dst_positive_exists_resultrowentry) + ge_balance_negative_exists_resultrowentryvalue = (dst_negative_exists_resultrowentry) + ge_balance_positive_exists_resultrowentryvalue))))))))) /\ (exists srs_slice_exists_resultrowrow_sum. ((((exists dst_positive_code_exists_resultrowrow_sumslicesource_table dst_positive_scale_exists_resultrowrow_sumslicesource_table dst_negative_code_exists_resultrowrow_sumslicesource_table dst_negative_scale_exists_resultrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_exists_resultrowrow_sumslicesource_table) + (dst_positive_scale_exists_resultrowrow_sumslicesource_table)) * S ((dst_positive_code_exists_resultrowrow_sumslicesource_table) + (dst_positive_scale_exists_resultrowrow_sumslicesource_table)) + ((dst_positive_scale_exists_resultrowrow_sumslicesource_table) + (dst_positive_scale_exists_resultrowrow_sumslicesource_table))) + (((dst_negative_code_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)) * S ((dst_negative_code_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)) + ((dst_negative_scale_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)))) * S ((((dst_positive_code_exists_resultrowrow_sumslicesource_table) + (dst_positive_scale_exists_resultrowrow_sumslicesource_table)) * S ((dst_positive_code_exists_resultrowrow_sumslicesource_table) + (dst_positive_scale_exists_resultrowrow_sumslicesource_table)) + ((dst_positive_scale_exists_resultrowrow_sumslicesource_table) + (dst_positive_scale_exists_resultrowrow_sumslicesource_table))) + (((dst_negative_code_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)) * S ((dst_negative_code_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)) + ((dst_negative_scale_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)))) + ((((dst_negative_code_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)) * S ((dst_negative_code_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)) + ((dst_negative_scale_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table))) + (((dst_negative_code_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)) * S ((dst_negative_code_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)) + ((dst_negative_scale_exists_resultrowrow_sumslicesource_table) + (dst_negative_scale_exists_resultrowrow_sumslicesource_table)))))) /\ (forall dst_index_exists_resultrowrow_sumslicesource_table. (exists pvs_le_gap_exists_resultrowrow_sumslicesource_tabledomain. pvs_le_gap_exists_resultrowrow_sumslicesource_tabledomain + (dst_index_exists_resultrowrow_sumslicesource_table) = (0)) -> exists dst_positive_exists_resultrowrow_sumslicesource_table dst_negative_exists_resultrowrow_sumslicesource_table dst_value_exists_resultrowrow_sumslicesource_table. ((((exists ff_h_pvs_exists_resultrowrow_sumslicesource_tableentrypositive. ff_h_pvs_exists_resultrowrow_sumslicesource_tableentrypositive + S (dst_positive_exists_resultrowrow_sumslicesource_table) = S ((S (dst_index_exists_resultrowrow_sumslicesource_table)) * dst_positive_scale_exists_resultrowrow_sumslicesource_table)) /\ exists ff_q_pvs_exists_resultrowrow_sumslicesource_tableentrypositive. dst_positive_code_exists_resultrowrow_sumslicesource_table = ff_q_pvs_exists_resultrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_exists_resultrowrow_sumslicesource_table)) * dst_positive_scale_exists_resultrowrow_sumslicesource_table) + (dst_positive_exists_resultrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_exists_resultrowrow_sumslicesource_tableentrynegative. ff_h_pvs_exists_resultrowrow_sumslicesource_tableentrynegative + S (dst_negative_exists_resultrowrow_sumslicesource_table) = S ((S (dst_index_exists_resultrowrow_sumslicesource_table)) * dst_negative_scale_exists_resultrowrow_sumslicesource_table)) /\ exists ff_q_pvs_exists_resultrowrow_sumslicesource_tableentrynegative. dst_negative_code_exists_resultrowrow_sumslicesource_table = ff_q_pvs_exists_resultrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_exists_resultrowrow_sumslicesource_table)) * dst_negative_scale_exists_resultrowrow_sumslicesource_table) + (dst_negative_exists_resultrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_exists_resultrowrow_sumslicesource_tableentryvalue ge_balance_negative_exists_resultrowrow_sumslicesource_tableentryvalue. (((((dst_value_exists_resultrowrow_sumslicesource_table) = 2 * (ge_balance_positive_exists_resultrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_exists_resultrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_exists_resultrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_exists_resultrowrow_sumslicesource_table) = 2 * ge_signed_half_exists_resultrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_resultrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_exists_resultrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_exists_resultrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_exists_resultrowrow_sumslicesource_table) + ge_balance_negative_exists_resultrowrow_sumslicesource_tableentryvalue = (dst_negative_exists_resultrowrow_sumslicesource_table) + ge_balance_positive_exists_resultrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_exists_resultrowrow_sumsliceoutput_table dst_positive_scale_exists_resultrowrow_sumsliceoutput_table dst_negative_code_exists_resultrowrow_sumsliceoutput_table dst_negative_scale_exists_resultrowrow_sumsliceoutput_table. (((srs_slice_exists_resultrowrow_sum) = (((((dst_positive_code_exists_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_exists_resultrowrow_sumsliceoutput_table)) * S ((dst_positive_code_exists_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_exists_resultrowrow_sumsliceoutput_table)) + ((dst_positive_scale_exists_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_exists_resultrowrow_sumsliceoutput_table))) + (((dst_negative_code_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)) * S ((dst_negative_code_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)) + ((dst_negative_scale_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_exists_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_exists_resultrowrow_sumsliceoutput_table)) * S ((dst_positive_code_exists_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_exists_resultrowrow_sumsliceoutput_table)) + ((dst_positive_scale_exists_resultrowrow_sumsliceoutput_table) + (dst_positive_scale_exists_resultrowrow_sumsliceoutput_table))) + (((dst_negative_code_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)) * S ((dst_negative_code_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)) + ((dst_negative_scale_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)) * S ((dst_negative_code_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)) + ((dst_negative_scale_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table))) + (((dst_negative_code_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)) * S ((dst_negative_code_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)) + ((dst_negative_scale_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_exists_resultrowrow_sumsliceoutput_table. (exists pvs_le_gap_exists_resultrowrow_sumsliceoutput_tabledomain. pvs_le_gap_exists_resultrowrow_sumsliceoutput_tabledomain + (dst_index_exists_resultrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_exists_resultrowrow_sumsliceoutput_table dst_negative_exists_resultrowrow_sumsliceoutput_table dst_value_exists_resultrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_exists_resultrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_exists_resultrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_exists_resultrowrow_sumsliceoutput_table) = S ((S (dst_index_exists_resultrowrow_sumsliceoutput_table)) * dst_positive_scale_exists_resultrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_exists_resultrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_exists_resultrowrow_sumsliceoutput_table = ff_q_pvs_exists_resultrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_exists_resultrowrow_sumsliceoutput_table)) * dst_positive_scale_exists_resultrowrow_sumsliceoutput_table) + (dst_positive_exists_resultrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_exists_resultrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_exists_resultrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_exists_resultrowrow_sumsliceoutput_table) = S ((S (dst_index_exists_resultrowrow_sumsliceoutput_table)) * dst_negative_scale_exists_resultrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_exists_resultrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_exists_resultrowrow_sumsliceoutput_table = ff_q_pvs_exists_resultrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_exists_resultrowrow_sumsliceoutput_table)) * dst_negative_scale_exists_resultrowrow_sumsliceoutput_table) + (dst_negative_exists_resultrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_exists_resultrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_exists_resultrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_exists_resultrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_exists_resultrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_exists_resultrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_exists_resultrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_exists_resultrowrow_sumsliceoutput_table) = 2 * ge_signed_half_exists_resultrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_resultrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_exists_resultrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_exists_resultrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_exists_resultrowrow_sumsliceoutput_table) + ge_balance_negative_exists_resultrowrow_sumsliceoutput_tableentryvalue = (dst_negative_exists_resultrowrow_sumsliceoutput_table) + ge_balance_positive_exists_resultrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_exists_resultrowrow_sumslice. (exists pvs_gap_exists_resultrowrow_sumslicebound. pvs_gap_exists_resultrowrow_sumslicebound + S (srs_index_exists_resultrowrow_sumslice) = (n)) -> exists srs_value_exists_resultrowrow_sumslice. (((exists dst_positive_code_exists_resultrowrow_sumsliceentrysource dst_positive_scale_exists_resultrowrow_sumsliceentrysource dst_negative_code_exists_resultrowrow_sumsliceentrysource dst_negative_scale_exists_resultrowrow_sumsliceentrysource dst_positive_exists_resultrowrow_sumsliceentrysource dst_negative_exists_resultrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_exists_resultrowrow_sumsliceentrysource) + (dst_positive_scale_exists_resultrowrow_sumsliceentrysource)) * S ((dst_positive_code_exists_resultrowrow_sumsliceentrysource) + (dst_positive_scale_exists_resultrowrow_sumsliceentrysource)) + ((dst_positive_scale_exists_resultrowrow_sumsliceentrysource) + (dst_positive_scale_exists_resultrowrow_sumsliceentrysource))) + (((dst_negative_code_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)) * S ((dst_negative_code_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)) + ((dst_negative_scale_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_exists_resultrowrow_sumsliceentrysource) + (dst_positive_scale_exists_resultrowrow_sumsliceentrysource)) * S ((dst_positive_code_exists_resultrowrow_sumsliceentrysource) + (dst_positive_scale_exists_resultrowrow_sumsliceentrysource)) + ((dst_positive_scale_exists_resultrowrow_sumsliceentrysource) + (dst_positive_scale_exists_resultrowrow_sumsliceentrysource))) + (((dst_negative_code_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)) * S ((dst_negative_code_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)) + ((dst_negative_scale_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)))) + ((((dst_negative_code_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)) * S ((dst_negative_code_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)) + ((dst_negative_scale_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource))) + (((dst_negative_code_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)) * S ((dst_negative_code_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)) + ((dst_negative_scale_exists_resultrowrow_sumsliceentrysource) + (dst_negative_scale_exists_resultrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_exists_resultrowrow_sumsliceentrysourcepositive. ff_h_pvs_exists_resultrowrow_sumsliceentrysourcepositive + S (dst_positive_exists_resultrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_exists_result)))) + ((t) * (srs_index_exists_resultrowrow_sumslice))))) * dst_positive_scale_exists_resultrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_exists_resultrowrow_sumsliceentrysourcepositive. dst_positive_code_exists_resultrowrow_sumsliceentrysource = ff_q_pvs_exists_resultrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((s) * (srt_index_exists_result)))) + ((t) * (srs_index_exists_resultrowrow_sumslice))))) * dst_positive_scale_exists_resultrowrow_sumsliceentrysource) + (dst_positive_exists_resultrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_exists_resultrowrow_sumsliceentrysourcenegative. ff_h_pvs_exists_resultrowrow_sumsliceentrysourcenegative + S (dst_negative_exists_resultrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_exists_result)))) + ((t) * (srs_index_exists_resultrowrow_sumslice))))) * dst_negative_scale_exists_resultrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_exists_resultrowrow_sumsliceentrysourcenegative. dst_negative_code_exists_resultrowrow_sumsliceentrysource = ff_q_pvs_exists_resultrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((s) * (srt_index_exists_result)))) + ((t) * (srs_index_exists_resultrowrow_sumslice))))) * dst_negative_scale_exists_resultrowrow_sumsliceentrysource) + (dst_negative_exists_resultrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_exists_resultrowrow_sumsliceentrysourcevalue ge_balance_negative_exists_resultrowrow_sumsliceentrysourcevalue. (((((srs_value_exists_resultrowrow_sumslice) = 2 * (ge_balance_positive_exists_resultrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_exists_resultrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_exists_resultrowrow_sumsliceentrysourcevaluedecode. (((srs_value_exists_resultrowrow_sumslice) = 2 * ge_signed_half_exists_resultrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_exists_resultrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_exists_resultrowrow_sumsliceentrysourcevalue) = S ge_signed_half_exists_resultrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_exists_resultrowrow_sumsliceentrysource) + ge_balance_negative_exists_resultrowrow_sumsliceentrysourcevalue = (dst_negative_exists_resultrowrow_sumsliceentrysource) + ge_balance_positive_exists_resultrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_exists_resultrowrow_sumsliceentryoutput dst_positive_scale_exists_resultrowrow_sumsliceentryoutput dst_negative_code_exists_resultrowrow_sumsliceentryoutput dst_negative_scale_exists_resultrowrow_sumsliceentryoutput dst_positive_exists_resultrowrow_sumsliceentryoutput dst_negative_exists_resultrowrow_sumsliceentryoutput. (((srs_slice_exists_resultrowrow_sum) = (((((dst_positive_code_exists_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_exists_resultrowrow_sumsliceentryoutput)) * S ((dst_positive_code_exists_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_exists_resultrowrow_sumsliceentryoutput)) + ((dst_positive_scale_exists_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_exists_resultrowrow_sumsliceentryoutput))) + (((dst_negative_code_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)) * S ((dst_negative_code_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)) + ((dst_negative_scale_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_exists_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_exists_resultrowrow_sumsliceentryoutput)) * S ((dst_positive_code_exists_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_exists_resultrowrow_sumsliceentryoutput)) + ((dst_positive_scale_exists_resultrowrow_sumsliceentryoutput) + (dst_positive_scale_exists_resultrowrow_sumsliceentryoutput))) + (((dst_negative_code_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)) * S ((dst_negative_code_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)) + ((dst_negative_scale_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)) * S ((dst_negative_code_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)) + ((dst_negative_scale_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput))) + (((dst_negative_code_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)) * S ((dst_negative_code_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)) + ((dst_negative_scale_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_exists_resultrowrow_sumsliceentryoutputpositive. ff_h_pvs_exists_resultrowrow_sumsliceentryoutputpositive + S (dst_positive_exists_resultrowrow_sumsliceentryoutput) = S ((S (srs_index_exists_resultrowrow_sumslice)) * dst_positive_scale_exists_resultrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_exists_resultrowrow_sumsliceentryoutputpositive. dst_positive_code_exists_resultrowrow_sumsliceentryoutput = ff_q_pvs_exists_resultrowrow_sumsliceentryoutputpositive * S ((S (srs_index_exists_resultrowrow_sumslice)) * dst_positive_scale_exists_resultrowrow_sumsliceentryoutput) + (dst_positive_exists_resultrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_exists_resultrowrow_sumsliceentryoutputnegative. ff_h_pvs_exists_resultrowrow_sumsliceentryoutputnegative + S (dst_negative_exists_resultrowrow_sumsliceentryoutput) = S ((S (srs_index_exists_resultrowrow_sumslice)) * dst_negative_scale_exists_resultrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_exists_resultrowrow_sumsliceentryoutputnegative. dst_negative_code_exists_resultrowrow_sumsliceentryoutput = ff_q_pvs_exists_resultrowrow_sumsliceentryoutputnegative * S ((S (srs_index_exists_resultrowrow_sumslice)) * dst_negative_scale_exists_resultrowrow_sumsliceentryoutput) + (dst_negative_exists_resultrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_exists_resultrowrow_sumsliceentryoutputvalue ge_balance_negative_exists_resultrowrow_sumsliceentryoutputvalue. (((((srs_value_exists_resultrowrow_sumslice) = 2 * (ge_balance_positive_exists_resultrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_exists_resultrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_exists_resultrowrow_sumsliceentryoutputvaluedecode. (((srs_value_exists_resultrowrow_sumslice) = 2 * ge_signed_half_exists_resultrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_exists_resultrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_exists_resultrowrow_sumsliceentryoutputvalue) = S ge_signed_half_exists_resultrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_exists_resultrowrow_sumsliceentryoutput) + ge_balance_negative_exists_resultrowrow_sumsliceentryoutputvalue = (dst_negative_exists_resultrowrow_sumsliceentryoutput) + ge_balance_positive_exists_resultrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_exists_resultrowrow_sumsum dst_positive_scale_exists_resultrowrow_sumsum dst_negative_code_exists_resultrowrow_sumsum dst_negative_scale_exists_resultrowrow_sumsum dst_positive_sum_exists_resultrowrow_sumsum dst_negative_sum_exists_resultrowrow_sumsum. (((srs_slice_exists_resultrowrow_sum) = (((((dst_positive_code_exists_resultrowrow_sumsum) + (dst_positive_scale_exists_resultrowrow_sumsum)) * S ((dst_positive_code_exists_resultrowrow_sumsum) + (dst_positive_scale_exists_resultrowrow_sumsum)) + ((dst_positive_scale_exists_resultrowrow_sumsum) + (dst_positive_scale_exists_resultrowrow_sumsum))) + (((dst_negative_code_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)) * S ((dst_negative_code_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)) + ((dst_negative_scale_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)))) * S ((((dst_positive_code_exists_resultrowrow_sumsum) + (dst_positive_scale_exists_resultrowrow_sumsum)) * S ((dst_positive_code_exists_resultrowrow_sumsum) + (dst_positive_scale_exists_resultrowrow_sumsum)) + ((dst_positive_scale_exists_resultrowrow_sumsum) + (dst_positive_scale_exists_resultrowrow_sumsum))) + (((dst_negative_code_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)) * S ((dst_negative_code_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)) + ((dst_negative_scale_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)))) + ((((dst_negative_code_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)) * S ((dst_negative_code_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)) + ((dst_negative_scale_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum))) + (((dst_negative_code_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)) * S ((dst_negative_code_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)) + ((dst_negative_scale_exists_resultrowrow_sumsum) + (dst_negative_scale_exists_resultrowrow_sumsum)))))) /\ (((exists fs_u_dst_exists_resultrowrow_sumsumpositive fs_v_dst_exists_resultrowrow_sumsumpositive. ((((exists fs_h_dst_exists_resultrowrow_sumsumpositive_body_start. fs_h_dst_exists_resultrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_exists_resultrowrow_sumsumpositive)) /\ exists fs_q_dst_exists_resultrowrow_sumsumpositive_body_start. fs_u_dst_exists_resultrowrow_sumsumpositive = fs_q_dst_exists_resultrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_exists_resultrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_exists_resultrowrow_sumsumpositive_body_terminal. fs_h_dst_exists_resultrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_exists_resultrowrow_sumsum) = S ((S (n)) * fs_v_dst_exists_resultrowrow_sumsumpositive)) /\ exists fs_q_dst_exists_resultrowrow_sumsumpositive_body_terminal. fs_u_dst_exists_resultrowrow_sumsumpositive = fs_q_dst_exists_resultrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_exists_resultrowrow_sumsumpositive) + (dst_positive_sum_exists_resultrowrow_sumsum))) /\ forall fs_i_dst_exists_resultrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_exists_resultrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_exists_resultrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_exists_resultrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_exists_resultrowrow_sumsumpositive_body_steps fs_r_dst_exists_resultrowrow_sumsumpositive_body_steps fs_s_dst_exists_resultrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_exists_resultrowrow_sumsumpositive_body_steps_summand. fs_h_dst_exists_resultrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_exists_resultrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_exists_resultrowrow_sumsumpositive_body_steps)) * dst_positive_scale_exists_resultrowrow_sumsum)) /\ exists fs_q_dst_exists_resultrowrow_sumsumpositive_body_steps_summand. dst_positive_code_exists_resultrowrow_sumsum = fs_q_dst_exists_resultrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_exists_resultrowrow_sumsumpositive_body_steps)) * dst_positive_scale_exists_resultrowrow_sumsum) + (fs_a_dst_exists_resultrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_exists_resultrowrow_sumsumpositive_body_steps_partial. fs_h_dst_exists_resultrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_exists_resultrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_exists_resultrowrow_sumsumpositive_body_steps)) * fs_v_dst_exists_resultrowrow_sumsumpositive)) /\ exists fs_q_dst_exists_resultrowrow_sumsumpositive_body_steps_partial. fs_u_dst_exists_resultrowrow_sumsumpositive = fs_q_dst_exists_resultrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_exists_resultrowrow_sumsumpositive_body_steps)) * fs_v_dst_exists_resultrowrow_sumsumpositive) + (fs_r_dst_exists_resultrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_exists_resultrowrow_sumsumpositive_body_steps_successor. fs_h_dst_exists_resultrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_exists_resultrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_exists_resultrowrow_sumsumpositive_body_steps)) * fs_v_dst_exists_resultrowrow_sumsumpositive)) /\ exists fs_q_dst_exists_resultrowrow_sumsumpositive_body_steps_successor. fs_u_dst_exists_resultrowrow_sumsumpositive = fs_q_dst_exists_resultrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_exists_resultrowrow_sumsumpositive_body_steps)) * fs_v_dst_exists_resultrowrow_sumsumpositive) + (fs_s_dst_exists_resultrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_exists_resultrowrow_sumsumpositive_body_steps = fs_r_dst_exists_resultrowrow_sumsumpositive_body_steps + fs_a_dst_exists_resultrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_exists_resultrowrow_sumsumnegative fs_v_dst_exists_resultrowrow_sumsumnegative. ((((exists fs_h_dst_exists_resultrowrow_sumsumnegative_body_start. fs_h_dst_exists_resultrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_exists_resultrowrow_sumsumnegative)) /\ exists fs_q_dst_exists_resultrowrow_sumsumnegative_body_start. fs_u_dst_exists_resultrowrow_sumsumnegative = fs_q_dst_exists_resultrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_exists_resultrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_exists_resultrowrow_sumsumnegative_body_terminal. fs_h_dst_exists_resultrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_exists_resultrowrow_sumsum) = S ((S (n)) * fs_v_dst_exists_resultrowrow_sumsumnegative)) /\ exists fs_q_dst_exists_resultrowrow_sumsumnegative_body_terminal. fs_u_dst_exists_resultrowrow_sumsumnegative = fs_q_dst_exists_resultrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_exists_resultrowrow_sumsumnegative) + (dst_negative_sum_exists_resultrowrow_sumsum))) /\ forall fs_i_dst_exists_resultrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_exists_resultrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_exists_resultrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_exists_resultrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_exists_resultrowrow_sumsumnegative_body_steps fs_r_dst_exists_resultrowrow_sumsumnegative_body_steps fs_s_dst_exists_resultrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_exists_resultrowrow_sumsumnegative_body_steps_summand. fs_h_dst_exists_resultrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_exists_resultrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_exists_resultrowrow_sumsumnegative_body_steps)) * dst_negative_scale_exists_resultrowrow_sumsum)) /\ exists fs_q_dst_exists_resultrowrow_sumsumnegative_body_steps_summand. dst_negative_code_exists_resultrowrow_sumsum = fs_q_dst_exists_resultrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_exists_resultrowrow_sumsumnegative_body_steps)) * dst_negative_scale_exists_resultrowrow_sumsum) + (fs_a_dst_exists_resultrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_exists_resultrowrow_sumsumnegative_body_steps_partial. fs_h_dst_exists_resultrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_exists_resultrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_exists_resultrowrow_sumsumnegative_body_steps)) * fs_v_dst_exists_resultrowrow_sumsumnegative)) /\ exists fs_q_dst_exists_resultrowrow_sumsumnegative_body_steps_partial. fs_u_dst_exists_resultrowrow_sumsumnegative = fs_q_dst_exists_resultrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_exists_resultrowrow_sumsumnegative_body_steps)) * fs_v_dst_exists_resultrowrow_sumsumnegative) + (fs_r_dst_exists_resultrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_exists_resultrowrow_sumsumnegative_body_steps_successor. fs_h_dst_exists_resultrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_exists_resultrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_exists_resultrowrow_sumsumnegative_body_steps)) * fs_v_dst_exists_resultrowrow_sumsumnegative)) /\ exists fs_q_dst_exists_resultrowrow_sumsumnegative_body_steps_successor. fs_u_dst_exists_resultrowrow_sumsumnegative = fs_q_dst_exists_resultrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_exists_resultrowrow_sumsumnegative_body_steps)) * fs_v_dst_exists_resultrowrow_sumsumnegative) + (fs_s_dst_exists_resultrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_exists_resultrowrow_sumsumnegative_body_steps = fs_r_dst_exists_resultrowrow_sumsumnegative_body_steps + fs_a_dst_exists_resultrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_exists_resultrowrow_sumsumresult ge_balance_negative_exists_resultrowrow_sumsumresult. (((((srt_value_exists_result) = 2 * (ge_balance_positive_exists_resultrowrow_sumsumresult) /\ (ge_balance_negative_exists_resultrowrow_sumsumresult) = 0) \/ exists ge_signed_half_exists_resultrowrow_sumsumresultdecode. (((srt_value_exists_result) = 2 * ge_signed_half_exists_resultrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_exists_resultrowrow_sumsumresult) = 0) /\ (ge_balance_negative_exists_resultrowrow_sumsumresult) = S ge_signed_half_exists_resultrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_exists_resultrowrow_sumsum) + ge_balance_negative_exists_resultrowrow_sumsumresult = (dst_negative_sum_exists_resultrowrow_sumsum) + ge_balance_positive_exists_resultrowrow_sumsumresult))))))))))))))))))

Complete tactic proof in conservative notation

All 75 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

75 script commands · 17 reading checkpoints · 3 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)
signed rectangular row sums emptysigned rectangular slice sum existssigned rectangular row sums extend
01Induction on mL1–7

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction m
  2. L2
    intro F
  3. L3
    intro o
  4. L4
    intro s
  5. L5
    intro t
  6. L6
    intro n
  7. L7
    intro hF
02Construct an explicit witnessL8–8

Supply the displayed value, then prove that it has the required property.

  1. L8
    exists ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))
03Use earlier factsL9–18

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L9
    specialize signed_rectangular_row_sums_empty (F)
  2. L10
    specialize signed_rectangular_row_sums_empty (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  3. L11
    specialize signed_rectangular_row_sums_empty (o)
  4. L12
    specialize signed_rectangular_row_sums_empty (s)
  5. L13
    specialize signed_rectangular_row_sums_empty (t)
  6. L14
    specialize signed_rectangular_row_sums_empty (n)
  7. L15
    apply signed_rectangular_row_sums_empty
  8. L16
    exact hF
  9. L17
    specialize divisor_signed_table_from_components (0)
  10. L18
    specialize divisor_signed_table_from_components (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
04Use earlier factsL19–23

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L19
    specialize divisor_signed_table_from_components (0)
  2. L20
    specialize divisor_signed_table_from_components (0)
  3. L21
    specialize divisor_signed_table_from_components (0)
  4. L22
    specialize divisor_signed_table_from_components (0)
  5. L23
    apply divisor_signed_table_from_components
05Calculate and transport equalitiesL24–24

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L24
    refl
06Fix variables and assumptionsL25–30

Work with arbitrary variables or the premises of the current implication.

  1. L25
    intro F
  2. L26
    intro o
  3. L27
    intro s
  4. L28
    intro t
  5. L29
    intro n
  6. L30
    intro hF
07Establish hpL31–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L31
    have hp : ∃ R. ArithRowSums(F,R,o,s,t,m,n)Definitions: ArithRowSums(F,R,o,s,t,m,n)Original native command in the exact edition
  2. L32
    specialize IH (F)
  3. L33
    specialize IH (o)
  4. L34
    specialize IH (s)
  5. L35
    specialize IH (t)
  6. L36
    specialize IH (n)
  7. L37
    apply IH
  8. L38
    exact hF
08Separate the logical casesL39–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    cases hp
09Establish hvL40–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed rectangular slice sum exists.

  1. L40
    have hv : ∃ z. SignedSliceSum(F,o + s · m,t,n,z)Definitions: SignedSliceSum(F,o + s · m,t,n,z)Original native command in the exact edition
  2. L41
    specialize signed_rectangular_slice_sum_exists (F)
  3. L42
    specialize signed_rectangular_slice_sum_exists (((o) + ((s) * (m))))
  4. L43
    specialize signed_rectangular_slice_sum_exists (t)
  5. L44
    specialize signed_rectangular_slice_sum_exists (n)
  6. L45
    apply signed_rectangular_slice_sum_exists
  7. L46
    exact hF
10Separate the logical casesL47–47

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L47
    cases hv
11Establish heL48–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed table extend at.

  1. L48
    have he : ∃ Q. ArithExtend(x,Q,m,x1)Definitions: ArithExtend(x,Q,m,x1)Original native command in the exact edition
  2. L49
    specialize arithmetic_signed_table_extend_at (m)
  3. L50
    specialize arithmetic_signed_table_extend_at (x)
  4. L51
    specialize arithmetic_signed_table_extend_at (m)
  5. L52
    specialize arithmetic_signed_table_extend_at (x1)
  6. L53
    apply arithmetic_signed_table_extend_at
12Separate the logical casesL54–55

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    cases hp_witness
  2. L55
    cases hp_witness_right
13Use earlier factsL56–56

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L56
    exact hp_witness_right_left
14Separate the logical casesL57–59

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L57
    cases he
  2. L58
    cases he_witness
  3. L59
    cases he_witness_right
15Construct an explicit witnessL60–60

Supply the displayed value, then prove that it has the required property.

  1. L60
    exists x2
16Use earlier factsL61–70

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L61
    specialize signed_rectangular_row_sums_extend (F)
  2. L62
    specialize signed_rectangular_row_sums_extend (x)
  3. L63
    specialize signed_rectangular_row_sums_extend (x2)
  4. L64
    specialize signed_rectangular_row_sums_extend (o)
  5. L65
    specialize signed_rectangular_row_sums_extend (s)
  6. L66
    specialize signed_rectangular_row_sums_extend (t)
  7. L67
    specialize signed_rectangular_row_sums_extend (m)
  8. L68
    specialize signed_rectangular_row_sums_extend (n)
  9. L69
    specialize signed_rectangular_row_sums_extend (x1)
  10. L70
    apply signed_rectangular_row_sums_extend
17Use earlier factsL71–75

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L71
    exact hp_witness
  2. L72
    exact he_witness_left
  3. L73
    exact he_witness_right_left
  4. L74
    exact he_witness_right_right
  5. L75
    exact hv_witness

Library-wide reading audit

Original defined command ledger · 75 lines
  1. 0001induction m
  2. 0002intro F
  3. 0003intro o
  4. 0004intro s
  5. 0005intro t
  6. 0006intro n
  7. 0007intro hF
  8. 0008exists ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))
  9. 0009specialize signed_rectangular_row_sums_empty (F)
  10. 0010specialize signed_rectangular_row_sums_empty (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  11. 0011specialize signed_rectangular_row_sums_empty (o)
  12. 0012specialize signed_rectangular_row_sums_empty (s)
  13. 0013specialize signed_rectangular_row_sums_empty (t)
  14. 0014specialize signed_rectangular_row_sums_empty (n)
  15. 0015apply signed_rectangular_row_sums_empty
  16. 0016exact hF
  17. 0017specialize divisor_signed_table_from_components (0)
  18. 0018specialize divisor_signed_table_from_components (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  19. 0019specialize divisor_signed_table_from_components (0)
  20. 0020specialize divisor_signed_table_from_components (0)
  21. 0021specialize divisor_signed_table_from_components (0)
  22. 0022specialize divisor_signed_table_from_components (0)
  23. 0023apply divisor_signed_table_from_components
  24. 0024refl
  25. 0025intro F
  26. 0026intro o
  27. 0027intro s
  28. 0028intro t
  29. 0029intro n
  30. 0030intro hF
  31. 0031have hp : ∃ R. ArithRowSums(F,R,o,s,t,m,n)
  32. 0032specialize IH (F)
  33. 0033specialize IH (o)
  34. 0034specialize IH (s)
  35. 0035specialize IH (t)
  36. 0036specialize IH (n)
  37. 0037apply IH
  38. 0038exact hF
  39. 0039cases hp
  40. 0040have hv : ∃ z. SignedSliceSum(F,o + s · m,t,n,z)
  41. 0041specialize signed_rectangular_slice_sum_exists (F)
  42. 0042specialize signed_rectangular_slice_sum_exists (((o) + ((s) * (m))))
  43. 0043specialize signed_rectangular_slice_sum_exists (t)
  44. 0044specialize signed_rectangular_slice_sum_exists (n)
  45. 0045apply signed_rectangular_slice_sum_exists
  46. 0046exact hF
  47. 0047cases hv
  48. 0048have he : ∃ Q. ArithExtend(x,Q,m,x1)
  49. 0049specialize arithmetic_signed_table_extend_at (m)
  50. 0050specialize arithmetic_signed_table_extend_at (x)
  51. 0051specialize arithmetic_signed_table_extend_at (m)
  52. 0052specialize arithmetic_signed_table_extend_at (x1)
  53. 0053apply arithmetic_signed_table_extend_at
  54. 0054cases hp_witness
  55. 0055cases hp_witness_right
  56. 0056exact hp_witness_right_left
  57. 0057cases he
  58. 0058cases he_witness
  59. 0059cases he_witness_right
  60. 0060exists x2
  61. 0061specialize signed_rectangular_row_sums_extend (F)
  62. 0062specialize signed_rectangular_row_sums_extend (x)
  63. 0063specialize signed_rectangular_row_sums_extend (x2)
  64. 0064specialize signed_rectangular_row_sums_extend (o)
  65. 0065specialize signed_rectangular_row_sums_extend (s)
  66. 0066specialize signed_rectangular_row_sums_extend (t)
  67. 0067specialize signed_rectangular_row_sums_extend (m)
  68. 0068specialize signed_rectangular_row_sums_extend (n)
  69. 0069specialize signed_rectangular_row_sums_extend (x1)
  70. 0070apply signed_rectangular_row_sums_extend
  71. 0071exact hp_witness
  72. 0072exact he_witness_left
  73. 0073exact he_witness_right_left
  74. 0074exact he_witness_right_right
  75. 0075exact hv_witness