signed_cartesian_product_row_scalar

Exact expanded first-order arithmetic statement

forall F G T V m n i a. (((exists dst_positive_code_row_productF dst_positive_scale_row_productF dst_negative_code_row_productF dst_negative_scale_row_productF. (((F) = (((((dst_positive_code_row_productF) + (dst_positive_scale_row_productF)) * S ((dst_positive_code_row_productF) + (dst_positive_scale_row_productF)) + ((dst_positive_scale_row_productF) + (dst_positive_scale_row_productF))) + (((dst_negative_code_row_productF) + (dst_negative_scale_row_productF)) * S ((dst_negative_code_row_productF) + (dst_negative_scale_row_productF)) + ((dst_negative_scale_row_productF) + (dst_negative_scale_row_productF)))) * S ((((dst_positive_code_row_productF) + (dst_positive_scale_row_productF)) * S ((dst_positive_code_row_productF) + (dst_positive_scale_row_productF)) + ((dst_positive_scale_row_productF) + (dst_positive_scale_row_productF))) + (((dst_negative_code_row_productF) + (dst_negative_scale_row_productF)) * S ((dst_negative_code_row_productF) + (dst_negative_scale_row_productF)) + ((dst_negative_scale_row_productF) + (dst_negative_scale_row_productF)))) + ((((dst_negative_code_row_productF) + (dst_negative_scale_row_productF)) * S ((dst_negative_code_row_productF) + (dst_negative_scale_row_productF)) + ((dst_negative_scale_row_productF) + (dst_negative_scale_row_productF))) + (((dst_negative_code_row_productF) + (dst_negative_scale_row_productF)) * S ((dst_negative_code_row_productF) + (dst_negative_scale_row_productF)) + ((dst_negative_scale_row_productF) + (dst_negative_scale_row_productF)))))) /\ (forall dst_index_row_productF. (exists pvs_le_gap_row_productFdomain. pvs_le_gap_row_productFdomain + (dst_index_row_productF) = (0)) -> exists dst_positive_row_productF dst_negative_row_productF dst_value_row_productF. ((((exists ff_h_pvs_row_productFentrypositive. ff_h_pvs_row_productFentrypositive + S (dst_positive_row_productF) = S ((S (dst_index_row_productF)) * dst_positive_scale_row_productF)) /\ exists ff_q_pvs_row_productFentrypositive. dst_positive_code_row_productF = ff_q_pvs_row_productFentrypositive * S ((S (dst_index_row_productF)) * dst_positive_scale_row_productF) + (dst_positive_row_productF))) /\ (((((exists ff_h_pvs_row_productFentrynegative. ff_h_pvs_row_productFentrynegative + S (dst_negative_row_productF) = S ((S (dst_index_row_productF)) * dst_negative_scale_row_productF)) /\ exists ff_q_pvs_row_productFentrynegative. dst_negative_code_row_productF = ff_q_pvs_row_productFentrynegative * S ((S (dst_index_row_productF)) * dst_negative_scale_row_productF) + (dst_negative_row_productF))) /\ (exists ge_balance_positive_row_productFentryvalue ge_balance_negative_row_productFentryvalue. (((((dst_value_row_productF) = 2 * (ge_balance_positive_row_productFentryvalue) /\ (ge_balance_negative_row_productFentryvalue) = 0) \/ exists ge_signed_half_row_productFentryvaluedecode. (((dst_value_row_productF) = 2 * ge_signed_half_row_productFentryvaluedecode + 1 /\ (ge_balance_positive_row_productFentryvalue) = 0) /\ (ge_balance_negative_row_productFentryvalue) = S ge_signed_half_row_productFentryvaluedecode))) /\ ((dst_positive_row_productF) + ge_balance_negative_row_productFentryvalue = (dst_negative_row_productF) + ge_balance_positive_row_productFentryvalue))))))))) /\ (((exists dst_positive_code_row_productG dst_positive_scale_row_productG dst_negative_code_row_productG dst_negative_scale_row_productG. (((G) = (((((dst_positive_code_row_productG) + (dst_positive_scale_row_productG)) * S ((dst_positive_code_row_productG) + (dst_positive_scale_row_productG)) + ((dst_positive_scale_row_productG) + (dst_positive_scale_row_productG))) + (((dst_negative_code_row_productG) + (dst_negative_scale_row_productG)) * S ((dst_negative_code_row_productG) + (dst_negative_scale_row_productG)) + ((dst_negative_scale_row_productG) + (dst_negative_scale_row_productG)))) * S ((((dst_positive_code_row_productG) + (dst_positive_scale_row_productG)) * S ((dst_positive_code_row_productG) + (dst_positive_scale_row_productG)) + ((dst_positive_scale_row_productG) + (dst_positive_scale_row_productG))) + (((dst_negative_code_row_productG) + (dst_negative_scale_row_productG)) * S ((dst_negative_code_row_productG) + (dst_negative_scale_row_productG)) + ((dst_negative_scale_row_productG) + (dst_negative_scale_row_productG)))) + ((((dst_negative_code_row_productG) + (dst_negative_scale_row_productG)) * S ((dst_negative_code_row_productG) + (dst_negative_scale_row_productG)) + ((dst_negative_scale_row_productG) + (dst_negative_scale_row_productG))) + (((dst_negative_code_row_productG) + (dst_negative_scale_row_productG)) * S ((dst_negative_code_row_productG) + (dst_negative_scale_row_productG)) + ((dst_negative_scale_row_productG) + (dst_negative_scale_row_productG)))))) /\ (forall dst_index_row_productG. (exists pvs_le_gap_row_productGdomain. pvs_le_gap_row_productGdomain + (dst_index_row_productG) = (0)) -> exists dst_positive_row_productG dst_negative_row_productG dst_value_row_productG. ((((exists ff_h_pvs_row_productGentrypositive. ff_h_pvs_row_productGentrypositive + S (dst_positive_row_productG) = S ((S (dst_index_row_productG)) * dst_positive_scale_row_productG)) /\ exists ff_q_pvs_row_productGentrypositive. dst_positive_code_row_productG = ff_q_pvs_row_productGentrypositive * S ((S (dst_index_row_productG)) * dst_positive_scale_row_productG) + (dst_positive_row_productG))) /\ (((((exists ff_h_pvs_row_productGentrynegative. ff_h_pvs_row_productGentrynegative + S (dst_negative_row_productG) = S ((S (dst_index_row_productG)) * dst_negative_scale_row_productG)) /\ exists ff_q_pvs_row_productGentrynegative. dst_negative_code_row_productG = ff_q_pvs_row_productGentrynegative * S ((S (dst_index_row_productG)) * dst_negative_scale_row_productG) + (dst_negative_row_productG))) /\ (exists ge_balance_positive_row_productGentryvalue ge_balance_negative_row_productGentryvalue. (((((dst_value_row_productG) = 2 * (ge_balance_positive_row_productGentryvalue) /\ (ge_balance_negative_row_productGentryvalue) = 0) \/ exists ge_signed_half_row_productGentryvaluedecode. (((dst_value_row_productG) = 2 * ge_signed_half_row_productGentryvaluedecode + 1 /\ (ge_balance_positive_row_productGentryvalue) = 0) /\ (ge_balance_negative_row_productGentryvalue) = S ge_signed_half_row_productGentryvaluedecode))) /\ ((dst_positive_row_productG) + ge_balance_negative_row_productGentryvalue = (dst_negative_row_productG) + ge_balance_positive_row_productGentryvalue))))))))) /\ (((exists dst_positive_code_row_productT dst_positive_scale_row_productT dst_negative_code_row_productT dst_negative_scale_row_productT. (((T) = (((((dst_positive_code_row_productT) + (dst_positive_scale_row_productT)) * S ((dst_positive_code_row_productT) + (dst_positive_scale_row_productT)) + ((dst_positive_scale_row_productT) + (dst_positive_scale_row_productT))) + (((dst_negative_code_row_productT) + (dst_negative_scale_row_productT)) * S ((dst_negative_code_row_productT) + (dst_negative_scale_row_productT)) + ((dst_negative_scale_row_productT) + (dst_negative_scale_row_productT)))) * S ((((dst_positive_code_row_productT) + (dst_positive_scale_row_productT)) * S ((dst_positive_code_row_productT) + (dst_positive_scale_row_productT)) + ((dst_positive_scale_row_productT) + (dst_positive_scale_row_productT))) + (((dst_negative_code_row_productT) + (dst_negative_scale_row_productT)) * S ((dst_negative_code_row_productT) + (dst_negative_scale_row_productT)) + ((dst_negative_scale_row_productT) + (dst_negative_scale_row_productT)))) + ((((dst_negative_code_row_productT) + (dst_negative_scale_row_productT)) * S ((dst_negative_code_row_productT) + (dst_negative_scale_row_productT)) + ((dst_negative_scale_row_productT) + (dst_negative_scale_row_productT))) + (((dst_negative_code_row_productT) + (dst_negative_scale_row_productT)) * S ((dst_negative_code_row_productT) + (dst_negative_scale_row_productT)) + ((dst_negative_scale_row_productT) + (dst_negative_scale_row_productT)))))) /\ (forall dst_index_row_productT. (exists pvs_le_gap_row_productTdomain. pvs_le_gap_row_productTdomain + (dst_index_row_productT) = ((m)*(n))) -> exists dst_positive_row_productT dst_negative_row_productT dst_value_row_productT. ((((exists ff_h_pvs_row_productTentrypositive. ff_h_pvs_row_productTentrypositive + S (dst_positive_row_productT) = S ((S (dst_index_row_productT)) * dst_positive_scale_row_productT)) /\ exists ff_q_pvs_row_productTentrypositive. dst_positive_code_row_productT = ff_q_pvs_row_productTentrypositive * S ((S (dst_index_row_productT)) * dst_positive_scale_row_productT) + (dst_positive_row_productT))) /\ (((((exists ff_h_pvs_row_productTentrynegative. ff_h_pvs_row_productTentrynegative + S (dst_negative_row_productT) = S ((S (dst_index_row_productT)) * dst_negative_scale_row_productT)) /\ exists ff_q_pvs_row_productTentrynegative. dst_negative_code_row_productT = ff_q_pvs_row_productTentrynegative * S ((S (dst_index_row_productT)) * dst_negative_scale_row_productT) + (dst_negative_row_productT))) /\ (exists ge_balance_positive_row_productTentryvalue ge_balance_negative_row_productTentryvalue. (((((dst_value_row_productT) = 2 * (ge_balance_positive_row_productTentryvalue) /\ (ge_balance_negative_row_productTentryvalue) = 0) \/ exists ge_signed_half_row_productTentryvaluedecode. (((dst_value_row_productT) = 2 * ge_signed_half_row_productTentryvaluedecode + 1 /\ (ge_balance_positive_row_productTentryvalue) = 0) /\ (ge_balance_negative_row_productTentryvalue) = S ge_signed_half_row_productTentryvaluedecode))) /\ ((dst_positive_row_productT) + ge_balance_negative_row_productTentryvalue = (dst_negative_row_productT) + ge_balance_positive_row_productTentryvalue))))))))) /\ (forall scp_row_row_product scp_column_row_product scp_first_row_product scp_second_row_product scp_value_row_product. (exists pvs_gap_row_productrows. pvs_gap_row_productrows + S (scp_row_row_product) = (m)) -> (exists pvs_gap_row_productcolumns. pvs_gap_row_productcolumns + S (scp_column_row_product) = (n)) -> (exists dst_positive_code_row_productfirst dst_positive_scale_row_productfirst dst_negative_code_row_productfirst dst_negative_scale_row_productfirst dst_positive_row_productfirst dst_negative_row_productfirst. (((F) = (((((dst_positive_code_row_productfirst) + (dst_positive_scale_row_productfirst)) * S ((dst_positive_code_row_productfirst) + (dst_positive_scale_row_productfirst)) + ((dst_positive_scale_row_productfirst) + (dst_positive_scale_row_productfirst))) + (((dst_negative_code_row_productfirst) + (dst_negative_scale_row_productfirst)) * S ((dst_negative_code_row_productfirst) + (dst_negative_scale_row_productfirst)) + ((dst_negative_scale_row_productfirst) + (dst_negative_scale_row_productfirst)))) * S ((((dst_positive_code_row_productfirst) + (dst_positive_scale_row_productfirst)) * S ((dst_positive_code_row_productfirst) + (dst_positive_scale_row_productfirst)) + ((dst_positive_scale_row_productfirst) + (dst_positive_scale_row_productfirst))) + (((dst_negative_code_row_productfirst) + (dst_negative_scale_row_productfirst)) * S ((dst_negative_code_row_productfirst) + (dst_negative_scale_row_productfirst)) + ((dst_negative_scale_row_productfirst) + (dst_negative_scale_row_productfirst)))) + ((((dst_negative_code_row_productfirst) + (dst_negative_scale_row_productfirst)) * S ((dst_negative_code_row_productfirst) + (dst_negative_scale_row_productfirst)) + ((dst_negative_scale_row_productfirst) + (dst_negative_scale_row_productfirst))) + (((dst_negative_code_row_productfirst) + (dst_negative_scale_row_productfirst)) * S ((dst_negative_code_row_productfirst) + (dst_negative_scale_row_productfirst)) + ((dst_negative_scale_row_productfirst) + (dst_negative_scale_row_productfirst)))))) /\ (((((exists ff_h_pvs_row_productfirstpositive. ff_h_pvs_row_productfirstpositive + S (dst_positive_row_productfirst) = S ((S (scp_row_row_product)) * dst_positive_scale_row_productfirst)) /\ exists ff_q_pvs_row_productfirstpositive. dst_positive_code_row_productfirst = ff_q_pvs_row_productfirstpositive * S ((S (scp_row_row_product)) * dst_positive_scale_row_productfirst) + (dst_positive_row_productfirst))) /\ (((((exists ff_h_pvs_row_productfirstnegative. ff_h_pvs_row_productfirstnegative + S (dst_negative_row_productfirst) = S ((S (scp_row_row_product)) * dst_negative_scale_row_productfirst)) /\ exists ff_q_pvs_row_productfirstnegative. dst_negative_code_row_productfirst = ff_q_pvs_row_productfirstnegative * S ((S (scp_row_row_product)) * dst_negative_scale_row_productfirst) + (dst_negative_row_productfirst))) /\ (exists ge_balance_positive_row_productfirstvalue ge_balance_negative_row_productfirstvalue. (((((scp_first_row_product) = 2 * (ge_balance_positive_row_productfirstvalue) /\ (ge_balance_negative_row_productfirstvalue) = 0) \/ exists ge_signed_half_row_productfirstvaluedecode. (((scp_first_row_product) = 2 * ge_signed_half_row_productfirstvaluedecode + 1 /\ (ge_balance_positive_row_productfirstvalue) = 0) /\ (ge_balance_negative_row_productfirstvalue) = S ge_signed_half_row_productfirstvaluedecode))) /\ ((dst_positive_row_productfirst) + ge_balance_negative_row_productfirstvalue = (dst_negative_row_productfirst) + ge_balance_positive_row_productfirstvalue))))))))) -> (exists dst_positive_code_row_productsecond dst_positive_scale_row_productsecond dst_negative_code_row_productsecond dst_negative_scale_row_productsecond dst_positive_row_productsecond dst_negative_row_productsecond. (((G) = (((((dst_positive_code_row_productsecond) + (dst_positive_scale_row_productsecond)) * S ((dst_positive_code_row_productsecond) + (dst_positive_scale_row_productsecond)) + ((dst_positive_scale_row_productsecond) + (dst_positive_scale_row_productsecond))) + (((dst_negative_code_row_productsecond) + (dst_negative_scale_row_productsecond)) * S ((dst_negative_code_row_productsecond) + (dst_negative_scale_row_productsecond)) + ((dst_negative_scale_row_productsecond) + (dst_negative_scale_row_productsecond)))) * S ((((dst_positive_code_row_productsecond) + (dst_positive_scale_row_productsecond)) * S ((dst_positive_code_row_productsecond) + (dst_positive_scale_row_productsecond)) + ((dst_positive_scale_row_productsecond) + (dst_positive_scale_row_productsecond))) + (((dst_negative_code_row_productsecond) + (dst_negative_scale_row_productsecond)) * S ((dst_negative_code_row_productsecond) + (dst_negative_scale_row_productsecond)) + ((dst_negative_scale_row_productsecond) + (dst_negative_scale_row_productsecond)))) + ((((dst_negative_code_row_productsecond) + (dst_negative_scale_row_productsecond)) * S ((dst_negative_code_row_productsecond) + (dst_negative_scale_row_productsecond)) + ((dst_negative_scale_row_productsecond) + (dst_negative_scale_row_productsecond))) + (((dst_negative_code_row_productsecond) + (dst_negative_scale_row_productsecond)) * S ((dst_negative_code_row_productsecond) + (dst_negative_scale_row_productsecond)) + ((dst_negative_scale_row_productsecond) + (dst_negative_scale_row_productsecond)))))) /\ (((((exists ff_h_pvs_row_productsecondpositive. ff_h_pvs_row_productsecondpositive + S (dst_positive_row_productsecond) = S ((S (scp_column_row_product)) * dst_positive_scale_row_productsecond)) /\ exists ff_q_pvs_row_productsecondpositive. dst_positive_code_row_productsecond = ff_q_pvs_row_productsecondpositive * S ((S (scp_column_row_product)) * dst_positive_scale_row_productsecond) + (dst_positive_row_productsecond))) /\ (((((exists ff_h_pvs_row_productsecondnegative. ff_h_pvs_row_productsecondnegative + S (dst_negative_row_productsecond) = S ((S (scp_column_row_product)) * dst_negative_scale_row_productsecond)) /\ exists ff_q_pvs_row_productsecondnegative. dst_negative_code_row_productsecond = ff_q_pvs_row_productsecondnegative * S ((S (scp_column_row_product)) * dst_negative_scale_row_productsecond) + (dst_negative_row_productsecond))) /\ (exists ge_balance_positive_row_productsecondvalue ge_balance_negative_row_productsecondvalue. (((((scp_second_row_product) = 2 * (ge_balance_positive_row_productsecondvalue) /\ (ge_balance_negative_row_productsecondvalue) = 0) \/ exists ge_signed_half_row_productsecondvaluedecode. (((scp_second_row_product) = 2 * ge_signed_half_row_productsecondvaluedecode + 1 /\ (ge_balance_positive_row_productsecondvalue) = 0) /\ (ge_balance_negative_row_productsecondvalue) = S ge_signed_half_row_productsecondvaluedecode))) /\ ((dst_positive_row_productsecond) + ge_balance_negative_row_productsecondvalue = (dst_negative_row_productsecond) + ge_balance_positive_row_productsecondvalue))))))))) -> (exists dst_positive_code_row_productentry dst_positive_scale_row_productentry dst_negative_code_row_productentry dst_negative_scale_row_productentry dst_positive_row_productentry dst_negative_row_productentry. (((T) = (((((dst_positive_code_row_productentry) + (dst_positive_scale_row_productentry)) * S ((dst_positive_code_row_productentry) + (dst_positive_scale_row_productentry)) + ((dst_positive_scale_row_productentry) + (dst_positive_scale_row_productentry))) + (((dst_negative_code_row_productentry) + (dst_negative_scale_row_productentry)) * S ((dst_negative_code_row_productentry) + (dst_negative_scale_row_productentry)) + ((dst_negative_scale_row_productentry) + (dst_negative_scale_row_productentry)))) * S ((((dst_positive_code_row_productentry) + (dst_positive_scale_row_productentry)) * S ((dst_positive_code_row_productentry) + (dst_positive_scale_row_productentry)) + ((dst_positive_scale_row_productentry) + (dst_positive_scale_row_productentry))) + (((dst_negative_code_row_productentry) + (dst_negative_scale_row_productentry)) * S ((dst_negative_code_row_productentry) + (dst_negative_scale_row_productentry)) + ((dst_negative_scale_row_productentry) + (dst_negative_scale_row_productentry)))) + ((((dst_negative_code_row_productentry) + (dst_negative_scale_row_productentry)) * S ((dst_negative_code_row_productentry) + (dst_negative_scale_row_productentry)) + ((dst_negative_scale_row_productentry) + (dst_negative_scale_row_productentry))) + (((dst_negative_code_row_productentry) + (dst_negative_scale_row_productentry)) * S ((dst_negative_code_row_productentry) + (dst_negative_scale_row_productentry)) + ((dst_negative_scale_row_productentry) + (dst_negative_scale_row_productentry)))))) /\ (((((exists ff_h_pvs_row_productentrypositive. ff_h_pvs_row_productentrypositive + S (dst_positive_row_productentry) = S ((S (((n)*(scp_row_row_product)+(scp_column_row_product)))) * dst_positive_scale_row_productentry)) /\ exists ff_q_pvs_row_productentrypositive. dst_positive_code_row_productentry = ff_q_pvs_row_productentrypositive * S ((S (((n)*(scp_row_row_product)+(scp_column_row_product)))) * dst_positive_scale_row_productentry) + (dst_positive_row_productentry))) /\ (((((exists ff_h_pvs_row_productentrynegative. ff_h_pvs_row_productentrynegative + S (dst_negative_row_productentry) = S ((S (((n)*(scp_row_row_product)+(scp_column_row_product)))) * dst_negative_scale_row_productentry)) /\ exists ff_q_pvs_row_productentrynegative. dst_negative_code_row_productentry = ff_q_pvs_row_productentrynegative * S ((S (((n)*(scp_row_row_product)+(scp_column_row_product)))) * dst_negative_scale_row_productentry) + (dst_negative_row_productentry))) /\ (exists ge_balance_positive_row_productentryvalue ge_balance_negative_row_productentryvalue. (((((scp_value_row_product) = 2 * (ge_balance_positive_row_productentryvalue) /\ (ge_balance_negative_row_productentryvalue) = 0) \/ exists ge_signed_half_row_productentryvaluedecode. (((scp_value_row_product) = 2 * ge_signed_half_row_productentryvaluedecode + 1 /\ (ge_balance_positive_row_productentryvalue) = 0) /\ (ge_balance_negative_row_productentryvalue) = S ge_signed_half_row_productentryvaluedecode))) /\ ((dst_positive_row_productentry) + ge_balance_negative_row_productentryvalue = (dst_negative_row_productentry) + ge_balance_positive_row_productentryvalue))))))))) -> (exists sto_ap_row_productmultiply sto_an_row_productmultiply sto_bp_row_productmultiply sto_bn_row_productmultiply sto_cp_row_productmultiply sto_cn_row_productmultiply. (((((scp_first_row_product) = 2 * (sto_ap_row_productmultiply) /\ (sto_an_row_productmultiply) = 0) \/ exists ge_signed_half_row_productmultiplyleft. (((scp_first_row_product) = 2 * ge_signed_half_row_productmultiplyleft + 1 /\ (sto_ap_row_productmultiply) = 0) /\ (sto_an_row_productmultiply) = S ge_signed_half_row_productmultiplyleft))) /\ ((((((scp_second_row_product) = 2 * (sto_bp_row_productmultiply) /\ (sto_bn_row_productmultiply) = 0) \/ exists ge_signed_half_row_productmultiplyright. (((scp_second_row_product) = 2 * ge_signed_half_row_productmultiplyright + 1 /\ (sto_bp_row_productmultiply) = 0) /\ (sto_bn_row_productmultiply) = S ge_signed_half_row_productmultiplyright))) /\ ((((((scp_value_row_product) = 2 * (sto_cp_row_productmultiply) /\ (sto_cn_row_productmultiply) = 0) \/ exists ge_signed_half_row_productmultiplyoutput. (((scp_value_row_product) = 2 * ge_signed_half_row_productmultiplyoutput + 1 /\ (sto_cp_row_productmultiply) = 0) /\ (sto_cn_row_productmultiply) = S ge_signed_half_row_productmultiplyoutput))) /\ ((sto_ap_row_productmultiply * sto_bp_row_productmultiply + sto_an_row_productmultiply * sto_bn_row_productmultiply) + sto_cn_row_productmultiply = (sto_ap_row_productmultiply * sto_bn_row_productmultiply + sto_an_row_productmultiply * sto_bp_row_productmultiply) + sto_cp_row_productmultiply)))))))))))))) -> (exists pvs_gap_row_bound. pvs_gap_row_bound + S (i) = (m)) -> (exists dst_positive_code_row_scalar dst_positive_scale_row_scalar dst_negative_code_row_scalar dst_negative_scale_row_scalar dst_positive_row_scalar dst_negative_row_scalar. (((F) = (((((dst_positive_code_row_scalar) + (dst_positive_scale_row_scalar)) * S ((dst_positive_code_row_scalar) + (dst_positive_scale_row_scalar)) + ((dst_positive_scale_row_scalar) + (dst_positive_scale_row_scalar))) + (((dst_negative_code_row_scalar) + (dst_negative_scale_row_scalar)) * S ((dst_negative_code_row_scalar) + (dst_negative_scale_row_scalar)) + ((dst_negative_scale_row_scalar) + (dst_negative_scale_row_scalar)))) * S ((((dst_positive_code_row_scalar) + (dst_positive_scale_row_scalar)) * S ((dst_positive_code_row_scalar) + (dst_positive_scale_row_scalar)) + ((dst_positive_scale_row_scalar) + (dst_positive_scale_row_scalar))) + (((dst_negative_code_row_scalar) + (dst_negative_scale_row_scalar)) * S ((dst_negative_code_row_scalar) + (dst_negative_scale_row_scalar)) + ((dst_negative_scale_row_scalar) + (dst_negative_scale_row_scalar)))) + ((((dst_negative_code_row_scalar) + (dst_negative_scale_row_scalar)) * S ((dst_negative_code_row_scalar) + (dst_negative_scale_row_scalar)) + ((dst_negative_scale_row_scalar) + (dst_negative_scale_row_scalar))) + (((dst_negative_code_row_scalar) + (dst_negative_scale_row_scalar)) * S ((dst_negative_code_row_scalar) + (dst_negative_scale_row_scalar)) + ((dst_negative_scale_row_scalar) + (dst_negative_scale_row_scalar)))))) /\ (((((exists ff_h_pvs_row_scalarpositive. ff_h_pvs_row_scalarpositive + S (dst_positive_row_scalar) = S ((S (i)) * dst_positive_scale_row_scalar)) /\ exists ff_q_pvs_row_scalarpositive. dst_positive_code_row_scalar = ff_q_pvs_row_scalarpositive * S ((S (i)) * dst_positive_scale_row_scalar) + (dst_positive_row_scalar))) /\ (((((exists ff_h_pvs_row_scalarnegative. ff_h_pvs_row_scalarnegative + S (dst_negative_row_scalar) = S ((S (i)) * dst_negative_scale_row_scalar)) /\ exists ff_q_pvs_row_scalarnegative. dst_negative_code_row_scalar = ff_q_pvs_row_scalarnegative * S ((S (i)) * dst_negative_scale_row_scalar) + (dst_negative_row_scalar))) /\ (exists ge_balance_positive_row_scalarvalue ge_balance_negative_row_scalarvalue. (((((a) = 2 * (ge_balance_positive_row_scalarvalue) /\ (ge_balance_negative_row_scalarvalue) = 0) \/ exists ge_signed_half_row_scalarvaluedecode. (((a) = 2 * ge_signed_half_row_scalarvaluedecode + 1 /\ (ge_balance_positive_row_scalarvalue) = 0) /\ (ge_balance_negative_row_scalarvalue) = S ge_signed_half_row_scalarvaluedecode))) /\ ((dst_positive_row_scalar) + ge_balance_negative_row_scalarvalue = (dst_negative_row_scalar) + ge_balance_positive_row_scalarvalue))))))))) -> (((exists dst_positive_code_row_slicesource_table dst_positive_scale_row_slicesource_table dst_negative_code_row_slicesource_table dst_negative_scale_row_slicesource_table. (((T) = (((((dst_positive_code_row_slicesource_table) + (dst_positive_scale_row_slicesource_table)) * S ((dst_positive_code_row_slicesource_table) + (dst_positive_scale_row_slicesource_table)) + ((dst_positive_scale_row_slicesource_table) + (dst_positive_scale_row_slicesource_table))) + (((dst_negative_code_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)) * S ((dst_negative_code_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)) + ((dst_negative_scale_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)))) * S ((((dst_positive_code_row_slicesource_table) + (dst_positive_scale_row_slicesource_table)) * S ((dst_positive_code_row_slicesource_table) + (dst_positive_scale_row_slicesource_table)) + ((dst_positive_scale_row_slicesource_table) + (dst_positive_scale_row_slicesource_table))) + (((dst_negative_code_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)) * S ((dst_negative_code_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)) + ((dst_negative_scale_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)))) + ((((dst_negative_code_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)) * S ((dst_negative_code_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)) + ((dst_negative_scale_row_slicesource_table) + (dst_negative_scale_row_slicesource_table))) + (((dst_negative_code_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)) * S ((dst_negative_code_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)) + ((dst_negative_scale_row_slicesource_table) + (dst_negative_scale_row_slicesource_table)))))) /\ (forall dst_index_row_slicesource_table. (exists pvs_le_gap_row_slicesource_tabledomain. pvs_le_gap_row_slicesource_tabledomain + (dst_index_row_slicesource_table) = (0)) -> exists dst_positive_row_slicesource_table dst_negative_row_slicesource_table dst_value_row_slicesource_table. ((((exists ff_h_pvs_row_slicesource_tableentrypositive. ff_h_pvs_row_slicesource_tableentrypositive + S (dst_positive_row_slicesource_table) = S ((S (dst_index_row_slicesource_table)) * dst_positive_scale_row_slicesource_table)) /\ exists ff_q_pvs_row_slicesource_tableentrypositive. dst_positive_code_row_slicesource_table = ff_q_pvs_row_slicesource_tableentrypositive * S ((S (dst_index_row_slicesource_table)) * dst_positive_scale_row_slicesource_table) + (dst_positive_row_slicesource_table))) /\ (((((exists ff_h_pvs_row_slicesource_tableentrynegative. ff_h_pvs_row_slicesource_tableentrynegative + S (dst_negative_row_slicesource_table) = S ((S (dst_index_row_slicesource_table)) * dst_negative_scale_row_slicesource_table)) /\ exists ff_q_pvs_row_slicesource_tableentrynegative. dst_negative_code_row_slicesource_table = ff_q_pvs_row_slicesource_tableentrynegative * S ((S (dst_index_row_slicesource_table)) * dst_negative_scale_row_slicesource_table) + (dst_negative_row_slicesource_table))) /\ (exists ge_balance_positive_row_slicesource_tableentryvalue ge_balance_negative_row_slicesource_tableentryvalue. (((((dst_value_row_slicesource_table) = 2 * (ge_balance_positive_row_slicesource_tableentryvalue) /\ (ge_balance_negative_row_slicesource_tableentryvalue) = 0) \/ exists ge_signed_half_row_slicesource_tableentryvaluedecode. (((dst_value_row_slicesource_table) = 2 * ge_signed_half_row_slicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_slicesource_tableentryvalue) = 0) /\ (ge_balance_negative_row_slicesource_tableentryvalue) = S ge_signed_half_row_slicesource_tableentryvaluedecode))) /\ ((dst_positive_row_slicesource_table) + ge_balance_negative_row_slicesource_tableentryvalue = (dst_negative_row_slicesource_table) + ge_balance_positive_row_slicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_row_sliceoutput_table dst_positive_scale_row_sliceoutput_table dst_negative_code_row_sliceoutput_table dst_negative_scale_row_sliceoutput_table. (((V) = (((((dst_positive_code_row_sliceoutput_table) + (dst_positive_scale_row_sliceoutput_table)) * S ((dst_positive_code_row_sliceoutput_table) + (dst_positive_scale_row_sliceoutput_table)) + ((dst_positive_scale_row_sliceoutput_table) + (dst_positive_scale_row_sliceoutput_table))) + (((dst_negative_code_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)) * S ((dst_negative_code_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)) + ((dst_negative_scale_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)))) * S ((((dst_positive_code_row_sliceoutput_table) + (dst_positive_scale_row_sliceoutput_table)) * S ((dst_positive_code_row_sliceoutput_table) + (dst_positive_scale_row_sliceoutput_table)) + ((dst_positive_scale_row_sliceoutput_table) + (dst_positive_scale_row_sliceoutput_table))) + (((dst_negative_code_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)) * S ((dst_negative_code_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)) + ((dst_negative_scale_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)))) + ((((dst_negative_code_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)) * S ((dst_negative_code_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)) + ((dst_negative_scale_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table))) + (((dst_negative_code_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)) * S ((dst_negative_code_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)) + ((dst_negative_scale_row_sliceoutput_table) + (dst_negative_scale_row_sliceoutput_table)))))) /\ (forall dst_index_row_sliceoutput_table. (exists pvs_le_gap_row_sliceoutput_tabledomain. pvs_le_gap_row_sliceoutput_tabledomain + (dst_index_row_sliceoutput_table) = (n)) -> exists dst_positive_row_sliceoutput_table dst_negative_row_sliceoutput_table dst_value_row_sliceoutput_table. ((((exists ff_h_pvs_row_sliceoutput_tableentrypositive. ff_h_pvs_row_sliceoutput_tableentrypositive + S (dst_positive_row_sliceoutput_table) = S ((S (dst_index_row_sliceoutput_table)) * dst_positive_scale_row_sliceoutput_table)) /\ exists ff_q_pvs_row_sliceoutput_tableentrypositive. dst_positive_code_row_sliceoutput_table = ff_q_pvs_row_sliceoutput_tableentrypositive * S ((S (dst_index_row_sliceoutput_table)) * dst_positive_scale_row_sliceoutput_table) + (dst_positive_row_sliceoutput_table))) /\ (((((exists ff_h_pvs_row_sliceoutput_tableentrynegative. ff_h_pvs_row_sliceoutput_tableentrynegative + S (dst_negative_row_sliceoutput_table) = S ((S (dst_index_row_sliceoutput_table)) * dst_negative_scale_row_sliceoutput_table)) /\ exists ff_q_pvs_row_sliceoutput_tableentrynegative. dst_negative_code_row_sliceoutput_table = ff_q_pvs_row_sliceoutput_tableentrynegative * S ((S (dst_index_row_sliceoutput_table)) * dst_negative_scale_row_sliceoutput_table) + (dst_negative_row_sliceoutput_table))) /\ (exists ge_balance_positive_row_sliceoutput_tableentryvalue ge_balance_negative_row_sliceoutput_tableentryvalue. (((((dst_value_row_sliceoutput_table) = 2 * (ge_balance_positive_row_sliceoutput_tableentryvalue) /\ (ge_balance_negative_row_sliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_row_sliceoutput_tableentryvaluedecode. (((dst_value_row_sliceoutput_table) = 2 * ge_signed_half_row_sliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_sliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_row_sliceoutput_tableentryvalue) = S ge_signed_half_row_sliceoutput_tableentryvaluedecode))) /\ ((dst_positive_row_sliceoutput_table) + ge_balance_negative_row_sliceoutput_tableentryvalue = (dst_negative_row_sliceoutput_table) + ge_balance_positive_row_sliceoutput_tableentryvalue))))))))) /\ (forall srs_index_row_slice. (exists pvs_gap_row_slicebound. pvs_gap_row_slicebound + S (srs_index_row_slice) = (n)) -> exists srs_value_row_slice. (((exists dst_positive_code_row_sliceentrysource dst_positive_scale_row_sliceentrysource dst_negative_code_row_sliceentrysource dst_negative_scale_row_sliceentrysource dst_positive_row_sliceentrysource dst_negative_row_sliceentrysource. (((T) = (((((dst_positive_code_row_sliceentrysource) + (dst_positive_scale_row_sliceentrysource)) * S ((dst_positive_code_row_sliceentrysource) + (dst_positive_scale_row_sliceentrysource)) + ((dst_positive_scale_row_sliceentrysource) + (dst_positive_scale_row_sliceentrysource))) + (((dst_negative_code_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)) * S ((dst_negative_code_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)) + ((dst_negative_scale_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)))) * S ((((dst_positive_code_row_sliceentrysource) + (dst_positive_scale_row_sliceentrysource)) * S ((dst_positive_code_row_sliceentrysource) + (dst_positive_scale_row_sliceentrysource)) + ((dst_positive_scale_row_sliceentrysource) + (dst_positive_scale_row_sliceentrysource))) + (((dst_negative_code_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)) * S ((dst_negative_code_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)) + ((dst_negative_scale_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)))) + ((((dst_negative_code_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)) * S ((dst_negative_code_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)) + ((dst_negative_scale_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource))) + (((dst_negative_code_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)) * S ((dst_negative_code_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)) + ((dst_negative_scale_row_sliceentrysource) + (dst_negative_scale_row_sliceentrysource)))))) /\ (((((exists ff_h_pvs_row_sliceentrysourcepositive. ff_h_pvs_row_sliceentrysourcepositive + S (dst_positive_row_sliceentrysource) = S ((S (((((0) + ((n) * (i)))) + ((1) * (srs_index_row_slice))))) * dst_positive_scale_row_sliceentrysource)) /\ exists ff_q_pvs_row_sliceentrysourcepositive. dst_positive_code_row_sliceentrysource = ff_q_pvs_row_sliceentrysourcepositive * S ((S (((((0) + ((n) * (i)))) + ((1) * (srs_index_row_slice))))) * dst_positive_scale_row_sliceentrysource) + (dst_positive_row_sliceentrysource))) /\ (((((exists ff_h_pvs_row_sliceentrysourcenegative. ff_h_pvs_row_sliceentrysourcenegative + S (dst_negative_row_sliceentrysource) = S ((S (((((0) + ((n) * (i)))) + ((1) * (srs_index_row_slice))))) * dst_negative_scale_row_sliceentrysource)) /\ exists ff_q_pvs_row_sliceentrysourcenegative. dst_negative_code_row_sliceentrysource = ff_q_pvs_row_sliceentrysourcenegative * S ((S (((((0) + ((n) * (i)))) + ((1) * (srs_index_row_slice))))) * dst_negative_scale_row_sliceentrysource) + (dst_negative_row_sliceentrysource))) /\ (exists ge_balance_positive_row_sliceentrysourcevalue ge_balance_negative_row_sliceentrysourcevalue. (((((srs_value_row_slice) = 2 * (ge_balance_positive_row_sliceentrysourcevalue) /\ (ge_balance_negative_row_sliceentrysourcevalue) = 0) \/ exists ge_signed_half_row_sliceentrysourcevaluedecode. (((srs_value_row_slice) = 2 * ge_signed_half_row_sliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_row_sliceentrysourcevalue) = 0) /\ (ge_balance_negative_row_sliceentrysourcevalue) = S ge_signed_half_row_sliceentrysourcevaluedecode))) /\ ((dst_positive_row_sliceentrysource) + ge_balance_negative_row_sliceentrysourcevalue = (dst_negative_row_sliceentrysource) + ge_balance_positive_row_sliceentrysourcevalue))))))))) /\ (exists dst_positive_code_row_sliceentryoutput dst_positive_scale_row_sliceentryoutput dst_negative_code_row_sliceentryoutput dst_negative_scale_row_sliceentryoutput dst_positive_row_sliceentryoutput dst_negative_row_sliceentryoutput. (((V) = (((((dst_positive_code_row_sliceentryoutput) + (dst_positive_scale_row_sliceentryoutput)) * S ((dst_positive_code_row_sliceentryoutput) + (dst_positive_scale_row_sliceentryoutput)) + ((dst_positive_scale_row_sliceentryoutput) + (dst_positive_scale_row_sliceentryoutput))) + (((dst_negative_code_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)) * S ((dst_negative_code_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)) + ((dst_negative_scale_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)))) * S ((((dst_positive_code_row_sliceentryoutput) + (dst_positive_scale_row_sliceentryoutput)) * S ((dst_positive_code_row_sliceentryoutput) + (dst_positive_scale_row_sliceentryoutput)) + ((dst_positive_scale_row_sliceentryoutput) + (dst_positive_scale_row_sliceentryoutput))) + (((dst_negative_code_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)) * S ((dst_negative_code_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)) + ((dst_negative_scale_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)))) + ((((dst_negative_code_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)) * S ((dst_negative_code_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)) + ((dst_negative_scale_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput))) + (((dst_negative_code_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)) * S ((dst_negative_code_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)) + ((dst_negative_scale_row_sliceentryoutput) + (dst_negative_scale_row_sliceentryoutput)))))) /\ (((((exists ff_h_pvs_row_sliceentryoutputpositive. ff_h_pvs_row_sliceentryoutputpositive + S (dst_positive_row_sliceentryoutput) = S ((S (srs_index_row_slice)) * dst_positive_scale_row_sliceentryoutput)) /\ exists ff_q_pvs_row_sliceentryoutputpositive. dst_positive_code_row_sliceentryoutput = ff_q_pvs_row_sliceentryoutputpositive * S ((S (srs_index_row_slice)) * dst_positive_scale_row_sliceentryoutput) + (dst_positive_row_sliceentryoutput))) /\ (((((exists ff_h_pvs_row_sliceentryoutputnegative. ff_h_pvs_row_sliceentryoutputnegative + S (dst_negative_row_sliceentryoutput) = S ((S (srs_index_row_slice)) * dst_negative_scale_row_sliceentryoutput)) /\ exists ff_q_pvs_row_sliceentryoutputnegative. dst_negative_code_row_sliceentryoutput = ff_q_pvs_row_sliceentryoutputnegative * S ((S (srs_index_row_slice)) * dst_negative_scale_row_sliceentryoutput) + (dst_negative_row_sliceentryoutput))) /\ (exists ge_balance_positive_row_sliceentryoutputvalue ge_balance_negative_row_sliceentryoutputvalue. (((((srs_value_row_slice) = 2 * (ge_balance_positive_row_sliceentryoutputvalue) /\ (ge_balance_negative_row_sliceentryoutputvalue) = 0) \/ exists ge_signed_half_row_sliceentryoutputvaluedecode. (((srs_value_row_slice) = 2 * ge_signed_half_row_sliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_row_sliceentryoutputvalue) = 0) /\ (ge_balance_negative_row_sliceentryoutputvalue) = S ge_signed_half_row_sliceentryoutputvaluedecode))) /\ ((dst_positive_row_sliceentryoutput) + ge_balance_negative_row_sliceentryoutputvalue = (dst_negative_row_sliceentryoutput) + ge_balance_positive_row_sliceentryoutputvalue)))))))))))))))) -> (((exists dst_positive_code_row_resultinput_table dst_positive_scale_row_resultinput_table dst_negative_code_row_resultinput_table dst_negative_scale_row_resultinput_table. (((G) = (((((dst_positive_code_row_resultinput_table) + (dst_positive_scale_row_resultinput_table)) * S ((dst_positive_code_row_resultinput_table) + (dst_positive_scale_row_resultinput_table)) + ((dst_positive_scale_row_resultinput_table) + (dst_positive_scale_row_resultinput_table))) + (((dst_negative_code_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)) * S ((dst_negative_code_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)) + ((dst_negative_scale_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)))) * S ((((dst_positive_code_row_resultinput_table) + (dst_positive_scale_row_resultinput_table)) * S ((dst_positive_code_row_resultinput_table) + (dst_positive_scale_row_resultinput_table)) + ((dst_positive_scale_row_resultinput_table) + (dst_positive_scale_row_resultinput_table))) + (((dst_negative_code_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)) * S ((dst_negative_code_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)) + ((dst_negative_scale_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)))) + ((((dst_negative_code_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)) * S ((dst_negative_code_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)) + ((dst_negative_scale_row_resultinput_table) + (dst_negative_scale_row_resultinput_table))) + (((dst_negative_code_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)) * S ((dst_negative_code_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)) + ((dst_negative_scale_row_resultinput_table) + (dst_negative_scale_row_resultinput_table)))))) /\ (forall dst_index_row_resultinput_table. (exists pvs_le_gap_row_resultinput_tabledomain. pvs_le_gap_row_resultinput_tabledomain + (dst_index_row_resultinput_table) = (n)) -> exists dst_positive_row_resultinput_table dst_negative_row_resultinput_table dst_value_row_resultinput_table. ((((exists ff_h_pvs_row_resultinput_tableentrypositive. ff_h_pvs_row_resultinput_tableentrypositive + S (dst_positive_row_resultinput_table) = S ((S (dst_index_row_resultinput_table)) * dst_positive_scale_row_resultinput_table)) /\ exists ff_q_pvs_row_resultinput_tableentrypositive. dst_positive_code_row_resultinput_table = ff_q_pvs_row_resultinput_tableentrypositive * S ((S (dst_index_row_resultinput_table)) * dst_positive_scale_row_resultinput_table) + (dst_positive_row_resultinput_table))) /\ (((((exists ff_h_pvs_row_resultinput_tableentrynegative. ff_h_pvs_row_resultinput_tableentrynegative + S (dst_negative_row_resultinput_table) = S ((S (dst_index_row_resultinput_table)) * dst_negative_scale_row_resultinput_table)) /\ exists ff_q_pvs_row_resultinput_tableentrynegative. dst_negative_code_row_resultinput_table = ff_q_pvs_row_resultinput_tableentrynegative * S ((S (dst_index_row_resultinput_table)) * dst_negative_scale_row_resultinput_table) + (dst_negative_row_resultinput_table))) /\ (exists ge_balance_positive_row_resultinput_tableentryvalue ge_balance_negative_row_resultinput_tableentryvalue. (((((dst_value_row_resultinput_table) = 2 * (ge_balance_positive_row_resultinput_tableentryvalue) /\ (ge_balance_negative_row_resultinput_tableentryvalue) = 0) \/ exists ge_signed_half_row_resultinput_tableentryvaluedecode. (((dst_value_row_resultinput_table) = 2 * ge_signed_half_row_resultinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_resultinput_tableentryvalue) = 0) /\ (ge_balance_negative_row_resultinput_tableentryvalue) = S ge_signed_half_row_resultinput_tableentryvaluedecode))) /\ ((dst_positive_row_resultinput_table) + ge_balance_negative_row_resultinput_tableentryvalue = (dst_negative_row_resultinput_table) + ge_balance_positive_row_resultinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_row_resultoutput_table dst_positive_scale_row_resultoutput_table dst_negative_code_row_resultoutput_table dst_negative_scale_row_resultoutput_table. (((V) = (((((dst_positive_code_row_resultoutput_table) + (dst_positive_scale_row_resultoutput_table)) * S ((dst_positive_code_row_resultoutput_table) + (dst_positive_scale_row_resultoutput_table)) + ((dst_positive_scale_row_resultoutput_table) + (dst_positive_scale_row_resultoutput_table))) + (((dst_negative_code_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)) * S ((dst_negative_code_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)) + ((dst_negative_scale_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)))) * S ((((dst_positive_code_row_resultoutput_table) + (dst_positive_scale_row_resultoutput_table)) * S ((dst_positive_code_row_resultoutput_table) + (dst_positive_scale_row_resultoutput_table)) + ((dst_positive_scale_row_resultoutput_table) + (dst_positive_scale_row_resultoutput_table))) + (((dst_negative_code_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)) * S ((dst_negative_code_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)) + ((dst_negative_scale_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)))) + ((((dst_negative_code_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)) * S ((dst_negative_code_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)) + ((dst_negative_scale_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table))) + (((dst_negative_code_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)) * S ((dst_negative_code_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)) + ((dst_negative_scale_row_resultoutput_table) + (dst_negative_scale_row_resultoutput_table)))))) /\ (forall dst_index_row_resultoutput_table. (exists pvs_le_gap_row_resultoutput_tabledomain. pvs_le_gap_row_resultoutput_tabledomain + (dst_index_row_resultoutput_table) = (n)) -> exists dst_positive_row_resultoutput_table dst_negative_row_resultoutput_table dst_value_row_resultoutput_table. ((((exists ff_h_pvs_row_resultoutput_tableentrypositive. ff_h_pvs_row_resultoutput_tableentrypositive + S (dst_positive_row_resultoutput_table) = S ((S (dst_index_row_resultoutput_table)) * dst_positive_scale_row_resultoutput_table)) /\ exists ff_q_pvs_row_resultoutput_tableentrypositive. dst_positive_code_row_resultoutput_table = ff_q_pvs_row_resultoutput_tableentrypositive * S ((S (dst_index_row_resultoutput_table)) * dst_positive_scale_row_resultoutput_table) + (dst_positive_row_resultoutput_table))) /\ (((((exists ff_h_pvs_row_resultoutput_tableentrynegative. ff_h_pvs_row_resultoutput_tableentrynegative + S (dst_negative_row_resultoutput_table) = S ((S (dst_index_row_resultoutput_table)) * dst_negative_scale_row_resultoutput_table)) /\ exists ff_q_pvs_row_resultoutput_tableentrynegative. dst_negative_code_row_resultoutput_table = ff_q_pvs_row_resultoutput_tableentrynegative * S ((S (dst_index_row_resultoutput_table)) * dst_negative_scale_row_resultoutput_table) + (dst_negative_row_resultoutput_table))) /\ (exists ge_balance_positive_row_resultoutput_tableentryvalue ge_balance_negative_row_resultoutput_tableentryvalue. (((((dst_value_row_resultoutput_table) = 2 * (ge_balance_positive_row_resultoutput_tableentryvalue) /\ (ge_balance_negative_row_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_row_resultoutput_tableentryvaluedecode. (((dst_value_row_resultoutput_table) = 2 * ge_signed_half_row_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_row_resultoutput_tableentryvalue) = S ge_signed_half_row_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_row_resultoutput_table) + ge_balance_negative_row_resultoutput_tableentryvalue = (dst_negative_row_resultoutput_table) + ge_balance_positive_row_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_row_resultentries. (exists pvs_gap_row_resultentriesbound. pvs_gap_row_resultentriesbound + S (sto_index_row_resultentries) = (n)) -> exists sto_input_row_resultentries sto_output_row_resultentries. ((exists dst_positive_code_row_resultentriesentryinput dst_positive_scale_row_resultentriesentryinput dst_negative_code_row_resultentriesentryinput dst_negative_scale_row_resultentriesentryinput dst_positive_row_resultentriesentryinput dst_negative_row_resultentriesentryinput. (((G) = (((((dst_positive_code_row_resultentriesentryinput) + (dst_positive_scale_row_resultentriesentryinput)) * S ((dst_positive_code_row_resultentriesentryinput) + (dst_positive_scale_row_resultentriesentryinput)) + ((dst_positive_scale_row_resultentriesentryinput) + (dst_positive_scale_row_resultentriesentryinput))) + (((dst_negative_code_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)) * S ((dst_negative_code_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)) + ((dst_negative_scale_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)))) * S ((((dst_positive_code_row_resultentriesentryinput) + (dst_positive_scale_row_resultentriesentryinput)) * S ((dst_positive_code_row_resultentriesentryinput) + (dst_positive_scale_row_resultentriesentryinput)) + ((dst_positive_scale_row_resultentriesentryinput) + (dst_positive_scale_row_resultentriesentryinput))) + (((dst_negative_code_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)) * S ((dst_negative_code_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)) + ((dst_negative_scale_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)))) + ((((dst_negative_code_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)) * S ((dst_negative_code_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)) + ((dst_negative_scale_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput))) + (((dst_negative_code_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)) * S ((dst_negative_code_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)) + ((dst_negative_scale_row_resultentriesentryinput) + (dst_negative_scale_row_resultentriesentryinput)))))) /\ (((((exists ff_h_pvs_row_resultentriesentryinputpositive. ff_h_pvs_row_resultentriesentryinputpositive + S (dst_positive_row_resultentriesentryinput) = S ((S (sto_index_row_resultentries)) * dst_positive_scale_row_resultentriesentryinput)) /\ exists ff_q_pvs_row_resultentriesentryinputpositive. dst_positive_code_row_resultentriesentryinput = ff_q_pvs_row_resultentriesentryinputpositive * S ((S (sto_index_row_resultentries)) * dst_positive_scale_row_resultentriesentryinput) + (dst_positive_row_resultentriesentryinput))) /\ (((((exists ff_h_pvs_row_resultentriesentryinputnegative. ff_h_pvs_row_resultentriesentryinputnegative + S (dst_negative_row_resultentriesentryinput) = S ((S (sto_index_row_resultentries)) * dst_negative_scale_row_resultentriesentryinput)) /\ exists ff_q_pvs_row_resultentriesentryinputnegative. dst_negative_code_row_resultentriesentryinput = ff_q_pvs_row_resultentriesentryinputnegative * S ((S (sto_index_row_resultentries)) * dst_negative_scale_row_resultentriesentryinput) + (dst_negative_row_resultentriesentryinput))) /\ (exists ge_balance_positive_row_resultentriesentryinputvalue ge_balance_negative_row_resultentriesentryinputvalue. (((((sto_input_row_resultentries) = 2 * (ge_balance_positive_row_resultentriesentryinputvalue) /\ (ge_balance_negative_row_resultentriesentryinputvalue) = 0) \/ exists ge_signed_half_row_resultentriesentryinputvaluedecode. (((sto_input_row_resultentries) = 2 * ge_signed_half_row_resultentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_row_resultentriesentryinputvalue) = 0) /\ (ge_balance_negative_row_resultentriesentryinputvalue) = S ge_signed_half_row_resultentriesentryinputvaluedecode))) /\ ((dst_positive_row_resultentriesentryinput) + ge_balance_negative_row_resultentriesentryinputvalue = (dst_negative_row_resultentriesentryinput) + ge_balance_positive_row_resultentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_row_resultentriesentryoutput dst_positive_scale_row_resultentriesentryoutput dst_negative_code_row_resultentriesentryoutput dst_negative_scale_row_resultentriesentryoutput dst_positive_row_resultentriesentryoutput dst_negative_row_resultentriesentryoutput. (((V) = (((((dst_positive_code_row_resultentriesentryoutput) + (dst_positive_scale_row_resultentriesentryoutput)) * S ((dst_positive_code_row_resultentriesentryoutput) + (dst_positive_scale_row_resultentriesentryoutput)) + ((dst_positive_scale_row_resultentriesentryoutput) + (dst_positive_scale_row_resultentriesentryoutput))) + (((dst_negative_code_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)) * S ((dst_negative_code_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)) + ((dst_negative_scale_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)))) * S ((((dst_positive_code_row_resultentriesentryoutput) + (dst_positive_scale_row_resultentriesentryoutput)) * S ((dst_positive_code_row_resultentriesentryoutput) + (dst_positive_scale_row_resultentriesentryoutput)) + ((dst_positive_scale_row_resultentriesentryoutput) + (dst_positive_scale_row_resultentriesentryoutput))) + (((dst_negative_code_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)) * S ((dst_negative_code_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)) + ((dst_negative_scale_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)))) + ((((dst_negative_code_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)) * S ((dst_negative_code_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)) + ((dst_negative_scale_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput))) + (((dst_negative_code_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)) * S ((dst_negative_code_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)) + ((dst_negative_scale_row_resultentriesentryoutput) + (dst_negative_scale_row_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_row_resultentriesentryoutputpositive. ff_h_pvs_row_resultentriesentryoutputpositive + S (dst_positive_row_resultentriesentryoutput) = S ((S (sto_index_row_resultentries)) * dst_positive_scale_row_resultentriesentryoutput)) /\ exists ff_q_pvs_row_resultentriesentryoutputpositive. dst_positive_code_row_resultentriesentryoutput = ff_q_pvs_row_resultentriesentryoutputpositive * S ((S (sto_index_row_resultentries)) * dst_positive_scale_row_resultentriesentryoutput) + (dst_positive_row_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_row_resultentriesentryoutputnegative. ff_h_pvs_row_resultentriesentryoutputnegative + S (dst_negative_row_resultentriesentryoutput) = S ((S (sto_index_row_resultentries)) * dst_negative_scale_row_resultentriesentryoutput)) /\ exists ff_q_pvs_row_resultentriesentryoutputnegative. dst_negative_code_row_resultentriesentryoutput = ff_q_pvs_row_resultentriesentryoutputnegative * S ((S (sto_index_row_resultentries)) * dst_negative_scale_row_resultentriesentryoutput) + (dst_negative_row_resultentriesentryoutput))) /\ (exists ge_balance_positive_row_resultentriesentryoutputvalue ge_balance_negative_row_resultentriesentryoutputvalue. (((((sto_output_row_resultentries) = 2 * (ge_balance_positive_row_resultentriesentryoutputvalue) /\ (ge_balance_negative_row_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_row_resultentriesentryoutputvaluedecode. (((sto_output_row_resultentries) = 2 * ge_signed_half_row_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_row_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_row_resultentriesentryoutputvalue) = S ge_signed_half_row_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_row_resultentriesentryoutput) + ge_balance_negative_row_resultentriesentryoutputvalue = (dst_negative_row_resultentriesentryoutput) + ge_balance_positive_row_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_row_resultentriesentryoperation sto_an_row_resultentriesentryoperation sto_bp_row_resultentriesentryoperation sto_bn_row_resultentriesentryoperation sto_cp_row_resultentriesentryoperation sto_cn_row_resultentriesentryoperation. (((((a) = 2 * (sto_ap_row_resultentriesentryoperation) /\ (sto_an_row_resultentriesentryoperation) = 0) \/ exists ge_signed_half_row_resultentriesentryoperationleft. (((a) = 2 * ge_signed_half_row_resultentriesentryoperationleft + 1 /\ (sto_ap_row_resultentriesentryoperation) = 0) /\ (sto_an_row_resultentriesentryoperation) = S ge_signed_half_row_resultentriesentryoperationleft))) /\ ((((((sto_input_row_resultentries) = 2 * (sto_bp_row_resultentriesentryoperation) /\ (sto_bn_row_resultentriesentryoperation) = 0) \/ exists ge_signed_half_row_resultentriesentryoperationright. (((sto_input_row_resultentries) = 2 * ge_signed_half_row_resultentriesentryoperationright + 1 /\ (sto_bp_row_resultentriesentryoperation) = 0) /\ (sto_bn_row_resultentriesentryoperation) = S ge_signed_half_row_resultentriesentryoperationright))) /\ ((((((sto_output_row_resultentries) = 2 * (sto_cp_row_resultentriesentryoperation) /\ (sto_cn_row_resultentriesentryoperation) = 0) \/ exists ge_signed_half_row_resultentriesentryoperationoutput. (((sto_output_row_resultentries) = 2 * ge_signed_half_row_resultentriesentryoperationoutput + 1 /\ (sto_cp_row_resultentriesentryoperation) = 0) /\ (sto_cn_row_resultentriesentryoperation) = S ge_signed_half_row_resultentriesentryoperationoutput))) /\ ((sto_ap_row_resultentriesentryoperation * sto_bp_row_resultentriesentryoperation + sto_an_row_resultentriesentryoperation * sto_bn_row_resultentriesentryoperation) + sto_cn_row_resultentriesentryoperation = (sto_ap_row_resultentriesentryoperation * sto_bn_row_resultentriesentryoperation + sto_an_row_resultentriesentryoperation * sto_bp_row_resultentriesentryoperation) + sto_cp_row_resultentriesentryoperation)))))))))))))))