signed_cartesian_product_rectangular_sum

Exact expanded first-order arithmetic statement

forall F G T m n a b c. (((exists dst_positive_code_rect_productF dst_positive_scale_rect_productF dst_negative_code_rect_productF dst_negative_scale_rect_productF. (((F) = (((((dst_positive_code_rect_productF) + (dst_positive_scale_rect_productF)) * S ((dst_positive_code_rect_productF) + (dst_positive_scale_rect_productF)) + ((dst_positive_scale_rect_productF) + (dst_positive_scale_rect_productF))) + (((dst_negative_code_rect_productF) + (dst_negative_scale_rect_productF)) * S ((dst_negative_code_rect_productF) + (dst_negative_scale_rect_productF)) + ((dst_negative_scale_rect_productF) + (dst_negative_scale_rect_productF)))) * S ((((dst_positive_code_rect_productF) + (dst_positive_scale_rect_productF)) * S ((dst_positive_code_rect_productF) + (dst_positive_scale_rect_productF)) + ((dst_positive_scale_rect_productF) + (dst_positive_scale_rect_productF))) + (((dst_negative_code_rect_productF) + (dst_negative_scale_rect_productF)) * S ((dst_negative_code_rect_productF) + (dst_negative_scale_rect_productF)) + ((dst_negative_scale_rect_productF) + (dst_negative_scale_rect_productF)))) + ((((dst_negative_code_rect_productF) + (dst_negative_scale_rect_productF)) * S ((dst_negative_code_rect_productF) + (dst_negative_scale_rect_productF)) + ((dst_negative_scale_rect_productF) + (dst_negative_scale_rect_productF))) + (((dst_negative_code_rect_productF) + (dst_negative_scale_rect_productF)) * S ((dst_negative_code_rect_productF) + (dst_negative_scale_rect_productF)) + ((dst_negative_scale_rect_productF) + (dst_negative_scale_rect_productF)))))) /\ (forall dst_index_rect_productF. (exists pvs_le_gap_rect_productFdomain. pvs_le_gap_rect_productFdomain + (dst_index_rect_productF) = (0)) -> exists dst_positive_rect_productF dst_negative_rect_productF dst_value_rect_productF. ((((exists ff_h_pvs_rect_productFentrypositive. ff_h_pvs_rect_productFentrypositive + S (dst_positive_rect_productF) = S ((S (dst_index_rect_productF)) * dst_positive_scale_rect_productF)) /\ exists ff_q_pvs_rect_productFentrypositive. dst_positive_code_rect_productF = ff_q_pvs_rect_productFentrypositive * S ((S (dst_index_rect_productF)) * dst_positive_scale_rect_productF) + (dst_positive_rect_productF))) /\ (((((exists ff_h_pvs_rect_productFentrynegative. ff_h_pvs_rect_productFentrynegative + S (dst_negative_rect_productF) = S ((S (dst_index_rect_productF)) * dst_negative_scale_rect_productF)) /\ exists ff_q_pvs_rect_productFentrynegative. dst_negative_code_rect_productF = ff_q_pvs_rect_productFentrynegative * S ((S (dst_index_rect_productF)) * dst_negative_scale_rect_productF) + (dst_negative_rect_productF))) /\ (exists ge_balance_positive_rect_productFentryvalue ge_balance_negative_rect_productFentryvalue. (((((dst_value_rect_productF) = 2 * (ge_balance_positive_rect_productFentryvalue) /\ (ge_balance_negative_rect_productFentryvalue) = 0) \/ exists ge_signed_half_rect_productFentryvaluedecode. (((dst_value_rect_productF) = 2 * ge_signed_half_rect_productFentryvaluedecode + 1 /\ (ge_balance_positive_rect_productFentryvalue) = 0) /\ (ge_balance_negative_rect_productFentryvalue) = S ge_signed_half_rect_productFentryvaluedecode))) /\ ((dst_positive_rect_productF) + ge_balance_negative_rect_productFentryvalue = (dst_negative_rect_productF) + ge_balance_positive_rect_productFentryvalue))))))))) /\ (((exists dst_positive_code_rect_productG dst_positive_scale_rect_productG dst_negative_code_rect_productG dst_negative_scale_rect_productG. (((G) = (((((dst_positive_code_rect_productG) + (dst_positive_scale_rect_productG)) * S ((dst_positive_code_rect_productG) + (dst_positive_scale_rect_productG)) + ((dst_positive_scale_rect_productG) + (dst_positive_scale_rect_productG))) + (((dst_negative_code_rect_productG) + (dst_negative_scale_rect_productG)) * S ((dst_negative_code_rect_productG) + (dst_negative_scale_rect_productG)) + ((dst_negative_scale_rect_productG) + (dst_negative_scale_rect_productG)))) * S ((((dst_positive_code_rect_productG) + (dst_positive_scale_rect_productG)) * S ((dst_positive_code_rect_productG) + (dst_positive_scale_rect_productG)) + ((dst_positive_scale_rect_productG) + (dst_positive_scale_rect_productG))) + (((dst_negative_code_rect_productG) + (dst_negative_scale_rect_productG)) * S ((dst_negative_code_rect_productG) + (dst_negative_scale_rect_productG)) + ((dst_negative_scale_rect_productG) + (dst_negative_scale_rect_productG)))) + ((((dst_negative_code_rect_productG) + (dst_negative_scale_rect_productG)) * S ((dst_negative_code_rect_productG) + (dst_negative_scale_rect_productG)) + ((dst_negative_scale_rect_productG) + (dst_negative_scale_rect_productG))) + (((dst_negative_code_rect_productG) + (dst_negative_scale_rect_productG)) * S ((dst_negative_code_rect_productG) + (dst_negative_scale_rect_productG)) + ((dst_negative_scale_rect_productG) + (dst_negative_scale_rect_productG)))))) /\ (forall dst_index_rect_productG. (exists pvs_le_gap_rect_productGdomain. pvs_le_gap_rect_productGdomain + (dst_index_rect_productG) = (0)) -> exists dst_positive_rect_productG dst_negative_rect_productG dst_value_rect_productG. ((((exists ff_h_pvs_rect_productGentrypositive. ff_h_pvs_rect_productGentrypositive + S (dst_positive_rect_productG) = S ((S (dst_index_rect_productG)) * dst_positive_scale_rect_productG)) /\ exists ff_q_pvs_rect_productGentrypositive. dst_positive_code_rect_productG = ff_q_pvs_rect_productGentrypositive * S ((S (dst_index_rect_productG)) * dst_positive_scale_rect_productG) + (dst_positive_rect_productG))) /\ (((((exists ff_h_pvs_rect_productGentrynegative. ff_h_pvs_rect_productGentrynegative + S (dst_negative_rect_productG) = S ((S (dst_index_rect_productG)) * dst_negative_scale_rect_productG)) /\ exists ff_q_pvs_rect_productGentrynegative. dst_negative_code_rect_productG = ff_q_pvs_rect_productGentrynegative * S ((S (dst_index_rect_productG)) * dst_negative_scale_rect_productG) + (dst_negative_rect_productG))) /\ (exists ge_balance_positive_rect_productGentryvalue ge_balance_negative_rect_productGentryvalue. (((((dst_value_rect_productG) = 2 * (ge_balance_positive_rect_productGentryvalue) /\ (ge_balance_negative_rect_productGentryvalue) = 0) \/ exists ge_signed_half_rect_productGentryvaluedecode. (((dst_value_rect_productG) = 2 * ge_signed_half_rect_productGentryvaluedecode + 1 /\ (ge_balance_positive_rect_productGentryvalue) = 0) /\ (ge_balance_negative_rect_productGentryvalue) = S ge_signed_half_rect_productGentryvaluedecode))) /\ ((dst_positive_rect_productG) + ge_balance_negative_rect_productGentryvalue = (dst_negative_rect_productG) + ge_balance_positive_rect_productGentryvalue))))))))) /\ (((exists dst_positive_code_rect_productT dst_positive_scale_rect_productT dst_negative_code_rect_productT dst_negative_scale_rect_productT. (((T) = (((((dst_positive_code_rect_productT) + (dst_positive_scale_rect_productT)) * S ((dst_positive_code_rect_productT) + (dst_positive_scale_rect_productT)) + ((dst_positive_scale_rect_productT) + (dst_positive_scale_rect_productT))) + (((dst_negative_code_rect_productT) + (dst_negative_scale_rect_productT)) * S ((dst_negative_code_rect_productT) + (dst_negative_scale_rect_productT)) + ((dst_negative_scale_rect_productT) + (dst_negative_scale_rect_productT)))) * S ((((dst_positive_code_rect_productT) + (dst_positive_scale_rect_productT)) * S ((dst_positive_code_rect_productT) + (dst_positive_scale_rect_productT)) + ((dst_positive_scale_rect_productT) + (dst_positive_scale_rect_productT))) + (((dst_negative_code_rect_productT) + (dst_negative_scale_rect_productT)) * S ((dst_negative_code_rect_productT) + (dst_negative_scale_rect_productT)) + ((dst_negative_scale_rect_productT) + (dst_negative_scale_rect_productT)))) + ((((dst_negative_code_rect_productT) + (dst_negative_scale_rect_productT)) * S ((dst_negative_code_rect_productT) + (dst_negative_scale_rect_productT)) + ((dst_negative_scale_rect_productT) + (dst_negative_scale_rect_productT))) + (((dst_negative_code_rect_productT) + (dst_negative_scale_rect_productT)) * S ((dst_negative_code_rect_productT) + (dst_negative_scale_rect_productT)) + ((dst_negative_scale_rect_productT) + (dst_negative_scale_rect_productT)))))) /\ (forall dst_index_rect_productT. (exists pvs_le_gap_rect_productTdomain. pvs_le_gap_rect_productTdomain + (dst_index_rect_productT) = ((m)*(n))) -> exists dst_positive_rect_productT dst_negative_rect_productT dst_value_rect_productT. ((((exists ff_h_pvs_rect_productTentrypositive. ff_h_pvs_rect_productTentrypositive + S (dst_positive_rect_productT) = S ((S (dst_index_rect_productT)) * dst_positive_scale_rect_productT)) /\ exists ff_q_pvs_rect_productTentrypositive. dst_positive_code_rect_productT = ff_q_pvs_rect_productTentrypositive * S ((S (dst_index_rect_productT)) * dst_positive_scale_rect_productT) + (dst_positive_rect_productT))) /\ (((((exists ff_h_pvs_rect_productTentrynegative. ff_h_pvs_rect_productTentrynegative + S (dst_negative_rect_productT) = S ((S (dst_index_rect_productT)) * dst_negative_scale_rect_productT)) /\ exists ff_q_pvs_rect_productTentrynegative. dst_negative_code_rect_productT = ff_q_pvs_rect_productTentrynegative * S ((S (dst_index_rect_productT)) * dst_negative_scale_rect_productT) + (dst_negative_rect_productT))) /\ (exists ge_balance_positive_rect_productTentryvalue ge_balance_negative_rect_productTentryvalue. (((((dst_value_rect_productT) = 2 * (ge_balance_positive_rect_productTentryvalue) /\ (ge_balance_negative_rect_productTentryvalue) = 0) \/ exists ge_signed_half_rect_productTentryvaluedecode. (((dst_value_rect_productT) = 2 * ge_signed_half_rect_productTentryvaluedecode + 1 /\ (ge_balance_positive_rect_productTentryvalue) = 0) /\ (ge_balance_negative_rect_productTentryvalue) = S ge_signed_half_rect_productTentryvaluedecode))) /\ ((dst_positive_rect_productT) + ge_balance_negative_rect_productTentryvalue = (dst_negative_rect_productT) + ge_balance_positive_rect_productTentryvalue))))))))) /\ (forall scp_row_rect_product scp_column_rect_product scp_first_rect_product scp_second_rect_product scp_value_rect_product. (exists pvs_gap_rect_productrows. pvs_gap_rect_productrows + S (scp_row_rect_product) = (m)) -> (exists pvs_gap_rect_productcolumns. pvs_gap_rect_productcolumns + S (scp_column_rect_product) = (n)) -> (exists dst_positive_code_rect_productfirst dst_positive_scale_rect_productfirst dst_negative_code_rect_productfirst dst_negative_scale_rect_productfirst dst_positive_rect_productfirst dst_negative_rect_productfirst. (((F) = (((((dst_positive_code_rect_productfirst) + (dst_positive_scale_rect_productfirst)) * S ((dst_positive_code_rect_productfirst) + (dst_positive_scale_rect_productfirst)) + ((dst_positive_scale_rect_productfirst) + (dst_positive_scale_rect_productfirst))) + (((dst_negative_code_rect_productfirst) + (dst_negative_scale_rect_productfirst)) * S ((dst_negative_code_rect_productfirst) + (dst_negative_scale_rect_productfirst)) + ((dst_negative_scale_rect_productfirst) + (dst_negative_scale_rect_productfirst)))) * S ((((dst_positive_code_rect_productfirst) + (dst_positive_scale_rect_productfirst)) * S ((dst_positive_code_rect_productfirst) + (dst_positive_scale_rect_productfirst)) + ((dst_positive_scale_rect_productfirst) + (dst_positive_scale_rect_productfirst))) + (((dst_negative_code_rect_productfirst) + (dst_negative_scale_rect_productfirst)) * S ((dst_negative_code_rect_productfirst) + (dst_negative_scale_rect_productfirst)) + ((dst_negative_scale_rect_productfirst) + (dst_negative_scale_rect_productfirst)))) + ((((dst_negative_code_rect_productfirst) + (dst_negative_scale_rect_productfirst)) * S ((dst_negative_code_rect_productfirst) + (dst_negative_scale_rect_productfirst)) + ((dst_negative_scale_rect_productfirst) + (dst_negative_scale_rect_productfirst))) + (((dst_negative_code_rect_productfirst) + (dst_negative_scale_rect_productfirst)) * S ((dst_negative_code_rect_productfirst) + (dst_negative_scale_rect_productfirst)) + ((dst_negative_scale_rect_productfirst) + (dst_negative_scale_rect_productfirst)))))) /\ (((((exists ff_h_pvs_rect_productfirstpositive. ff_h_pvs_rect_productfirstpositive + S (dst_positive_rect_productfirst) = S ((S (scp_row_rect_product)) * dst_positive_scale_rect_productfirst)) /\ exists ff_q_pvs_rect_productfirstpositive. dst_positive_code_rect_productfirst = ff_q_pvs_rect_productfirstpositive * S ((S (scp_row_rect_product)) * dst_positive_scale_rect_productfirst) + (dst_positive_rect_productfirst))) /\ (((((exists ff_h_pvs_rect_productfirstnegative. ff_h_pvs_rect_productfirstnegative + S (dst_negative_rect_productfirst) = S ((S (scp_row_rect_product)) * dst_negative_scale_rect_productfirst)) /\ exists ff_q_pvs_rect_productfirstnegative. dst_negative_code_rect_productfirst = ff_q_pvs_rect_productfirstnegative * S ((S (scp_row_rect_product)) * dst_negative_scale_rect_productfirst) + (dst_negative_rect_productfirst))) /\ (exists ge_balance_positive_rect_productfirstvalue ge_balance_negative_rect_productfirstvalue. (((((scp_first_rect_product) = 2 * (ge_balance_positive_rect_productfirstvalue) /\ (ge_balance_negative_rect_productfirstvalue) = 0) \/ exists ge_signed_half_rect_productfirstvaluedecode. (((scp_first_rect_product) = 2 * ge_signed_half_rect_productfirstvaluedecode + 1 /\ (ge_balance_positive_rect_productfirstvalue) = 0) /\ (ge_balance_negative_rect_productfirstvalue) = S ge_signed_half_rect_productfirstvaluedecode))) /\ ((dst_positive_rect_productfirst) + ge_balance_negative_rect_productfirstvalue = (dst_negative_rect_productfirst) + ge_balance_positive_rect_productfirstvalue))))))))) -> (exists dst_positive_code_rect_productsecond dst_positive_scale_rect_productsecond dst_negative_code_rect_productsecond dst_negative_scale_rect_productsecond dst_positive_rect_productsecond dst_negative_rect_productsecond. (((G) = (((((dst_positive_code_rect_productsecond) + (dst_positive_scale_rect_productsecond)) * S ((dst_positive_code_rect_productsecond) + (dst_positive_scale_rect_productsecond)) + ((dst_positive_scale_rect_productsecond) + (dst_positive_scale_rect_productsecond))) + (((dst_negative_code_rect_productsecond) + (dst_negative_scale_rect_productsecond)) * S ((dst_negative_code_rect_productsecond) + (dst_negative_scale_rect_productsecond)) + ((dst_negative_scale_rect_productsecond) + (dst_negative_scale_rect_productsecond)))) * S ((((dst_positive_code_rect_productsecond) + (dst_positive_scale_rect_productsecond)) * S ((dst_positive_code_rect_productsecond) + (dst_positive_scale_rect_productsecond)) + ((dst_positive_scale_rect_productsecond) + (dst_positive_scale_rect_productsecond))) + (((dst_negative_code_rect_productsecond) + (dst_negative_scale_rect_productsecond)) * S ((dst_negative_code_rect_productsecond) + (dst_negative_scale_rect_productsecond)) + ((dst_negative_scale_rect_productsecond) + (dst_negative_scale_rect_productsecond)))) + ((((dst_negative_code_rect_productsecond) + (dst_negative_scale_rect_productsecond)) * S ((dst_negative_code_rect_productsecond) + (dst_negative_scale_rect_productsecond)) + ((dst_negative_scale_rect_productsecond) + (dst_negative_scale_rect_productsecond))) + (((dst_negative_code_rect_productsecond) + (dst_negative_scale_rect_productsecond)) * S ((dst_negative_code_rect_productsecond) + (dst_negative_scale_rect_productsecond)) + ((dst_negative_scale_rect_productsecond) + (dst_negative_scale_rect_productsecond)))))) /\ (((((exists ff_h_pvs_rect_productsecondpositive. ff_h_pvs_rect_productsecondpositive + S (dst_positive_rect_productsecond) = S ((S (scp_column_rect_product)) * dst_positive_scale_rect_productsecond)) /\ exists ff_q_pvs_rect_productsecondpositive. dst_positive_code_rect_productsecond = ff_q_pvs_rect_productsecondpositive * S ((S (scp_column_rect_product)) * dst_positive_scale_rect_productsecond) + (dst_positive_rect_productsecond))) /\ (((((exists ff_h_pvs_rect_productsecondnegative. ff_h_pvs_rect_productsecondnegative + S (dst_negative_rect_productsecond) = S ((S (scp_column_rect_product)) * dst_negative_scale_rect_productsecond)) /\ exists ff_q_pvs_rect_productsecondnegative. dst_negative_code_rect_productsecond = ff_q_pvs_rect_productsecondnegative * S ((S (scp_column_rect_product)) * dst_negative_scale_rect_productsecond) + (dst_negative_rect_productsecond))) /\ (exists ge_balance_positive_rect_productsecondvalue ge_balance_negative_rect_productsecondvalue. (((((scp_second_rect_product) = 2 * (ge_balance_positive_rect_productsecondvalue) /\ (ge_balance_negative_rect_productsecondvalue) = 0) \/ exists ge_signed_half_rect_productsecondvaluedecode. (((scp_second_rect_product) = 2 * ge_signed_half_rect_productsecondvaluedecode + 1 /\ (ge_balance_positive_rect_productsecondvalue) = 0) /\ (ge_balance_negative_rect_productsecondvalue) = S ge_signed_half_rect_productsecondvaluedecode))) /\ ((dst_positive_rect_productsecond) + ge_balance_negative_rect_productsecondvalue = (dst_negative_rect_productsecond) + ge_balance_positive_rect_productsecondvalue))))))))) -> (exists dst_positive_code_rect_productentry dst_positive_scale_rect_productentry dst_negative_code_rect_productentry dst_negative_scale_rect_productentry dst_positive_rect_productentry dst_negative_rect_productentry. (((T) = (((((dst_positive_code_rect_productentry) + (dst_positive_scale_rect_productentry)) * S ((dst_positive_code_rect_productentry) + (dst_positive_scale_rect_productentry)) + ((dst_positive_scale_rect_productentry) + (dst_positive_scale_rect_productentry))) + (((dst_negative_code_rect_productentry) + (dst_negative_scale_rect_productentry)) * S ((dst_negative_code_rect_productentry) + (dst_negative_scale_rect_productentry)) + ((dst_negative_scale_rect_productentry) + (dst_negative_scale_rect_productentry)))) * S ((((dst_positive_code_rect_productentry) + (dst_positive_scale_rect_productentry)) * S ((dst_positive_code_rect_productentry) + (dst_positive_scale_rect_productentry)) + ((dst_positive_scale_rect_productentry) + (dst_positive_scale_rect_productentry))) + (((dst_negative_code_rect_productentry) + (dst_negative_scale_rect_productentry)) * S ((dst_negative_code_rect_productentry) + (dst_negative_scale_rect_productentry)) + ((dst_negative_scale_rect_productentry) + (dst_negative_scale_rect_productentry)))) + ((((dst_negative_code_rect_productentry) + (dst_negative_scale_rect_productentry)) * S ((dst_negative_code_rect_productentry) + (dst_negative_scale_rect_productentry)) + ((dst_negative_scale_rect_productentry) + (dst_negative_scale_rect_productentry))) + (((dst_negative_code_rect_productentry) + (dst_negative_scale_rect_productentry)) * S ((dst_negative_code_rect_productentry) + (dst_negative_scale_rect_productentry)) + ((dst_negative_scale_rect_productentry) + (dst_negative_scale_rect_productentry)))))) /\ (((((exists ff_h_pvs_rect_productentrypositive. ff_h_pvs_rect_productentrypositive + S (dst_positive_rect_productentry) = S ((S (((n)*(scp_row_rect_product)+(scp_column_rect_product)))) * dst_positive_scale_rect_productentry)) /\ exists ff_q_pvs_rect_productentrypositive. dst_positive_code_rect_productentry = ff_q_pvs_rect_productentrypositive * S ((S (((n)*(scp_row_rect_product)+(scp_column_rect_product)))) * dst_positive_scale_rect_productentry) + (dst_positive_rect_productentry))) /\ (((((exists ff_h_pvs_rect_productentrynegative. ff_h_pvs_rect_productentrynegative + S (dst_negative_rect_productentry) = S ((S (((n)*(scp_row_rect_product)+(scp_column_rect_product)))) * dst_negative_scale_rect_productentry)) /\ exists ff_q_pvs_rect_productentrynegative. dst_negative_code_rect_productentry = ff_q_pvs_rect_productentrynegative * S ((S (((n)*(scp_row_rect_product)+(scp_column_rect_product)))) * dst_negative_scale_rect_productentry) + (dst_negative_rect_productentry))) /\ (exists ge_balance_positive_rect_productentryvalue ge_balance_negative_rect_productentryvalue. (((((scp_value_rect_product) = 2 * (ge_balance_positive_rect_productentryvalue) /\ (ge_balance_negative_rect_productentryvalue) = 0) \/ exists ge_signed_half_rect_productentryvaluedecode. (((scp_value_rect_product) = 2 * ge_signed_half_rect_productentryvaluedecode + 1 /\ (ge_balance_positive_rect_productentryvalue) = 0) /\ (ge_balance_negative_rect_productentryvalue) = S ge_signed_half_rect_productentryvaluedecode))) /\ ((dst_positive_rect_productentry) + ge_balance_negative_rect_productentryvalue = (dst_negative_rect_productentry) + ge_balance_positive_rect_productentryvalue))))))))) -> (exists sto_ap_rect_productmultiply sto_an_rect_productmultiply sto_bp_rect_productmultiply sto_bn_rect_productmultiply sto_cp_rect_productmultiply sto_cn_rect_productmultiply. (((((scp_first_rect_product) = 2 * (sto_ap_rect_productmultiply) /\ (sto_an_rect_productmultiply) = 0) \/ exists ge_signed_half_rect_productmultiplyleft. (((scp_first_rect_product) = 2 * ge_signed_half_rect_productmultiplyleft + 1 /\ (sto_ap_rect_productmultiply) = 0) /\ (sto_an_rect_productmultiply) = S ge_signed_half_rect_productmultiplyleft))) /\ ((((((scp_second_rect_product) = 2 * (sto_bp_rect_productmultiply) /\ (sto_bn_rect_productmultiply) = 0) \/ exists ge_signed_half_rect_productmultiplyright. (((scp_second_rect_product) = 2 * ge_signed_half_rect_productmultiplyright + 1 /\ (sto_bp_rect_productmultiply) = 0) /\ (sto_bn_rect_productmultiply) = S ge_signed_half_rect_productmultiplyright))) /\ ((((((scp_value_rect_product) = 2 * (sto_cp_rect_productmultiply) /\ (sto_cn_rect_productmultiply) = 0) \/ exists ge_signed_half_rect_productmultiplyoutput. (((scp_value_rect_product) = 2 * ge_signed_half_rect_productmultiplyoutput + 1 /\ (sto_cp_rect_productmultiply) = 0) /\ (sto_cn_rect_productmultiply) = S ge_signed_half_rect_productmultiplyoutput))) /\ ((sto_ap_rect_productmultiply * sto_bp_rect_productmultiply + sto_an_rect_productmultiply * sto_bn_rect_productmultiply) + sto_cn_rect_productmultiply = (sto_ap_rect_productmultiply * sto_bn_rect_productmultiply + sto_an_rect_productmultiply * sto_bp_rect_productmultiply) + sto_cp_rect_productmultiply)))))))))))))) -> (exists dst_positive_code_rect_first dst_positive_scale_rect_first dst_negative_code_rect_first dst_negative_scale_rect_first dst_positive_sum_rect_first dst_negative_sum_rect_first. (((F) = (((((dst_positive_code_rect_first) + (dst_positive_scale_rect_first)) * S ((dst_positive_code_rect_first) + (dst_positive_scale_rect_first)) + ((dst_positive_scale_rect_first) + (dst_positive_scale_rect_first))) + (((dst_negative_code_rect_first) + (dst_negative_scale_rect_first)) * S ((dst_negative_code_rect_first) + (dst_negative_scale_rect_first)) + ((dst_negative_scale_rect_first) + (dst_negative_scale_rect_first)))) * S ((((dst_positive_code_rect_first) + (dst_positive_scale_rect_first)) * S ((dst_positive_code_rect_first) + (dst_positive_scale_rect_first)) + ((dst_positive_scale_rect_first) + (dst_positive_scale_rect_first))) + (((dst_negative_code_rect_first) + (dst_negative_scale_rect_first)) * S ((dst_negative_code_rect_first) + (dst_negative_scale_rect_first)) + ((dst_negative_scale_rect_first) + (dst_negative_scale_rect_first)))) + ((((dst_negative_code_rect_first) + (dst_negative_scale_rect_first)) * S ((dst_negative_code_rect_first) + (dst_negative_scale_rect_first)) + ((dst_negative_scale_rect_first) + (dst_negative_scale_rect_first))) + (((dst_negative_code_rect_first) + (dst_negative_scale_rect_first)) * S ((dst_negative_code_rect_first) + (dst_negative_scale_rect_first)) + ((dst_negative_scale_rect_first) + (dst_negative_scale_rect_first)))))) /\ (((exists fs_u_dst_rect_firstpositive fs_v_dst_rect_firstpositive. ((((exists fs_h_dst_rect_firstpositive_body_start. fs_h_dst_rect_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_rect_firstpositive)) /\ exists fs_q_dst_rect_firstpositive_body_start. fs_u_dst_rect_firstpositive = fs_q_dst_rect_firstpositive_body_start * S ((S (0)) * fs_v_dst_rect_firstpositive) + (0))) /\ ((((exists fs_h_dst_rect_firstpositive_body_terminal. fs_h_dst_rect_firstpositive_body_terminal + S (dst_positive_sum_rect_first) = S ((S (m)) * fs_v_dst_rect_firstpositive)) /\ exists fs_q_dst_rect_firstpositive_body_terminal. fs_u_dst_rect_firstpositive = fs_q_dst_rect_firstpositive_body_terminal * S ((S (m)) * fs_v_dst_rect_firstpositive) + (dst_positive_sum_rect_first))) /\ forall fs_i_dst_rect_firstpositive_body_steps. (exists fs_lt_dst_rect_firstpositive_body_steps_bound. fs_lt_dst_rect_firstpositive_body_steps_bound + S fs_i_dst_rect_firstpositive_body_steps = m) -> exists fs_a_dst_rect_firstpositive_body_steps fs_r_dst_rect_firstpositive_body_steps fs_s_dst_rect_firstpositive_body_steps. ((((exists fs_h_dst_rect_firstpositive_body_steps_summand. fs_h_dst_rect_firstpositive_body_steps_summand + S (fs_a_dst_rect_firstpositive_body_steps) = S ((S (fs_i_dst_rect_firstpositive_body_steps)) * dst_positive_scale_rect_first)) /\ exists fs_q_dst_rect_firstpositive_body_steps_summand. dst_positive_code_rect_first = fs_q_dst_rect_firstpositive_body_steps_summand * S ((S (fs_i_dst_rect_firstpositive_body_steps)) * dst_positive_scale_rect_first) + (fs_a_dst_rect_firstpositive_body_steps))) /\ ((((exists fs_h_dst_rect_firstpositive_body_steps_partial. fs_h_dst_rect_firstpositive_body_steps_partial + S (fs_r_dst_rect_firstpositive_body_steps) = S ((S (fs_i_dst_rect_firstpositive_body_steps)) * fs_v_dst_rect_firstpositive)) /\ exists fs_q_dst_rect_firstpositive_body_steps_partial. fs_u_dst_rect_firstpositive = fs_q_dst_rect_firstpositive_body_steps_partial * S ((S (fs_i_dst_rect_firstpositive_body_steps)) * fs_v_dst_rect_firstpositive) + (fs_r_dst_rect_firstpositive_body_steps))) /\ ((((exists fs_h_dst_rect_firstpositive_body_steps_successor. fs_h_dst_rect_firstpositive_body_steps_successor + S (fs_s_dst_rect_firstpositive_body_steps) = S ((S (S fs_i_dst_rect_firstpositive_body_steps)) * fs_v_dst_rect_firstpositive)) /\ exists fs_q_dst_rect_firstpositive_body_steps_successor. fs_u_dst_rect_firstpositive = fs_q_dst_rect_firstpositive_body_steps_successor * S ((S (S fs_i_dst_rect_firstpositive_body_steps)) * fs_v_dst_rect_firstpositive) + (fs_s_dst_rect_firstpositive_body_steps))) /\ fs_s_dst_rect_firstpositive_body_steps = fs_r_dst_rect_firstpositive_body_steps + fs_a_dst_rect_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_rect_firstnegative fs_v_dst_rect_firstnegative. ((((exists fs_h_dst_rect_firstnegative_body_start. fs_h_dst_rect_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_rect_firstnegative)) /\ exists fs_q_dst_rect_firstnegative_body_start. fs_u_dst_rect_firstnegative = fs_q_dst_rect_firstnegative_body_start * S ((S (0)) * fs_v_dst_rect_firstnegative) + (0))) /\ ((((exists fs_h_dst_rect_firstnegative_body_terminal. fs_h_dst_rect_firstnegative_body_terminal + S (dst_negative_sum_rect_first) = S ((S (m)) * fs_v_dst_rect_firstnegative)) /\ exists fs_q_dst_rect_firstnegative_body_terminal. fs_u_dst_rect_firstnegative = fs_q_dst_rect_firstnegative_body_terminal * S ((S (m)) * fs_v_dst_rect_firstnegative) + (dst_negative_sum_rect_first))) /\ forall fs_i_dst_rect_firstnegative_body_steps. (exists fs_lt_dst_rect_firstnegative_body_steps_bound. fs_lt_dst_rect_firstnegative_body_steps_bound + S fs_i_dst_rect_firstnegative_body_steps = m) -> exists fs_a_dst_rect_firstnegative_body_steps fs_r_dst_rect_firstnegative_body_steps fs_s_dst_rect_firstnegative_body_steps. ((((exists fs_h_dst_rect_firstnegative_body_steps_summand. fs_h_dst_rect_firstnegative_body_steps_summand + S (fs_a_dst_rect_firstnegative_body_steps) = S ((S (fs_i_dst_rect_firstnegative_body_steps)) * dst_negative_scale_rect_first)) /\ exists fs_q_dst_rect_firstnegative_body_steps_summand. dst_negative_code_rect_first = fs_q_dst_rect_firstnegative_body_steps_summand * S ((S (fs_i_dst_rect_firstnegative_body_steps)) * dst_negative_scale_rect_first) + (fs_a_dst_rect_firstnegative_body_steps))) /\ ((((exists fs_h_dst_rect_firstnegative_body_steps_partial. fs_h_dst_rect_firstnegative_body_steps_partial + S (fs_r_dst_rect_firstnegative_body_steps) = S ((S (fs_i_dst_rect_firstnegative_body_steps)) * fs_v_dst_rect_firstnegative)) /\ exists fs_q_dst_rect_firstnegative_body_steps_partial. fs_u_dst_rect_firstnegative = fs_q_dst_rect_firstnegative_body_steps_partial * S ((S (fs_i_dst_rect_firstnegative_body_steps)) * fs_v_dst_rect_firstnegative) + (fs_r_dst_rect_firstnegative_body_steps))) /\ ((((exists fs_h_dst_rect_firstnegative_body_steps_successor. fs_h_dst_rect_firstnegative_body_steps_successor + S (fs_s_dst_rect_firstnegative_body_steps) = S ((S (S fs_i_dst_rect_firstnegative_body_steps)) * fs_v_dst_rect_firstnegative)) /\ exists fs_q_dst_rect_firstnegative_body_steps_successor. fs_u_dst_rect_firstnegative = fs_q_dst_rect_firstnegative_body_steps_successor * S ((S (S fs_i_dst_rect_firstnegative_body_steps)) * fs_v_dst_rect_firstnegative) + (fs_s_dst_rect_firstnegative_body_steps))) /\ fs_s_dst_rect_firstnegative_body_steps = fs_r_dst_rect_firstnegative_body_steps + fs_a_dst_rect_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_rect_firstresult ge_balance_negative_rect_firstresult. (((((a) = 2 * (ge_balance_positive_rect_firstresult) /\ (ge_balance_negative_rect_firstresult) = 0) \/ exists ge_signed_half_rect_firstresultdecode. (((a) = 2 * ge_signed_half_rect_firstresultdecode + 1 /\ (ge_balance_positive_rect_firstresult) = 0) /\ (ge_balance_negative_rect_firstresult) = S ge_signed_half_rect_firstresultdecode))) /\ ((dst_positive_sum_rect_first) + ge_balance_negative_rect_firstresult = (dst_negative_sum_rect_first) + ge_balance_positive_rect_firstresult))))))))) -> (exists dst_positive_code_rect_second dst_positive_scale_rect_second dst_negative_code_rect_second dst_negative_scale_rect_second dst_positive_sum_rect_second dst_negative_sum_rect_second. (((G) = (((((dst_positive_code_rect_second) + (dst_positive_scale_rect_second)) * S ((dst_positive_code_rect_second) + (dst_positive_scale_rect_second)) + ((dst_positive_scale_rect_second) + (dst_positive_scale_rect_second))) + (((dst_negative_code_rect_second) + (dst_negative_scale_rect_second)) * S ((dst_negative_code_rect_second) + (dst_negative_scale_rect_second)) + ((dst_negative_scale_rect_second) + (dst_negative_scale_rect_second)))) * S ((((dst_positive_code_rect_second) + (dst_positive_scale_rect_second)) * S ((dst_positive_code_rect_second) + (dst_positive_scale_rect_second)) + ((dst_positive_scale_rect_second) + (dst_positive_scale_rect_second))) + (((dst_negative_code_rect_second) + (dst_negative_scale_rect_second)) * S ((dst_negative_code_rect_second) + (dst_negative_scale_rect_second)) + ((dst_negative_scale_rect_second) + (dst_negative_scale_rect_second)))) + ((((dst_negative_code_rect_second) + (dst_negative_scale_rect_second)) * S ((dst_negative_code_rect_second) + (dst_negative_scale_rect_second)) + ((dst_negative_scale_rect_second) + (dst_negative_scale_rect_second))) + (((dst_negative_code_rect_second) + (dst_negative_scale_rect_second)) * S ((dst_negative_code_rect_second) + (dst_negative_scale_rect_second)) + ((dst_negative_scale_rect_second) + (dst_negative_scale_rect_second)))))) /\ (((exists fs_u_dst_rect_secondpositive fs_v_dst_rect_secondpositive. ((((exists fs_h_dst_rect_secondpositive_body_start. fs_h_dst_rect_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_rect_secondpositive)) /\ exists fs_q_dst_rect_secondpositive_body_start. fs_u_dst_rect_secondpositive = fs_q_dst_rect_secondpositive_body_start * S ((S (0)) * fs_v_dst_rect_secondpositive) + (0))) /\ ((((exists fs_h_dst_rect_secondpositive_body_terminal. fs_h_dst_rect_secondpositive_body_terminal + S (dst_positive_sum_rect_second) = S ((S (n)) * fs_v_dst_rect_secondpositive)) /\ exists fs_q_dst_rect_secondpositive_body_terminal. fs_u_dst_rect_secondpositive = fs_q_dst_rect_secondpositive_body_terminal * S ((S (n)) * fs_v_dst_rect_secondpositive) + (dst_positive_sum_rect_second))) /\ forall fs_i_dst_rect_secondpositive_body_steps. (exists fs_lt_dst_rect_secondpositive_body_steps_bound. fs_lt_dst_rect_secondpositive_body_steps_bound + S fs_i_dst_rect_secondpositive_body_steps = n) -> exists fs_a_dst_rect_secondpositive_body_steps fs_r_dst_rect_secondpositive_body_steps fs_s_dst_rect_secondpositive_body_steps. ((((exists fs_h_dst_rect_secondpositive_body_steps_summand. fs_h_dst_rect_secondpositive_body_steps_summand + S (fs_a_dst_rect_secondpositive_body_steps) = S ((S (fs_i_dst_rect_secondpositive_body_steps)) * dst_positive_scale_rect_second)) /\ exists fs_q_dst_rect_secondpositive_body_steps_summand. dst_positive_code_rect_second = fs_q_dst_rect_secondpositive_body_steps_summand * S ((S (fs_i_dst_rect_secondpositive_body_steps)) * dst_positive_scale_rect_second) + (fs_a_dst_rect_secondpositive_body_steps))) /\ ((((exists fs_h_dst_rect_secondpositive_body_steps_partial. fs_h_dst_rect_secondpositive_body_steps_partial + S (fs_r_dst_rect_secondpositive_body_steps) = S ((S (fs_i_dst_rect_secondpositive_body_steps)) * fs_v_dst_rect_secondpositive)) /\ exists fs_q_dst_rect_secondpositive_body_steps_partial. fs_u_dst_rect_secondpositive = fs_q_dst_rect_secondpositive_body_steps_partial * S ((S (fs_i_dst_rect_secondpositive_body_steps)) * fs_v_dst_rect_secondpositive) + (fs_r_dst_rect_secondpositive_body_steps))) /\ ((((exists fs_h_dst_rect_secondpositive_body_steps_successor. fs_h_dst_rect_secondpositive_body_steps_successor + S (fs_s_dst_rect_secondpositive_body_steps) = S ((S (S fs_i_dst_rect_secondpositive_body_steps)) * fs_v_dst_rect_secondpositive)) /\ exists fs_q_dst_rect_secondpositive_body_steps_successor. fs_u_dst_rect_secondpositive = fs_q_dst_rect_secondpositive_body_steps_successor * S ((S (S fs_i_dst_rect_secondpositive_body_steps)) * fs_v_dst_rect_secondpositive) + (fs_s_dst_rect_secondpositive_body_steps))) /\ fs_s_dst_rect_secondpositive_body_steps = fs_r_dst_rect_secondpositive_body_steps + fs_a_dst_rect_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_rect_secondnegative fs_v_dst_rect_secondnegative. ((((exists fs_h_dst_rect_secondnegative_body_start. fs_h_dst_rect_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_rect_secondnegative)) /\ exists fs_q_dst_rect_secondnegative_body_start. fs_u_dst_rect_secondnegative = fs_q_dst_rect_secondnegative_body_start * S ((S (0)) * fs_v_dst_rect_secondnegative) + (0))) /\ ((((exists fs_h_dst_rect_secondnegative_body_terminal. fs_h_dst_rect_secondnegative_body_terminal + S (dst_negative_sum_rect_second) = S ((S (n)) * fs_v_dst_rect_secondnegative)) /\ exists fs_q_dst_rect_secondnegative_body_terminal. fs_u_dst_rect_secondnegative = fs_q_dst_rect_secondnegative_body_terminal * S ((S (n)) * fs_v_dst_rect_secondnegative) + (dst_negative_sum_rect_second))) /\ forall fs_i_dst_rect_secondnegative_body_steps. (exists fs_lt_dst_rect_secondnegative_body_steps_bound. fs_lt_dst_rect_secondnegative_body_steps_bound + S fs_i_dst_rect_secondnegative_body_steps = n) -> exists fs_a_dst_rect_secondnegative_body_steps fs_r_dst_rect_secondnegative_body_steps fs_s_dst_rect_secondnegative_body_steps. ((((exists fs_h_dst_rect_secondnegative_body_steps_summand. fs_h_dst_rect_secondnegative_body_steps_summand + S (fs_a_dst_rect_secondnegative_body_steps) = S ((S (fs_i_dst_rect_secondnegative_body_steps)) * dst_negative_scale_rect_second)) /\ exists fs_q_dst_rect_secondnegative_body_steps_summand. dst_negative_code_rect_second = fs_q_dst_rect_secondnegative_body_steps_summand * S ((S (fs_i_dst_rect_secondnegative_body_steps)) * dst_negative_scale_rect_second) + (fs_a_dst_rect_secondnegative_body_steps))) /\ ((((exists fs_h_dst_rect_secondnegative_body_steps_partial. fs_h_dst_rect_secondnegative_body_steps_partial + S (fs_r_dst_rect_secondnegative_body_steps) = S ((S (fs_i_dst_rect_secondnegative_body_steps)) * fs_v_dst_rect_secondnegative)) /\ exists fs_q_dst_rect_secondnegative_body_steps_partial. fs_u_dst_rect_secondnegative = fs_q_dst_rect_secondnegative_body_steps_partial * S ((S (fs_i_dst_rect_secondnegative_body_steps)) * fs_v_dst_rect_secondnegative) + (fs_r_dst_rect_secondnegative_body_steps))) /\ ((((exists fs_h_dst_rect_secondnegative_body_steps_successor. fs_h_dst_rect_secondnegative_body_steps_successor + S (fs_s_dst_rect_secondnegative_body_steps) = S ((S (S fs_i_dst_rect_secondnegative_body_steps)) * fs_v_dst_rect_secondnegative)) /\ exists fs_q_dst_rect_secondnegative_body_steps_successor. fs_u_dst_rect_secondnegative = fs_q_dst_rect_secondnegative_body_steps_successor * S ((S (S fs_i_dst_rect_secondnegative_body_steps)) * fs_v_dst_rect_secondnegative) + (fs_s_dst_rect_secondnegative_body_steps))) /\ fs_s_dst_rect_secondnegative_body_steps = fs_r_dst_rect_secondnegative_body_steps + fs_a_dst_rect_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_rect_secondresult ge_balance_negative_rect_secondresult. (((((b) = 2 * (ge_balance_positive_rect_secondresult) /\ (ge_balance_negative_rect_secondresult) = 0) \/ exists ge_signed_half_rect_secondresultdecode. (((b) = 2 * ge_signed_half_rect_secondresultdecode + 1 /\ (ge_balance_positive_rect_secondresult) = 0) /\ (ge_balance_negative_rect_secondresult) = S ge_signed_half_rect_secondresultdecode))) /\ ((dst_positive_sum_rect_second) + ge_balance_negative_rect_secondresult = (dst_negative_sum_rect_second) + ge_balance_positive_rect_secondresult))))))))) -> (exists srt_rows_rect_total. ((((exists dst_positive_code_rect_totalrowssource_table dst_positive_scale_rect_totalrowssource_table dst_negative_code_rect_totalrowssource_table dst_negative_scale_rect_totalrowssource_table. (((T) = (((((dst_positive_code_rect_totalrowssource_table) + (dst_positive_scale_rect_totalrowssource_table)) * S ((dst_positive_code_rect_totalrowssource_table) + (dst_positive_scale_rect_totalrowssource_table)) + ((dst_positive_scale_rect_totalrowssource_table) + (dst_positive_scale_rect_totalrowssource_table))) + (((dst_negative_code_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)) * S ((dst_negative_code_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)) + ((dst_negative_scale_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)))) * S ((((dst_positive_code_rect_totalrowssource_table) + (dst_positive_scale_rect_totalrowssource_table)) * S ((dst_positive_code_rect_totalrowssource_table) + (dst_positive_scale_rect_totalrowssource_table)) + ((dst_positive_scale_rect_totalrowssource_table) + (dst_positive_scale_rect_totalrowssource_table))) + (((dst_negative_code_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)) * S ((dst_negative_code_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)) + ((dst_negative_scale_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)))) + ((((dst_negative_code_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)) * S ((dst_negative_code_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)) + ((dst_negative_scale_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table))) + (((dst_negative_code_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)) * S ((dst_negative_code_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)) + ((dst_negative_scale_rect_totalrowssource_table) + (dst_negative_scale_rect_totalrowssource_table)))))) /\ (forall dst_index_rect_totalrowssource_table. (exists pvs_le_gap_rect_totalrowssource_tabledomain. pvs_le_gap_rect_totalrowssource_tabledomain + (dst_index_rect_totalrowssource_table) = (0)) -> exists dst_positive_rect_totalrowssource_table dst_negative_rect_totalrowssource_table dst_value_rect_totalrowssource_table. ((((exists ff_h_pvs_rect_totalrowssource_tableentrypositive. ff_h_pvs_rect_totalrowssource_tableentrypositive + S (dst_positive_rect_totalrowssource_table) = S ((S (dst_index_rect_totalrowssource_table)) * dst_positive_scale_rect_totalrowssource_table)) /\ exists ff_q_pvs_rect_totalrowssource_tableentrypositive. dst_positive_code_rect_totalrowssource_table = ff_q_pvs_rect_totalrowssource_tableentrypositive * S ((S (dst_index_rect_totalrowssource_table)) * dst_positive_scale_rect_totalrowssource_table) + (dst_positive_rect_totalrowssource_table))) /\ (((((exists ff_h_pvs_rect_totalrowssource_tableentrynegative. ff_h_pvs_rect_totalrowssource_tableentrynegative + S (dst_negative_rect_totalrowssource_table) = S ((S (dst_index_rect_totalrowssource_table)) * dst_negative_scale_rect_totalrowssource_table)) /\ exists ff_q_pvs_rect_totalrowssource_tableentrynegative. dst_negative_code_rect_totalrowssource_table = ff_q_pvs_rect_totalrowssource_tableentrynegative * S ((S (dst_index_rect_totalrowssource_table)) * dst_negative_scale_rect_totalrowssource_table) + (dst_negative_rect_totalrowssource_table))) /\ (exists ge_balance_positive_rect_totalrowssource_tableentryvalue ge_balance_negative_rect_totalrowssource_tableentryvalue. (((((dst_value_rect_totalrowssource_table) = 2 * (ge_balance_positive_rect_totalrowssource_tableentryvalue) /\ (ge_balance_negative_rect_totalrowssource_tableentryvalue) = 0) \/ exists ge_signed_half_rect_totalrowssource_tableentryvaluedecode. (((dst_value_rect_totalrowssource_table) = 2 * ge_signed_half_rect_totalrowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_rect_totalrowssource_tableentryvalue) = 0) /\ (ge_balance_negative_rect_totalrowssource_tableentryvalue) = S ge_signed_half_rect_totalrowssource_tableentryvaluedecode))) /\ ((dst_positive_rect_totalrowssource_table) + ge_balance_negative_rect_totalrowssource_tableentryvalue = (dst_negative_rect_totalrowssource_table) + ge_balance_positive_rect_totalrowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_rect_totalrowsrow_table dst_positive_scale_rect_totalrowsrow_table dst_negative_code_rect_totalrowsrow_table dst_negative_scale_rect_totalrowsrow_table. (((srt_rows_rect_total) = (((((dst_positive_code_rect_totalrowsrow_table) + (dst_positive_scale_rect_totalrowsrow_table)) * S ((dst_positive_code_rect_totalrowsrow_table) + (dst_positive_scale_rect_totalrowsrow_table)) + ((dst_positive_scale_rect_totalrowsrow_table) + (dst_positive_scale_rect_totalrowsrow_table))) + (((dst_negative_code_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)) * S ((dst_negative_code_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)) + ((dst_negative_scale_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)))) * S ((((dst_positive_code_rect_totalrowsrow_table) + (dst_positive_scale_rect_totalrowsrow_table)) * S ((dst_positive_code_rect_totalrowsrow_table) + (dst_positive_scale_rect_totalrowsrow_table)) + ((dst_positive_scale_rect_totalrowsrow_table) + (dst_positive_scale_rect_totalrowsrow_table))) + (((dst_negative_code_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)) * S ((dst_negative_code_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)) + ((dst_negative_scale_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)))) + ((((dst_negative_code_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)) * S ((dst_negative_code_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)) + ((dst_negative_scale_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table))) + (((dst_negative_code_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)) * S ((dst_negative_code_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)) + ((dst_negative_scale_rect_totalrowsrow_table) + (dst_negative_scale_rect_totalrowsrow_table)))))) /\ (forall dst_index_rect_totalrowsrow_table. (exists pvs_le_gap_rect_totalrowsrow_tabledomain. pvs_le_gap_rect_totalrowsrow_tabledomain + (dst_index_rect_totalrowsrow_table) = (m)) -> exists dst_positive_rect_totalrowsrow_table dst_negative_rect_totalrowsrow_table dst_value_rect_totalrowsrow_table. ((((exists ff_h_pvs_rect_totalrowsrow_tableentrypositive. ff_h_pvs_rect_totalrowsrow_tableentrypositive + S (dst_positive_rect_totalrowsrow_table) = S ((S (dst_index_rect_totalrowsrow_table)) * dst_positive_scale_rect_totalrowsrow_table)) /\ exists ff_q_pvs_rect_totalrowsrow_tableentrypositive. dst_positive_code_rect_totalrowsrow_table = ff_q_pvs_rect_totalrowsrow_tableentrypositive * S ((S (dst_index_rect_totalrowsrow_table)) * dst_positive_scale_rect_totalrowsrow_table) + (dst_positive_rect_totalrowsrow_table))) /\ (((((exists ff_h_pvs_rect_totalrowsrow_tableentrynegative. ff_h_pvs_rect_totalrowsrow_tableentrynegative + S (dst_negative_rect_totalrowsrow_table) = S ((S (dst_index_rect_totalrowsrow_table)) * dst_negative_scale_rect_totalrowsrow_table)) /\ exists ff_q_pvs_rect_totalrowsrow_tableentrynegative. dst_negative_code_rect_totalrowsrow_table = ff_q_pvs_rect_totalrowsrow_tableentrynegative * S ((S (dst_index_rect_totalrowsrow_table)) * dst_negative_scale_rect_totalrowsrow_table) + (dst_negative_rect_totalrowsrow_table))) /\ (exists ge_balance_positive_rect_totalrowsrow_tableentryvalue ge_balance_negative_rect_totalrowsrow_tableentryvalue. (((((dst_value_rect_totalrowsrow_table) = 2 * (ge_balance_positive_rect_totalrowsrow_tableentryvalue) /\ (ge_balance_negative_rect_totalrowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_rect_totalrowsrow_tableentryvaluedecode. (((dst_value_rect_totalrowsrow_table) = 2 * ge_signed_half_rect_totalrowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_rect_totalrowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_rect_totalrowsrow_tableentryvalue) = S ge_signed_half_rect_totalrowsrow_tableentryvaluedecode))) /\ ((dst_positive_rect_totalrowsrow_table) + ge_balance_negative_rect_totalrowsrow_tableentryvalue = (dst_negative_rect_totalrowsrow_table) + ge_balance_positive_rect_totalrowsrow_tableentryvalue))))))))) /\ (forall srt_index_rect_totalrows. (exists pvs_gap_rect_totalrowsbound. pvs_gap_rect_totalrowsbound + S (srt_index_rect_totalrows) = (m)) -> exists srt_value_rect_totalrows. (((exists dst_positive_code_rect_totalrowsrowentry dst_positive_scale_rect_totalrowsrowentry dst_negative_code_rect_totalrowsrowentry dst_negative_scale_rect_totalrowsrowentry dst_positive_rect_totalrowsrowentry dst_negative_rect_totalrowsrowentry. (((srt_rows_rect_total) = (((((dst_positive_code_rect_totalrowsrowentry) + (dst_positive_scale_rect_totalrowsrowentry)) * S ((dst_positive_code_rect_totalrowsrowentry) + (dst_positive_scale_rect_totalrowsrowentry)) + ((dst_positive_scale_rect_totalrowsrowentry) + (dst_positive_scale_rect_totalrowsrowentry))) + (((dst_negative_code_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)) * S ((dst_negative_code_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)) + ((dst_negative_scale_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)))) * S ((((dst_positive_code_rect_totalrowsrowentry) + (dst_positive_scale_rect_totalrowsrowentry)) * S ((dst_positive_code_rect_totalrowsrowentry) + (dst_positive_scale_rect_totalrowsrowentry)) + ((dst_positive_scale_rect_totalrowsrowentry) + (dst_positive_scale_rect_totalrowsrowentry))) + (((dst_negative_code_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)) * S ((dst_negative_code_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)) + ((dst_negative_scale_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)))) + ((((dst_negative_code_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)) * S ((dst_negative_code_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)) + ((dst_negative_scale_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry))) + (((dst_negative_code_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)) * S ((dst_negative_code_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)) + ((dst_negative_scale_rect_totalrowsrowentry) + (dst_negative_scale_rect_totalrowsrowentry)))))) /\ (((((exists ff_h_pvs_rect_totalrowsrowentrypositive. ff_h_pvs_rect_totalrowsrowentrypositive + S (dst_positive_rect_totalrowsrowentry) = S ((S (srt_index_rect_totalrows)) * dst_positive_scale_rect_totalrowsrowentry)) /\ exists ff_q_pvs_rect_totalrowsrowentrypositive. dst_positive_code_rect_totalrowsrowentry = ff_q_pvs_rect_totalrowsrowentrypositive * S ((S (srt_index_rect_totalrows)) * dst_positive_scale_rect_totalrowsrowentry) + (dst_positive_rect_totalrowsrowentry))) /\ (((((exists ff_h_pvs_rect_totalrowsrowentrynegative. ff_h_pvs_rect_totalrowsrowentrynegative + S (dst_negative_rect_totalrowsrowentry) = S ((S (srt_index_rect_totalrows)) * dst_negative_scale_rect_totalrowsrowentry)) /\ exists ff_q_pvs_rect_totalrowsrowentrynegative. dst_negative_code_rect_totalrowsrowentry = ff_q_pvs_rect_totalrowsrowentrynegative * S ((S (srt_index_rect_totalrows)) * dst_negative_scale_rect_totalrowsrowentry) + (dst_negative_rect_totalrowsrowentry))) /\ (exists ge_balance_positive_rect_totalrowsrowentryvalue ge_balance_negative_rect_totalrowsrowentryvalue. (((((srt_value_rect_totalrows) = 2 * (ge_balance_positive_rect_totalrowsrowentryvalue) /\ (ge_balance_negative_rect_totalrowsrowentryvalue) = 0) \/ exists ge_signed_half_rect_totalrowsrowentryvaluedecode. (((srt_value_rect_totalrows) = 2 * ge_signed_half_rect_totalrowsrowentryvaluedecode + 1 /\ (ge_balance_positive_rect_totalrowsrowentryvalue) = 0) /\ (ge_balance_negative_rect_totalrowsrowentryvalue) = S ge_signed_half_rect_totalrowsrowentryvaluedecode))) /\ ((dst_positive_rect_totalrowsrowentry) + ge_balance_negative_rect_totalrowsrowentryvalue = (dst_negative_rect_totalrowsrowentry) + ge_balance_positive_rect_totalrowsrowentryvalue))))))))) /\ (exists srs_slice_rect_totalrowsrowrow_sum. ((((exists dst_positive_code_rect_totalrowsrowrow_sumslicesource_table dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table dst_negative_code_rect_totalrowsrowrow_sumslicesource_table dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table. (((T) = (((((dst_positive_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table) + (dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table))) + (((dst_negative_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table)) * S ((dst_positive_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table)) + ((dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table) + (dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table))) + (((dst_negative_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table))) + (((dst_negative_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)) * S ((dst_negative_code_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)) + ((dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_rect_totalrowsrowrow_sumslicesource_table. (exists pvs_le_gap_rect_totalrowsrowrow_sumslicesource_tabledomain. pvs_le_gap_rect_totalrowsrowrow_sumslicesource_tabledomain + (dst_index_rect_totalrowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_rect_totalrowsrowrow_sumslicesource_table dst_negative_rect_totalrowsrowrow_sumslicesource_table dst_value_rect_totalrowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_rect_totalrowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_rect_totalrowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_rect_totalrowsrowrow_sumslicesource_table) = S ((S (dst_index_rect_totalrowsrowrow_sumslicesource_table)) * dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_rect_totalrowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_rect_totalrowsrowrow_sumslicesource_table = ff_q_pvs_rect_totalrowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_rect_totalrowsrowrow_sumslicesource_table)) * dst_positive_scale_rect_totalrowsrowrow_sumslicesource_table) + (dst_positive_rect_totalrowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_rect_totalrowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_rect_totalrowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_rect_totalrowsrowrow_sumslicesource_table) = S ((S (dst_index_rect_totalrowsrowrow_sumslicesource_table)) * dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_rect_totalrowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_rect_totalrowsrowrow_sumslicesource_table = ff_q_pvs_rect_totalrowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_rect_totalrowsrowrow_sumslicesource_table)) * dst_negative_scale_rect_totalrowsrowrow_sumslicesource_table) + (dst_negative_rect_totalrowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_rect_totalrowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_rect_totalrowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_rect_totalrowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_rect_totalrowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_rect_totalrowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_rect_totalrowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_rect_totalrowsrowrow_sumslicesource_table) = 2 * ge_signed_half_rect_totalrowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_rect_totalrowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_rect_totalrowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_rect_totalrowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_rect_totalrowsrowrow_sumslicesource_table) + ge_balance_negative_rect_totalrowsrowrow_sumslicesource_tableentryvalue = (dst_negative_rect_totalrowsrowrow_sumslicesource_table) + ge_balance_positive_rect_totalrowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_rect_totalrowsrowrow_sumsliceoutput_table dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table dst_negative_code_rect_totalrowsrowrow_sumsliceoutput_table dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table. (((srs_slice_rect_totalrowsrowrow_sum) = (((((dst_positive_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_rect_totalrowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_rect_totalrowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_rect_totalrowsrowrow_sumsliceoutput_tabledomain + (dst_index_rect_totalrowsrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_rect_totalrowsrowrow_sumsliceoutput_table dst_negative_rect_totalrowsrowrow_sumsliceoutput_table dst_value_rect_totalrowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_rect_totalrowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_rect_totalrowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_rect_totalrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_rect_totalrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_rect_totalrowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_rect_totalrowsrowrow_sumsliceoutput_table = ff_q_pvs_rect_totalrowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_rect_totalrowsrowrow_sumsliceoutput_table)) * dst_positive_scale_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_positive_rect_totalrowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_rect_totalrowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_rect_totalrowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_rect_totalrowsrowrow_sumsliceoutput_table) = S ((S (dst_index_rect_totalrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_rect_totalrowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_rect_totalrowsrowrow_sumsliceoutput_table = ff_q_pvs_rect_totalrowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_rect_totalrowsrowrow_sumsliceoutput_table)) * dst_negative_scale_rect_totalrowsrowrow_sumsliceoutput_table) + (dst_negative_rect_totalrowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_rect_totalrowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_rect_totalrowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_rect_totalrowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_rect_totalrowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_rect_totalrowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_rect_totalrowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_rect_totalrowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_rect_totalrowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_rect_totalrowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_rect_totalrowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_rect_totalrowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_rect_totalrowsrowrow_sumsliceoutput_table) + ge_balance_negative_rect_totalrowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_rect_totalrowsrowrow_sumsliceoutput_table) + ge_balance_positive_rect_totalrowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_rect_totalrowsrowrow_sumslice. (exists pvs_gap_rect_totalrowsrowrow_sumslicebound. pvs_gap_rect_totalrowsrowrow_sumslicebound + S (srs_index_rect_totalrowsrowrow_sumslice) = (n)) -> exists srs_value_rect_totalrowsrowrow_sumslice. (((exists dst_positive_code_rect_totalrowsrowrow_sumsliceentrysource dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource dst_negative_code_rect_totalrowsrowrow_sumsliceentrysource dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource dst_positive_rect_totalrowsrowrow_sumsliceentrysource dst_negative_rect_totalrowsrowrow_sumsliceentrysource. (((T) = (((((dst_positive_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource))) + (((dst_negative_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_rect_totalrowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_rect_totalrowsrowrow_sumsliceentrysourcepositive + S (dst_positive_rect_totalrowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((n) * (srt_index_rect_totalrows)))) + ((1) * (srs_index_rect_totalrowsrowrow_sumslice))))) * dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_rect_totalrowsrowrow_sumsliceentrysourcepositive. dst_positive_code_rect_totalrowsrowrow_sumsliceentrysource = ff_q_pvs_rect_totalrowsrowrow_sumsliceentrysourcepositive * S ((S (((((0) + ((n) * (srt_index_rect_totalrows)))) + ((1) * (srs_index_rect_totalrowsrowrow_sumslice))))) * dst_positive_scale_rect_totalrowsrowrow_sumsliceentrysource) + (dst_positive_rect_totalrowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_rect_totalrowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_rect_totalrowsrowrow_sumsliceentrysourcenegative + S (dst_negative_rect_totalrowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((n) * (srt_index_rect_totalrows)))) + ((1) * (srs_index_rect_totalrowsrowrow_sumslice))))) * dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_rect_totalrowsrowrow_sumsliceentrysourcenegative. dst_negative_code_rect_totalrowsrowrow_sumsliceentrysource = ff_q_pvs_rect_totalrowsrowrow_sumsliceentrysourcenegative * S ((S (((((0) + ((n) * (srt_index_rect_totalrows)))) + ((1) * (srs_index_rect_totalrowsrowrow_sumslice))))) * dst_negative_scale_rect_totalrowsrowrow_sumsliceentrysource) + (dst_negative_rect_totalrowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_rect_totalrowsrowrow_sumsliceentrysourcevalue ge_balance_negative_rect_totalrowsrowrow_sumsliceentrysourcevalue. (((((srs_value_rect_totalrowsrowrow_sumslice) = 2 * (ge_balance_positive_rect_totalrowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_rect_totalrowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_rect_totalrowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_rect_totalrowsrowrow_sumslice) = 2 * ge_signed_half_rect_totalrowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_rect_totalrowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_rect_totalrowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_rect_totalrowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_rect_totalrowsrowrow_sumsliceentrysource) + ge_balance_negative_rect_totalrowsrowrow_sumsliceentrysourcevalue = (dst_negative_rect_totalrowsrowrow_sumsliceentrysource) + ge_balance_positive_rect_totalrowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_rect_totalrowsrowrow_sumsliceentryoutput dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput dst_negative_code_rect_totalrowsrowrow_sumsliceentryoutput dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput dst_positive_rect_totalrowsrowrow_sumsliceentryoutput dst_negative_rect_totalrowsrowrow_sumsliceentryoutput. (((srs_slice_rect_totalrowsrowrow_sum) = (((((dst_positive_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_rect_totalrowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_rect_totalrowsrowrow_sumsliceentryoutputpositive + S (dst_positive_rect_totalrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_rect_totalrowsrowrow_sumslice)) * dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_rect_totalrowsrowrow_sumsliceentryoutputpositive. dst_positive_code_rect_totalrowsrowrow_sumsliceentryoutput = ff_q_pvs_rect_totalrowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_rect_totalrowsrowrow_sumslice)) * dst_positive_scale_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_positive_rect_totalrowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_rect_totalrowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_rect_totalrowsrowrow_sumsliceentryoutputnegative + S (dst_negative_rect_totalrowsrowrow_sumsliceentryoutput) = S ((S (srs_index_rect_totalrowsrowrow_sumslice)) * dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_rect_totalrowsrowrow_sumsliceentryoutputnegative. dst_negative_code_rect_totalrowsrowrow_sumsliceentryoutput = ff_q_pvs_rect_totalrowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_rect_totalrowsrowrow_sumslice)) * dst_negative_scale_rect_totalrowsrowrow_sumsliceentryoutput) + (dst_negative_rect_totalrowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_rect_totalrowsrowrow_sumsliceentryoutputvalue ge_balance_negative_rect_totalrowsrowrow_sumsliceentryoutputvalue. (((((srs_value_rect_totalrowsrowrow_sumslice) = 2 * (ge_balance_positive_rect_totalrowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_rect_totalrowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_rect_totalrowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_rect_totalrowsrowrow_sumslice) = 2 * ge_signed_half_rect_totalrowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_rect_totalrowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_rect_totalrowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_rect_totalrowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_rect_totalrowsrowrow_sumsliceentryoutput) + ge_balance_negative_rect_totalrowsrowrow_sumsliceentryoutputvalue = (dst_negative_rect_totalrowsrowrow_sumsliceentryoutput) + ge_balance_positive_rect_totalrowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_rect_totalrowsrowrow_sumsum dst_positive_scale_rect_totalrowsrowrow_sumsum dst_negative_code_rect_totalrowsrowrow_sumsum dst_negative_scale_rect_totalrowsrowrow_sumsum dst_positive_sum_rect_totalrowsrowrow_sumsum dst_negative_sum_rect_totalrowsrowrow_sumsum. (((srs_slice_rect_totalrowsrowrow_sum) = (((((dst_positive_code_rect_totalrowsrowrow_sumsum) + (dst_positive_scale_rect_totalrowsrowrow_sumsum)) * S ((dst_positive_code_rect_totalrowsrowrow_sumsum) + (dst_positive_scale_rect_totalrowsrowrow_sumsum)) + ((dst_positive_scale_rect_totalrowsrowrow_sumsum) + (dst_positive_scale_rect_totalrowsrowrow_sumsum))) + (((dst_negative_code_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)))) * S ((((dst_positive_code_rect_totalrowsrowrow_sumsum) + (dst_positive_scale_rect_totalrowsrowrow_sumsum)) * S ((dst_positive_code_rect_totalrowsrowrow_sumsum) + (dst_positive_scale_rect_totalrowsrowrow_sumsum)) + ((dst_positive_scale_rect_totalrowsrowrow_sumsum) + (dst_positive_scale_rect_totalrowsrowrow_sumsum))) + (((dst_negative_code_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)))) + ((((dst_negative_code_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum))) + (((dst_negative_code_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)) * S ((dst_negative_code_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)) + ((dst_negative_scale_rect_totalrowsrowrow_sumsum) + (dst_negative_scale_rect_totalrowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_rect_totalrowsrowrow_sumsumpositive fs_v_dst_rect_totalrowsrowrow_sumsumpositive. ((((exists fs_h_dst_rect_totalrowsrowrow_sumsumpositive_body_start. fs_h_dst_rect_totalrowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_rect_totalrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_rect_totalrowsrowrow_sumsumpositive_body_start. fs_u_dst_rect_totalrowsrowrow_sumsumpositive = fs_q_dst_rect_totalrowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_rect_totalrowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_rect_totalrowsrowrow_sumsumpositive_body_terminal. fs_h_dst_rect_totalrowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_rect_totalrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_rect_totalrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_rect_totalrowsrowrow_sumsumpositive_body_terminal. fs_u_dst_rect_totalrowsrowrow_sumsumpositive = fs_q_dst_rect_totalrowsrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_rect_totalrowsrowrow_sumsumpositive) + (dst_positive_sum_rect_totalrowsrowrow_sumsum))) /\ forall fs_i_dst_rect_totalrowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_rect_totalrowsrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_rect_totalrowsrowrow_sumsumpositive_body_steps fs_r_dst_rect_totalrowsrowrow_sumsumpositive_body_steps fs_s_dst_rect_totalrowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_rect_totalrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_rect_totalrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_rect_totalrowsrowrow_sumsum)) /\ exists fs_q_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_rect_totalrowsrowrow_sumsum = fs_q_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_rect_totalrowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_rect_totalrowsrowrow_sumsum) + (fs_a_dst_rect_totalrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_rect_totalrowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_rect_totalrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_rect_totalrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_rect_totalrowsrowrow_sumsumpositive = fs_q_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_rect_totalrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_rect_totalrowsrowrow_sumsumpositive) + (fs_r_dst_rect_totalrowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_rect_totalrowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_rect_totalrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_rect_totalrowsrowrow_sumsumpositive)) /\ exists fs_q_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_rect_totalrowsrowrow_sumsumpositive = fs_q_dst_rect_totalrowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_rect_totalrowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_rect_totalrowsrowrow_sumsumpositive) + (fs_s_dst_rect_totalrowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_rect_totalrowsrowrow_sumsumpositive_body_steps = fs_r_dst_rect_totalrowsrowrow_sumsumpositive_body_steps + fs_a_dst_rect_totalrowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_rect_totalrowsrowrow_sumsumnegative fs_v_dst_rect_totalrowsrowrow_sumsumnegative. ((((exists fs_h_dst_rect_totalrowsrowrow_sumsumnegative_body_start. fs_h_dst_rect_totalrowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_rect_totalrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_rect_totalrowsrowrow_sumsumnegative_body_start. fs_u_dst_rect_totalrowsrowrow_sumsumnegative = fs_q_dst_rect_totalrowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_rect_totalrowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_rect_totalrowsrowrow_sumsumnegative_body_terminal. fs_h_dst_rect_totalrowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_rect_totalrowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_rect_totalrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_rect_totalrowsrowrow_sumsumnegative_body_terminal. fs_u_dst_rect_totalrowsrowrow_sumsumnegative = fs_q_dst_rect_totalrowsrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_rect_totalrowsrowrow_sumsumnegative) + (dst_negative_sum_rect_totalrowsrowrow_sumsum))) /\ forall fs_i_dst_rect_totalrowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_rect_totalrowsrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_rect_totalrowsrowrow_sumsumnegative_body_steps fs_r_dst_rect_totalrowsrowrow_sumsumnegative_body_steps fs_s_dst_rect_totalrowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_rect_totalrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_rect_totalrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_rect_totalrowsrowrow_sumsum)) /\ exists fs_q_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_rect_totalrowsrowrow_sumsum = fs_q_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_rect_totalrowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_rect_totalrowsrowrow_sumsum) + (fs_a_dst_rect_totalrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_rect_totalrowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_rect_totalrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_rect_totalrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_rect_totalrowsrowrow_sumsumnegative = fs_q_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_rect_totalrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_rect_totalrowsrowrow_sumsumnegative) + (fs_r_dst_rect_totalrowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_rect_totalrowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_rect_totalrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_rect_totalrowsrowrow_sumsumnegative)) /\ exists fs_q_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_rect_totalrowsrowrow_sumsumnegative = fs_q_dst_rect_totalrowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_rect_totalrowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_rect_totalrowsrowrow_sumsumnegative) + (fs_s_dst_rect_totalrowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_rect_totalrowsrowrow_sumsumnegative_body_steps = fs_r_dst_rect_totalrowsrowrow_sumsumnegative_body_steps + fs_a_dst_rect_totalrowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_rect_totalrowsrowrow_sumsumresult ge_balance_negative_rect_totalrowsrowrow_sumsumresult. (((((srt_value_rect_totalrows) = 2 * (ge_balance_positive_rect_totalrowsrowrow_sumsumresult) /\ (ge_balance_negative_rect_totalrowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_rect_totalrowsrowrow_sumsumresultdecode. (((srt_value_rect_totalrows) = 2 * ge_signed_half_rect_totalrowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_rect_totalrowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_rect_totalrowsrowrow_sumsumresult) = S ge_signed_half_rect_totalrowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_rect_totalrowsrowrow_sumsum) + ge_balance_negative_rect_totalrowsrowrow_sumsumresult = (dst_negative_sum_rect_totalrowsrowrow_sumsum) + ge_balance_positive_rect_totalrowsrowrow_sumsumresult)))))))))))))))))) /\ (exists dst_positive_code_rect_totaltotal dst_positive_scale_rect_totaltotal dst_negative_code_rect_totaltotal dst_negative_scale_rect_totaltotal dst_positive_sum_rect_totaltotal dst_negative_sum_rect_totaltotal. (((srt_rows_rect_total) = (((((dst_positive_code_rect_totaltotal) + (dst_positive_scale_rect_totaltotal)) * S ((dst_positive_code_rect_totaltotal) + (dst_positive_scale_rect_totaltotal)) + ((dst_positive_scale_rect_totaltotal) + (dst_positive_scale_rect_totaltotal))) + (((dst_negative_code_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)) * S ((dst_negative_code_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)) + ((dst_negative_scale_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)))) * S ((((dst_positive_code_rect_totaltotal) + (dst_positive_scale_rect_totaltotal)) * S ((dst_positive_code_rect_totaltotal) + (dst_positive_scale_rect_totaltotal)) + ((dst_positive_scale_rect_totaltotal) + (dst_positive_scale_rect_totaltotal))) + (((dst_negative_code_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)) * S ((dst_negative_code_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)) + ((dst_negative_scale_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)))) + ((((dst_negative_code_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)) * S ((dst_negative_code_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)) + ((dst_negative_scale_rect_totaltotal) + (dst_negative_scale_rect_totaltotal))) + (((dst_negative_code_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)) * S ((dst_negative_code_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)) + ((dst_negative_scale_rect_totaltotal) + (dst_negative_scale_rect_totaltotal)))))) /\ (((exists fs_u_dst_rect_totaltotalpositive fs_v_dst_rect_totaltotalpositive. ((((exists fs_h_dst_rect_totaltotalpositive_body_start. fs_h_dst_rect_totaltotalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_rect_totaltotalpositive)) /\ exists fs_q_dst_rect_totaltotalpositive_body_start. fs_u_dst_rect_totaltotalpositive = fs_q_dst_rect_totaltotalpositive_body_start * S ((S (0)) * fs_v_dst_rect_totaltotalpositive) + (0))) /\ ((((exists fs_h_dst_rect_totaltotalpositive_body_terminal. fs_h_dst_rect_totaltotalpositive_body_terminal + S (dst_positive_sum_rect_totaltotal) = S ((S (m)) * fs_v_dst_rect_totaltotalpositive)) /\ exists fs_q_dst_rect_totaltotalpositive_body_terminal. fs_u_dst_rect_totaltotalpositive = fs_q_dst_rect_totaltotalpositive_body_terminal * S ((S (m)) * fs_v_dst_rect_totaltotalpositive) + (dst_positive_sum_rect_totaltotal))) /\ forall fs_i_dst_rect_totaltotalpositive_body_steps. (exists fs_lt_dst_rect_totaltotalpositive_body_steps_bound. fs_lt_dst_rect_totaltotalpositive_body_steps_bound + S fs_i_dst_rect_totaltotalpositive_body_steps = m) -> exists fs_a_dst_rect_totaltotalpositive_body_steps fs_r_dst_rect_totaltotalpositive_body_steps fs_s_dst_rect_totaltotalpositive_body_steps. ((((exists fs_h_dst_rect_totaltotalpositive_body_steps_summand. fs_h_dst_rect_totaltotalpositive_body_steps_summand + S (fs_a_dst_rect_totaltotalpositive_body_steps) = S ((S (fs_i_dst_rect_totaltotalpositive_body_steps)) * dst_positive_scale_rect_totaltotal)) /\ exists fs_q_dst_rect_totaltotalpositive_body_steps_summand. dst_positive_code_rect_totaltotal = fs_q_dst_rect_totaltotalpositive_body_steps_summand * S ((S (fs_i_dst_rect_totaltotalpositive_body_steps)) * dst_positive_scale_rect_totaltotal) + (fs_a_dst_rect_totaltotalpositive_body_steps))) /\ ((((exists fs_h_dst_rect_totaltotalpositive_body_steps_partial. fs_h_dst_rect_totaltotalpositive_body_steps_partial + S (fs_r_dst_rect_totaltotalpositive_body_steps) = S ((S (fs_i_dst_rect_totaltotalpositive_body_steps)) * fs_v_dst_rect_totaltotalpositive)) /\ exists fs_q_dst_rect_totaltotalpositive_body_steps_partial. fs_u_dst_rect_totaltotalpositive = fs_q_dst_rect_totaltotalpositive_body_steps_partial * S ((S (fs_i_dst_rect_totaltotalpositive_body_steps)) * fs_v_dst_rect_totaltotalpositive) + (fs_r_dst_rect_totaltotalpositive_body_steps))) /\ ((((exists fs_h_dst_rect_totaltotalpositive_body_steps_successor. fs_h_dst_rect_totaltotalpositive_body_steps_successor + S (fs_s_dst_rect_totaltotalpositive_body_steps) = S ((S (S fs_i_dst_rect_totaltotalpositive_body_steps)) * fs_v_dst_rect_totaltotalpositive)) /\ exists fs_q_dst_rect_totaltotalpositive_body_steps_successor. fs_u_dst_rect_totaltotalpositive = fs_q_dst_rect_totaltotalpositive_body_steps_successor * S ((S (S fs_i_dst_rect_totaltotalpositive_body_steps)) * fs_v_dst_rect_totaltotalpositive) + (fs_s_dst_rect_totaltotalpositive_body_steps))) /\ fs_s_dst_rect_totaltotalpositive_body_steps = fs_r_dst_rect_totaltotalpositive_body_steps + fs_a_dst_rect_totaltotalpositive_body_steps)))))) /\ (((exists fs_u_dst_rect_totaltotalnegative fs_v_dst_rect_totaltotalnegative. ((((exists fs_h_dst_rect_totaltotalnegative_body_start. fs_h_dst_rect_totaltotalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_rect_totaltotalnegative)) /\ exists fs_q_dst_rect_totaltotalnegative_body_start. fs_u_dst_rect_totaltotalnegative = fs_q_dst_rect_totaltotalnegative_body_start * S ((S (0)) * fs_v_dst_rect_totaltotalnegative) + (0))) /\ ((((exists fs_h_dst_rect_totaltotalnegative_body_terminal. fs_h_dst_rect_totaltotalnegative_body_terminal + S (dst_negative_sum_rect_totaltotal) = S ((S (m)) * fs_v_dst_rect_totaltotalnegative)) /\ exists fs_q_dst_rect_totaltotalnegative_body_terminal. fs_u_dst_rect_totaltotalnegative = fs_q_dst_rect_totaltotalnegative_body_terminal * S ((S (m)) * fs_v_dst_rect_totaltotalnegative) + (dst_negative_sum_rect_totaltotal))) /\ forall fs_i_dst_rect_totaltotalnegative_body_steps. (exists fs_lt_dst_rect_totaltotalnegative_body_steps_bound. fs_lt_dst_rect_totaltotalnegative_body_steps_bound + S fs_i_dst_rect_totaltotalnegative_body_steps = m) -> exists fs_a_dst_rect_totaltotalnegative_body_steps fs_r_dst_rect_totaltotalnegative_body_steps fs_s_dst_rect_totaltotalnegative_body_steps. ((((exists fs_h_dst_rect_totaltotalnegative_body_steps_summand. fs_h_dst_rect_totaltotalnegative_body_steps_summand + S (fs_a_dst_rect_totaltotalnegative_body_steps) = S ((S (fs_i_dst_rect_totaltotalnegative_body_steps)) * dst_negative_scale_rect_totaltotal)) /\ exists fs_q_dst_rect_totaltotalnegative_body_steps_summand. dst_negative_code_rect_totaltotal = fs_q_dst_rect_totaltotalnegative_body_steps_summand * S ((S (fs_i_dst_rect_totaltotalnegative_body_steps)) * dst_negative_scale_rect_totaltotal) + (fs_a_dst_rect_totaltotalnegative_body_steps))) /\ ((((exists fs_h_dst_rect_totaltotalnegative_body_steps_partial. fs_h_dst_rect_totaltotalnegative_body_steps_partial + S (fs_r_dst_rect_totaltotalnegative_body_steps) = S ((S (fs_i_dst_rect_totaltotalnegative_body_steps)) * fs_v_dst_rect_totaltotalnegative)) /\ exists fs_q_dst_rect_totaltotalnegative_body_steps_partial. fs_u_dst_rect_totaltotalnegative = fs_q_dst_rect_totaltotalnegative_body_steps_partial * S ((S (fs_i_dst_rect_totaltotalnegative_body_steps)) * fs_v_dst_rect_totaltotalnegative) + (fs_r_dst_rect_totaltotalnegative_body_steps))) /\ ((((exists fs_h_dst_rect_totaltotalnegative_body_steps_successor. fs_h_dst_rect_totaltotalnegative_body_steps_successor + S (fs_s_dst_rect_totaltotalnegative_body_steps) = S ((S (S fs_i_dst_rect_totaltotalnegative_body_steps)) * fs_v_dst_rect_totaltotalnegative)) /\ exists fs_q_dst_rect_totaltotalnegative_body_steps_successor. fs_u_dst_rect_totaltotalnegative = fs_q_dst_rect_totaltotalnegative_body_steps_successor * S ((S (S fs_i_dst_rect_totaltotalnegative_body_steps)) * fs_v_dst_rect_totaltotalnegative) + (fs_s_dst_rect_totaltotalnegative_body_steps))) /\ fs_s_dst_rect_totaltotalnegative_body_steps = fs_r_dst_rect_totaltotalnegative_body_steps + fs_a_dst_rect_totaltotalnegative_body_steps)))))) /\ (exists ge_balance_positive_rect_totaltotalresult ge_balance_negative_rect_totaltotalresult. (((((c) = 2 * (ge_balance_positive_rect_totaltotalresult) /\ (ge_balance_negative_rect_totaltotalresult) = 0) \/ exists ge_signed_half_rect_totaltotalresultdecode. (((c) = 2 * ge_signed_half_rect_totaltotalresultdecode + 1 /\ (ge_balance_positive_rect_totaltotalresult) = 0) /\ (ge_balance_negative_rect_totaltotalresult) = S ge_signed_half_rect_totaltotalresultdecode))) /\ ((dst_positive_sum_rect_totaltotal) + ge_balance_negative_rect_totaltotalresult = (dst_negative_sum_rect_totaltotal) + ge_balance_positive_rect_totaltotalresult))))))))))) -> (exists sto_ap_rect_result sto_an_rect_result sto_bp_rect_result sto_bn_rect_result sto_cp_rect_result sto_cn_rect_result. (((((a) = 2 * (sto_ap_rect_result) /\ (sto_an_rect_result) = 0) \/ exists ge_signed_half_rect_resultleft. (((a) = 2 * ge_signed_half_rect_resultleft + 1 /\ (sto_ap_rect_result) = 0) /\ (sto_an_rect_result) = S ge_signed_half_rect_resultleft))) /\ ((((((b) = 2 * (sto_bp_rect_result) /\ (sto_bn_rect_result) = 0) \/ exists ge_signed_half_rect_resultright. (((b) = 2 * ge_signed_half_rect_resultright + 1 /\ (sto_bp_rect_result) = 0) /\ (sto_bn_rect_result) = S ge_signed_half_rect_resultright))) /\ ((((((c) = 2 * (sto_cp_rect_result) /\ (sto_cn_rect_result) = 0) \/ exists ge_signed_half_rect_resultoutput. (((c) = 2 * ge_signed_half_rect_resultoutput + 1 /\ (sto_cp_rect_result) = 0) /\ (sto_cn_rect_result) = S ge_signed_half_rect_resultoutput))) /\ ((sto_ap_rect_result * sto_bp_rect_result + sto_an_rect_result * sto_bn_rect_result) + sto_cn_rect_result = (sto_ap_rect_result * sto_bn_rect_result + sto_an_rect_result * sto_bp_rect_result) + sto_cp_rect_result)))))))