RS001B

signed_rectangular_row_sums_zero_inner

Induction proves the sum of any actual table of empty row sums is zero; a positive number of zero-length rows is not silently discarded.

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. ∀ R. ∀ o. ∀ s. ∀ t. ∀ z. ArithRowSums(F,R,o,s,t,m,0) → SignedPrefixSum(R,m,z) → z = 0

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

Definition DAG

SignedAdd(a,b,c) · 1ArithAt(F,i,z) · 1SignedPrefixSum(F,l,z) · 2ArithRowSums(F,R,o,s,t,m,n) · 1

Actual proof prerequisites

divisor_signed_sum_empty_value · checked external prerequisitedivisor_signed_sum_successor_decompose · checked external prerequisitesigned_rectangular_row_sums_restrict_outersigned_rectangular_slice_sum_empty_valuesigned_rectangular_row_sums_lookuple_refl · checked external prerequisitesigned_add_functional · checked external prerequisitesigned_add_zero_left · checked external prerequisite
Original expanded first-order statement 
forall m F R o s t z. (((exists dst_positive_code_zero_inner_rowssource_table dst_positive_scale_zero_inner_rowssource_table dst_negative_code_zero_inner_rowssource_table dst_negative_scale_zero_inner_rowssource_table. (((F) = (((((dst_positive_code_zero_inner_rowssource_table) + (dst_positive_scale_zero_inner_rowssource_table)) * S ((dst_positive_code_zero_inner_rowssource_table) + (dst_positive_scale_zero_inner_rowssource_table)) + ((dst_positive_scale_zero_inner_rowssource_table) + (dst_positive_scale_zero_inner_rowssource_table))) + (((dst_negative_code_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)) * S ((dst_negative_code_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)) + ((dst_negative_scale_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)))) * S ((((dst_positive_code_zero_inner_rowssource_table) + (dst_positive_scale_zero_inner_rowssource_table)) * S ((dst_positive_code_zero_inner_rowssource_table) + (dst_positive_scale_zero_inner_rowssource_table)) + ((dst_positive_scale_zero_inner_rowssource_table) + (dst_positive_scale_zero_inner_rowssource_table))) + (((dst_negative_code_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)) * S ((dst_negative_code_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)) + ((dst_negative_scale_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)))) + ((((dst_negative_code_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)) * S ((dst_negative_code_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)) + ((dst_negative_scale_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table))) + (((dst_negative_code_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)) * S ((dst_negative_code_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)) + ((dst_negative_scale_zero_inner_rowssource_table) + (dst_negative_scale_zero_inner_rowssource_table)))))) /\ (forall dst_index_zero_inner_rowssource_table. (exists pvs_le_gap_zero_inner_rowssource_tabledomain. pvs_le_gap_zero_inner_rowssource_tabledomain + (dst_index_zero_inner_rowssource_table) = (0)) -> exists dst_positive_zero_inner_rowssource_table dst_negative_zero_inner_rowssource_table dst_value_zero_inner_rowssource_table. ((((exists ff_h_pvs_zero_inner_rowssource_tableentrypositive. ff_h_pvs_zero_inner_rowssource_tableentrypositive + S (dst_positive_zero_inner_rowssource_table) = S ((S (dst_index_zero_inner_rowssource_table)) * dst_positive_scale_zero_inner_rowssource_table)) /\ exists ff_q_pvs_zero_inner_rowssource_tableentrypositive. dst_positive_code_zero_inner_rowssource_table = ff_q_pvs_zero_inner_rowssource_tableentrypositive * S ((S (dst_index_zero_inner_rowssource_table)) * dst_positive_scale_zero_inner_rowssource_table) + (dst_positive_zero_inner_rowssource_table))) /\ (((((exists ff_h_pvs_zero_inner_rowssource_tableentrynegative. ff_h_pvs_zero_inner_rowssource_tableentrynegative + S (dst_negative_zero_inner_rowssource_table) = S ((S (dst_index_zero_inner_rowssource_table)) * dst_negative_scale_zero_inner_rowssource_table)) /\ exists ff_q_pvs_zero_inner_rowssource_tableentrynegative. dst_negative_code_zero_inner_rowssource_table = ff_q_pvs_zero_inner_rowssource_tableentrynegative * S ((S (dst_index_zero_inner_rowssource_table)) * dst_negative_scale_zero_inner_rowssource_table) + (dst_negative_zero_inner_rowssource_table))) /\ (exists ge_balance_positive_zero_inner_rowssource_tableentryvalue ge_balance_negative_zero_inner_rowssource_tableentryvalue. (((((dst_value_zero_inner_rowssource_table) = 2 * (ge_balance_positive_zero_inner_rowssource_tableentryvalue) /\ (ge_balance_negative_zero_inner_rowssource_tableentryvalue) = 0) \/ exists ge_signed_half_zero_inner_rowssource_tableentryvaluedecode. (((dst_value_zero_inner_rowssource_table) = 2 * ge_signed_half_zero_inner_rowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_zero_inner_rowssource_tableentryvalue) = 0) /\ (ge_balance_negative_zero_inner_rowssource_tableentryvalue) = S ge_signed_half_zero_inner_rowssource_tableentryvaluedecode))) /\ ((dst_positive_zero_inner_rowssource_table) + ge_balance_negative_zero_inner_rowssource_tableentryvalue = (dst_negative_zero_inner_rowssource_table) + ge_balance_positive_zero_inner_rowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_zero_inner_rowsrow_table dst_positive_scale_zero_inner_rowsrow_table dst_negative_code_zero_inner_rowsrow_table dst_negative_scale_zero_inner_rowsrow_table. (((R) = (((((dst_positive_code_zero_inner_rowsrow_table) + (dst_positive_scale_zero_inner_rowsrow_table)) * S ((dst_positive_code_zero_inner_rowsrow_table) + (dst_positive_scale_zero_inner_rowsrow_table)) + ((dst_positive_scale_zero_inner_rowsrow_table) + (dst_positive_scale_zero_inner_rowsrow_table))) + (((dst_negative_code_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)) * S ((dst_negative_code_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)) + ((dst_negative_scale_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)))) * S ((((dst_positive_code_zero_inner_rowsrow_table) + (dst_positive_scale_zero_inner_rowsrow_table)) * S ((dst_positive_code_zero_inner_rowsrow_table) + (dst_positive_scale_zero_inner_rowsrow_table)) + ((dst_positive_scale_zero_inner_rowsrow_table) + (dst_positive_scale_zero_inner_rowsrow_table))) + (((dst_negative_code_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)) * S ((dst_negative_code_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)) + ((dst_negative_scale_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)))) + ((((dst_negative_code_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)) * S ((dst_negative_code_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)) + ((dst_negative_scale_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table))) + (((dst_negative_code_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)) * S ((dst_negative_code_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)) + ((dst_negative_scale_zero_inner_rowsrow_table) + (dst_negative_scale_zero_inner_rowsrow_table)))))) /\ (forall dst_index_zero_inner_rowsrow_table. (exists pvs_le_gap_zero_inner_rowsrow_tabledomain. pvs_le_gap_zero_inner_rowsrow_tabledomain + (dst_index_zero_inner_rowsrow_table) = (m)) -> exists dst_positive_zero_inner_rowsrow_table dst_negative_zero_inner_rowsrow_table dst_value_zero_inner_rowsrow_table. ((((exists ff_h_pvs_zero_inner_rowsrow_tableentrypositive. ff_h_pvs_zero_inner_rowsrow_tableentrypositive + S (dst_positive_zero_inner_rowsrow_table) = S ((S (dst_index_zero_inner_rowsrow_table)) * dst_positive_scale_zero_inner_rowsrow_table)) /\ exists ff_q_pvs_zero_inner_rowsrow_tableentrypositive. dst_positive_code_zero_inner_rowsrow_table = ff_q_pvs_zero_inner_rowsrow_tableentrypositive * S ((S (dst_index_zero_inner_rowsrow_table)) * dst_positive_scale_zero_inner_rowsrow_table) + (dst_positive_zero_inner_rowsrow_table))) /\ (((((exists ff_h_pvs_zero_inner_rowsrow_tableentrynegative. ff_h_pvs_zero_inner_rowsrow_tableentrynegative + S (dst_negative_zero_inner_rowsrow_table) = S ((S (dst_index_zero_inner_rowsrow_table)) * dst_negative_scale_zero_inner_rowsrow_table)) /\ exists ff_q_pvs_zero_inner_rowsrow_tableentrynegative. dst_negative_code_zero_inner_rowsrow_table = ff_q_pvs_zero_inner_rowsrow_tableentrynegative * S ((S (dst_index_zero_inner_rowsrow_table)) * dst_negative_scale_zero_inner_rowsrow_table) + (dst_negative_zero_inner_rowsrow_table))) /\ (exists ge_balance_positive_zero_inner_rowsrow_tableentryvalue ge_balance_negative_zero_inner_rowsrow_tableentryvalue. (((((dst_value_zero_inner_rowsrow_table) = 2 * (ge_balance_positive_zero_inner_rowsrow_tableentryvalue) /\ (ge_balance_negative_zero_inner_rowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_zero_inner_rowsrow_tableentryvaluedecode. (((dst_value_zero_inner_rowsrow_table) = 2 * ge_signed_half_zero_inner_rowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_zero_inner_rowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_zero_inner_rowsrow_tableentryvalue) = S ge_signed_half_zero_inner_rowsrow_tableentryvaluedecode))) /\ ((dst_positive_zero_inner_rowsrow_table) + ge_balance_negative_zero_inner_rowsrow_tableentryvalue = (dst_negative_zero_inner_rowsrow_table) + ge_balance_positive_zero_inner_rowsrow_tableentryvalue))))))))) /\ (forall srt_index_zero_inner_rows. (exists pvs_gap_zero_inner_rowsbound. pvs_gap_zero_inner_rowsbound + S (srt_index_zero_inner_rows) = (m)) -> exists srt_value_zero_inner_rows. (((exists dst_positive_code_zero_inner_rowsrowentry dst_positive_scale_zero_inner_rowsrowentry dst_negative_code_zero_inner_rowsrowentry dst_negative_scale_zero_inner_rowsrowentry dst_positive_zero_inner_rowsrowentry dst_negative_zero_inner_rowsrowentry. (((R) = (((((dst_positive_code_zero_inner_rowsrowentry) + (dst_positive_scale_zero_inner_rowsrowentry)) * S ((dst_positive_code_zero_inner_rowsrowentry) + (dst_positive_scale_zero_inner_rowsrowentry)) + ((dst_positive_scale_zero_inner_rowsrowentry) + (dst_positive_scale_zero_inner_rowsrowentry))) + (((dst_negative_code_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)) * S ((dst_negative_code_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)) + ((dst_negative_scale_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)))) * S ((((dst_positive_code_zero_inner_rowsrowentry) + (dst_positive_scale_zero_inner_rowsrowentry)) * S ((dst_positive_code_zero_inner_rowsrowentry) + (dst_positive_scale_zero_inner_rowsrowentry)) + ((dst_positive_scale_zero_inner_rowsrowentry) + (dst_positive_scale_zero_inner_rowsrowentry))) + (((dst_negative_code_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)) * S ((dst_negative_code_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)) + ((dst_negative_scale_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)))) + ((((dst_negative_code_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)) * S ((dst_negative_code_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)) + ((dst_negative_scale_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry))) + (((dst_negative_code_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)) * S ((dst_negative_code_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)) + ((dst_negative_scale_zero_inner_rowsrowentry) + (dst_negative_scale_zero_inner_rowsrowentry)))))) /\ (((((exists ff_h_pvs_zero_inner_rowsrowentrypositive. ff_h_pvs_zero_inner_rowsrowentrypositive + S (dst_positive_zero_inner_rowsrowentry) = S ((S (srt_index_zero_inner_rows)) * dst_positive_scale_zero_inner_rowsrowentry)) /\ exists ff_q_pvs_zero_inner_rowsrowentrypositive. dst_positive_code_zero_inner_rowsrowentry = ff_q_pvs_zero_inner_rowsrowentrypositive * S ((S (srt_index_zero_inner_rows)) * dst_positive_scale_zero_inner_rowsrowentry) + (dst_positive_zero_inner_rowsrowentry))) /\ (((((exists ff_h_pvs_zero_inner_rowsrowentrynegative. ff_h_pvs_zero_inner_rowsrowentrynegative + S (dst_negative_zero_inner_rowsrowentry) = S ((S (srt_index_zero_inner_rows)) * dst_negative_scale_zero_inner_rowsrowentry)) /\ exists ff_q_pvs_zero_inner_rowsrowentrynegative. dst_negative_code_zero_inner_rowsrowentry = ff_q_pvs_zero_inner_rowsrowentrynegative * S ((S (srt_index_zero_inner_rows)) * dst_negative_scale_zero_inner_rowsrowentry) + (dst_negative_zero_inner_rowsrowentry))) /\ (exists ge_balance_positive_zero_inner_rowsrowentryvalue ge_balance_negative_zero_inner_rowsrowentryvalue. (((((srt_value_zero_inner_rows) = 2 * (ge_balance_positive_zero_inner_rowsrowentryvalue) /\ (ge_balance_negative_zero_inner_rowsrowentryvalue) = 0) \/ exists ge_signed_half_zero_inner_rowsrowentryvaluedecode. (((srt_value_zero_inner_rows) = 2 * ge_signed_half_zero_inner_rowsrowentryvaluedecode + 1 /\ (ge_balance_positive_zero_inner_rowsrowentryvalue) = 0) /\ (ge_balance_negative_zero_inner_rowsrowentryvalue) = S ge_signed_half_zero_inner_rowsrowentryvaluedecode))) /\ ((dst_positive_zero_inner_rowsrowentry) + ge_balance_negative_zero_inner_rowsrowentryvalue = (dst_negative_zero_inner_rowsrowentry) + ge_balance_positive_zero_inner_rowsrowentryvalue))))))))) /\ (exists srs_slice_zero_inner_rowsrowrow_sum. ((((exists dst_positive_code_zero_inner_rowsrowrow_sumslicesource_table dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table dst_negative_code_zero_inner_rowsrowrow_sumslicesource_table dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table)) * S ((dst_positive_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table)) + ((dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table)) * S ((dst_positive_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table)) + ((dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_zero_inner_rowsrowrow_sumslicesource_table. (exists pvs_le_gap_zero_inner_rowsrowrow_sumslicesource_tabledomain. pvs_le_gap_zero_inner_rowsrowrow_sumslicesource_tabledomain + (dst_index_zero_inner_rowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_zero_inner_rowsrowrow_sumslicesource_table dst_negative_zero_inner_rowsrowrow_sumslicesource_table dst_value_zero_inner_rowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_zero_inner_rowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_zero_inner_rowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_zero_inner_rowsrowrow_sumslicesource_table) = S ((S (dst_index_zero_inner_rowsrowrow_sumslicesource_table)) * dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_zero_inner_rowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_zero_inner_rowsrowrow_sumslicesource_table = ff_q_pvs_zero_inner_rowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_zero_inner_rowsrowrow_sumslicesource_table)) * dst_positive_scale_zero_inner_rowsrowrow_sumslicesource_table) + (dst_positive_zero_inner_rowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_zero_inner_rowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_zero_inner_rowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_zero_inner_rowsrowrow_sumslicesource_table) = S ((S (dst_index_zero_inner_rowsrowrow_sumslicesource_table)) * dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_zero_inner_rowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_zero_inner_rowsrowrow_sumslicesource_table = ff_q_pvs_zero_inner_rowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_zero_inner_rowsrowrow_sumslicesource_table)) * dst_negative_scale_zero_inner_rowsrowrow_sumslicesource_table) + (dst_negative_zero_inner_rowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_zero_inner_rowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_zero_inner_rowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_zero_inner_rowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_zero_inner_rowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_zero_inner_rowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_zero_inner_rowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_zero_inner_rowsrowrow_sumslicesource_table) = 2 * ge_signed_half_zero_inner_rowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_zero_inner_rowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_zero_inner_rowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_zero_inner_rowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_zero_inner_rowsrowrow_sumslicesource_table) + ge_balance_negative_zero_inner_rowsrowrow_sumslicesource_tableentryvalue = (dst_negative_zero_inner_rowsrowrow_sumslicesource_table) + ge_balance_positive_zero_inner_rowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_zero_inner_rowsrowrow_sumsliceoutput_table dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table dst_negative_code_zero_inner_rowsrowrow_sumsliceoutput_table dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table. (((srs_slice_zero_inner_rowsrowrow_sum) = (((((dst_positive_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_zero_inner_rowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_zero_inner_rowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_zero_inner_rowsrowrow_sumsliceoutput_tabledomain + (dst_index_zero_inner_rowsrowrow_sumsliceoutput_table) = (0)) -> exists dst_positive_zero_inner_rowsrowrow_sumsliceoutput_table dst_negative_zero_inner_rowsrowrow_sumsliceoutput_table dst_value_zero_inner_rowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_zero_inner_rowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_zero_inner_rowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_zero_inner_rowsrowrow_sumsliceoutput_table) = S ((S (dst_index_zero_inner_rowsrowrow_sumsliceoutput_table)) * dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_zero_inner_rowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_zero_inner_rowsrowrow_sumsliceoutput_table = ff_q_pvs_zero_inner_rowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_zero_inner_rowsrowrow_sumsliceoutput_table)) * dst_positive_scale_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_positive_zero_inner_rowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_zero_inner_rowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_zero_inner_rowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_zero_inner_rowsrowrow_sumsliceoutput_table) = S ((S (dst_index_zero_inner_rowsrowrow_sumsliceoutput_table)) * dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_zero_inner_rowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_zero_inner_rowsrowrow_sumsliceoutput_table = ff_q_pvs_zero_inner_rowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_zero_inner_rowsrowrow_sumsliceoutput_table)) * dst_negative_scale_zero_inner_rowsrowrow_sumsliceoutput_table) + (dst_negative_zero_inner_rowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_zero_inner_rowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_zero_inner_rowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_zero_inner_rowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_zero_inner_rowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_zero_inner_rowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_zero_inner_rowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_zero_inner_rowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_zero_inner_rowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_zero_inner_rowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_zero_inner_rowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_zero_inner_rowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_zero_inner_rowsrowrow_sumsliceoutput_table) + ge_balance_negative_zero_inner_rowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_zero_inner_rowsrowrow_sumsliceoutput_table) + ge_balance_positive_zero_inner_rowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_zero_inner_rowsrowrow_sumslice. (exists pvs_gap_zero_inner_rowsrowrow_sumslicebound. pvs_gap_zero_inner_rowsrowrow_sumslicebound + S (srs_index_zero_inner_rowsrowrow_sumslice) = (0)) -> exists srs_value_zero_inner_rowsrowrow_sumslice. (((exists dst_positive_code_zero_inner_rowsrowrow_sumsliceentrysource dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource dst_negative_code_zero_inner_rowsrowrow_sumsliceentrysource dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource dst_positive_zero_inner_rowsrowrow_sumsliceentrysource dst_negative_zero_inner_rowsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_zero_inner_rowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_zero_inner_rowsrowrow_sumsliceentrysourcepositive + S (dst_positive_zero_inner_rowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_zero_inner_rows)))) + ((t) * (srs_index_zero_inner_rowsrowrow_sumslice))))) * dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_zero_inner_rowsrowrow_sumsliceentrysourcepositive. dst_positive_code_zero_inner_rowsrowrow_sumsliceentrysource = ff_q_pvs_zero_inner_rowsrowrow_sumsliceentrysourcepositive * S ((S (((((o) + ((s) * (srt_index_zero_inner_rows)))) + ((t) * (srs_index_zero_inner_rowsrowrow_sumslice))))) * dst_positive_scale_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_positive_zero_inner_rowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_zero_inner_rowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_zero_inner_rowsrowrow_sumsliceentrysourcenegative + S (dst_negative_zero_inner_rowsrowrow_sumsliceentrysource) = S ((S (((((o) + ((s) * (srt_index_zero_inner_rows)))) + ((t) * (srs_index_zero_inner_rowsrowrow_sumslice))))) * dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_zero_inner_rowsrowrow_sumsliceentrysourcenegative. dst_negative_code_zero_inner_rowsrowrow_sumsliceentrysource = ff_q_pvs_zero_inner_rowsrowrow_sumsliceentrysourcenegative * S ((S (((((o) + ((s) * (srt_index_zero_inner_rows)))) + ((t) * (srs_index_zero_inner_rowsrowrow_sumslice))))) * dst_negative_scale_zero_inner_rowsrowrow_sumsliceentrysource) + (dst_negative_zero_inner_rowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_zero_inner_rowsrowrow_sumsliceentrysourcevalue ge_balance_negative_zero_inner_rowsrowrow_sumsliceentrysourcevalue. (((((srs_value_zero_inner_rowsrowrow_sumslice) = 2 * (ge_balance_positive_zero_inner_rowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_zero_inner_rowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_zero_inner_rowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_zero_inner_rowsrowrow_sumslice) = 2 * ge_signed_half_zero_inner_rowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_zero_inner_rowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_zero_inner_rowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_zero_inner_rowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_zero_inner_rowsrowrow_sumsliceentrysource) + ge_balance_negative_zero_inner_rowsrowrow_sumsliceentrysourcevalue = (dst_negative_zero_inner_rowsrowrow_sumsliceentrysource) + ge_balance_positive_zero_inner_rowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_zero_inner_rowsrowrow_sumsliceentryoutput dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput dst_negative_code_zero_inner_rowsrowrow_sumsliceentryoutput dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput dst_positive_zero_inner_rowsrowrow_sumsliceentryoutput dst_negative_zero_inner_rowsrowrow_sumsliceentryoutput. (((srs_slice_zero_inner_rowsrowrow_sum) = (((((dst_positive_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_zero_inner_rowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_zero_inner_rowsrowrow_sumsliceentryoutputpositive + S (dst_positive_zero_inner_rowsrowrow_sumsliceentryoutput) = S ((S (srs_index_zero_inner_rowsrowrow_sumslice)) * dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_zero_inner_rowsrowrow_sumsliceentryoutputpositive. dst_positive_code_zero_inner_rowsrowrow_sumsliceentryoutput = ff_q_pvs_zero_inner_rowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_zero_inner_rowsrowrow_sumslice)) * dst_positive_scale_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_positive_zero_inner_rowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_zero_inner_rowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_zero_inner_rowsrowrow_sumsliceentryoutputnegative + S (dst_negative_zero_inner_rowsrowrow_sumsliceentryoutput) = S ((S (srs_index_zero_inner_rowsrowrow_sumslice)) * dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_zero_inner_rowsrowrow_sumsliceentryoutputnegative. dst_negative_code_zero_inner_rowsrowrow_sumsliceentryoutput = ff_q_pvs_zero_inner_rowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_zero_inner_rowsrowrow_sumslice)) * dst_negative_scale_zero_inner_rowsrowrow_sumsliceentryoutput) + (dst_negative_zero_inner_rowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_zero_inner_rowsrowrow_sumsliceentryoutputvalue ge_balance_negative_zero_inner_rowsrowrow_sumsliceentryoutputvalue. (((((srs_value_zero_inner_rowsrowrow_sumslice) = 2 * (ge_balance_positive_zero_inner_rowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_zero_inner_rowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_zero_inner_rowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_zero_inner_rowsrowrow_sumslice) = 2 * ge_signed_half_zero_inner_rowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_zero_inner_rowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_zero_inner_rowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_zero_inner_rowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_zero_inner_rowsrowrow_sumsliceentryoutput) + ge_balance_negative_zero_inner_rowsrowrow_sumsliceentryoutputvalue = (dst_negative_zero_inner_rowsrowrow_sumsliceentryoutput) + ge_balance_positive_zero_inner_rowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_zero_inner_rowsrowrow_sumsum dst_positive_scale_zero_inner_rowsrowrow_sumsum dst_negative_code_zero_inner_rowsrowrow_sumsum dst_negative_scale_zero_inner_rowsrowrow_sumsum dst_positive_sum_zero_inner_rowsrowrow_sumsum dst_negative_sum_zero_inner_rowsrowrow_sumsum. (((srs_slice_zero_inner_rowsrowrow_sum) = (((((dst_positive_code_zero_inner_rowsrowrow_sumsum) + (dst_positive_scale_zero_inner_rowsrowrow_sumsum)) * S ((dst_positive_code_zero_inner_rowsrowrow_sumsum) + (dst_positive_scale_zero_inner_rowsrowrow_sumsum)) + ((dst_positive_scale_zero_inner_rowsrowrow_sumsum) + (dst_positive_scale_zero_inner_rowsrowrow_sumsum))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)))) * S ((((dst_positive_code_zero_inner_rowsrowrow_sumsum) + (dst_positive_scale_zero_inner_rowsrowrow_sumsum)) * S ((dst_positive_code_zero_inner_rowsrowrow_sumsum) + (dst_positive_scale_zero_inner_rowsrowrow_sumsum)) + ((dst_positive_scale_zero_inner_rowsrowrow_sumsum) + (dst_positive_scale_zero_inner_rowsrowrow_sumsum))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)))) + ((((dst_negative_code_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum))) + (((dst_negative_code_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)) * S ((dst_negative_code_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)) + ((dst_negative_scale_zero_inner_rowsrowrow_sumsum) + (dst_negative_scale_zero_inner_rowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_zero_inner_rowsrowrow_sumsumpositive fs_v_dst_zero_inner_rowsrowrow_sumsumpositive. ((((exists fs_h_dst_zero_inner_rowsrowrow_sumsumpositive_body_start. fs_h_dst_zero_inner_rowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_inner_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_zero_inner_rowsrowrow_sumsumpositive_body_start. fs_u_dst_zero_inner_rowsrowrow_sumsumpositive = fs_q_dst_zero_inner_rowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_zero_inner_rowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_zero_inner_rowsrowrow_sumsumpositive_body_terminal. fs_h_dst_zero_inner_rowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_zero_inner_rowsrowrow_sumsum) = S ((S (0)) * fs_v_dst_zero_inner_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_zero_inner_rowsrowrow_sumsumpositive_body_terminal. fs_u_dst_zero_inner_rowsrowrow_sumsumpositive = fs_q_dst_zero_inner_rowsrowrow_sumsumpositive_body_terminal * S ((S (0)) * fs_v_dst_zero_inner_rowsrowrow_sumsumpositive) + (dst_positive_sum_zero_inner_rowsrowrow_sumsum))) /\ forall fs_i_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps = 0) -> exists fs_a_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps fs_r_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps fs_s_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_zero_inner_rowsrowrow_sumsum)) /\ exists fs_q_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_zero_inner_rowsrowrow_sumsum = fs_q_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_zero_inner_rowsrowrow_sumsum) + (fs_a_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_zero_inner_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_zero_inner_rowsrowrow_sumsumpositive = fs_q_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_zero_inner_rowsrowrow_sumsumpositive) + (fs_r_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_zero_inner_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_zero_inner_rowsrowrow_sumsumpositive = fs_q_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_zero_inner_rowsrowrow_sumsumpositive) + (fs_s_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps = fs_r_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps + fs_a_dst_zero_inner_rowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_zero_inner_rowsrowrow_sumsumnegative fs_v_dst_zero_inner_rowsrowrow_sumsumnegative. ((((exists fs_h_dst_zero_inner_rowsrowrow_sumsumnegative_body_start. fs_h_dst_zero_inner_rowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_inner_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_zero_inner_rowsrowrow_sumsumnegative_body_start. fs_u_dst_zero_inner_rowsrowrow_sumsumnegative = fs_q_dst_zero_inner_rowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_zero_inner_rowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_zero_inner_rowsrowrow_sumsumnegative_body_terminal. fs_h_dst_zero_inner_rowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_zero_inner_rowsrowrow_sumsum) = S ((S (0)) * fs_v_dst_zero_inner_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_zero_inner_rowsrowrow_sumsumnegative_body_terminal. fs_u_dst_zero_inner_rowsrowrow_sumsumnegative = fs_q_dst_zero_inner_rowsrowrow_sumsumnegative_body_terminal * S ((S (0)) * fs_v_dst_zero_inner_rowsrowrow_sumsumnegative) + (dst_negative_sum_zero_inner_rowsrowrow_sumsum))) /\ forall fs_i_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps = 0) -> exists fs_a_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps fs_r_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps fs_s_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_zero_inner_rowsrowrow_sumsum)) /\ exists fs_q_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_zero_inner_rowsrowrow_sumsum = fs_q_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_zero_inner_rowsrowrow_sumsum) + (fs_a_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_zero_inner_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_zero_inner_rowsrowrow_sumsumnegative = fs_q_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_zero_inner_rowsrowrow_sumsumnegative) + (fs_r_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_zero_inner_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_zero_inner_rowsrowrow_sumsumnegative = fs_q_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_zero_inner_rowsrowrow_sumsumnegative) + (fs_s_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps = fs_r_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps + fs_a_dst_zero_inner_rowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_zero_inner_rowsrowrow_sumsumresult ge_balance_negative_zero_inner_rowsrowrow_sumsumresult. (((((srt_value_zero_inner_rows) = 2 * (ge_balance_positive_zero_inner_rowsrowrow_sumsumresult) /\ (ge_balance_negative_zero_inner_rowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_zero_inner_rowsrowrow_sumsumresultdecode. (((srt_value_zero_inner_rows) = 2 * ge_signed_half_zero_inner_rowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_zero_inner_rowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_zero_inner_rowsrowrow_sumsumresult) = S ge_signed_half_zero_inner_rowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_zero_inner_rowsrowrow_sumsum) + ge_balance_negative_zero_inner_rowsrowrow_sumsumresult = (dst_negative_sum_zero_inner_rowsrowrow_sumsum) + ge_balance_positive_zero_inner_rowsrowrow_sumsumresult)))))))))))))))))) -> (exists dst_positive_code_zero_inner_sum dst_positive_scale_zero_inner_sum dst_negative_code_zero_inner_sum dst_negative_scale_zero_inner_sum dst_positive_sum_zero_inner_sum dst_negative_sum_zero_inner_sum. (((R) = (((((dst_positive_code_zero_inner_sum) + (dst_positive_scale_zero_inner_sum)) * S ((dst_positive_code_zero_inner_sum) + (dst_positive_scale_zero_inner_sum)) + ((dst_positive_scale_zero_inner_sum) + (dst_positive_scale_zero_inner_sum))) + (((dst_negative_code_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)) * S ((dst_negative_code_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)) + ((dst_negative_scale_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)))) * S ((((dst_positive_code_zero_inner_sum) + (dst_positive_scale_zero_inner_sum)) * S ((dst_positive_code_zero_inner_sum) + (dst_positive_scale_zero_inner_sum)) + ((dst_positive_scale_zero_inner_sum) + (dst_positive_scale_zero_inner_sum))) + (((dst_negative_code_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)) * S ((dst_negative_code_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)) + ((dst_negative_scale_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)))) + ((((dst_negative_code_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)) * S ((dst_negative_code_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)) + ((dst_negative_scale_zero_inner_sum) + (dst_negative_scale_zero_inner_sum))) + (((dst_negative_code_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)) * S ((dst_negative_code_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)) + ((dst_negative_scale_zero_inner_sum) + (dst_negative_scale_zero_inner_sum)))))) /\ (((exists fs_u_dst_zero_inner_sumpositive fs_v_dst_zero_inner_sumpositive. ((((exists fs_h_dst_zero_inner_sumpositive_body_start. fs_h_dst_zero_inner_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_inner_sumpositive)) /\ exists fs_q_dst_zero_inner_sumpositive_body_start. fs_u_dst_zero_inner_sumpositive = fs_q_dst_zero_inner_sumpositive_body_start * S ((S (0)) * fs_v_dst_zero_inner_sumpositive) + (0))) /\ ((((exists fs_h_dst_zero_inner_sumpositive_body_terminal. fs_h_dst_zero_inner_sumpositive_body_terminal + S (dst_positive_sum_zero_inner_sum) = S ((S (m)) * fs_v_dst_zero_inner_sumpositive)) /\ exists fs_q_dst_zero_inner_sumpositive_body_terminal. fs_u_dst_zero_inner_sumpositive = fs_q_dst_zero_inner_sumpositive_body_terminal * S ((S (m)) * fs_v_dst_zero_inner_sumpositive) + (dst_positive_sum_zero_inner_sum))) /\ forall fs_i_dst_zero_inner_sumpositive_body_steps. (exists fs_lt_dst_zero_inner_sumpositive_body_steps_bound. fs_lt_dst_zero_inner_sumpositive_body_steps_bound + S fs_i_dst_zero_inner_sumpositive_body_steps = m) -> exists fs_a_dst_zero_inner_sumpositive_body_steps fs_r_dst_zero_inner_sumpositive_body_steps fs_s_dst_zero_inner_sumpositive_body_steps. ((((exists fs_h_dst_zero_inner_sumpositive_body_steps_summand. fs_h_dst_zero_inner_sumpositive_body_steps_summand + S (fs_a_dst_zero_inner_sumpositive_body_steps) = S ((S (fs_i_dst_zero_inner_sumpositive_body_steps)) * dst_positive_scale_zero_inner_sum)) /\ exists fs_q_dst_zero_inner_sumpositive_body_steps_summand. dst_positive_code_zero_inner_sum = fs_q_dst_zero_inner_sumpositive_body_steps_summand * S ((S (fs_i_dst_zero_inner_sumpositive_body_steps)) * dst_positive_scale_zero_inner_sum) + (fs_a_dst_zero_inner_sumpositive_body_steps))) /\ ((((exists fs_h_dst_zero_inner_sumpositive_body_steps_partial. fs_h_dst_zero_inner_sumpositive_body_steps_partial + S (fs_r_dst_zero_inner_sumpositive_body_steps) = S ((S (fs_i_dst_zero_inner_sumpositive_body_steps)) * fs_v_dst_zero_inner_sumpositive)) /\ exists fs_q_dst_zero_inner_sumpositive_body_steps_partial. fs_u_dst_zero_inner_sumpositive = fs_q_dst_zero_inner_sumpositive_body_steps_partial * S ((S (fs_i_dst_zero_inner_sumpositive_body_steps)) * fs_v_dst_zero_inner_sumpositive) + (fs_r_dst_zero_inner_sumpositive_body_steps))) /\ ((((exists fs_h_dst_zero_inner_sumpositive_body_steps_successor. fs_h_dst_zero_inner_sumpositive_body_steps_successor + S (fs_s_dst_zero_inner_sumpositive_body_steps) = S ((S (S fs_i_dst_zero_inner_sumpositive_body_steps)) * fs_v_dst_zero_inner_sumpositive)) /\ exists fs_q_dst_zero_inner_sumpositive_body_steps_successor. fs_u_dst_zero_inner_sumpositive = fs_q_dst_zero_inner_sumpositive_body_steps_successor * S ((S (S fs_i_dst_zero_inner_sumpositive_body_steps)) * fs_v_dst_zero_inner_sumpositive) + (fs_s_dst_zero_inner_sumpositive_body_steps))) /\ fs_s_dst_zero_inner_sumpositive_body_steps = fs_r_dst_zero_inner_sumpositive_body_steps + fs_a_dst_zero_inner_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_zero_inner_sumnegative fs_v_dst_zero_inner_sumnegative. ((((exists fs_h_dst_zero_inner_sumnegative_body_start. fs_h_dst_zero_inner_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_inner_sumnegative)) /\ exists fs_q_dst_zero_inner_sumnegative_body_start. fs_u_dst_zero_inner_sumnegative = fs_q_dst_zero_inner_sumnegative_body_start * S ((S (0)) * fs_v_dst_zero_inner_sumnegative) + (0))) /\ ((((exists fs_h_dst_zero_inner_sumnegative_body_terminal. fs_h_dst_zero_inner_sumnegative_body_terminal + S (dst_negative_sum_zero_inner_sum) = S ((S (m)) * fs_v_dst_zero_inner_sumnegative)) /\ exists fs_q_dst_zero_inner_sumnegative_body_terminal. fs_u_dst_zero_inner_sumnegative = fs_q_dst_zero_inner_sumnegative_body_terminal * S ((S (m)) * fs_v_dst_zero_inner_sumnegative) + (dst_negative_sum_zero_inner_sum))) /\ forall fs_i_dst_zero_inner_sumnegative_body_steps. (exists fs_lt_dst_zero_inner_sumnegative_body_steps_bound. fs_lt_dst_zero_inner_sumnegative_body_steps_bound + S fs_i_dst_zero_inner_sumnegative_body_steps = m) -> exists fs_a_dst_zero_inner_sumnegative_body_steps fs_r_dst_zero_inner_sumnegative_body_steps fs_s_dst_zero_inner_sumnegative_body_steps. ((((exists fs_h_dst_zero_inner_sumnegative_body_steps_summand. fs_h_dst_zero_inner_sumnegative_body_steps_summand + S (fs_a_dst_zero_inner_sumnegative_body_steps) = S ((S (fs_i_dst_zero_inner_sumnegative_body_steps)) * dst_negative_scale_zero_inner_sum)) /\ exists fs_q_dst_zero_inner_sumnegative_body_steps_summand. dst_negative_code_zero_inner_sum = fs_q_dst_zero_inner_sumnegative_body_steps_summand * S ((S (fs_i_dst_zero_inner_sumnegative_body_steps)) * dst_negative_scale_zero_inner_sum) + (fs_a_dst_zero_inner_sumnegative_body_steps))) /\ ((((exists fs_h_dst_zero_inner_sumnegative_body_steps_partial. fs_h_dst_zero_inner_sumnegative_body_steps_partial + S (fs_r_dst_zero_inner_sumnegative_body_steps) = S ((S (fs_i_dst_zero_inner_sumnegative_body_steps)) * fs_v_dst_zero_inner_sumnegative)) /\ exists fs_q_dst_zero_inner_sumnegative_body_steps_partial. fs_u_dst_zero_inner_sumnegative = fs_q_dst_zero_inner_sumnegative_body_steps_partial * S ((S (fs_i_dst_zero_inner_sumnegative_body_steps)) * fs_v_dst_zero_inner_sumnegative) + (fs_r_dst_zero_inner_sumnegative_body_steps))) /\ ((((exists fs_h_dst_zero_inner_sumnegative_body_steps_successor. fs_h_dst_zero_inner_sumnegative_body_steps_successor + S (fs_s_dst_zero_inner_sumnegative_body_steps) = S ((S (S fs_i_dst_zero_inner_sumnegative_body_steps)) * fs_v_dst_zero_inner_sumnegative)) /\ exists fs_q_dst_zero_inner_sumnegative_body_steps_successor. fs_u_dst_zero_inner_sumnegative = fs_q_dst_zero_inner_sumnegative_body_steps_successor * S ((S (S fs_i_dst_zero_inner_sumnegative_body_steps)) * fs_v_dst_zero_inner_sumnegative) + (fs_s_dst_zero_inner_sumnegative_body_steps))) /\ fs_s_dst_zero_inner_sumnegative_body_steps = fs_r_dst_zero_inner_sumnegative_body_steps + fs_a_dst_zero_inner_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_zero_inner_sumresult ge_balance_negative_zero_inner_sumresult. (((((z) = 2 * (ge_balance_positive_zero_inner_sumresult) /\ (ge_balance_negative_zero_inner_sumresult) = 0) \/ exists ge_signed_half_zero_inner_sumresultdecode. (((z) = 2 * ge_signed_half_zero_inner_sumresultdecode + 1 /\ (ge_balance_positive_zero_inner_sumresult) = 0) /\ (ge_balance_negative_zero_inner_sumresult) = S ge_signed_half_zero_inner_sumresultdecode))) /\ ((dst_positive_sum_zero_inner_sum) + ge_balance_negative_zero_inner_sumresult = (dst_negative_sum_zero_inner_sum) + ge_balance_positive_zero_inner_sumresult))))))))) -> z=0

Complete tactic proof in conservative notation

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

81 script commands · 11 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 restrict outersigned rectangular slice sum empty valuesigned rectangular row sums lookup
01Induction on mL1–10

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 R
  4. L4
    intro o
  5. L5
    intro s
  6. L6
    intro t
  7. L7
    intro z
  8. L8
    intro hr
  9. L9
    intro hz
  10. L10
    specialize divisor_signed_sum_empty_value (R)
02Use earlier factsL11–13

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

  1. L11
    specialize divisor_signed_sum_empty_value (z)
  2. L12
    apply divisor_signed_sum_empty_value
  3. L13
    exact hz
03Fix variables and assumptionsL14–21

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

  1. L14
    intro F
  2. L15
    intro R
  3. L16
    intro o
  4. L17
    intro s
  5. L18
    intro t
  6. L19
    intro z
  7. L20
    intro hr
  8. L21
    intro hz
04Establish hdL22–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed sum successor decompose.

  1. L22
    have hd : ∃ a. ∃ b. SignedPrefixSum(R,m,a) ∧ (ArithAt(R,m,b) ∧ SignedAdd(a,b,z))Definitions: SignedPrefixSum(R,m,a)ArithAt(R,m,b)SignedAdd(a,b,z)Original native command in the exact edition
  2. L23
    specialize divisor_signed_sum_successor_decompose (R)
  3. L24
    specialize divisor_signed_sum_successor_decompose (m)
  4. L25
    specialize divisor_signed_sum_successor_decompose (z)
  5. L26
    apply divisor_signed_sum_successor_decompose
  6. L27
    exact hz
05Separate the logical casesL28–31

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

  1. L28
    cases hd
  2. L29
    cases hd_witness
  3. L30
    cases hd_witness_witness
  4. L31
    cases hd_witness_witness_right
06Establish haL32–41

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

  1. L32
    have ha : x=0
  2. L33
    specialize IH (F)
  3. L34
    specialize IH (R)
  4. L35
    specialize IH (o)
  5. L36
    specialize IH (s)
  6. L37
    specialize IH (t)
  7. L38
    specialize IH (x)
  8. L39
    apply IH
  9. L40
    specialize signed_rectangular_row_sums_restrict_outer (F)
  10. L41
    specialize signed_rectangular_row_sums_restrict_outer (R)
07Use earlier factsL42–49

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

  1. L42
    specialize signed_rectangular_row_sums_restrict_outer (o)
  2. L43
    specialize signed_rectangular_row_sums_restrict_outer (s)
  3. L44
    specialize signed_rectangular_row_sums_restrict_outer (t)
  4. L45
    specialize signed_rectangular_row_sums_restrict_outer (m)
  5. L46
    specialize signed_rectangular_row_sums_restrict_outer (0)
  6. L47
    apply signed_rectangular_row_sums_restrict_outer
  7. L48
    exact hr
  8. L49
    exact hd_witness_witness_left
08Establish hbL50–59

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

  1. L50
    have hb : x1=0
  2. L51
    specialize signed_rectangular_slice_sum_empty_value (F)
  3. L52
    specialize signed_rectangular_slice_sum_empty_value (((o) + ((s) * (m))))
  4. L53
    specialize signed_rectangular_slice_sum_empty_value (t)
  5. L54
    specialize signed_rectangular_slice_sum_empty_value (x1)
  6. L55
    apply signed_rectangular_slice_sum_empty_value
  7. L56
    specialize signed_rectangular_row_sums_lookup (F)
  8. L57
    specialize signed_rectangular_row_sums_lookup (R)
  9. L58
    specialize signed_rectangular_row_sums_lookup (o)
  10. L59
    specialize signed_rectangular_row_sums_lookup (s)
09Use earlier factsL60–69

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

  1. L60
    specialize signed_rectangular_row_sums_lookup (t)
  2. L61
    specialize signed_rectangular_row_sums_lookup (S m)
  3. L62
    specialize signed_rectangular_row_sums_lookup (0)
  4. L63
    specialize signed_rectangular_row_sums_lookup (m)
  5. L64
    specialize signed_rectangular_row_sums_lookup (x1)
  6. L65
    apply signed_rectangular_row_sums_lookup
  7. L66
    exact hr
  8. L67
    specialize le_refl (S m)
  9. L68
    apply le_refl
  10. L69
    exact hd_witness_witness_right_left
10Calculate and transport equalitiesL70–73

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

  1. L70
    rewrite ha at hd_witness_witness_right_right
  2. L71
    rewrite ha at hd_witness_witness_right_right
  3. L72
    rewrite hb at hd_witness_witness_right_right
  4. L73
    rewrite hb at hd_witness_witness_right_right
11Use earlier factsL74–81

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

  1. L74
    specialize signed_add_functional (0)
  2. L75
    specialize signed_add_functional (0)
  3. L76
    specialize signed_add_functional (z)
  4. L77
    specialize signed_add_functional (0)
  5. L78
    apply signed_add_functional
  6. L79
    exact hd_witness_witness_right_right
  7. L80
    specialize signed_add_zero_left (0)
  8. L81
    apply signed_add_zero_left

Library-wide reading audit

Original defined command ledger · 81 lines
  1. 0001induction m
  2. 0002intro F
  3. 0003intro R
  4. 0004intro o
  5. 0005intro s
  6. 0006intro t
  7. 0007intro z
  8. 0008intro hr
  9. 0009intro hz
  10. 0010specialize divisor_signed_sum_empty_value (R)
  11. 0011specialize divisor_signed_sum_empty_value (z)
  12. 0012apply divisor_signed_sum_empty_value
  13. 0013exact hz
  14. 0014intro F
  15. 0015intro R
  16. 0016intro o
  17. 0017intro s
  18. 0018intro t
  19. 0019intro z
  20. 0020intro hr
  21. 0021intro hz
  22. 0022have hd : ∃ a. ∃ b. SignedPrefixSum(R,m,a) ∧ (ArithAt(R,m,b) ∧ SignedAdd(a,b,z))
  23. 0023specialize divisor_signed_sum_successor_decompose (R)
  24. 0024specialize divisor_signed_sum_successor_decompose (m)
  25. 0025specialize divisor_signed_sum_successor_decompose (z)
  26. 0026apply divisor_signed_sum_successor_decompose
  27. 0027exact hz
  28. 0028cases hd
  29. 0029cases hd_witness
  30. 0030cases hd_witness_witness
  31. 0031cases hd_witness_witness_right
  32. 0032have ha : x=0
  33. 0033specialize IH (F)
  34. 0034specialize IH (R)
  35. 0035specialize IH (o)
  36. 0036specialize IH (s)
  37. 0037specialize IH (t)
  38. 0038specialize IH (x)
  39. 0039apply IH
  40. 0040specialize signed_rectangular_row_sums_restrict_outer (F)
  41. 0041specialize signed_rectangular_row_sums_restrict_outer (R)
  42. 0042specialize signed_rectangular_row_sums_restrict_outer (o)
  43. 0043specialize signed_rectangular_row_sums_restrict_outer (s)
  44. 0044specialize signed_rectangular_row_sums_restrict_outer (t)
  45. 0045specialize signed_rectangular_row_sums_restrict_outer (m)
  46. 0046specialize signed_rectangular_row_sums_restrict_outer (0)
  47. 0047apply signed_rectangular_row_sums_restrict_outer
  48. 0048exact hr
  49. 0049exact hd_witness_witness_left
  50. 0050have hb : x1=0
  51. 0051specialize signed_rectangular_slice_sum_empty_value (F)
  52. 0052specialize signed_rectangular_slice_sum_empty_value (((o) + ((s) * (m))))
  53. 0053specialize signed_rectangular_slice_sum_empty_value (t)
  54. 0054specialize signed_rectangular_slice_sum_empty_value (x1)
  55. 0055apply signed_rectangular_slice_sum_empty_value
  56. 0056specialize signed_rectangular_row_sums_lookup (F)
  57. 0057specialize signed_rectangular_row_sums_lookup (R)
  58. 0058specialize signed_rectangular_row_sums_lookup (o)
  59. 0059specialize signed_rectangular_row_sums_lookup (s)
  60. 0060specialize signed_rectangular_row_sums_lookup (t)
  61. 0061specialize signed_rectangular_row_sums_lookup (S m)
  62. 0062specialize signed_rectangular_row_sums_lookup (0)
  63. 0063specialize signed_rectangular_row_sums_lookup (m)
  64. 0064specialize signed_rectangular_row_sums_lookup (x1)
  65. 0065apply signed_rectangular_row_sums_lookup
  66. 0066exact hr
  67. 0067specialize le_refl (S m)
  68. 0068apply le_refl
  69. 0069exact hd_witness_witness_right_left
  70. 0070rewrite ha at hd_witness_witness_right_right
  71. 0071rewrite ha at hd_witness_witness_right_right
  72. 0072rewrite hb at hd_witness_witness_right_right
  73. 0073rewrite hb at hd_witness_witness_right_right
  74. 0074specialize signed_add_functional (0)
  75. 0075specialize signed_add_functional (0)
  76. 0076specialize signed_add_functional (z)
  77. 0077specialize signed_add_functional (0)
  78. 0078apply signed_add_functional
  79. 0079exact hd_witness_witness_right_right
  80. 0080specialize signed_add_zero_left (0)
  81. 0081apply signed_add_zero_left