signed_cartesian_product_flat_lookup

Exact expanded first-order arithmetic statement

forall F G T m n k z. (((exists dst_positive_code_lookup_productF dst_positive_scale_lookup_productF dst_negative_code_lookup_productF dst_negative_scale_lookup_productF. (((F) = (((((dst_positive_code_lookup_productF) + (dst_positive_scale_lookup_productF)) * S ((dst_positive_code_lookup_productF) + (dst_positive_scale_lookup_productF)) + ((dst_positive_scale_lookup_productF) + (dst_positive_scale_lookup_productF))) + (((dst_negative_code_lookup_productF) + (dst_negative_scale_lookup_productF)) * S ((dst_negative_code_lookup_productF) + (dst_negative_scale_lookup_productF)) + ((dst_negative_scale_lookup_productF) + (dst_negative_scale_lookup_productF)))) * S ((((dst_positive_code_lookup_productF) + (dst_positive_scale_lookup_productF)) * S ((dst_positive_code_lookup_productF) + (dst_positive_scale_lookup_productF)) + ((dst_positive_scale_lookup_productF) + (dst_positive_scale_lookup_productF))) + (((dst_negative_code_lookup_productF) + (dst_negative_scale_lookup_productF)) * S ((dst_negative_code_lookup_productF) + (dst_negative_scale_lookup_productF)) + ((dst_negative_scale_lookup_productF) + (dst_negative_scale_lookup_productF)))) + ((((dst_negative_code_lookup_productF) + (dst_negative_scale_lookup_productF)) * S ((dst_negative_code_lookup_productF) + (dst_negative_scale_lookup_productF)) + ((dst_negative_scale_lookup_productF) + (dst_negative_scale_lookup_productF))) + (((dst_negative_code_lookup_productF) + (dst_negative_scale_lookup_productF)) * S ((dst_negative_code_lookup_productF) + (dst_negative_scale_lookup_productF)) + ((dst_negative_scale_lookup_productF) + (dst_negative_scale_lookup_productF)))))) /\ (forall dst_index_lookup_productF. (exists pvs_le_gap_lookup_productFdomain. pvs_le_gap_lookup_productFdomain + (dst_index_lookup_productF) = (0)) -> exists dst_positive_lookup_productF dst_negative_lookup_productF dst_value_lookup_productF. ((((exists ff_h_pvs_lookup_productFentrypositive. ff_h_pvs_lookup_productFentrypositive + S (dst_positive_lookup_productF) = S ((S (dst_index_lookup_productF)) * dst_positive_scale_lookup_productF)) /\ exists ff_q_pvs_lookup_productFentrypositive. dst_positive_code_lookup_productF = ff_q_pvs_lookup_productFentrypositive * S ((S (dst_index_lookup_productF)) * dst_positive_scale_lookup_productF) + (dst_positive_lookup_productF))) /\ (((((exists ff_h_pvs_lookup_productFentrynegative. ff_h_pvs_lookup_productFentrynegative + S (dst_negative_lookup_productF) = S ((S (dst_index_lookup_productF)) * dst_negative_scale_lookup_productF)) /\ exists ff_q_pvs_lookup_productFentrynegative. dst_negative_code_lookup_productF = ff_q_pvs_lookup_productFentrynegative * S ((S (dst_index_lookup_productF)) * dst_negative_scale_lookup_productF) + (dst_negative_lookup_productF))) /\ (exists ge_balance_positive_lookup_productFentryvalue ge_balance_negative_lookup_productFentryvalue. (((((dst_value_lookup_productF) = 2 * (ge_balance_positive_lookup_productFentryvalue) /\ (ge_balance_negative_lookup_productFentryvalue) = 0) \/ exists ge_signed_half_lookup_productFentryvaluedecode. (((dst_value_lookup_productF) = 2 * ge_signed_half_lookup_productFentryvaluedecode + 1 /\ (ge_balance_positive_lookup_productFentryvalue) = 0) /\ (ge_balance_negative_lookup_productFentryvalue) = S ge_signed_half_lookup_productFentryvaluedecode))) /\ ((dst_positive_lookup_productF) + ge_balance_negative_lookup_productFentryvalue = (dst_negative_lookup_productF) + ge_balance_positive_lookup_productFentryvalue))))))))) /\ (((exists dst_positive_code_lookup_productG dst_positive_scale_lookup_productG dst_negative_code_lookup_productG dst_negative_scale_lookup_productG. (((G) = (((((dst_positive_code_lookup_productG) + (dst_positive_scale_lookup_productG)) * S ((dst_positive_code_lookup_productG) + (dst_positive_scale_lookup_productG)) + ((dst_positive_scale_lookup_productG) + (dst_positive_scale_lookup_productG))) + (((dst_negative_code_lookup_productG) + (dst_negative_scale_lookup_productG)) * S ((dst_negative_code_lookup_productG) + (dst_negative_scale_lookup_productG)) + ((dst_negative_scale_lookup_productG) + (dst_negative_scale_lookup_productG)))) * S ((((dst_positive_code_lookup_productG) + (dst_positive_scale_lookup_productG)) * S ((dst_positive_code_lookup_productG) + (dst_positive_scale_lookup_productG)) + ((dst_positive_scale_lookup_productG) + (dst_positive_scale_lookup_productG))) + (((dst_negative_code_lookup_productG) + (dst_negative_scale_lookup_productG)) * S ((dst_negative_code_lookup_productG) + (dst_negative_scale_lookup_productG)) + ((dst_negative_scale_lookup_productG) + (dst_negative_scale_lookup_productG)))) + ((((dst_negative_code_lookup_productG) + (dst_negative_scale_lookup_productG)) * S ((dst_negative_code_lookup_productG) + (dst_negative_scale_lookup_productG)) + ((dst_negative_scale_lookup_productG) + (dst_negative_scale_lookup_productG))) + (((dst_negative_code_lookup_productG) + (dst_negative_scale_lookup_productG)) * S ((dst_negative_code_lookup_productG) + (dst_negative_scale_lookup_productG)) + ((dst_negative_scale_lookup_productG) + (dst_negative_scale_lookup_productG)))))) /\ (forall dst_index_lookup_productG. (exists pvs_le_gap_lookup_productGdomain. pvs_le_gap_lookup_productGdomain + (dst_index_lookup_productG) = (0)) -> exists dst_positive_lookup_productG dst_negative_lookup_productG dst_value_lookup_productG. ((((exists ff_h_pvs_lookup_productGentrypositive. ff_h_pvs_lookup_productGentrypositive + S (dst_positive_lookup_productG) = S ((S (dst_index_lookup_productG)) * dst_positive_scale_lookup_productG)) /\ exists ff_q_pvs_lookup_productGentrypositive. dst_positive_code_lookup_productG = ff_q_pvs_lookup_productGentrypositive * S ((S (dst_index_lookup_productG)) * dst_positive_scale_lookup_productG) + (dst_positive_lookup_productG))) /\ (((((exists ff_h_pvs_lookup_productGentrynegative. ff_h_pvs_lookup_productGentrynegative + S (dst_negative_lookup_productG) = S ((S (dst_index_lookup_productG)) * dst_negative_scale_lookup_productG)) /\ exists ff_q_pvs_lookup_productGentrynegative. dst_negative_code_lookup_productG = ff_q_pvs_lookup_productGentrynegative * S ((S (dst_index_lookup_productG)) * dst_negative_scale_lookup_productG) + (dst_negative_lookup_productG))) /\ (exists ge_balance_positive_lookup_productGentryvalue ge_balance_negative_lookup_productGentryvalue. (((((dst_value_lookup_productG) = 2 * (ge_balance_positive_lookup_productGentryvalue) /\ (ge_balance_negative_lookup_productGentryvalue) = 0) \/ exists ge_signed_half_lookup_productGentryvaluedecode. (((dst_value_lookup_productG) = 2 * ge_signed_half_lookup_productGentryvaluedecode + 1 /\ (ge_balance_positive_lookup_productGentryvalue) = 0) /\ (ge_balance_negative_lookup_productGentryvalue) = S ge_signed_half_lookup_productGentryvaluedecode))) /\ ((dst_positive_lookup_productG) + ge_balance_negative_lookup_productGentryvalue = (dst_negative_lookup_productG) + ge_balance_positive_lookup_productGentryvalue))))))))) /\ (((exists dst_positive_code_lookup_productT dst_positive_scale_lookup_productT dst_negative_code_lookup_productT dst_negative_scale_lookup_productT. (((T) = (((((dst_positive_code_lookup_productT) + (dst_positive_scale_lookup_productT)) * S ((dst_positive_code_lookup_productT) + (dst_positive_scale_lookup_productT)) + ((dst_positive_scale_lookup_productT) + (dst_positive_scale_lookup_productT))) + (((dst_negative_code_lookup_productT) + (dst_negative_scale_lookup_productT)) * S ((dst_negative_code_lookup_productT) + (dst_negative_scale_lookup_productT)) + ((dst_negative_scale_lookup_productT) + (dst_negative_scale_lookup_productT)))) * S ((((dst_positive_code_lookup_productT) + (dst_positive_scale_lookup_productT)) * S ((dst_positive_code_lookup_productT) + (dst_positive_scale_lookup_productT)) + ((dst_positive_scale_lookup_productT) + (dst_positive_scale_lookup_productT))) + (((dst_negative_code_lookup_productT) + (dst_negative_scale_lookup_productT)) * S ((dst_negative_code_lookup_productT) + (dst_negative_scale_lookup_productT)) + ((dst_negative_scale_lookup_productT) + (dst_negative_scale_lookup_productT)))) + ((((dst_negative_code_lookup_productT) + (dst_negative_scale_lookup_productT)) * S ((dst_negative_code_lookup_productT) + (dst_negative_scale_lookup_productT)) + ((dst_negative_scale_lookup_productT) + (dst_negative_scale_lookup_productT))) + (((dst_negative_code_lookup_productT) + (dst_negative_scale_lookup_productT)) * S ((dst_negative_code_lookup_productT) + (dst_negative_scale_lookup_productT)) + ((dst_negative_scale_lookup_productT) + (dst_negative_scale_lookup_productT)))))) /\ (forall dst_index_lookup_productT. (exists pvs_le_gap_lookup_productTdomain. pvs_le_gap_lookup_productTdomain + (dst_index_lookup_productT) = ((m)*(n))) -> exists dst_positive_lookup_productT dst_negative_lookup_productT dst_value_lookup_productT. ((((exists ff_h_pvs_lookup_productTentrypositive. ff_h_pvs_lookup_productTentrypositive + S (dst_positive_lookup_productT) = S ((S (dst_index_lookup_productT)) * dst_positive_scale_lookup_productT)) /\ exists ff_q_pvs_lookup_productTentrypositive. dst_positive_code_lookup_productT = ff_q_pvs_lookup_productTentrypositive * S ((S (dst_index_lookup_productT)) * dst_positive_scale_lookup_productT) + (dst_positive_lookup_productT))) /\ (((((exists ff_h_pvs_lookup_productTentrynegative. ff_h_pvs_lookup_productTentrynegative + S (dst_negative_lookup_productT) = S ((S (dst_index_lookup_productT)) * dst_negative_scale_lookup_productT)) /\ exists ff_q_pvs_lookup_productTentrynegative. dst_negative_code_lookup_productT = ff_q_pvs_lookup_productTentrynegative * S ((S (dst_index_lookup_productT)) * dst_negative_scale_lookup_productT) + (dst_negative_lookup_productT))) /\ (exists ge_balance_positive_lookup_productTentryvalue ge_balance_negative_lookup_productTentryvalue. (((((dst_value_lookup_productT) = 2 * (ge_balance_positive_lookup_productTentryvalue) /\ (ge_balance_negative_lookup_productTentryvalue) = 0) \/ exists ge_signed_half_lookup_productTentryvaluedecode. (((dst_value_lookup_productT) = 2 * ge_signed_half_lookup_productTentryvaluedecode + 1 /\ (ge_balance_positive_lookup_productTentryvalue) = 0) /\ (ge_balance_negative_lookup_productTentryvalue) = S ge_signed_half_lookup_productTentryvaluedecode))) /\ ((dst_positive_lookup_productT) + ge_balance_negative_lookup_productTentryvalue = (dst_negative_lookup_productT) + ge_balance_positive_lookup_productTentryvalue))))))))) /\ (forall scp_row_lookup_product scp_column_lookup_product scp_first_lookup_product scp_second_lookup_product scp_value_lookup_product. (exists pvs_gap_lookup_productrows. pvs_gap_lookup_productrows + S (scp_row_lookup_product) = (m)) -> (exists pvs_gap_lookup_productcolumns. pvs_gap_lookup_productcolumns + S (scp_column_lookup_product) = (n)) -> (exists dst_positive_code_lookup_productfirst dst_positive_scale_lookup_productfirst dst_negative_code_lookup_productfirst dst_negative_scale_lookup_productfirst dst_positive_lookup_productfirst dst_negative_lookup_productfirst. (((F) = (((((dst_positive_code_lookup_productfirst) + (dst_positive_scale_lookup_productfirst)) * S ((dst_positive_code_lookup_productfirst) + (dst_positive_scale_lookup_productfirst)) + ((dst_positive_scale_lookup_productfirst) + (dst_positive_scale_lookup_productfirst))) + (((dst_negative_code_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)) * S ((dst_negative_code_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)) + ((dst_negative_scale_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)))) * S ((((dst_positive_code_lookup_productfirst) + (dst_positive_scale_lookup_productfirst)) * S ((dst_positive_code_lookup_productfirst) + (dst_positive_scale_lookup_productfirst)) + ((dst_positive_scale_lookup_productfirst) + (dst_positive_scale_lookup_productfirst))) + (((dst_negative_code_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)) * S ((dst_negative_code_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)) + ((dst_negative_scale_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)))) + ((((dst_negative_code_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)) * S ((dst_negative_code_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)) + ((dst_negative_scale_lookup_productfirst) + (dst_negative_scale_lookup_productfirst))) + (((dst_negative_code_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)) * S ((dst_negative_code_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)) + ((dst_negative_scale_lookup_productfirst) + (dst_negative_scale_lookup_productfirst)))))) /\ (((((exists ff_h_pvs_lookup_productfirstpositive. ff_h_pvs_lookup_productfirstpositive + S (dst_positive_lookup_productfirst) = S ((S (scp_row_lookup_product)) * dst_positive_scale_lookup_productfirst)) /\ exists ff_q_pvs_lookup_productfirstpositive. dst_positive_code_lookup_productfirst = ff_q_pvs_lookup_productfirstpositive * S ((S (scp_row_lookup_product)) * dst_positive_scale_lookup_productfirst) + (dst_positive_lookup_productfirst))) /\ (((((exists ff_h_pvs_lookup_productfirstnegative. ff_h_pvs_lookup_productfirstnegative + S (dst_negative_lookup_productfirst) = S ((S (scp_row_lookup_product)) * dst_negative_scale_lookup_productfirst)) /\ exists ff_q_pvs_lookup_productfirstnegative. dst_negative_code_lookup_productfirst = ff_q_pvs_lookup_productfirstnegative * S ((S (scp_row_lookup_product)) * dst_negative_scale_lookup_productfirst) + (dst_negative_lookup_productfirst))) /\ (exists ge_balance_positive_lookup_productfirstvalue ge_balance_negative_lookup_productfirstvalue. (((((scp_first_lookup_product) = 2 * (ge_balance_positive_lookup_productfirstvalue) /\ (ge_balance_negative_lookup_productfirstvalue) = 0) \/ exists ge_signed_half_lookup_productfirstvaluedecode. (((scp_first_lookup_product) = 2 * ge_signed_half_lookup_productfirstvaluedecode + 1 /\ (ge_balance_positive_lookup_productfirstvalue) = 0) /\ (ge_balance_negative_lookup_productfirstvalue) = S ge_signed_half_lookup_productfirstvaluedecode))) /\ ((dst_positive_lookup_productfirst) + ge_balance_negative_lookup_productfirstvalue = (dst_negative_lookup_productfirst) + ge_balance_positive_lookup_productfirstvalue))))))))) -> (exists dst_positive_code_lookup_productsecond dst_positive_scale_lookup_productsecond dst_negative_code_lookup_productsecond dst_negative_scale_lookup_productsecond dst_positive_lookup_productsecond dst_negative_lookup_productsecond. (((G) = (((((dst_positive_code_lookup_productsecond) + (dst_positive_scale_lookup_productsecond)) * S ((dst_positive_code_lookup_productsecond) + (dst_positive_scale_lookup_productsecond)) + ((dst_positive_scale_lookup_productsecond) + (dst_positive_scale_lookup_productsecond))) + (((dst_negative_code_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)) * S ((dst_negative_code_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)) + ((dst_negative_scale_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)))) * S ((((dst_positive_code_lookup_productsecond) + (dst_positive_scale_lookup_productsecond)) * S ((dst_positive_code_lookup_productsecond) + (dst_positive_scale_lookup_productsecond)) + ((dst_positive_scale_lookup_productsecond) + (dst_positive_scale_lookup_productsecond))) + (((dst_negative_code_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)) * S ((dst_negative_code_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)) + ((dst_negative_scale_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)))) + ((((dst_negative_code_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)) * S ((dst_negative_code_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)) + ((dst_negative_scale_lookup_productsecond) + (dst_negative_scale_lookup_productsecond))) + (((dst_negative_code_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)) * S ((dst_negative_code_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)) + ((dst_negative_scale_lookup_productsecond) + (dst_negative_scale_lookup_productsecond)))))) /\ (((((exists ff_h_pvs_lookup_productsecondpositive. ff_h_pvs_lookup_productsecondpositive + S (dst_positive_lookup_productsecond) = S ((S (scp_column_lookup_product)) * dst_positive_scale_lookup_productsecond)) /\ exists ff_q_pvs_lookup_productsecondpositive. dst_positive_code_lookup_productsecond = ff_q_pvs_lookup_productsecondpositive * S ((S (scp_column_lookup_product)) * dst_positive_scale_lookup_productsecond) + (dst_positive_lookup_productsecond))) /\ (((((exists ff_h_pvs_lookup_productsecondnegative. ff_h_pvs_lookup_productsecondnegative + S (dst_negative_lookup_productsecond) = S ((S (scp_column_lookup_product)) * dst_negative_scale_lookup_productsecond)) /\ exists ff_q_pvs_lookup_productsecondnegative. dst_negative_code_lookup_productsecond = ff_q_pvs_lookup_productsecondnegative * S ((S (scp_column_lookup_product)) * dst_negative_scale_lookup_productsecond) + (dst_negative_lookup_productsecond))) /\ (exists ge_balance_positive_lookup_productsecondvalue ge_balance_negative_lookup_productsecondvalue. (((((scp_second_lookup_product) = 2 * (ge_balance_positive_lookup_productsecondvalue) /\ (ge_balance_negative_lookup_productsecondvalue) = 0) \/ exists ge_signed_half_lookup_productsecondvaluedecode. (((scp_second_lookup_product) = 2 * ge_signed_half_lookup_productsecondvaluedecode + 1 /\ (ge_balance_positive_lookup_productsecondvalue) = 0) /\ (ge_balance_negative_lookup_productsecondvalue) = S ge_signed_half_lookup_productsecondvaluedecode))) /\ ((dst_positive_lookup_productsecond) + ge_balance_negative_lookup_productsecondvalue = (dst_negative_lookup_productsecond) + ge_balance_positive_lookup_productsecondvalue))))))))) -> (exists dst_positive_code_lookup_productentry dst_positive_scale_lookup_productentry dst_negative_code_lookup_productentry dst_negative_scale_lookup_productentry dst_positive_lookup_productentry dst_negative_lookup_productentry. (((T) = (((((dst_positive_code_lookup_productentry) + (dst_positive_scale_lookup_productentry)) * S ((dst_positive_code_lookup_productentry) + (dst_positive_scale_lookup_productentry)) + ((dst_positive_scale_lookup_productentry) + (dst_positive_scale_lookup_productentry))) + (((dst_negative_code_lookup_productentry) + (dst_negative_scale_lookup_productentry)) * S ((dst_negative_code_lookup_productentry) + (dst_negative_scale_lookup_productentry)) + ((dst_negative_scale_lookup_productentry) + (dst_negative_scale_lookup_productentry)))) * S ((((dst_positive_code_lookup_productentry) + (dst_positive_scale_lookup_productentry)) * S ((dst_positive_code_lookup_productentry) + (dst_positive_scale_lookup_productentry)) + ((dst_positive_scale_lookup_productentry) + (dst_positive_scale_lookup_productentry))) + (((dst_negative_code_lookup_productentry) + (dst_negative_scale_lookup_productentry)) * S ((dst_negative_code_lookup_productentry) + (dst_negative_scale_lookup_productentry)) + ((dst_negative_scale_lookup_productentry) + (dst_negative_scale_lookup_productentry)))) + ((((dst_negative_code_lookup_productentry) + (dst_negative_scale_lookup_productentry)) * S ((dst_negative_code_lookup_productentry) + (dst_negative_scale_lookup_productentry)) + ((dst_negative_scale_lookup_productentry) + (dst_negative_scale_lookup_productentry))) + (((dst_negative_code_lookup_productentry) + (dst_negative_scale_lookup_productentry)) * S ((dst_negative_code_lookup_productentry) + (dst_negative_scale_lookup_productentry)) + ((dst_negative_scale_lookup_productentry) + (dst_negative_scale_lookup_productentry)))))) /\ (((((exists ff_h_pvs_lookup_productentrypositive. ff_h_pvs_lookup_productentrypositive + S (dst_positive_lookup_productentry) = S ((S (((n)*(scp_row_lookup_product)+(scp_column_lookup_product)))) * dst_positive_scale_lookup_productentry)) /\ exists ff_q_pvs_lookup_productentrypositive. dst_positive_code_lookup_productentry = ff_q_pvs_lookup_productentrypositive * S ((S (((n)*(scp_row_lookup_product)+(scp_column_lookup_product)))) * dst_positive_scale_lookup_productentry) + (dst_positive_lookup_productentry))) /\ (((((exists ff_h_pvs_lookup_productentrynegative. ff_h_pvs_lookup_productentrynegative + S (dst_negative_lookup_productentry) = S ((S (((n)*(scp_row_lookup_product)+(scp_column_lookup_product)))) * dst_negative_scale_lookup_productentry)) /\ exists ff_q_pvs_lookup_productentrynegative. dst_negative_code_lookup_productentry = ff_q_pvs_lookup_productentrynegative * S ((S (((n)*(scp_row_lookup_product)+(scp_column_lookup_product)))) * dst_negative_scale_lookup_productentry) + (dst_negative_lookup_productentry))) /\ (exists ge_balance_positive_lookup_productentryvalue ge_balance_negative_lookup_productentryvalue. (((((scp_value_lookup_product) = 2 * (ge_balance_positive_lookup_productentryvalue) /\ (ge_balance_negative_lookup_productentryvalue) = 0) \/ exists ge_signed_half_lookup_productentryvaluedecode. (((scp_value_lookup_product) = 2 * ge_signed_half_lookup_productentryvaluedecode + 1 /\ (ge_balance_positive_lookup_productentryvalue) = 0) /\ (ge_balance_negative_lookup_productentryvalue) = S ge_signed_half_lookup_productentryvaluedecode))) /\ ((dst_positive_lookup_productentry) + ge_balance_negative_lookup_productentryvalue = (dst_negative_lookup_productentry) + ge_balance_positive_lookup_productentryvalue))))))))) -> (exists sto_ap_lookup_productmultiply sto_an_lookup_productmultiply sto_bp_lookup_productmultiply sto_bn_lookup_productmultiply sto_cp_lookup_productmultiply sto_cn_lookup_productmultiply. (((((scp_first_lookup_product) = 2 * (sto_ap_lookup_productmultiply) /\ (sto_an_lookup_productmultiply) = 0) \/ exists ge_signed_half_lookup_productmultiplyleft. (((scp_first_lookup_product) = 2 * ge_signed_half_lookup_productmultiplyleft + 1 /\ (sto_ap_lookup_productmultiply) = 0) /\ (sto_an_lookup_productmultiply) = S ge_signed_half_lookup_productmultiplyleft))) /\ ((((((scp_second_lookup_product) = 2 * (sto_bp_lookup_productmultiply) /\ (sto_bn_lookup_productmultiply) = 0) \/ exists ge_signed_half_lookup_productmultiplyright. (((scp_second_lookup_product) = 2 * ge_signed_half_lookup_productmultiplyright + 1 /\ (sto_bp_lookup_productmultiply) = 0) /\ (sto_bn_lookup_productmultiply) = S ge_signed_half_lookup_productmultiplyright))) /\ ((((((scp_value_lookup_product) = 2 * (sto_cp_lookup_productmultiply) /\ (sto_cn_lookup_productmultiply) = 0) \/ exists ge_signed_half_lookup_productmultiplyoutput. (((scp_value_lookup_product) = 2 * ge_signed_half_lookup_productmultiplyoutput + 1 /\ (sto_cp_lookup_productmultiply) = 0) /\ (sto_cn_lookup_productmultiply) = S ge_signed_half_lookup_productmultiplyoutput))) /\ ((sto_ap_lookup_productmultiply * sto_bp_lookup_productmultiply + sto_an_lookup_productmultiply * sto_bn_lookup_productmultiply) + sto_cn_lookup_productmultiply = (sto_ap_lookup_productmultiply * sto_bn_lookup_productmultiply + sto_an_lookup_productmultiply * sto_bp_lookup_productmultiply) + sto_cp_lookup_productmultiply)))))))))))))) -> (exists pvs_gap_lookup_bound. pvs_gap_lookup_bound + S (k) = (m*n)) -> (exists dst_positive_code_lookup_value dst_positive_scale_lookup_value dst_negative_code_lookup_value dst_negative_scale_lookup_value dst_positive_lookup_value dst_negative_lookup_value. (((T) = (((((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) * S ((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) + ((dst_positive_scale_lookup_value) + (dst_positive_scale_lookup_value))) + (((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value)))) * S ((((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) * S ((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) + ((dst_positive_scale_lookup_value) + (dst_positive_scale_lookup_value))) + (((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value)))) + ((((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value))) + (((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value)))))) /\ (((((exists ff_h_pvs_lookup_valuepositive. ff_h_pvs_lookup_valuepositive + S (dst_positive_lookup_value) = S ((S (k)) * dst_positive_scale_lookup_value)) /\ exists ff_q_pvs_lookup_valuepositive. dst_positive_code_lookup_value = ff_q_pvs_lookup_valuepositive * S ((S (k)) * dst_positive_scale_lookup_value) + (dst_positive_lookup_value))) /\ (((((exists ff_h_pvs_lookup_valuenegative. ff_h_pvs_lookup_valuenegative + S (dst_negative_lookup_value) = S ((S (k)) * dst_negative_scale_lookup_value)) /\ exists ff_q_pvs_lookup_valuenegative. dst_negative_code_lookup_value = ff_q_pvs_lookup_valuenegative * S ((S (k)) * dst_negative_scale_lookup_value) + (dst_negative_lookup_value))) /\ (exists ge_balance_positive_lookup_valuevalue ge_balance_negative_lookup_valuevalue. (((((z) = 2 * (ge_balance_positive_lookup_valuevalue) /\ (ge_balance_negative_lookup_valuevalue) = 0) \/ exists ge_signed_half_lookup_valuevaluedecode. (((z) = 2 * ge_signed_half_lookup_valuevaluedecode + 1 /\ (ge_balance_positive_lookup_valuevalue) = 0) /\ (ge_balance_negative_lookup_valuevalue) = S ge_signed_half_lookup_valuevaluedecode))) /\ ((dst_positive_lookup_value) + ge_balance_negative_lookup_valuevalue = (dst_negative_lookup_value) + ge_balance_positive_lookup_valuevalue))))))))) -> exists d e a b. ((k=n*d+e) /\ (((exists pvs_gap_lookup_row. pvs_gap_lookup_row + S (d) = (m)) /\ (((exists pvs_gap_lookup_column. pvs_gap_lookup_column + S (e) = (n)) /\ (((exists dst_positive_code_lookup_F dst_positive_scale_lookup_F dst_negative_code_lookup_F dst_negative_scale_lookup_F dst_positive_lookup_F dst_negative_lookup_F. (((F) = (((((dst_positive_code_lookup_F) + (dst_positive_scale_lookup_F)) * S ((dst_positive_code_lookup_F) + (dst_positive_scale_lookup_F)) + ((dst_positive_scale_lookup_F) + (dst_positive_scale_lookup_F))) + (((dst_negative_code_lookup_F) + (dst_negative_scale_lookup_F)) * S ((dst_negative_code_lookup_F) + (dst_negative_scale_lookup_F)) + ((dst_negative_scale_lookup_F) + (dst_negative_scale_lookup_F)))) * S ((((dst_positive_code_lookup_F) + (dst_positive_scale_lookup_F)) * S ((dst_positive_code_lookup_F) + (dst_positive_scale_lookup_F)) + ((dst_positive_scale_lookup_F) + (dst_positive_scale_lookup_F))) + (((dst_negative_code_lookup_F) + (dst_negative_scale_lookup_F)) * S ((dst_negative_code_lookup_F) + (dst_negative_scale_lookup_F)) + ((dst_negative_scale_lookup_F) + (dst_negative_scale_lookup_F)))) + ((((dst_negative_code_lookup_F) + (dst_negative_scale_lookup_F)) * S ((dst_negative_code_lookup_F) + (dst_negative_scale_lookup_F)) + ((dst_negative_scale_lookup_F) + (dst_negative_scale_lookup_F))) + (((dst_negative_code_lookup_F) + (dst_negative_scale_lookup_F)) * S ((dst_negative_code_lookup_F) + (dst_negative_scale_lookup_F)) + ((dst_negative_scale_lookup_F) + (dst_negative_scale_lookup_F)))))) /\ (((((exists ff_h_pvs_lookup_Fpositive. ff_h_pvs_lookup_Fpositive + S (dst_positive_lookup_F) = S ((S (d)) * dst_positive_scale_lookup_F)) /\ exists ff_q_pvs_lookup_Fpositive. dst_positive_code_lookup_F = ff_q_pvs_lookup_Fpositive * S ((S (d)) * dst_positive_scale_lookup_F) + (dst_positive_lookup_F))) /\ (((((exists ff_h_pvs_lookup_Fnegative. ff_h_pvs_lookup_Fnegative + S (dst_negative_lookup_F) = S ((S (d)) * dst_negative_scale_lookup_F)) /\ exists ff_q_pvs_lookup_Fnegative. dst_negative_code_lookup_F = ff_q_pvs_lookup_Fnegative * S ((S (d)) * dst_negative_scale_lookup_F) + (dst_negative_lookup_F))) /\ (exists ge_balance_positive_lookup_Fvalue ge_balance_negative_lookup_Fvalue. (((((a) = 2 * (ge_balance_positive_lookup_Fvalue) /\ (ge_balance_negative_lookup_Fvalue) = 0) \/ exists ge_signed_half_lookup_Fvaluedecode. (((a) = 2 * ge_signed_half_lookup_Fvaluedecode + 1 /\ (ge_balance_positive_lookup_Fvalue) = 0) /\ (ge_balance_negative_lookup_Fvalue) = S ge_signed_half_lookup_Fvaluedecode))) /\ ((dst_positive_lookup_F) + ge_balance_negative_lookup_Fvalue = (dst_negative_lookup_F) + ge_balance_positive_lookup_Fvalue))))))))) /\ (((exists dst_positive_code_lookup_G dst_positive_scale_lookup_G dst_negative_code_lookup_G dst_negative_scale_lookup_G dst_positive_lookup_G dst_negative_lookup_G. (((G) = (((((dst_positive_code_lookup_G) + (dst_positive_scale_lookup_G)) * S ((dst_positive_code_lookup_G) + (dst_positive_scale_lookup_G)) + ((dst_positive_scale_lookup_G) + (dst_positive_scale_lookup_G))) + (((dst_negative_code_lookup_G) + (dst_negative_scale_lookup_G)) * S ((dst_negative_code_lookup_G) + (dst_negative_scale_lookup_G)) + ((dst_negative_scale_lookup_G) + (dst_negative_scale_lookup_G)))) * S ((((dst_positive_code_lookup_G) + (dst_positive_scale_lookup_G)) * S ((dst_positive_code_lookup_G) + (dst_positive_scale_lookup_G)) + ((dst_positive_scale_lookup_G) + (dst_positive_scale_lookup_G))) + (((dst_negative_code_lookup_G) + (dst_negative_scale_lookup_G)) * S ((dst_negative_code_lookup_G) + (dst_negative_scale_lookup_G)) + ((dst_negative_scale_lookup_G) + (dst_negative_scale_lookup_G)))) + ((((dst_negative_code_lookup_G) + (dst_negative_scale_lookup_G)) * S ((dst_negative_code_lookup_G) + (dst_negative_scale_lookup_G)) + ((dst_negative_scale_lookup_G) + (dst_negative_scale_lookup_G))) + (((dst_negative_code_lookup_G) + (dst_negative_scale_lookup_G)) * S ((dst_negative_code_lookup_G) + (dst_negative_scale_lookup_G)) + ((dst_negative_scale_lookup_G) + (dst_negative_scale_lookup_G)))))) /\ (((((exists ff_h_pvs_lookup_Gpositive. ff_h_pvs_lookup_Gpositive + S (dst_positive_lookup_G) = S ((S (e)) * dst_positive_scale_lookup_G)) /\ exists ff_q_pvs_lookup_Gpositive. dst_positive_code_lookup_G = ff_q_pvs_lookup_Gpositive * S ((S (e)) * dst_positive_scale_lookup_G) + (dst_positive_lookup_G))) /\ (((((exists ff_h_pvs_lookup_Gnegative. ff_h_pvs_lookup_Gnegative + S (dst_negative_lookup_G) = S ((S (e)) * dst_negative_scale_lookup_G)) /\ exists ff_q_pvs_lookup_Gnegative. dst_negative_code_lookup_G = ff_q_pvs_lookup_Gnegative * S ((S (e)) * dst_negative_scale_lookup_G) + (dst_negative_lookup_G))) /\ (exists ge_balance_positive_lookup_Gvalue ge_balance_negative_lookup_Gvalue. (((((b) = 2 * (ge_balance_positive_lookup_Gvalue) /\ (ge_balance_negative_lookup_Gvalue) = 0) \/ exists ge_signed_half_lookup_Gvaluedecode. (((b) = 2 * ge_signed_half_lookup_Gvaluedecode + 1 /\ (ge_balance_positive_lookup_Gvalue) = 0) /\ (ge_balance_negative_lookup_Gvalue) = S ge_signed_half_lookup_Gvaluedecode))) /\ ((dst_positive_lookup_G) + ge_balance_negative_lookup_Gvalue = (dst_negative_lookup_G) + ge_balance_positive_lookup_Gvalue))))))))) /\ (exists sto_ap_lookup_result sto_an_lookup_result sto_bp_lookup_result sto_bn_lookup_result sto_cp_lookup_result sto_cn_lookup_result. (((((a) = 2 * (sto_ap_lookup_result) /\ (sto_an_lookup_result) = 0) \/ exists ge_signed_half_lookup_resultleft. (((a) = 2 * ge_signed_half_lookup_resultleft + 1 /\ (sto_ap_lookup_result) = 0) /\ (sto_an_lookup_result) = S ge_signed_half_lookup_resultleft))) /\ ((((((b) = 2 * (sto_bp_lookup_result) /\ (sto_bn_lookup_result) = 0) \/ exists ge_signed_half_lookup_resultright. (((b) = 2 * ge_signed_half_lookup_resultright + 1 /\ (sto_bp_lookup_result) = 0) /\ (sto_bn_lookup_result) = S ge_signed_half_lookup_resultright))) /\ ((((((z) = 2 * (sto_cp_lookup_result) /\ (sto_cn_lookup_result) = 0) \/ exists ge_signed_half_lookup_resultoutput. (((z) = 2 * ge_signed_half_lookup_resultoutput + 1 /\ (sto_cp_lookup_result) = 0) /\ (sto_cn_lookup_result) = S ge_signed_half_lookup_resultoutput))) /\ ((sto_ap_lookup_result * sto_bp_lookup_result + sto_an_lookup_result * sto_bn_lookup_result) + sto_cn_lookup_result = (sto_ap_lookup_result * sto_bn_lookup_result + sto_an_lookup_result * sto_bp_lookup_result) + sto_cp_lookup_result))))))))))))))))