Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall F G T R m n b. (((exists dst_positive_code_row_sums_productF dst_positive_scale_row_sums_productF dst_negative_code_row_sums_productF dst_negative_scale_row_sums_productF. (((F) = (((((dst_positive_code_row_sums_productF) + (dst_positive_scale_row_sums_productF)) * S ((dst_positive_code_row_sums_productF) + (dst_positive_scale_row_sums_productF)) + ((dst_positive_scale_row_sums_productF) + (dst_positive_scale_row_sums_productF))) + (((dst_negative_code_row_sums_productF) + (dst_negative_scale_row_sums_productF)) * S ((dst_negative_code_row_sums_productF) + (dst_negative_scale_row_sums_productF)) + ((dst_negative_scale_row_sums_productF) + (dst_negative_scale_row_sums_productF)))) * S ((((dst_positive_code_row_sums_productF) + (dst_positive_scale_row_sums_productF)) * S ((dst_positive_code_row_sums_productF) + (dst_positive_scale_row_sums_productF)) + ((dst_positive_scale_row_sums_productF) + (dst_positive_scale_row_sums_productF))) + (((dst_negative_code_row_sums_productF) + (dst_negative_scale_row_sums_productF)) * S ((dst_negative_code_row_sums_productF) + (dst_negative_scale_row_sums_productF)) + ((dst_negative_scale_row_sums_productF) + (dst_negative_scale_row_sums_productF)))) + ((((dst_negative_code_row_sums_productF) + (dst_negative_scale_row_sums_productF)) * S ((dst_negative_code_row_sums_productF) + (dst_negative_scale_row_sums_productF)) + ((dst_negative_scale_row_sums_productF) + (dst_negative_scale_row_sums_productF))) + (((dst_negative_code_row_sums_productF) + (dst_negative_scale_row_sums_productF)) * S ((dst_negative_code_row_sums_productF) + (dst_negative_scale_row_sums_productF)) + ((dst_negative_scale_row_sums_productF) + (dst_negative_scale_row_sums_productF)))))) /\ (forall dst_index_row_sums_productF. (exists pvs_le_gap_row_sums_productFdomain. pvs_le_gap_row_sums_productFdomain + (dst_index_row_sums_productF) = (0)) -> exists dst_positive_row_sums_productF dst_negative_row_sums_productF dst_value_row_sums_productF. ((((exists ff_h_pvs_row_sums_productFentrypositive. ff_h_pvs_row_sums_productFentrypositive + S (dst_positive_row_sums_productF) = S ((S (dst_index_row_sums_productF)) * dst_positive_scale_row_sums_productF)) /\ exists ff_q_pvs_row_sums_productFentrypositive. dst_positive_code_row_sums_productF = ff_q_pvs_row_sums_productFentrypositive * S ((S (dst_index_row_sums_productF)) * dst_positive_scale_row_sums_productF) + (dst_positive_row_sums_productF))) /\ (((((exists ff_h_pvs_row_sums_productFentrynegative. ff_h_pvs_row_sums_productFentrynegative + S (dst_negative_row_sums_productF) = S ((S (dst_index_row_sums_productF)) * dst_negative_scale_row_sums_productF)) /\ exists ff_q_pvs_row_sums_productFentrynegative. dst_negative_code_row_sums_productF = ff_q_pvs_row_sums_productFentrynegative * S ((S (dst_index_row_sums_productF)) * dst_negative_scale_row_sums_productF) + (dst_negative_row_sums_productF))) /\ (exists ge_balance_positive_row_sums_productFentryvalue ge_balance_negative_row_sums_productFentryvalue. (((((dst_value_row_sums_productF) = 2 * (ge_balance_positive_row_sums_productFentryvalue) /\ (ge_balance_negative_row_sums_productFentryvalue) = 0) \/ exists ge_signed_half_row_sums_productFentryvaluedecode. (((dst_value_row_sums_productF) = 2 * ge_signed_half_row_sums_productFentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_productFentryvalue) = 0) /\ (ge_balance_negative_row_sums_productFentryvalue) = S ge_signed_half_row_sums_productFentryvaluedecode))) /\ ((dst_positive_row_sums_productF) + ge_balance_negative_row_sums_productFentryvalue = (dst_negative_row_sums_productF) + ge_balance_positive_row_sums_productFentryvalue))))))))) /\ (((exists dst_positive_code_row_sums_productG dst_positive_scale_row_sums_productG dst_negative_code_row_sums_productG dst_negative_scale_row_sums_productG. (((G) = (((((dst_positive_code_row_sums_productG) + (dst_positive_scale_row_sums_productG)) * S ((dst_positive_code_row_sums_productG) + (dst_positive_scale_row_sums_productG)) + ((dst_positive_scale_row_sums_productG) + (dst_positive_scale_row_sums_productG))) + (((dst_negative_code_row_sums_productG) + (dst_negative_scale_row_sums_productG)) * S ((dst_negative_code_row_sums_productG) + (dst_negative_scale_row_sums_productG)) + ((dst_negative_scale_row_sums_productG) + (dst_negative_scale_row_sums_productG)))) * S ((((dst_positive_code_row_sums_productG) + (dst_positive_scale_row_sums_productG)) * S ((dst_positive_code_row_sums_productG) + (dst_positive_scale_row_sums_productG)) + ((dst_positive_scale_row_sums_productG) + (dst_positive_scale_row_sums_productG))) + (((dst_negative_code_row_sums_productG) + (dst_negative_scale_row_sums_productG)) * S ((dst_negative_code_row_sums_productG) + (dst_negative_scale_row_sums_productG)) + ((dst_negative_scale_row_sums_productG) + (dst_negative_scale_row_sums_productG)))) + ((((dst_negative_code_row_sums_productG) + (dst_negative_scale_row_sums_productG)) * S ((dst_negative_code_row_sums_productG) + (dst_negative_scale_row_sums_productG)) + ((dst_negative_scale_row_sums_productG) + (dst_negative_scale_row_sums_productG))) + (((dst_negative_code_row_sums_productG) + (dst_negative_scale_row_sums_productG)) * S ((dst_negative_code_row_sums_productG) + (dst_negative_scale_row_sums_productG)) + ((dst_negative_scale_row_sums_productG) + (dst_negative_scale_row_sums_productG)))))) /\ (forall dst_index_row_sums_productG. (exists pvs_le_gap_row_sums_productGdomain. pvs_le_gap_row_sums_productGdomain + (dst_index_row_sums_productG) = (0)) -> exists dst_positive_row_sums_productG dst_negative_row_sums_productG dst_value_row_sums_productG. ((((exists ff_h_pvs_row_sums_productGentrypositive. ff_h_pvs_row_sums_productGentrypositive + S (dst_positive_row_sums_productG) = S ((S (dst_index_row_sums_productG)) * dst_positive_scale_row_sums_productG)) /\ exists ff_q_pvs_row_sums_productGentrypositive. dst_positive_code_row_sums_productG = ff_q_pvs_row_sums_productGentrypositive * S ((S (dst_index_row_sums_productG)) * dst_positive_scale_row_sums_productG) + (dst_positive_row_sums_productG))) /\ (((((exists ff_h_pvs_row_sums_productGentrynegative. ff_h_pvs_row_sums_productGentrynegative + S (dst_negative_row_sums_productG) = S ((S (dst_index_row_sums_productG)) * dst_negative_scale_row_sums_productG)) /\ exists ff_q_pvs_row_sums_productGentrynegative. dst_negative_code_row_sums_productG = ff_q_pvs_row_sums_productGentrynegative * S ((S (dst_index_row_sums_productG)) * dst_negative_scale_row_sums_productG) + (dst_negative_row_sums_productG))) /\ (exists ge_balance_positive_row_sums_productGentryvalue ge_balance_negative_row_sums_productGentryvalue. (((((dst_value_row_sums_productG) = 2 * (ge_balance_positive_row_sums_productGentryvalue) /\ (ge_balance_negative_row_sums_productGentryvalue) = 0) \/ exists ge_signed_half_row_sums_productGentryvaluedecode. (((dst_value_row_sums_productG) = 2 * ge_signed_half_row_sums_productGentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_productGentryvalue) = 0) /\ (ge_balance_negative_row_sums_productGentryvalue) = S ge_signed_half_row_sums_productGentryvaluedecode))) /\ ((dst_positive_row_sums_productG) + ge_balance_negative_row_sums_productGentryvalue = (dst_negative_row_sums_productG) + ge_balance_positive_row_sums_productGentryvalue))))))))) /\ (((exists dst_positive_code_row_sums_productT dst_positive_scale_row_sums_productT dst_negative_code_row_sums_productT dst_negative_scale_row_sums_productT. (((T) = (((((dst_positive_code_row_sums_productT) + (dst_positive_scale_row_sums_productT)) * S ((dst_positive_code_row_sums_productT) + (dst_positive_scale_row_sums_productT)) + ((dst_positive_scale_row_sums_productT) + (dst_positive_scale_row_sums_productT))) + (((dst_negative_code_row_sums_productT) + (dst_negative_scale_row_sums_productT)) * S ((dst_negative_code_row_sums_productT) + (dst_negative_scale_row_sums_productT)) + ((dst_negative_scale_row_sums_productT) + (dst_negative_scale_row_sums_productT)))) * S ((((dst_positive_code_row_sums_productT) + (dst_positive_scale_row_sums_productT)) * S ((dst_positive_code_row_sums_productT) + (dst_positive_scale_row_sums_productT)) + ((dst_positive_scale_row_sums_productT) + (dst_positive_scale_row_sums_productT))) + (((dst_negative_code_row_sums_productT) + (dst_negative_scale_row_sums_productT)) * S ((dst_negative_code_row_sums_productT) + (dst_negative_scale_row_sums_productT)) + ((dst_negative_scale_row_sums_productT) + (dst_negative_scale_row_sums_productT)))) + ((((dst_negative_code_row_sums_productT) + (dst_negative_scale_row_sums_productT)) * S ((dst_negative_code_row_sums_productT) + (dst_negative_scale_row_sums_productT)) + ((dst_negative_scale_row_sums_productT) + (dst_negative_scale_row_sums_productT))) + (((dst_negative_code_row_sums_productT) + (dst_negative_scale_row_sums_productT)) * S ((dst_negative_code_row_sums_productT) + (dst_negative_scale_row_sums_productT)) + ((dst_negative_scale_row_sums_productT) + (dst_negative_scale_row_sums_productT)))))) /\ (forall dst_index_row_sums_productT. (exists pvs_le_gap_row_sums_productTdomain. pvs_le_gap_row_sums_productTdomain + (dst_index_row_sums_productT) = ((m)*(n))) -> exists dst_positive_row_sums_productT dst_negative_row_sums_productT dst_value_row_sums_productT. ((((exists ff_h_pvs_row_sums_productTentrypositive. ff_h_pvs_row_sums_productTentrypositive + S (dst_positive_row_sums_productT) = S ((S (dst_index_row_sums_productT)) * dst_positive_scale_row_sums_productT)) /\ exists ff_q_pvs_row_sums_productTentrypositive. dst_positive_code_row_sums_productT = ff_q_pvs_row_sums_productTentrypositive * S ((S (dst_index_row_sums_productT)) * dst_positive_scale_row_sums_productT) + (dst_positive_row_sums_productT))) /\ (((((exists ff_h_pvs_row_sums_productTentrynegative. ff_h_pvs_row_sums_productTentrynegative + S (dst_negative_row_sums_productT) = S ((S (dst_index_row_sums_productT)) * dst_negative_scale_row_sums_productT)) /\ exists ff_q_pvs_row_sums_productTentrynegative. dst_negative_code_row_sums_productT = ff_q_pvs_row_sums_productTentrynegative * S ((S (dst_index_row_sums_productT)) * dst_negative_scale_row_sums_productT) + (dst_negative_row_sums_productT))) /\ (exists ge_balance_positive_row_sums_productTentryvalue ge_balance_negative_row_sums_productTentryvalue. (((((dst_value_row_sums_productT) = 2 * (ge_balance_positive_row_sums_productTentryvalue) /\ (ge_balance_negative_row_sums_productTentryvalue) = 0) \/ exists ge_signed_half_row_sums_productTentryvaluedecode. (((dst_value_row_sums_productT) = 2 * ge_signed_half_row_sums_productTentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_productTentryvalue) = 0) /\ (ge_balance_negative_row_sums_productTentryvalue) = S ge_signed_half_row_sums_productTentryvaluedecode))) /\ ((dst_positive_row_sums_productT) + ge_balance_negative_row_sums_productTentryvalue = (dst_negative_row_sums_productT) + ge_balance_positive_row_sums_productTentryvalue))))))))) /\ (forall scp_row_row_sums_product scp_column_row_sums_product scp_first_row_sums_product scp_second_row_sums_product scp_value_row_sums_product. (exists pvs_gap_row_sums_productrows. pvs_gap_row_sums_productrows + S (scp_row_row_sums_product) = (m)) -> (exists pvs_gap_row_sums_productcolumns. pvs_gap_row_sums_productcolumns + S (scp_column_row_sums_product) = (n)) -> (exists dst_positive_code_row_sums_productfirst dst_positive_scale_row_sums_productfirst dst_negative_code_row_sums_productfirst dst_negative_scale_row_sums_productfirst dst_positive_row_sums_productfirst dst_negative_row_sums_productfirst. (((F) = (((((dst_positive_code_row_sums_productfirst) + (dst_positive_scale_row_sums_productfirst)) * S ((dst_positive_code_row_sums_productfirst) + (dst_positive_scale_row_sums_productfirst)) + ((dst_positive_scale_row_sums_productfirst) + (dst_positive_scale_row_sums_productfirst))) + (((dst_negative_code_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)) * S ((dst_negative_code_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)) + ((dst_negative_scale_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)))) * S ((((dst_positive_code_row_sums_productfirst) + (dst_positive_scale_row_sums_productfirst)) * S ((dst_positive_code_row_sums_productfirst) + (dst_positive_scale_row_sums_productfirst)) + ((dst_positive_scale_row_sums_productfirst) + (dst_positive_scale_row_sums_productfirst))) + (((dst_negative_code_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)) * S ((dst_negative_code_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)) + ((dst_negative_scale_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)))) + ((((dst_negative_code_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)) * S ((dst_negative_code_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)) + ((dst_negative_scale_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst))) + (((dst_negative_code_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)) * S ((dst_negative_code_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)) + ((dst_negative_scale_row_sums_productfirst) + (dst_negative_scale_row_sums_productfirst)))))) /\ (((((exists ff_h_pvs_row_sums_productfirstpositive. ff_h_pvs_row_sums_productfirstpositive + S (dst_positive_row_sums_productfirst) = S ((S (scp_row_row_sums_product)) * dst_positive_scale_row_sums_productfirst)) /\ exists ff_q_pvs_row_sums_productfirstpositive. dst_positive_code_row_sums_productfirst = ff_q_pvs_row_sums_productfirstpositive * S ((S (scp_row_row_sums_product)) * dst_positive_scale_row_sums_productfirst) + (dst_positive_row_sums_productfirst))) /\ (((((exists ff_h_pvs_row_sums_productfirstnegative. ff_h_pvs_row_sums_productfirstnegative + S (dst_negative_row_sums_productfirst) = S ((S (scp_row_row_sums_product)) * dst_negative_scale_row_sums_productfirst)) /\ exists ff_q_pvs_row_sums_productfirstnegative. dst_negative_code_row_sums_productfirst = ff_q_pvs_row_sums_productfirstnegative * S ((S (scp_row_row_sums_product)) * dst_negative_scale_row_sums_productfirst) + (dst_negative_row_sums_productfirst))) /\ (exists ge_balance_positive_row_sums_productfirstvalue ge_balance_negative_row_sums_productfirstvalue. (((((scp_first_row_sums_product) = 2 * (ge_balance_positive_row_sums_productfirstvalue) /\ (ge_balance_negative_row_sums_productfirstvalue) = 0) \/ exists ge_signed_half_row_sums_productfirstvaluedecode. (((scp_first_row_sums_product) = 2 * ge_signed_half_row_sums_productfirstvaluedecode + 1 /\ (ge_balance_positive_row_sums_productfirstvalue) = 0) /\ (ge_balance_negative_row_sums_productfirstvalue) = S ge_signed_half_row_sums_productfirstvaluedecode))) /\ ((dst_positive_row_sums_productfirst) + ge_balance_negative_row_sums_productfirstvalue = (dst_negative_row_sums_productfirst) + ge_balance_positive_row_sums_productfirstvalue))))))))) -> (exists dst_positive_code_row_sums_productsecond dst_positive_scale_row_sums_productsecond dst_negative_code_row_sums_productsecond dst_negative_scale_row_sums_productsecond dst_positive_row_sums_productsecond dst_negative_row_sums_productsecond. (((G) = (((((dst_positive_code_row_sums_productsecond) + (dst_positive_scale_row_sums_productsecond)) * S ((dst_positive_code_row_sums_productsecond) + (dst_positive_scale_row_sums_productsecond)) + ((dst_positive_scale_row_sums_productsecond) + (dst_positive_scale_row_sums_productsecond))) + (((dst_negative_code_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)) * S ((dst_negative_code_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)) + ((dst_negative_scale_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)))) * S ((((dst_positive_code_row_sums_productsecond) + (dst_positive_scale_row_sums_productsecond)) * S ((dst_positive_code_row_sums_productsecond) + (dst_positive_scale_row_sums_productsecond)) + ((dst_positive_scale_row_sums_productsecond) + (dst_positive_scale_row_sums_productsecond))) + (((dst_negative_code_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)) * S ((dst_negative_code_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)) + ((dst_negative_scale_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)))) + ((((dst_negative_code_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)) * S ((dst_negative_code_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)) + ((dst_negative_scale_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond))) + (((dst_negative_code_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)) * S ((dst_negative_code_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)) + ((dst_negative_scale_row_sums_productsecond) + (dst_negative_scale_row_sums_productsecond)))))) /\ (((((exists ff_h_pvs_row_sums_productsecondpositive. ff_h_pvs_row_sums_productsecondpositive + S (dst_positive_row_sums_productsecond) = S ((S (scp_column_row_sums_product)) * dst_positive_scale_row_sums_productsecond)) /\ exists ff_q_pvs_row_sums_productsecondpositive. dst_positive_code_row_sums_productsecond = ff_q_pvs_row_sums_productsecondpositive * S ((S (scp_column_row_sums_product)) * dst_positive_scale_row_sums_productsecond) + (dst_positive_row_sums_productsecond))) /\ (((((exists ff_h_pvs_row_sums_productsecondnegative. ff_h_pvs_row_sums_productsecondnegative + S (dst_negative_row_sums_productsecond) = S ((S (scp_column_row_sums_product)) * dst_negative_scale_row_sums_productsecond)) /\ exists ff_q_pvs_row_sums_productsecondnegative. dst_negative_code_row_sums_productsecond = ff_q_pvs_row_sums_productsecondnegative * S ((S (scp_column_row_sums_product)) * dst_negative_scale_row_sums_productsecond) + (dst_negative_row_sums_productsecond))) /\ (exists ge_balance_positive_row_sums_productsecondvalue ge_balance_negative_row_sums_productsecondvalue. (((((scp_second_row_sums_product) = 2 * (ge_balance_positive_row_sums_productsecondvalue) /\ (ge_balance_negative_row_sums_productsecondvalue) = 0) \/ exists ge_signed_half_row_sums_productsecondvaluedecode. (((scp_second_row_sums_product) = 2 * ge_signed_half_row_sums_productsecondvaluedecode + 1 /\ (ge_balance_positive_row_sums_productsecondvalue) = 0) /\ (ge_balance_negative_row_sums_productsecondvalue) = S ge_signed_half_row_sums_productsecondvaluedecode))) /\ ((dst_positive_row_sums_productsecond) + ge_balance_negative_row_sums_productsecondvalue = (dst_negative_row_sums_productsecond) + ge_balance_positive_row_sums_productsecondvalue))))))))) -> (exists dst_positive_code_row_sums_productentry dst_positive_scale_row_sums_productentry dst_negative_code_row_sums_productentry dst_negative_scale_row_sums_productentry dst_positive_row_sums_productentry dst_negative_row_sums_productentry. (((T) = (((((dst_positive_code_row_sums_productentry) + (dst_positive_scale_row_sums_productentry)) * S ((dst_positive_code_row_sums_productentry) + (dst_positive_scale_row_sums_productentry)) + ((dst_positive_scale_row_sums_productentry) + (dst_positive_scale_row_sums_productentry))) + (((dst_negative_code_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)) * S ((dst_negative_code_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)) + ((dst_negative_scale_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)))) * S ((((dst_positive_code_row_sums_productentry) + (dst_positive_scale_row_sums_productentry)) * S ((dst_positive_code_row_sums_productentry) + (dst_positive_scale_row_sums_productentry)) + ((dst_positive_scale_row_sums_productentry) + (dst_positive_scale_row_sums_productentry))) + (((dst_negative_code_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)) * S ((dst_negative_code_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)) + ((dst_negative_scale_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)))) + ((((dst_negative_code_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)) * S ((dst_negative_code_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)) + ((dst_negative_scale_row_sums_productentry) + (dst_negative_scale_row_sums_productentry))) + (((dst_negative_code_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)) * S ((dst_negative_code_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)) + ((dst_negative_scale_row_sums_productentry) + (dst_negative_scale_row_sums_productentry)))))) /\ (((((exists ff_h_pvs_row_sums_productentrypositive. ff_h_pvs_row_sums_productentrypositive + S (dst_positive_row_sums_productentry) = S ((S (((n)*(scp_row_row_sums_product)+(scp_column_row_sums_product)))) * dst_positive_scale_row_sums_productentry)) /\ exists ff_q_pvs_row_sums_productentrypositive. dst_positive_code_row_sums_productentry = ff_q_pvs_row_sums_productentrypositive * S ((S (((n)*(scp_row_row_sums_product)+(scp_column_row_sums_product)))) * dst_positive_scale_row_sums_productentry) + (dst_positive_row_sums_productentry))) /\ (((((exists ff_h_pvs_row_sums_productentrynegative. ff_h_pvs_row_sums_productentrynegative + S (dst_negative_row_sums_productentry) = S ((S (((n)*(scp_row_row_sums_product)+(scp_column_row_sums_product)))) * dst_negative_scale_row_sums_productentry)) /\ exists ff_q_pvs_row_sums_productentrynegative. dst_negative_code_row_sums_productentry = ff_q_pvs_row_sums_productentrynegative * S ((S (((n)*(scp_row_row_sums_product)+(scp_column_row_sums_product)))) * dst_negative_scale_row_sums_productentry) + (dst_negative_row_sums_productentry))) /\ (exists ge_balance_positive_row_sums_productentryvalue ge_balance_negative_row_sums_productentryvalue. (((((scp_value_row_sums_product) = 2 * (ge_balance_positive_row_sums_productentryvalue) /\ (ge_balance_negative_row_sums_productentryvalue) = 0) \/ exists ge_signed_half_row_sums_productentryvaluedecode. (((scp_value_row_sums_product) = 2 * ge_signed_half_row_sums_productentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_productentryvalue) = 0) /\ (ge_balance_negative_row_sums_productentryvalue) = S ge_signed_half_row_sums_productentryvaluedecode))) /\ ((dst_positive_row_sums_productentry) + ge_balance_negative_row_sums_productentryvalue = (dst_negative_row_sums_productentry) + ge_balance_positive_row_sums_productentryvalue))))))))) -> (exists sto_ap_row_sums_productmultiply sto_an_row_sums_productmultiply sto_bp_row_sums_productmultiply sto_bn_row_sums_productmultiply sto_cp_row_sums_productmultiply sto_cn_row_sums_productmultiply. (((((scp_first_row_sums_product) = 2 * (sto_ap_row_sums_productmultiply) /\ (sto_an_row_sums_productmultiply) = 0) \/ exists ge_signed_half_row_sums_productmultiplyleft. (((scp_first_row_sums_product) = 2 * ge_signed_half_row_sums_productmultiplyleft + 1 /\ (sto_ap_row_sums_productmultiply) = 0) /\ (sto_an_row_sums_productmultiply) = S ge_signed_half_row_sums_productmultiplyleft))) /\ ((((((scp_second_row_sums_product) = 2 * (sto_bp_row_sums_productmultiply) /\ (sto_bn_row_sums_productmultiply) = 0) \/ exists ge_signed_half_row_sums_productmultiplyright. (((scp_second_row_sums_product) = 2 * ge_signed_half_row_sums_productmultiplyright + 1 /\ (sto_bp_row_sums_productmultiply) = 0) /\ (sto_bn_row_sums_productmultiply) = S ge_signed_half_row_sums_productmultiplyright))) /\ ((((((scp_value_row_sums_product) = 2 * (sto_cp_row_sums_productmultiply) /\ (sto_cn_row_sums_productmultiply) = 0) \/ exists ge_signed_half_row_sums_productmultiplyoutput. (((scp_value_row_sums_product) = 2 * ge_signed_half_row_sums_productmultiplyoutput + 1 /\ (sto_cp_row_sums_productmultiply) = 0) /\ (sto_cn_row_sums_productmultiply) = S ge_signed_half_row_sums_productmultiplyoutput))) /\ ((sto_ap_row_sums_productmultiply * sto_bp_row_sums_productmultiply + sto_an_row_sums_productmultiply * sto_bn_row_sums_productmultiply) + sto_cn_row_sums_productmultiply = (sto_ap_row_sums_productmultiply * sto_bn_row_sums_productmultiply + sto_an_row_sums_productmultiply * sto_bp_row_sums_productmultiply) + sto_cp_row_sums_productmultiply)))))))))))))) -> (exists dst_positive_code_row_sums_second dst_positive_scale_row_sums_second dst_negative_code_row_sums_second dst_negative_scale_row_sums_second dst_positive_sum_row_sums_second dst_negative_sum_row_sums_second. (((G) = (((((dst_positive_code_row_sums_second) + (dst_positive_scale_row_sums_second)) * S ((dst_positive_code_row_sums_second) + (dst_positive_scale_row_sums_second)) + ((dst_positive_scale_row_sums_second) + (dst_positive_scale_row_sums_second))) + (((dst_negative_code_row_sums_second) + (dst_negative_scale_row_sums_second)) * S ((dst_negative_code_row_sums_second) + (dst_negative_scale_row_sums_second)) + ((dst_negative_scale_row_sums_second) + (dst_negative_scale_row_sums_second)))) * S ((((dst_positive_code_row_sums_second) + (dst_positive_scale_row_sums_second)) * S ((dst_positive_code_row_sums_second) + (dst_positive_scale_row_sums_second)) + ((dst_positive_scale_row_sums_second) + (dst_positive_scale_row_sums_second))) + (((dst_negative_code_row_sums_second) + (dst_negative_scale_row_sums_second)) * S ((dst_negative_code_row_sums_second) + (dst_negative_scale_row_sums_second)) + ((dst_negative_scale_row_sums_second) + (dst_negative_scale_row_sums_second)))) + ((((dst_negative_code_row_sums_second) + (dst_negative_scale_row_sums_second)) * S ((dst_negative_code_row_sums_second) + (dst_negative_scale_row_sums_second)) + ((dst_negative_scale_row_sums_second) + (dst_negative_scale_row_sums_second))) + (((dst_negative_code_row_sums_second) + (dst_negative_scale_row_sums_second)) * S ((dst_negative_code_row_sums_second) + (dst_negative_scale_row_sums_second)) + ((dst_negative_scale_row_sums_second) + (dst_negative_scale_row_sums_second)))))) /\ (((exists fs_u_dst_row_sums_secondpositive fs_v_dst_row_sums_secondpositive. ((((exists fs_h_dst_row_sums_secondpositive_body_start. fs_h_dst_row_sums_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_row_sums_secondpositive)) /\ exists fs_q_dst_row_sums_secondpositive_body_start. fs_u_dst_row_sums_secondpositive = fs_q_dst_row_sums_secondpositive_body_start * S ((S (0)) * fs_v_dst_row_sums_secondpositive) + (0))) /\ ((((exists fs_h_dst_row_sums_secondpositive_body_terminal. fs_h_dst_row_sums_secondpositive_body_terminal + S (dst_positive_sum_row_sums_second) = S ((S (n)) * fs_v_dst_row_sums_secondpositive)) /\ exists fs_q_dst_row_sums_secondpositive_body_terminal. fs_u_dst_row_sums_secondpositive = fs_q_dst_row_sums_secondpositive_body_terminal * S ((S (n)) * fs_v_dst_row_sums_secondpositive) + (dst_positive_sum_row_sums_second))) /\ forall fs_i_dst_row_sums_secondpositive_body_steps. (exists fs_lt_dst_row_sums_secondpositive_body_steps_bound. fs_lt_dst_row_sums_secondpositive_body_steps_bound + S fs_i_dst_row_sums_secondpositive_body_steps = n) -> exists fs_a_dst_row_sums_secondpositive_body_steps fs_r_dst_row_sums_secondpositive_body_steps fs_s_dst_row_sums_secondpositive_body_steps. ((((exists fs_h_dst_row_sums_secondpositive_body_steps_summand. fs_h_dst_row_sums_secondpositive_body_steps_summand + S (fs_a_dst_row_sums_secondpositive_body_steps) = S ((S (fs_i_dst_row_sums_secondpositive_body_steps)) * dst_positive_scale_row_sums_second)) /\ exists fs_q_dst_row_sums_secondpositive_body_steps_summand. dst_positive_code_row_sums_second = fs_q_dst_row_sums_secondpositive_body_steps_summand * S ((S (fs_i_dst_row_sums_secondpositive_body_steps)) * dst_positive_scale_row_sums_second) + (fs_a_dst_row_sums_secondpositive_body_steps))) /\ ((((exists fs_h_dst_row_sums_secondpositive_body_steps_partial. fs_h_dst_row_sums_secondpositive_body_steps_partial + S (fs_r_dst_row_sums_secondpositive_body_steps) = S ((S (fs_i_dst_row_sums_secondpositive_body_steps)) * fs_v_dst_row_sums_secondpositive)) /\ exists fs_q_dst_row_sums_secondpositive_body_steps_partial. fs_u_dst_row_sums_secondpositive = fs_q_dst_row_sums_secondpositive_body_steps_partial * S ((S (fs_i_dst_row_sums_secondpositive_body_steps)) * fs_v_dst_row_sums_secondpositive) + (fs_r_dst_row_sums_secondpositive_body_steps))) /\ ((((exists fs_h_dst_row_sums_secondpositive_body_steps_successor. fs_h_dst_row_sums_secondpositive_body_steps_successor + S (fs_s_dst_row_sums_secondpositive_body_steps) = S ((S (S fs_i_dst_row_sums_secondpositive_body_steps)) * fs_v_dst_row_sums_secondpositive)) /\ exists fs_q_dst_row_sums_secondpositive_body_steps_successor. fs_u_dst_row_sums_secondpositive = fs_q_dst_row_sums_secondpositive_body_steps_successor * S ((S (S fs_i_dst_row_sums_secondpositive_body_steps)) * fs_v_dst_row_sums_secondpositive) + (fs_s_dst_row_sums_secondpositive_body_steps))) /\ fs_s_dst_row_sums_secondpositive_body_steps = fs_r_dst_row_sums_secondpositive_body_steps + fs_a_dst_row_sums_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_row_sums_secondnegative fs_v_dst_row_sums_secondnegative. ((((exists fs_h_dst_row_sums_secondnegative_body_start. fs_h_dst_row_sums_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_row_sums_secondnegative)) /\ exists fs_q_dst_row_sums_secondnegative_body_start. fs_u_dst_row_sums_secondnegative = fs_q_dst_row_sums_secondnegative_body_start * S ((S (0)) * fs_v_dst_row_sums_secondnegative) + (0))) /\ ((((exists fs_h_dst_row_sums_secondnegative_body_terminal. fs_h_dst_row_sums_secondnegative_body_terminal + S (dst_negative_sum_row_sums_second) = S ((S (n)) * fs_v_dst_row_sums_secondnegative)) /\ exists fs_q_dst_row_sums_secondnegative_body_terminal. fs_u_dst_row_sums_secondnegative = fs_q_dst_row_sums_secondnegative_body_terminal * S ((S (n)) * fs_v_dst_row_sums_secondnegative) + (dst_negative_sum_row_sums_second))) /\ forall fs_i_dst_row_sums_secondnegative_body_steps. (exists fs_lt_dst_row_sums_secondnegative_body_steps_bound. fs_lt_dst_row_sums_secondnegative_body_steps_bound + S fs_i_dst_row_sums_secondnegative_body_steps = n) -> exists fs_a_dst_row_sums_secondnegative_body_steps fs_r_dst_row_sums_secondnegative_body_steps fs_s_dst_row_sums_secondnegative_body_steps. ((((exists fs_h_dst_row_sums_secondnegative_body_steps_summand. fs_h_dst_row_sums_secondnegative_body_steps_summand + S (fs_a_dst_row_sums_secondnegative_body_steps) = S ((S (fs_i_dst_row_sums_secondnegative_body_steps)) * dst_negative_scale_row_sums_second)) /\ exists fs_q_dst_row_sums_secondnegative_body_steps_summand. dst_negative_code_row_sums_second = fs_q_dst_row_sums_secondnegative_body_steps_summand * S ((S (fs_i_dst_row_sums_secondnegative_body_steps)) * dst_negative_scale_row_sums_second) + (fs_a_dst_row_sums_secondnegative_body_steps))) /\ ((((exists fs_h_dst_row_sums_secondnegative_body_steps_partial. fs_h_dst_row_sums_secondnegative_body_steps_partial + S (fs_r_dst_row_sums_secondnegative_body_steps) = S ((S (fs_i_dst_row_sums_secondnegative_body_steps)) * fs_v_dst_row_sums_secondnegative)) /\ exists fs_q_dst_row_sums_secondnegative_body_steps_partial. fs_u_dst_row_sums_secondnegative = fs_q_dst_row_sums_secondnegative_body_steps_partial * S ((S (fs_i_dst_row_sums_secondnegative_body_steps)) * fs_v_dst_row_sums_secondnegative) + (fs_r_dst_row_sums_secondnegative_body_steps))) /\ ((((exists fs_h_dst_row_sums_secondnegative_body_steps_successor. fs_h_dst_row_sums_secondnegative_body_steps_successor + S (fs_s_dst_row_sums_secondnegative_body_steps) = S ((S (S fs_i_dst_row_sums_secondnegative_body_steps)) * fs_v_dst_row_sums_secondnegative)) /\ exists fs_q_dst_row_sums_secondnegative_body_steps_successor. fs_u_dst_row_sums_secondnegative = fs_q_dst_row_sums_secondnegative_body_steps_successor * S ((S (S fs_i_dst_row_sums_secondnegative_body_steps)) * fs_v_dst_row_sums_secondnegative) + (fs_s_dst_row_sums_secondnegative_body_steps))) /\ fs_s_dst_row_sums_secondnegative_body_steps = fs_r_dst_row_sums_secondnegative_body_steps + fs_a_dst_row_sums_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_row_sums_secondresult ge_balance_negative_row_sums_secondresult. (((((b) = 2 * (ge_balance_positive_row_sums_secondresult) /\ (ge_balance_negative_row_sums_secondresult) = 0) \/ exists ge_signed_half_row_sums_secondresultdecode. (((b) = 2 * ge_signed_half_row_sums_secondresultdecode + 1 /\ (ge_balance_positive_row_sums_secondresult) = 0) /\ (ge_balance_negative_row_sums_secondresult) = S ge_signed_half_row_sums_secondresultdecode))) /\ ((dst_positive_sum_row_sums_second) + ge_balance_negative_row_sums_secondresult = (dst_negative_sum_row_sums_second) + ge_balance_positive_row_sums_secondresult))))))))) -> (((exists dst_positive_code_row_sums_actualsource_table dst_positive_scale_row_sums_actualsource_table dst_negative_code_row_sums_actualsource_table dst_negative_scale_row_sums_actualsource_table. (((T) = (((((dst_positive_code_row_sums_actualsource_table) + (dst_positive_scale_row_sums_actualsource_table)) * S ((dst_positive_code_row_sums_actualsource_table) + (dst_positive_scale_row_sums_actualsource_table)) + ((dst_positive_scale_row_sums_actualsource_table) + (dst_positive_scale_row_sums_actualsource_table))) + (((dst_negative_code_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)) * S ((dst_negative_code_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)) + ((dst_negative_scale_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)))) * S ((((dst_positive_code_row_sums_actualsource_table) + (dst_positive_scale_row_sums_actualsource_table)) * S ((dst_positive_code_row_sums_actualsource_table) + (dst_positive_scale_row_sums_actualsource_table)) + ((dst_positive_scale_row_sums_actualsource_table) + (dst_positive_scale_row_sums_actualsource_table))) + (((dst_negative_code_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)) * S ((dst_negative_code_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)) + ((dst_negative_scale_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)))) + ((((dst_negative_code_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)) * S ((dst_negative_code_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)) + ((dst_negative_scale_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table))) + (((dst_negative_code_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)) * S ((dst_negative_code_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)) + ((dst_negative_scale_row_sums_actualsource_table) + (dst_negative_scale_row_sums_actualsource_table)))))) /\ (forall dst_index_row_sums_actualsource_table. (exists pvs_le_gap_row_sums_actualsource_tabledomain. pvs_le_gap_row_sums_actualsource_tabledomain + (dst_index_row_sums_actualsource_table) = (0)) -> exists dst_positive_row_sums_actualsource_table dst_negative_row_sums_actualsource_table dst_value_row_sums_actualsource_table. ((((exists ff_h_pvs_row_sums_actualsource_tableentrypositive. ff_h_pvs_row_sums_actualsource_tableentrypositive + S (dst_positive_row_sums_actualsource_table) = S ((S (dst_index_row_sums_actualsource_table)) * dst_positive_scale_row_sums_actualsource_table)) /\ exists ff_q_pvs_row_sums_actualsource_tableentrypositive. dst_positive_code_row_sums_actualsource_table = ff_q_pvs_row_sums_actualsource_tableentrypositive * S ((S (dst_index_row_sums_actualsource_table)) * dst_positive_scale_row_sums_actualsource_table) + (dst_positive_row_sums_actualsource_table))) /\ (((((exists ff_h_pvs_row_sums_actualsource_tableentrynegative. ff_h_pvs_row_sums_actualsource_tableentrynegative + S (dst_negative_row_sums_actualsource_table) = S ((S (dst_index_row_sums_actualsource_table)) * dst_negative_scale_row_sums_actualsource_table)) /\ exists ff_q_pvs_row_sums_actualsource_tableentrynegative. dst_negative_code_row_sums_actualsource_table = ff_q_pvs_row_sums_actualsource_tableentrynegative * S ((S (dst_index_row_sums_actualsource_table)) * dst_negative_scale_row_sums_actualsource_table) + (dst_negative_row_sums_actualsource_table))) /\ (exists ge_balance_positive_row_sums_actualsource_tableentryvalue ge_balance_negative_row_sums_actualsource_tableentryvalue. (((((dst_value_row_sums_actualsource_table) = 2 * (ge_balance_positive_row_sums_actualsource_tableentryvalue) /\ (ge_balance_negative_row_sums_actualsource_tableentryvalue) = 0) \/ exists ge_signed_half_row_sums_actualsource_tableentryvaluedecode. (((dst_value_row_sums_actualsource_table) = 2 * ge_signed_half_row_sums_actualsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_actualsource_tableentryvalue) = 0) /\ (ge_balance_negative_row_sums_actualsource_tableentryvalue) = S ge_signed_half_row_sums_actualsource_tableentryvaluedecode))) /\ ((dst_positive_row_sums_actualsource_table) + ge_balance_negative_row_sums_actualsource_tableentryvalue = (dst_negative_row_sums_actualsource_table) + ge_balance_positive_row_sums_actualsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_row_sums_actualrow_table dst_positive_scale_row_sums_actualrow_table dst_negative_code_row_sums_actualrow_table dst_negative_scale_row_sums_actualrow_table. (((R) = (((((dst_positive_code_row_sums_actualrow_table) + (dst_positive_scale_row_sums_actualrow_table)) * S ((dst_positive_code_row_sums_actualrow_table) + (dst_positive_scale_row_sums_actualrow_table)) + ((dst_positive_scale_row_sums_actualrow_table) + (dst_positive_scale_row_sums_actualrow_table))) + (((dst_negative_code_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)) * S ((dst_negative_code_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)) + ((dst_negative_scale_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)))) * S ((((dst_positive_code_row_sums_actualrow_table) + (dst_positive_scale_row_sums_actualrow_table)) * S ((dst_positive_code_row_sums_actualrow_table) + (dst_positive_scale_row_sums_actualrow_table)) + ((dst_positive_scale_row_sums_actualrow_table) + (dst_positive_scale_row_sums_actualrow_table))) + (((dst_negative_code_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)) * S ((dst_negative_code_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)) + ((dst_negative_scale_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)))) + ((((dst_negative_code_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)) * S ((dst_negative_code_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)) + ((dst_negative_scale_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table))) + (((dst_negative_code_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)) * S ((dst_negative_code_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)) + ((dst_negative_scale_row_sums_actualrow_table) + (dst_negative_scale_row_sums_actualrow_table)))))) /\ (forall dst_index_row_sums_actualrow_table. (exists pvs_le_gap_row_sums_actualrow_tabledomain. pvs_le_gap_row_sums_actualrow_tabledomain + (dst_index_row_sums_actualrow_table) = (m)) -> exists dst_positive_row_sums_actualrow_table dst_negative_row_sums_actualrow_table dst_value_row_sums_actualrow_table. ((((exists ff_h_pvs_row_sums_actualrow_tableentrypositive. ff_h_pvs_row_sums_actualrow_tableentrypositive + S (dst_positive_row_sums_actualrow_table) = S ((S (dst_index_row_sums_actualrow_table)) * dst_positive_scale_row_sums_actualrow_table)) /\ exists ff_q_pvs_row_sums_actualrow_tableentrypositive. dst_positive_code_row_sums_actualrow_table = ff_q_pvs_row_sums_actualrow_tableentrypositive * S ((S (dst_index_row_sums_actualrow_table)) * dst_positive_scale_row_sums_actualrow_table) + (dst_positive_row_sums_actualrow_table))) /\ (((((exists ff_h_pvs_row_sums_actualrow_tableentrynegative. ff_h_pvs_row_sums_actualrow_tableentrynegative + S (dst_negative_row_sums_actualrow_table) = S ((S (dst_index_row_sums_actualrow_table)) * dst_negative_scale_row_sums_actualrow_table)) /\ exists ff_q_pvs_row_sums_actualrow_tableentrynegative. dst_negative_code_row_sums_actualrow_table = ff_q_pvs_row_sums_actualrow_tableentrynegative * S ((S (dst_index_row_sums_actualrow_table)) * dst_negative_scale_row_sums_actualrow_table) + (dst_negative_row_sums_actualrow_table))) /\ (exists ge_balance_positive_row_sums_actualrow_tableentryvalue ge_balance_negative_row_sums_actualrow_tableentryvalue. (((((dst_value_row_sums_actualrow_table) = 2 * (ge_balance_positive_row_sums_actualrow_tableentryvalue) /\ (ge_balance_negative_row_sums_actualrow_tableentryvalue) = 0) \/ exists ge_signed_half_row_sums_actualrow_tableentryvaluedecode. (((dst_value_row_sums_actualrow_table) = 2 * ge_signed_half_row_sums_actualrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_actualrow_tableentryvalue) = 0) /\ (ge_balance_negative_row_sums_actualrow_tableentryvalue) = S ge_signed_half_row_sums_actualrow_tableentryvaluedecode))) /\ ((dst_positive_row_sums_actualrow_table) + ge_balance_negative_row_sums_actualrow_tableentryvalue = (dst_negative_row_sums_actualrow_table) + ge_balance_positive_row_sums_actualrow_tableentryvalue))))))))) /\ (forall srt_index_row_sums_actual. (exists pvs_gap_row_sums_actualbound. pvs_gap_row_sums_actualbound + S (srt_index_row_sums_actual) = (m)) -> exists srt_value_row_sums_actual. (((exists dst_positive_code_row_sums_actualrowentry dst_positive_scale_row_sums_actualrowentry dst_negative_code_row_sums_actualrowentry dst_negative_scale_row_sums_actualrowentry dst_positive_row_sums_actualrowentry dst_negative_row_sums_actualrowentry. (((R) = (((((dst_positive_code_row_sums_actualrowentry) + (dst_positive_scale_row_sums_actualrowentry)) * S ((dst_positive_code_row_sums_actualrowentry) + (dst_positive_scale_row_sums_actualrowentry)) + ((dst_positive_scale_row_sums_actualrowentry) + (dst_positive_scale_row_sums_actualrowentry))) + (((dst_negative_code_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)) * S ((dst_negative_code_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)) + ((dst_negative_scale_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)))) * S ((((dst_positive_code_row_sums_actualrowentry) + (dst_positive_scale_row_sums_actualrowentry)) * S ((dst_positive_code_row_sums_actualrowentry) + (dst_positive_scale_row_sums_actualrowentry)) + ((dst_positive_scale_row_sums_actualrowentry) + (dst_positive_scale_row_sums_actualrowentry))) + (((dst_negative_code_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)) * S ((dst_negative_code_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)) + ((dst_negative_scale_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)))) + ((((dst_negative_code_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)) * S ((dst_negative_code_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)) + ((dst_negative_scale_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry))) + (((dst_negative_code_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)) * S ((dst_negative_code_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)) + ((dst_negative_scale_row_sums_actualrowentry) + (dst_negative_scale_row_sums_actualrowentry)))))) /\ (((((exists ff_h_pvs_row_sums_actualrowentrypositive. ff_h_pvs_row_sums_actualrowentrypositive + S (dst_positive_row_sums_actualrowentry) = S ((S (srt_index_row_sums_actual)) * dst_positive_scale_row_sums_actualrowentry)) /\ exists ff_q_pvs_row_sums_actualrowentrypositive. dst_positive_code_row_sums_actualrowentry = ff_q_pvs_row_sums_actualrowentrypositive * S ((S (srt_index_row_sums_actual)) * dst_positive_scale_row_sums_actualrowentry) + (dst_positive_row_sums_actualrowentry))) /\ (((((exists ff_h_pvs_row_sums_actualrowentrynegative. ff_h_pvs_row_sums_actualrowentrynegative + S (dst_negative_row_sums_actualrowentry) = S ((S (srt_index_row_sums_actual)) * dst_negative_scale_row_sums_actualrowentry)) /\ exists ff_q_pvs_row_sums_actualrowentrynegative. dst_negative_code_row_sums_actualrowentry = ff_q_pvs_row_sums_actualrowentrynegative * S ((S (srt_index_row_sums_actual)) * dst_negative_scale_row_sums_actualrowentry) + (dst_negative_row_sums_actualrowentry))) /\ (exists ge_balance_positive_row_sums_actualrowentryvalue ge_balance_negative_row_sums_actualrowentryvalue. (((((srt_value_row_sums_actual) = 2 * (ge_balance_positive_row_sums_actualrowentryvalue) /\ (ge_balance_negative_row_sums_actualrowentryvalue) = 0) \/ exists ge_signed_half_row_sums_actualrowentryvaluedecode. (((srt_value_row_sums_actual) = 2 * ge_signed_half_row_sums_actualrowentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_actualrowentryvalue) = 0) /\ (ge_balance_negative_row_sums_actualrowentryvalue) = S ge_signed_half_row_sums_actualrowentryvaluedecode))) /\ ((dst_positive_row_sums_actualrowentry) + ge_balance_negative_row_sums_actualrowentryvalue = (dst_negative_row_sums_actualrowentry) + ge_balance_positive_row_sums_actualrowentryvalue))))))))) /\ (exists srs_slice_row_sums_actualrowrow_sum. ((((exists dst_positive_code_row_sums_actualrowrow_sumslicesource_table dst_positive_scale_row_sums_actualrowrow_sumslicesource_table dst_negative_code_row_sums_actualrowrow_sumslicesource_table dst_negative_scale_row_sums_actualrowrow_sumslicesource_table. (((T) = (((((dst_positive_code_row_sums_actualrowrow_sumslicesource_table) + (dst_positive_scale_row_sums_actualrowrow_sumslicesource_table)) * S ((dst_positive_code_row_sums_actualrowrow_sumslicesource_table) + (dst_positive_scale_row_sums_actualrowrow_sumslicesource_table)) + ((dst_positive_scale_row_sums_actualrowrow_sumslicesource_table) + (dst_positive_scale_row_sums_actualrowrow_sumslicesource_table))) + (((dst_negative_code_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)) * S ((dst_negative_code_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)) + ((dst_negative_scale_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)))) * S ((((dst_positive_code_row_sums_actualrowrow_sumslicesource_table) + (dst_positive_scale_row_sums_actualrowrow_sumslicesource_table)) * S ((dst_positive_code_row_sums_actualrowrow_sumslicesource_table) + (dst_positive_scale_row_sums_actualrowrow_sumslicesource_table)) + ((dst_positive_scale_row_sums_actualrowrow_sumslicesource_table) + (dst_positive_scale_row_sums_actualrowrow_sumslicesource_table))) + (((dst_negative_code_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)) * S ((dst_negative_code_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)) + ((dst_negative_scale_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)))) + ((((dst_negative_code_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)) * S ((dst_negative_code_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)) + ((dst_negative_scale_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table))) + (((dst_negative_code_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)) * S ((dst_negative_code_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)) + ((dst_negative_scale_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)))))) /\ (forall dst_index_row_sums_actualrowrow_sumslicesource_table. (exists pvs_le_gap_row_sums_actualrowrow_sumslicesource_tabledomain. pvs_le_gap_row_sums_actualrowrow_sumslicesource_tabledomain + (dst_index_row_sums_actualrowrow_sumslicesource_table) = (0)) -> exists dst_positive_row_sums_actualrowrow_sumslicesource_table dst_negative_row_sums_actualrowrow_sumslicesource_table dst_value_row_sums_actualrowrow_sumslicesource_table. ((((exists ff_h_pvs_row_sums_actualrowrow_sumslicesource_tableentrypositive. ff_h_pvs_row_sums_actualrowrow_sumslicesource_tableentrypositive + S (dst_positive_row_sums_actualrowrow_sumslicesource_table) = S ((S (dst_index_row_sums_actualrowrow_sumslicesource_table)) * dst_positive_scale_row_sums_actualrowrow_sumslicesource_table)) /\ exists ff_q_pvs_row_sums_actualrowrow_sumslicesource_tableentrypositive. dst_positive_code_row_sums_actualrowrow_sumslicesource_table = ff_q_pvs_row_sums_actualrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_row_sums_actualrowrow_sumslicesource_table)) * dst_positive_scale_row_sums_actualrowrow_sumslicesource_table) + (dst_positive_row_sums_actualrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_row_sums_actualrowrow_sumslicesource_tableentrynegative. ff_h_pvs_row_sums_actualrowrow_sumslicesource_tableentrynegative + S (dst_negative_row_sums_actualrowrow_sumslicesource_table) = S ((S (dst_index_row_sums_actualrowrow_sumslicesource_table)) * dst_negative_scale_row_sums_actualrowrow_sumslicesource_table)) /\ exists ff_q_pvs_row_sums_actualrowrow_sumslicesource_tableentrynegative. dst_negative_code_row_sums_actualrowrow_sumslicesource_table = ff_q_pvs_row_sums_actualrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_row_sums_actualrowrow_sumslicesource_table)) * dst_negative_scale_row_sums_actualrowrow_sumslicesource_table) + (dst_negative_row_sums_actualrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_row_sums_actualrowrow_sumslicesource_tableentryvalue ge_balance_negative_row_sums_actualrowrow_sumslicesource_tableentryvalue. (((((dst_value_row_sums_actualrowrow_sumslicesource_table) = 2 * (ge_balance_positive_row_sums_actualrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_row_sums_actualrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_row_sums_actualrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_row_sums_actualrowrow_sumslicesource_table) = 2 * ge_signed_half_row_sums_actualrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_actualrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_row_sums_actualrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_row_sums_actualrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_row_sums_actualrowrow_sumslicesource_table) + ge_balance_negative_row_sums_actualrowrow_sumslicesource_tableentryvalue = (dst_negative_row_sums_actualrowrow_sumslicesource_table) + ge_balance_positive_row_sums_actualrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_row_sums_actualrowrow_sumsliceoutput_table dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table dst_negative_code_row_sums_actualrowrow_sumsliceoutput_table dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table. (((srs_slice_row_sums_actualrowrow_sum) = (((((dst_positive_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table)) * S ((dst_positive_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table)) + ((dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table) + (dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table))) + (((dst_negative_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table)) * S ((dst_positive_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table)) + ((dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table) + (dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table))) + (((dst_negative_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table))) + (((dst_negative_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_row_sums_actualrowrow_sumsliceoutput_table. (exists pvs_le_gap_row_sums_actualrowrow_sumsliceoutput_tabledomain. pvs_le_gap_row_sums_actualrowrow_sumsliceoutput_tabledomain + (dst_index_row_sums_actualrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_row_sums_actualrowrow_sumsliceoutput_table dst_negative_row_sums_actualrowrow_sumsliceoutput_table dst_value_row_sums_actualrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_row_sums_actualrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_row_sums_actualrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_row_sums_actualrowrow_sumsliceoutput_table) = S ((S (dst_index_row_sums_actualrowrow_sumsliceoutput_table)) * dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_row_sums_actualrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_row_sums_actualrowrow_sumsliceoutput_table = ff_q_pvs_row_sums_actualrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_row_sums_actualrowrow_sumsliceoutput_table)) * dst_positive_scale_row_sums_actualrowrow_sumsliceoutput_table) + (dst_positive_row_sums_actualrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_row_sums_actualrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_row_sums_actualrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_row_sums_actualrowrow_sumsliceoutput_table) = S ((S (dst_index_row_sums_actualrowrow_sumsliceoutput_table)) * dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_row_sums_actualrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_row_sums_actualrowrow_sumsliceoutput_table = ff_q_pvs_row_sums_actualrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_row_sums_actualrowrow_sumsliceoutput_table)) * dst_negative_scale_row_sums_actualrowrow_sumsliceoutput_table) + (dst_negative_row_sums_actualrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_row_sums_actualrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_row_sums_actualrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_row_sums_actualrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_row_sums_actualrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_row_sums_actualrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_row_sums_actualrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_row_sums_actualrowrow_sumsliceoutput_table) = 2 * ge_signed_half_row_sums_actualrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_actualrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_row_sums_actualrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_row_sums_actualrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_row_sums_actualrowrow_sumsliceoutput_table) + ge_balance_negative_row_sums_actualrowrow_sumsliceoutput_tableentryvalue = (dst_negative_row_sums_actualrowrow_sumsliceoutput_table) + ge_balance_positive_row_sums_actualrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_row_sums_actualrowrow_sumslice. (exists pvs_gap_row_sums_actualrowrow_sumslicebound. pvs_gap_row_sums_actualrowrow_sumslicebound + S (srs_index_row_sums_actualrowrow_sumslice) = (n)) -> exists srs_value_row_sums_actualrowrow_sumslice. (((exists dst_positive_code_row_sums_actualrowrow_sumsliceentrysource dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource dst_negative_code_row_sums_actualrowrow_sumsliceentrysource dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource dst_positive_row_sums_actualrowrow_sumsliceentrysource dst_negative_row_sums_actualrowrow_sumsliceentrysource. (((T) = (((((dst_positive_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource)) * S ((dst_positive_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource)) + ((dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource))) + (((dst_negative_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource)) * S ((dst_positive_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource)) + ((dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource))) + (((dst_negative_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)))) + ((((dst_negative_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource))) + (((dst_negative_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_row_sums_actualrowrow_sumsliceentrysourcepositive. ff_h_pvs_row_sums_actualrowrow_sumsliceentrysourcepositive + S (dst_positive_row_sums_actualrowrow_sumsliceentrysource) = S ((S (((((0) + ((n) * (srt_index_row_sums_actual)))) + ((1) * (srs_index_row_sums_actualrowrow_sumslice))))) * dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_row_sums_actualrowrow_sumsliceentrysourcepositive. dst_positive_code_row_sums_actualrowrow_sumsliceentrysource = ff_q_pvs_row_sums_actualrowrow_sumsliceentrysourcepositive * S ((S (((((0) + ((n) * (srt_index_row_sums_actual)))) + ((1) * (srs_index_row_sums_actualrowrow_sumslice))))) * dst_positive_scale_row_sums_actualrowrow_sumsliceentrysource) + (dst_positive_row_sums_actualrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_row_sums_actualrowrow_sumsliceentrysourcenegative. ff_h_pvs_row_sums_actualrowrow_sumsliceentrysourcenegative + S (dst_negative_row_sums_actualrowrow_sumsliceentrysource) = S ((S (((((0) + ((n) * (srt_index_row_sums_actual)))) + ((1) * (srs_index_row_sums_actualrowrow_sumslice))))) * dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_row_sums_actualrowrow_sumsliceentrysourcenegative. dst_negative_code_row_sums_actualrowrow_sumsliceentrysource = ff_q_pvs_row_sums_actualrowrow_sumsliceentrysourcenegative * S ((S (((((0) + ((n) * (srt_index_row_sums_actual)))) + ((1) * (srs_index_row_sums_actualrowrow_sumslice))))) * dst_negative_scale_row_sums_actualrowrow_sumsliceentrysource) + (dst_negative_row_sums_actualrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_row_sums_actualrowrow_sumsliceentrysourcevalue ge_balance_negative_row_sums_actualrowrow_sumsliceentrysourcevalue. (((((srs_value_row_sums_actualrowrow_sumslice) = 2 * (ge_balance_positive_row_sums_actualrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_row_sums_actualrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_row_sums_actualrowrow_sumsliceentrysourcevaluedecode. (((srs_value_row_sums_actualrowrow_sumslice) = 2 * ge_signed_half_row_sums_actualrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_row_sums_actualrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_row_sums_actualrowrow_sumsliceentrysourcevalue) = S ge_signed_half_row_sums_actualrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_row_sums_actualrowrow_sumsliceentrysource) + ge_balance_negative_row_sums_actualrowrow_sumsliceentrysourcevalue = (dst_negative_row_sums_actualrowrow_sumsliceentrysource) + ge_balance_positive_row_sums_actualrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_row_sums_actualrowrow_sumsliceentryoutput dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput dst_negative_code_row_sums_actualrowrow_sumsliceentryoutput dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput dst_positive_row_sums_actualrowrow_sumsliceentryoutput dst_negative_row_sums_actualrowrow_sumsliceentryoutput. (((srs_slice_row_sums_actualrowrow_sum) = (((((dst_positive_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput)) * S ((dst_positive_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput)) + ((dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput))) + (((dst_negative_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput)) * S ((dst_positive_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput)) + ((dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput) + (dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput))) + (((dst_negative_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput))) + (((dst_negative_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)) * S ((dst_negative_code_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)) + ((dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_row_sums_actualrowrow_sumsliceentryoutputpositive. ff_h_pvs_row_sums_actualrowrow_sumsliceentryoutputpositive + S (dst_positive_row_sums_actualrowrow_sumsliceentryoutput) = S ((S (srs_index_row_sums_actualrowrow_sumslice)) * dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_row_sums_actualrowrow_sumsliceentryoutputpositive. dst_positive_code_row_sums_actualrowrow_sumsliceentryoutput = ff_q_pvs_row_sums_actualrowrow_sumsliceentryoutputpositive * S ((S (srs_index_row_sums_actualrowrow_sumslice)) * dst_positive_scale_row_sums_actualrowrow_sumsliceentryoutput) + (dst_positive_row_sums_actualrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_row_sums_actualrowrow_sumsliceentryoutputnegative. ff_h_pvs_row_sums_actualrowrow_sumsliceentryoutputnegative + S (dst_negative_row_sums_actualrowrow_sumsliceentryoutput) = S ((S (srs_index_row_sums_actualrowrow_sumslice)) * dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_row_sums_actualrowrow_sumsliceentryoutputnegative. dst_negative_code_row_sums_actualrowrow_sumsliceentryoutput = ff_q_pvs_row_sums_actualrowrow_sumsliceentryoutputnegative * S ((S (srs_index_row_sums_actualrowrow_sumslice)) * dst_negative_scale_row_sums_actualrowrow_sumsliceentryoutput) + (dst_negative_row_sums_actualrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_row_sums_actualrowrow_sumsliceentryoutputvalue ge_balance_negative_row_sums_actualrowrow_sumsliceentryoutputvalue. (((((srs_value_row_sums_actualrowrow_sumslice) = 2 * (ge_balance_positive_row_sums_actualrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_row_sums_actualrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_row_sums_actualrowrow_sumsliceentryoutputvaluedecode. (((srs_value_row_sums_actualrowrow_sumslice) = 2 * ge_signed_half_row_sums_actualrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_row_sums_actualrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_row_sums_actualrowrow_sumsliceentryoutputvalue) = S ge_signed_half_row_sums_actualrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_row_sums_actualrowrow_sumsliceentryoutput) + ge_balance_negative_row_sums_actualrowrow_sumsliceentryoutputvalue = (dst_negative_row_sums_actualrowrow_sumsliceentryoutput) + ge_balance_positive_row_sums_actualrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_row_sums_actualrowrow_sumsum dst_positive_scale_row_sums_actualrowrow_sumsum dst_negative_code_row_sums_actualrowrow_sumsum dst_negative_scale_row_sums_actualrowrow_sumsum dst_positive_sum_row_sums_actualrowrow_sumsum dst_negative_sum_row_sums_actualrowrow_sumsum. (((srs_slice_row_sums_actualrowrow_sum) = (((((dst_positive_code_row_sums_actualrowrow_sumsum) + (dst_positive_scale_row_sums_actualrowrow_sumsum)) * S ((dst_positive_code_row_sums_actualrowrow_sumsum) + (dst_positive_scale_row_sums_actualrowrow_sumsum)) + ((dst_positive_scale_row_sums_actualrowrow_sumsum) + (dst_positive_scale_row_sums_actualrowrow_sumsum))) + (((dst_negative_code_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)) * S ((dst_negative_code_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)) + ((dst_negative_scale_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)))) * S ((((dst_positive_code_row_sums_actualrowrow_sumsum) + (dst_positive_scale_row_sums_actualrowrow_sumsum)) * S ((dst_positive_code_row_sums_actualrowrow_sumsum) + (dst_positive_scale_row_sums_actualrowrow_sumsum)) + ((dst_positive_scale_row_sums_actualrowrow_sumsum) + (dst_positive_scale_row_sums_actualrowrow_sumsum))) + (((dst_negative_code_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)) * S ((dst_negative_code_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)) + ((dst_negative_scale_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)))) + ((((dst_negative_code_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)) * S ((dst_negative_code_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)) + ((dst_negative_scale_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum))) + (((dst_negative_code_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)) * S ((dst_negative_code_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)) + ((dst_negative_scale_row_sums_actualrowrow_sumsum) + (dst_negative_scale_row_sums_actualrowrow_sumsum)))))) /\ (((exists fs_u_dst_row_sums_actualrowrow_sumsumpositive fs_v_dst_row_sums_actualrowrow_sumsumpositive. ((((exists fs_h_dst_row_sums_actualrowrow_sumsumpositive_body_start. fs_h_dst_row_sums_actualrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_row_sums_actualrowrow_sumsumpositive)) /\ exists fs_q_dst_row_sums_actualrowrow_sumsumpositive_body_start. fs_u_dst_row_sums_actualrowrow_sumsumpositive = fs_q_dst_row_sums_actualrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_row_sums_actualrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_row_sums_actualrowrow_sumsumpositive_body_terminal. fs_h_dst_row_sums_actualrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_row_sums_actualrowrow_sumsum) = S ((S (n)) * fs_v_dst_row_sums_actualrowrow_sumsumpositive)) /\ exists fs_q_dst_row_sums_actualrowrow_sumsumpositive_body_terminal. fs_u_dst_row_sums_actualrowrow_sumsumpositive = fs_q_dst_row_sums_actualrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_row_sums_actualrowrow_sumsumpositive) + (dst_positive_sum_row_sums_actualrowrow_sumsum))) /\ forall fs_i_dst_row_sums_actualrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_row_sums_actualrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_row_sums_actualrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_row_sums_actualrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_row_sums_actualrowrow_sumsumpositive_body_steps fs_r_dst_row_sums_actualrowrow_sumsumpositive_body_steps fs_s_dst_row_sums_actualrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_row_sums_actualrowrow_sumsumpositive_body_steps_summand. fs_h_dst_row_sums_actualrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_row_sums_actualrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_row_sums_actualrowrow_sumsumpositive_body_steps)) * dst_positive_scale_row_sums_actualrowrow_sumsum)) /\ exists fs_q_dst_row_sums_actualrowrow_sumsumpositive_body_steps_summand. dst_positive_code_row_sums_actualrowrow_sumsum = fs_q_dst_row_sums_actualrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_row_sums_actualrowrow_sumsumpositive_body_steps)) * dst_positive_scale_row_sums_actualrowrow_sumsum) + (fs_a_dst_row_sums_actualrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_row_sums_actualrowrow_sumsumpositive_body_steps_partial. fs_h_dst_row_sums_actualrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_row_sums_actualrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_row_sums_actualrowrow_sumsumpositive_body_steps)) * fs_v_dst_row_sums_actualrowrow_sumsumpositive)) /\ exists fs_q_dst_row_sums_actualrowrow_sumsumpositive_body_steps_partial. fs_u_dst_row_sums_actualrowrow_sumsumpositive = fs_q_dst_row_sums_actualrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_row_sums_actualrowrow_sumsumpositive_body_steps)) * fs_v_dst_row_sums_actualrowrow_sumsumpositive) + (fs_r_dst_row_sums_actualrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_row_sums_actualrowrow_sumsumpositive_body_steps_successor. fs_h_dst_row_sums_actualrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_row_sums_actualrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_row_sums_actualrowrow_sumsumpositive_body_steps)) * fs_v_dst_row_sums_actualrowrow_sumsumpositive)) /\ exists fs_q_dst_row_sums_actualrowrow_sumsumpositive_body_steps_successor. fs_u_dst_row_sums_actualrowrow_sumsumpositive = fs_q_dst_row_sums_actualrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_row_sums_actualrowrow_sumsumpositive_body_steps)) * fs_v_dst_row_sums_actualrowrow_sumsumpositive) + (fs_s_dst_row_sums_actualrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_row_sums_actualrowrow_sumsumpositive_body_steps = fs_r_dst_row_sums_actualrowrow_sumsumpositive_body_steps + fs_a_dst_row_sums_actualrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_row_sums_actualrowrow_sumsumnegative fs_v_dst_row_sums_actualrowrow_sumsumnegative. ((((exists fs_h_dst_row_sums_actualrowrow_sumsumnegative_body_start. fs_h_dst_row_sums_actualrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_row_sums_actualrowrow_sumsumnegative)) /\ exists fs_q_dst_row_sums_actualrowrow_sumsumnegative_body_start. fs_u_dst_row_sums_actualrowrow_sumsumnegative = fs_q_dst_row_sums_actualrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_row_sums_actualrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_row_sums_actualrowrow_sumsumnegative_body_terminal. fs_h_dst_row_sums_actualrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_row_sums_actualrowrow_sumsum) = S ((S (n)) * fs_v_dst_row_sums_actualrowrow_sumsumnegative)) /\ exists fs_q_dst_row_sums_actualrowrow_sumsumnegative_body_terminal. fs_u_dst_row_sums_actualrowrow_sumsumnegative = fs_q_dst_row_sums_actualrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_row_sums_actualrowrow_sumsumnegative) + (dst_negative_sum_row_sums_actualrowrow_sumsum))) /\ forall fs_i_dst_row_sums_actualrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_row_sums_actualrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_row_sums_actualrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_row_sums_actualrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_row_sums_actualrowrow_sumsumnegative_body_steps fs_r_dst_row_sums_actualrowrow_sumsumnegative_body_steps fs_s_dst_row_sums_actualrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_row_sums_actualrowrow_sumsumnegative_body_steps_summand. fs_h_dst_row_sums_actualrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_row_sums_actualrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_row_sums_actualrowrow_sumsumnegative_body_steps)) * dst_negative_scale_row_sums_actualrowrow_sumsum)) /\ exists fs_q_dst_row_sums_actualrowrow_sumsumnegative_body_steps_summand. dst_negative_code_row_sums_actualrowrow_sumsum = fs_q_dst_row_sums_actualrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_row_sums_actualrowrow_sumsumnegative_body_steps)) * dst_negative_scale_row_sums_actualrowrow_sumsum) + (fs_a_dst_row_sums_actualrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_row_sums_actualrowrow_sumsumnegative_body_steps_partial. fs_h_dst_row_sums_actualrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_row_sums_actualrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_row_sums_actualrowrow_sumsumnegative_body_steps)) * fs_v_dst_row_sums_actualrowrow_sumsumnegative)) /\ exists fs_q_dst_row_sums_actualrowrow_sumsumnegative_body_steps_partial. fs_u_dst_row_sums_actualrowrow_sumsumnegative = fs_q_dst_row_sums_actualrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_row_sums_actualrowrow_sumsumnegative_body_steps)) * fs_v_dst_row_sums_actualrowrow_sumsumnegative) + (fs_r_dst_row_sums_actualrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_row_sums_actualrowrow_sumsumnegative_body_steps_successor. fs_h_dst_row_sums_actualrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_row_sums_actualrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_row_sums_actualrowrow_sumsumnegative_body_steps)) * fs_v_dst_row_sums_actualrowrow_sumsumnegative)) /\ exists fs_q_dst_row_sums_actualrowrow_sumsumnegative_body_steps_successor. fs_u_dst_row_sums_actualrowrow_sumsumnegative = fs_q_dst_row_sums_actualrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_row_sums_actualrowrow_sumsumnegative_body_steps)) * fs_v_dst_row_sums_actualrowrow_sumsumnegative) + (fs_s_dst_row_sums_actualrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_row_sums_actualrowrow_sumsumnegative_body_steps = fs_r_dst_row_sums_actualrowrow_sumsumnegative_body_steps + fs_a_dst_row_sums_actualrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_row_sums_actualrowrow_sumsumresult ge_balance_negative_row_sums_actualrowrow_sumsumresult. (((((srt_value_row_sums_actual) = 2 * (ge_balance_positive_row_sums_actualrowrow_sumsumresult) /\ (ge_balance_negative_row_sums_actualrowrow_sumsumresult) = 0) \/ exists ge_signed_half_row_sums_actualrowrow_sumsumresultdecode. (((srt_value_row_sums_actual) = 2 * ge_signed_half_row_sums_actualrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_row_sums_actualrowrow_sumsumresult) = 0) /\ (ge_balance_negative_row_sums_actualrowrow_sumsumresult) = S ge_signed_half_row_sums_actualrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_row_sums_actualrowrow_sumsum) + ge_balance_negative_row_sums_actualrowrow_sumsumresult = (dst_negative_sum_row_sums_actualrowrow_sumsum) + ge_balance_positive_row_sums_actualrowrow_sumsumresult)))))))))))))))))) -> (((exists dst_positive_code_row_sums_resultinput_table dst_positive_scale_row_sums_resultinput_table dst_negative_code_row_sums_resultinput_table dst_negative_scale_row_sums_resultinput_table. (((F) = (((((dst_positive_code_row_sums_resultinput_table) + (dst_positive_scale_row_sums_resultinput_table)) * S ((dst_positive_code_row_sums_resultinput_table) + (dst_positive_scale_row_sums_resultinput_table)) + ((dst_positive_scale_row_sums_resultinput_table) + (dst_positive_scale_row_sums_resultinput_table))) + (((dst_negative_code_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)) * S ((dst_negative_code_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)) + ((dst_negative_scale_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)))) * S ((((dst_positive_code_row_sums_resultinput_table) + (dst_positive_scale_row_sums_resultinput_table)) * S ((dst_positive_code_row_sums_resultinput_table) + (dst_positive_scale_row_sums_resultinput_table)) + ((dst_positive_scale_row_sums_resultinput_table) + (dst_positive_scale_row_sums_resultinput_table))) + (((dst_negative_code_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)) * S ((dst_negative_code_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)) + ((dst_negative_scale_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)))) + ((((dst_negative_code_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)) * S ((dst_negative_code_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)) + ((dst_negative_scale_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table))) + (((dst_negative_code_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)) * S ((dst_negative_code_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)) + ((dst_negative_scale_row_sums_resultinput_table) + (dst_negative_scale_row_sums_resultinput_table)))))) /\ (forall dst_index_row_sums_resultinput_table. (exists pvs_le_gap_row_sums_resultinput_tabledomain. pvs_le_gap_row_sums_resultinput_tabledomain + (dst_index_row_sums_resultinput_table) = (m)) -> exists dst_positive_row_sums_resultinput_table dst_negative_row_sums_resultinput_table dst_value_row_sums_resultinput_table. ((((exists ff_h_pvs_row_sums_resultinput_tableentrypositive. ff_h_pvs_row_sums_resultinput_tableentrypositive + S (dst_positive_row_sums_resultinput_table) = S ((S (dst_index_row_sums_resultinput_table)) * dst_positive_scale_row_sums_resultinput_table)) /\ exists ff_q_pvs_row_sums_resultinput_tableentrypositive. dst_positive_code_row_sums_resultinput_table = ff_q_pvs_row_sums_resultinput_tableentrypositive * S ((S (dst_index_row_sums_resultinput_table)) * dst_positive_scale_row_sums_resultinput_table) + (dst_positive_row_sums_resultinput_table))) /\ (((((exists ff_h_pvs_row_sums_resultinput_tableentrynegative. ff_h_pvs_row_sums_resultinput_tableentrynegative + S (dst_negative_row_sums_resultinput_table) = S ((S (dst_index_row_sums_resultinput_table)) * dst_negative_scale_row_sums_resultinput_table)) /\ exists ff_q_pvs_row_sums_resultinput_tableentrynegative. dst_negative_code_row_sums_resultinput_table = ff_q_pvs_row_sums_resultinput_tableentrynegative * S ((S (dst_index_row_sums_resultinput_table)) * dst_negative_scale_row_sums_resultinput_table) + (dst_negative_row_sums_resultinput_table))) /\ (exists ge_balance_positive_row_sums_resultinput_tableentryvalue ge_balance_negative_row_sums_resultinput_tableentryvalue. (((((dst_value_row_sums_resultinput_table) = 2 * (ge_balance_positive_row_sums_resultinput_tableentryvalue) /\ (ge_balance_negative_row_sums_resultinput_tableentryvalue) = 0) \/ exists ge_signed_half_row_sums_resultinput_tableentryvaluedecode. (((dst_value_row_sums_resultinput_table) = 2 * ge_signed_half_row_sums_resultinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_resultinput_tableentryvalue) = 0) /\ (ge_balance_negative_row_sums_resultinput_tableentryvalue) = S ge_signed_half_row_sums_resultinput_tableentryvaluedecode))) /\ ((dst_positive_row_sums_resultinput_table) + ge_balance_negative_row_sums_resultinput_tableentryvalue = (dst_negative_row_sums_resultinput_table) + ge_balance_positive_row_sums_resultinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_row_sums_resultoutput_table dst_positive_scale_row_sums_resultoutput_table dst_negative_code_row_sums_resultoutput_table dst_negative_scale_row_sums_resultoutput_table. (((R) = (((((dst_positive_code_row_sums_resultoutput_table) + (dst_positive_scale_row_sums_resultoutput_table)) * S ((dst_positive_code_row_sums_resultoutput_table) + (dst_positive_scale_row_sums_resultoutput_table)) + ((dst_positive_scale_row_sums_resultoutput_table) + (dst_positive_scale_row_sums_resultoutput_table))) + (((dst_negative_code_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)) * S ((dst_negative_code_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)) + ((dst_negative_scale_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)))) * S ((((dst_positive_code_row_sums_resultoutput_table) + (dst_positive_scale_row_sums_resultoutput_table)) * S ((dst_positive_code_row_sums_resultoutput_table) + (dst_positive_scale_row_sums_resultoutput_table)) + ((dst_positive_scale_row_sums_resultoutput_table) + (dst_positive_scale_row_sums_resultoutput_table))) + (((dst_negative_code_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)) * S ((dst_negative_code_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)) + ((dst_negative_scale_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)))) + ((((dst_negative_code_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)) * S ((dst_negative_code_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)) + ((dst_negative_scale_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table))) + (((dst_negative_code_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)) * S ((dst_negative_code_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)) + ((dst_negative_scale_row_sums_resultoutput_table) + (dst_negative_scale_row_sums_resultoutput_table)))))) /\ (forall dst_index_row_sums_resultoutput_table. (exists pvs_le_gap_row_sums_resultoutput_tabledomain. pvs_le_gap_row_sums_resultoutput_tabledomain + (dst_index_row_sums_resultoutput_table) = (m)) -> exists dst_positive_row_sums_resultoutput_table dst_negative_row_sums_resultoutput_table dst_value_row_sums_resultoutput_table. ((((exists ff_h_pvs_row_sums_resultoutput_tableentrypositive. ff_h_pvs_row_sums_resultoutput_tableentrypositive + S (dst_positive_row_sums_resultoutput_table) = S ((S (dst_index_row_sums_resultoutput_table)) * dst_positive_scale_row_sums_resultoutput_table)) /\ exists ff_q_pvs_row_sums_resultoutput_tableentrypositive. dst_positive_code_row_sums_resultoutput_table = ff_q_pvs_row_sums_resultoutput_tableentrypositive * S ((S (dst_index_row_sums_resultoutput_table)) * dst_positive_scale_row_sums_resultoutput_table) + (dst_positive_row_sums_resultoutput_table))) /\ (((((exists ff_h_pvs_row_sums_resultoutput_tableentrynegative. ff_h_pvs_row_sums_resultoutput_tableentrynegative + S (dst_negative_row_sums_resultoutput_table) = S ((S (dst_index_row_sums_resultoutput_table)) * dst_negative_scale_row_sums_resultoutput_table)) /\ exists ff_q_pvs_row_sums_resultoutput_tableentrynegative. dst_negative_code_row_sums_resultoutput_table = ff_q_pvs_row_sums_resultoutput_tableentrynegative * S ((S (dst_index_row_sums_resultoutput_table)) * dst_negative_scale_row_sums_resultoutput_table) + (dst_negative_row_sums_resultoutput_table))) /\ (exists ge_balance_positive_row_sums_resultoutput_tableentryvalue ge_balance_negative_row_sums_resultoutput_tableentryvalue. (((((dst_value_row_sums_resultoutput_table) = 2 * (ge_balance_positive_row_sums_resultoutput_tableentryvalue) /\ (ge_balance_negative_row_sums_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_row_sums_resultoutput_tableentryvaluedecode. (((dst_value_row_sums_resultoutput_table) = 2 * ge_signed_half_row_sums_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_sums_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_row_sums_resultoutput_tableentryvalue) = S ge_signed_half_row_sums_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_row_sums_resultoutput_table) + ge_balance_negative_row_sums_resultoutput_tableentryvalue = (dst_negative_row_sums_resultoutput_table) + ge_balance_positive_row_sums_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_row_sums_resultentries. (exists pvs_gap_row_sums_resultentriesbound. pvs_gap_row_sums_resultentriesbound + S (sto_index_row_sums_resultentries) = (m)) -> exists sto_input_row_sums_resultentries sto_output_row_sums_resultentries. ((exists dst_positive_code_row_sums_resultentriesentryinput dst_positive_scale_row_sums_resultentriesentryinput dst_negative_code_row_sums_resultentriesentryinput dst_negative_scale_row_sums_resultentriesentryinput dst_positive_row_sums_resultentriesentryinput dst_negative_row_sums_resultentriesentryinput. (((F) = (((((dst_positive_code_row_sums_resultentriesentryinput) + (dst_positive_scale_row_sums_resultentriesentryinput)) * S ((dst_positive_code_row_sums_resultentriesentryinput) + (dst_positive_scale_row_sums_resultentriesentryinput)) + ((dst_positive_scale_row_sums_resultentriesentryinput) + (dst_positive_scale_row_sums_resultentriesentryinput))) + (((dst_negative_code_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)) * S ((dst_negative_code_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)) + ((dst_negative_scale_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)))) * S ((((dst_positive_code_row_sums_resultentriesentryinput) + (dst_positive_scale_row_sums_resultentriesentryinput)) * S ((dst_positive_code_row_sums_resultentriesentryinput) + (dst_positive_scale_row_sums_resultentriesentryinput)) + ((dst_positive_scale_row_sums_resultentriesentryinput) + (dst_positive_scale_row_sums_resultentriesentryinput))) + (((dst_negative_code_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)) * S ((dst_negative_code_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)) + ((dst_negative_scale_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)))) + ((((dst_negative_code_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)) * S ((dst_negative_code_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)) + ((dst_negative_scale_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput))) + (((dst_negative_code_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)) * S ((dst_negative_code_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)) + ((dst_negative_scale_row_sums_resultentriesentryinput) + (dst_negative_scale_row_sums_resultentriesentryinput)))))) /\ (((((exists ff_h_pvs_row_sums_resultentriesentryinputpositive. ff_h_pvs_row_sums_resultentriesentryinputpositive + S (dst_positive_row_sums_resultentriesentryinput) = S ((S (sto_index_row_sums_resultentries)) * dst_positive_scale_row_sums_resultentriesentryinput)) /\ exists ff_q_pvs_row_sums_resultentriesentryinputpositive. dst_positive_code_row_sums_resultentriesentryinput = ff_q_pvs_row_sums_resultentriesentryinputpositive * S ((S (sto_index_row_sums_resultentries)) * dst_positive_scale_row_sums_resultentriesentryinput) + (dst_positive_row_sums_resultentriesentryinput))) /\ (((((exists ff_h_pvs_row_sums_resultentriesentryinputnegative. ff_h_pvs_row_sums_resultentriesentryinputnegative + S (dst_negative_row_sums_resultentriesentryinput) = S ((S (sto_index_row_sums_resultentries)) * dst_negative_scale_row_sums_resultentriesentryinput)) /\ exists ff_q_pvs_row_sums_resultentriesentryinputnegative. dst_negative_code_row_sums_resultentriesentryinput = ff_q_pvs_row_sums_resultentriesentryinputnegative * S ((S (sto_index_row_sums_resultentries)) * dst_negative_scale_row_sums_resultentriesentryinput) + (dst_negative_row_sums_resultentriesentryinput))) /\ (exists ge_balance_positive_row_sums_resultentriesentryinputvalue ge_balance_negative_row_sums_resultentriesentryinputvalue. (((((sto_input_row_sums_resultentries) = 2 * (ge_balance_positive_row_sums_resultentriesentryinputvalue) /\ (ge_balance_negative_row_sums_resultentriesentryinputvalue) = 0) \/ exists ge_signed_half_row_sums_resultentriesentryinputvaluedecode. (((sto_input_row_sums_resultentries) = 2 * ge_signed_half_row_sums_resultentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_row_sums_resultentriesentryinputvalue) = 0) /\ (ge_balance_negative_row_sums_resultentriesentryinputvalue) = S ge_signed_half_row_sums_resultentriesentryinputvaluedecode))) /\ ((dst_positive_row_sums_resultentriesentryinput) + ge_balance_negative_row_sums_resultentriesentryinputvalue = (dst_negative_row_sums_resultentriesentryinput) + ge_balance_positive_row_sums_resultentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_row_sums_resultentriesentryoutput dst_positive_scale_row_sums_resultentriesentryoutput dst_negative_code_row_sums_resultentriesentryoutput dst_negative_scale_row_sums_resultentriesentryoutput dst_positive_row_sums_resultentriesentryoutput dst_negative_row_sums_resultentriesentryoutput. (((R) = (((((dst_positive_code_row_sums_resultentriesentryoutput) + (dst_positive_scale_row_sums_resultentriesentryoutput)) * S ((dst_positive_code_row_sums_resultentriesentryoutput) + (dst_positive_scale_row_sums_resultentriesentryoutput)) + ((dst_positive_scale_row_sums_resultentriesentryoutput) + (dst_positive_scale_row_sums_resultentriesentryoutput))) + (((dst_negative_code_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)) * S ((dst_negative_code_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)) + ((dst_negative_scale_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)))) * S ((((dst_positive_code_row_sums_resultentriesentryoutput) + (dst_positive_scale_row_sums_resultentriesentryoutput)) * S ((dst_positive_code_row_sums_resultentriesentryoutput) + (dst_positive_scale_row_sums_resultentriesentryoutput)) + ((dst_positive_scale_row_sums_resultentriesentryoutput) + (dst_positive_scale_row_sums_resultentriesentryoutput))) + (((dst_negative_code_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)) * S ((dst_negative_code_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)) + ((dst_negative_scale_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)))) + ((((dst_negative_code_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)) * S ((dst_negative_code_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)) + ((dst_negative_scale_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput))) + (((dst_negative_code_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)) * S ((dst_negative_code_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)) + ((dst_negative_scale_row_sums_resultentriesentryoutput) + (dst_negative_scale_row_sums_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_row_sums_resultentriesentryoutputpositive. ff_h_pvs_row_sums_resultentriesentryoutputpositive + S (dst_positive_row_sums_resultentriesentryoutput) = S ((S (sto_index_row_sums_resultentries)) * dst_positive_scale_row_sums_resultentriesentryoutput)) /\ exists ff_q_pvs_row_sums_resultentriesentryoutputpositive. dst_positive_code_row_sums_resultentriesentryoutput = ff_q_pvs_row_sums_resultentriesentryoutputpositive * S ((S (sto_index_row_sums_resultentries)) * dst_positive_scale_row_sums_resultentriesentryoutput) + (dst_positive_row_sums_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_row_sums_resultentriesentryoutputnegative. ff_h_pvs_row_sums_resultentriesentryoutputnegative + S (dst_negative_row_sums_resultentriesentryoutput) = S ((S (sto_index_row_sums_resultentries)) * dst_negative_scale_row_sums_resultentriesentryoutput)) /\ exists ff_q_pvs_row_sums_resultentriesentryoutputnegative. dst_negative_code_row_sums_resultentriesentryoutput = ff_q_pvs_row_sums_resultentriesentryoutputnegative * S ((S (sto_index_row_sums_resultentries)) * dst_negative_scale_row_sums_resultentriesentryoutput) + (dst_negative_row_sums_resultentriesentryoutput))) /\ (exists ge_balance_positive_row_sums_resultentriesentryoutputvalue ge_balance_negative_row_sums_resultentriesentryoutputvalue. (((((sto_output_row_sums_resultentries) = 2 * (ge_balance_positive_row_sums_resultentriesentryoutputvalue) /\ (ge_balance_negative_row_sums_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_row_sums_resultentriesentryoutputvaluedecode. (((sto_output_row_sums_resultentries) = 2 * ge_signed_half_row_sums_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_row_sums_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_row_sums_resultentriesentryoutputvalue) = S ge_signed_half_row_sums_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_row_sums_resultentriesentryoutput) + ge_balance_negative_row_sums_resultentriesentryoutputvalue = (dst_negative_row_sums_resultentriesentryoutput) + ge_balance_positive_row_sums_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_row_sums_resultentriesentryoperation sto_an_row_sums_resultentriesentryoperation sto_bp_row_sums_resultentriesentryoperation sto_bn_row_sums_resultentriesentryoperation sto_cp_row_sums_resultentriesentryoperation sto_cn_row_sums_resultentriesentryoperation. (((((b) = 2 * (sto_ap_row_sums_resultentriesentryoperation) /\ (sto_an_row_sums_resultentriesentryoperation) = 0) \/ exists ge_signed_half_row_sums_resultentriesentryoperationleft. (((b) = 2 * ge_signed_half_row_sums_resultentriesentryoperationleft + 1 /\ (sto_ap_row_sums_resultentriesentryoperation) = 0) /\ (sto_an_row_sums_resultentriesentryoperation) = S ge_signed_half_row_sums_resultentriesentryoperationleft))) /\ ((((((sto_input_row_sums_resultentries) = 2 * (sto_bp_row_sums_resultentriesentryoperation) /\ (sto_bn_row_sums_resultentriesentryoperation) = 0) \/ exists ge_signed_half_row_sums_resultentriesentryoperationright. (((sto_input_row_sums_resultentries) = 2 * ge_signed_half_row_sums_resultentriesentryoperationright + 1 /\ (sto_bp_row_sums_resultentriesentryoperation) = 0) /\ (sto_bn_row_sums_resultentriesentryoperation) = S ge_signed_half_row_sums_resultentriesentryoperationright))) /\ ((((((sto_output_row_sums_resultentries) = 2 * (sto_cp_row_sums_resultentriesentryoperation) /\ (sto_cn_row_sums_resultentriesentryoperation) = 0) \/ exists ge_signed_half_row_sums_resultentriesentryoperationoutput. (((sto_output_row_sums_resultentries) = 2 * ge_signed_half_row_sums_resultentriesentryoperationoutput + 1 /\ (sto_cp_row_sums_resultentriesentryoperation) = 0) /\ (sto_cn_row_sums_resultentriesentryoperation) = S ge_signed_half_row_sums_resultentriesentryoperationoutput))) /\ ((sto_ap_row_sums_resultentriesentryoperation * sto_bp_row_sums_resultentriesentryoperation + sto_an_row_sums_resultentriesentryoperation * sto_bn_row_sums_resultentriesentryoperation) + sto_cn_row_sums_resultentriesentryoperation = (sto_ap_row_sums_resultentriesentryoperation * sto_bn_row_sums_resultentriesentryoperation + sto_an_row_sums_resultentriesentryoperation * sto_bp_row_sums_resultentriesentryoperation) + sto_cp_row_sums_resultentriesentryoperation)))))))))))))))Constructive proof overview
Generated structural guide
The genuinely constructed row-sum table is pointwise the first input multiplied by the actual second-input sum.
The unchanged tactic script uses 5 declared prerequisites and contains 76 exact native proof lines.
Alpha v34 checked-use · first admitted v32 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
signed_table_domain_resize Alpha theorem; checked-use authorized signed_table_lookup_any Alpha theorem; checked-use authorized signed_mul_commutative Alpha theorem; checked-use authorized MX0028 signed_cartesian_product_row_sum signed_rectangular_row_sums_lookup Alpha theorem; checked-use authorizedDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
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.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Separate the logical casesL11–16
03Use earlier factsL17–21
04Separate the logical casesL22–22
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L22
split
05Use earlier factsL23–23
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L23
exact hr_right_left
06Fix variables and assumptionsL24–25
07Establish haL26–31
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.
08Separate the logical casesL32–32
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L32
cases ha
09Establish hcL33–38
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.
10Separate the logical casesL39–39
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L39
cases hc
11Construct an explicit witnessL40–41
12Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
split
13Use earlier factsL43–43
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L43
exact ha_witness
14Separate the logical casesL44–44
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L44
split
15Use earlier factsL45–54
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L45
exact hc_witness - L46
specialize signed_mul_commutative (x) - L47
specialize signed_mul_commutative (b) - L48
specialize signed_mul_commutative (x1) - L49
apply signed_mul_commutative - L50
specialize signed_cartesian_product_row_sum (F) - L51
specialize signed_cartesian_product_row_sum (G) - L52
specialize signed_cartesian_product_row_sum (T) - L53
specialize signed_cartesian_product_row_sum (m) - L54
specialize signed_cartesian_product_row_sum (n)
16Use earlier factsL55–64
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L55
specialize signed_cartesian_product_row_sum (i) - L56
specialize signed_cartesian_product_row_sum (x) - L57
specialize signed_cartesian_product_row_sum (b) - L58
specialize signed_cartesian_product_row_sum (x1) - L59
apply signed_cartesian_product_row_sum - L60
exact hp - L61
exact hi - L62
exact ha_witness - L63
exact hb - L64
specialize signed_rectangular_row_sums_lookup (T)
17Use earlier factsL65–74
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L65
specialize signed_rectangular_row_sums_lookup (R) - L66
specialize signed_rectangular_row_sums_lookup (0) - L67
specialize signed_rectangular_row_sums_lookup (n) - L68
specialize signed_rectangular_row_sums_lookup (1) - L69
specialize signed_rectangular_row_sums_lookup (m) - L70
specialize signed_rectangular_row_sums_lookup (n) - L71
specialize signed_rectangular_row_sums_lookup (i) - L72
specialize signed_rectangular_row_sums_lookup (x1) - L73
apply signed_rectangular_row_sums_lookup - L74
exact hr
Original exact command ledger · 76 lines
- 0001
intro F - 0002
intro G - 0003
intro T - 0004
intro R - 0005
intro m - 0006
intro n - 0007
intro b - 0008
intro hp - 0009
intro hb - 0010
intro hr - 0011
cases hp - 0012
cases hp_right - 0013
cases hp_right_right - 0014
cases hr - 0015
cases hr_right - 0016
split - 0017
specialize signed_table_domain_resize (0) - 0018
specialize signed_table_domain_resize (m) - 0019
specialize signed_table_domain_resize (F) - 0020
apply signed_table_domain_resize - 0021
exact hp_left - 0022
split - 0023
exact hr_right_left - 0024
intro i - 0025
intro hi - 0026
have ha : exists a. (exists dst_positive_code_rows_scalar_source dst_positive_scale_rows_scalar_source dst_negative_code_rows_scalar_source dst_negative_scale_rows_scalar_source dst_positive_rows_scalar_source dst_negative_rows_scalar_source. (((F) = (((((dst_positive_code_rows_scalar_source) + (dst_positive_scale_rows_scalar_source)) * S ((dst_positive_code_rows_scalar_source) + (dst_positive_scale_rows_scalar_source)) + ((dst_positive_scale_rows_scalar_source) + (dst_positive_scale_rows_scalar_source))) + (((dst_negative_code_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)) * S ((dst_negative_code_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)) + ((dst_negative_scale_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)))) * S ((((dst_positive_code_rows_scalar_source) + (dst_positive_scale_rows_scalar_source)) * S ((dst_positive_code_rows_scalar_source) + (dst_positive_scale_rows_scalar_source)) + ((dst_positive_scale_rows_scalar_source) + (dst_positive_scale_rows_scalar_source))) + (((dst_negative_code_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)) * S ((dst_negative_code_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)) + ((dst_negative_scale_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)))) + ((((dst_negative_code_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)) * S ((dst_negative_code_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)) + ((dst_negative_scale_rows_scalar_source) + (dst_negative_scale_rows_scalar_source))) + (((dst_negative_code_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)) * S ((dst_negative_code_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)) + ((dst_negative_scale_rows_scalar_source) + (dst_negative_scale_rows_scalar_source)))))) /\ (((((exists ff_h_pvs_rows_scalar_sourcepositive. ff_h_pvs_rows_scalar_sourcepositive + S (dst_positive_rows_scalar_source) = S ((S (i)) * dst_positive_scale_rows_scalar_source)) /\ exists ff_q_pvs_rows_scalar_sourcepositive. dst_positive_code_rows_scalar_source = ff_q_pvs_rows_scalar_sourcepositive * S ((S (i)) * dst_positive_scale_rows_scalar_source) + (dst_positive_rows_scalar_source))) /\ (((((exists ff_h_pvs_rows_scalar_sourcenegative. ff_h_pvs_rows_scalar_sourcenegative + S (dst_negative_rows_scalar_source) = S ((S (i)) * dst_negative_scale_rows_scalar_source)) /\ exists ff_q_pvs_rows_scalar_sourcenegative. dst_negative_code_rows_scalar_source = ff_q_pvs_rows_scalar_sourcenegative * S ((S (i)) * dst_negative_scale_rows_scalar_source) + (dst_negative_rows_scalar_source))) /\ (exists ge_balance_positive_rows_scalar_sourcevalue ge_balance_negative_rows_scalar_sourcevalue. (((((a) = 2 * (ge_balance_positive_rows_scalar_sourcevalue) /\ (ge_balance_negative_rows_scalar_sourcevalue) = 0) \/ exists ge_signed_half_rows_scalar_sourcevaluedecode. (((a) = 2 * ge_signed_half_rows_scalar_sourcevaluedecode + 1 /\ (ge_balance_positive_rows_scalar_sourcevalue) = 0) /\ (ge_balance_negative_rows_scalar_sourcevalue) = S ge_signed_half_rows_scalar_sourcevaluedecode))) /\ ((dst_positive_rows_scalar_source) + ge_balance_negative_rows_scalar_sourcevalue = (dst_negative_rows_scalar_source) + ge_balance_positive_rows_scalar_sourcevalue))))))))) - 0027
specialize signed_table_lookup_any (0) - 0028
specialize signed_table_lookup_any (F) - 0029
specialize signed_table_lookup_any (i) - 0030
apply signed_table_lookup_any - 0031
exact hp_left - 0032
cases ha - 0033
have hc : exists c. (exists dst_positive_code_rows_scalar_output dst_positive_scale_rows_scalar_output dst_negative_code_rows_scalar_output dst_negative_scale_rows_scalar_output dst_positive_rows_scalar_output dst_negative_rows_scalar_output. (((R) = (((((dst_positive_code_rows_scalar_output) + (dst_positive_scale_rows_scalar_output)) * S ((dst_positive_code_rows_scalar_output) + (dst_positive_scale_rows_scalar_output)) + ((dst_positive_scale_rows_scalar_output) + (dst_positive_scale_rows_scalar_output))) + (((dst_negative_code_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)) * S ((dst_negative_code_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)) + ((dst_negative_scale_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)))) * S ((((dst_positive_code_rows_scalar_output) + (dst_positive_scale_rows_scalar_output)) * S ((dst_positive_code_rows_scalar_output) + (dst_positive_scale_rows_scalar_output)) + ((dst_positive_scale_rows_scalar_output) + (dst_positive_scale_rows_scalar_output))) + (((dst_negative_code_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)) * S ((dst_negative_code_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)) + ((dst_negative_scale_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)))) + ((((dst_negative_code_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)) * S ((dst_negative_code_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)) + ((dst_negative_scale_rows_scalar_output) + (dst_negative_scale_rows_scalar_output))) + (((dst_negative_code_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)) * S ((dst_negative_code_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)) + ((dst_negative_scale_rows_scalar_output) + (dst_negative_scale_rows_scalar_output)))))) /\ (((((exists ff_h_pvs_rows_scalar_outputpositive. ff_h_pvs_rows_scalar_outputpositive + S (dst_positive_rows_scalar_output) = S ((S (i)) * dst_positive_scale_rows_scalar_output)) /\ exists ff_q_pvs_rows_scalar_outputpositive. dst_positive_code_rows_scalar_output = ff_q_pvs_rows_scalar_outputpositive * S ((S (i)) * dst_positive_scale_rows_scalar_output) + (dst_positive_rows_scalar_output))) /\ (((((exists ff_h_pvs_rows_scalar_outputnegative. ff_h_pvs_rows_scalar_outputnegative + S (dst_negative_rows_scalar_output) = S ((S (i)) * dst_negative_scale_rows_scalar_output)) /\ exists ff_q_pvs_rows_scalar_outputnegative. dst_negative_code_rows_scalar_output = ff_q_pvs_rows_scalar_outputnegative * S ((S (i)) * dst_negative_scale_rows_scalar_output) + (dst_negative_rows_scalar_output))) /\ (exists ge_balance_positive_rows_scalar_outputvalue ge_balance_negative_rows_scalar_outputvalue. (((((c) = 2 * (ge_balance_positive_rows_scalar_outputvalue) /\ (ge_balance_negative_rows_scalar_outputvalue) = 0) \/ exists ge_signed_half_rows_scalar_outputvaluedecode. (((c) = 2 * ge_signed_half_rows_scalar_outputvaluedecode + 1 /\ (ge_balance_positive_rows_scalar_outputvalue) = 0) /\ (ge_balance_negative_rows_scalar_outputvalue) = S ge_signed_half_rows_scalar_outputvaluedecode))) /\ ((dst_positive_rows_scalar_output) + ge_balance_negative_rows_scalar_outputvalue = (dst_negative_rows_scalar_output) + ge_balance_positive_rows_scalar_outputvalue))))))))) - 0034
specialize signed_table_lookup_any (m) - 0035
specialize signed_table_lookup_any (R) - 0036
specialize signed_table_lookup_any (i) - 0037
apply signed_table_lookup_any - 0038
exact hr_right_left - 0039
cases hc - 0040
exists x - 0041
exists x1 - 0042
split - 0043
exact ha_witness - 0044
split - 0045
exact hc_witness - 0046
specialize signed_mul_commutative (x) - 0047
specialize signed_mul_commutative (b) - 0048
specialize signed_mul_commutative (x1) - 0049
apply signed_mul_commutative - 0050
specialize signed_cartesian_product_row_sum (F) - 0051
specialize signed_cartesian_product_row_sum (G) - 0052
specialize signed_cartesian_product_row_sum (T) - 0053
specialize signed_cartesian_product_row_sum (m) - 0054
specialize signed_cartesian_product_row_sum (n) - 0055
specialize signed_cartesian_product_row_sum (i) - 0056
specialize signed_cartesian_product_row_sum (x) - 0057
specialize signed_cartesian_product_row_sum (b) - 0058
specialize signed_cartesian_product_row_sum (x1) - 0059
apply signed_cartesian_product_row_sum - 0060
exact hp - 0061
exact hi - 0062
exact ha_witness - 0063
exact hb - 0064
specialize signed_rectangular_row_sums_lookup (T) - 0065
specialize signed_rectangular_row_sums_lookup (R) - 0066
specialize signed_rectangular_row_sums_lookup (0) - 0067
specialize signed_rectangular_row_sums_lookup (n) - 0068
specialize signed_rectangular_row_sums_lookup (1) - 0069
specialize signed_rectangular_row_sums_lookup (m) - 0070
specialize signed_rectangular_row_sums_lookup (n) - 0071
specialize signed_rectangular_row_sums_lookup (i) - 0072
specialize signed_rectangular_row_sums_lookup (x1) - 0073
apply signed_rectangular_row_sums_lookup - 0074
exact hr - 0075
exact hi - 0076
exact hc_witness