dirichlet_grid_table_lookup

Exact expanded first-order arithmetic statement

forall F G H n T a e z. (((exists dst_positive_code_grid_lookuptable dst_positive_scale_grid_lookuptable dst_negative_code_grid_lookuptable dst_negative_scale_grid_lookuptable. (((T) = (((((dst_positive_code_grid_lookuptable) + (dst_positive_scale_grid_lookuptable)) * S ((dst_positive_code_grid_lookuptable) + (dst_positive_scale_grid_lookuptable)) + ((dst_positive_scale_grid_lookuptable) + (dst_positive_scale_grid_lookuptable))) + (((dst_negative_code_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)) * S ((dst_negative_code_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)) + ((dst_negative_scale_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)))) * S ((((dst_positive_code_grid_lookuptable) + (dst_positive_scale_grid_lookuptable)) * S ((dst_positive_code_grid_lookuptable) + (dst_positive_scale_grid_lookuptable)) + ((dst_positive_scale_grid_lookuptable) + (dst_positive_scale_grid_lookuptable))) + (((dst_negative_code_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)) * S ((dst_negative_code_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)) + ((dst_negative_scale_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)))) + ((((dst_negative_code_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)) * S ((dst_negative_code_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)) + ((dst_negative_scale_grid_lookuptable) + (dst_negative_scale_grid_lookuptable))) + (((dst_negative_code_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)) * S ((dst_negative_code_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)) + ((dst_negative_scale_grid_lookuptable) + (dst_negative_scale_grid_lookuptable)))))) /\ (forall dst_index_grid_lookuptable. (exists pvs_le_gap_grid_lookuptabledomain. pvs_le_gap_grid_lookuptabledomain + (dst_index_grid_lookuptable) = ((S (n))*(S (n)))) -> exists dst_positive_grid_lookuptable dst_negative_grid_lookuptable dst_value_grid_lookuptable. ((((exists ff_h_pvs_grid_lookuptableentrypositive. ff_h_pvs_grid_lookuptableentrypositive + S (dst_positive_grid_lookuptable) = S ((S (dst_index_grid_lookuptable)) * dst_positive_scale_grid_lookuptable)) /\ exists ff_q_pvs_grid_lookuptableentrypositive. dst_positive_code_grid_lookuptable = ff_q_pvs_grid_lookuptableentrypositive * S ((S (dst_index_grid_lookuptable)) * dst_positive_scale_grid_lookuptable) + (dst_positive_grid_lookuptable))) /\ (((((exists ff_h_pvs_grid_lookuptableentrynegative. ff_h_pvs_grid_lookuptableentrynegative + S (dst_negative_grid_lookuptable) = S ((S (dst_index_grid_lookuptable)) * dst_negative_scale_grid_lookuptable)) /\ exists ff_q_pvs_grid_lookuptableentrynegative. dst_negative_code_grid_lookuptable = ff_q_pvs_grid_lookuptableentrynegative * S ((S (dst_index_grid_lookuptable)) * dst_negative_scale_grid_lookuptable) + (dst_negative_grid_lookuptable))) /\ (exists ge_balance_positive_grid_lookuptableentryvalue ge_balance_negative_grid_lookuptableentryvalue. (((((dst_value_grid_lookuptable) = 2 * (ge_balance_positive_grid_lookuptableentryvalue) /\ (ge_balance_negative_grid_lookuptableentryvalue) = 0) \/ exists ge_signed_half_grid_lookuptableentryvaluedecode. (((dst_value_grid_lookuptable) = 2 * ge_signed_half_grid_lookuptableentryvaluedecode + 1 /\ (ge_balance_positive_grid_lookuptableentryvalue) = 0) /\ (ge_balance_negative_grid_lookuptableentryvalue) = S ge_signed_half_grid_lookuptableentryvaluedecode))) /\ ((dst_positive_grid_lookuptable) + ge_balance_negative_grid_lookuptableentryvalue = (dst_negative_grid_lookuptable) + ge_balance_positive_grid_lookuptableentryvalue))))))))) /\ (forall dfg_grid_row_grid_lookup dfg_grid_column_grid_lookup dfg_grid_value_grid_lookup. (exists pvs_le_gap_grid_lookuprow. pvs_le_gap_grid_lookuprow + (dfg_grid_row_grid_lookup) = (n)) -> (exists pvs_le_gap_grid_lookupcolumn. pvs_le_gap_grid_lookupcolumn + (dfg_grid_column_grid_lookup) = (n)) -> (exists dst_positive_code_grid_lookuplookup dst_positive_scale_grid_lookuplookup dst_negative_code_grid_lookuplookup dst_negative_scale_grid_lookuplookup dst_positive_grid_lookuplookup dst_negative_grid_lookuplookup. (((T) = (((((dst_positive_code_grid_lookuplookup) + (dst_positive_scale_grid_lookuplookup)) * S ((dst_positive_code_grid_lookuplookup) + (dst_positive_scale_grid_lookuplookup)) + ((dst_positive_scale_grid_lookuplookup) + (dst_positive_scale_grid_lookuplookup))) + (((dst_negative_code_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)) * S ((dst_negative_code_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)) + ((dst_negative_scale_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)))) * S ((((dst_positive_code_grid_lookuplookup) + (dst_positive_scale_grid_lookuplookup)) * S ((dst_positive_code_grid_lookuplookup) + (dst_positive_scale_grid_lookuplookup)) + ((dst_positive_scale_grid_lookuplookup) + (dst_positive_scale_grid_lookuplookup))) + (((dst_negative_code_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)) * S ((dst_negative_code_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)) + ((dst_negative_scale_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)))) + ((((dst_negative_code_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)) * S ((dst_negative_code_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)) + ((dst_negative_scale_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup))) + (((dst_negative_code_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)) * S ((dst_negative_code_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)) + ((dst_negative_scale_grid_lookuplookup) + (dst_negative_scale_grid_lookuplookup)))))) /\ (((((exists ff_h_pvs_grid_lookuplookuppositive. ff_h_pvs_grid_lookuplookuppositive + S (dst_positive_grid_lookuplookup) = S ((S ((S (n))*(dfg_grid_row_grid_lookup)+(dfg_grid_column_grid_lookup))) * dst_positive_scale_grid_lookuplookup)) /\ exists ff_q_pvs_grid_lookuplookuppositive. dst_positive_code_grid_lookuplookup = ff_q_pvs_grid_lookuplookuppositive * S ((S ((S (n))*(dfg_grid_row_grid_lookup)+(dfg_grid_column_grid_lookup))) * dst_positive_scale_grid_lookuplookup) + (dst_positive_grid_lookuplookup))) /\ (((((exists ff_h_pvs_grid_lookuplookupnegative. ff_h_pvs_grid_lookuplookupnegative + S (dst_negative_grid_lookuplookup) = S ((S ((S (n))*(dfg_grid_row_grid_lookup)+(dfg_grid_column_grid_lookup))) * dst_negative_scale_grid_lookuplookup)) /\ exists ff_q_pvs_grid_lookuplookupnegative. dst_negative_code_grid_lookuplookup = ff_q_pvs_grid_lookuplookupnegative * S ((S ((S (n))*(dfg_grid_row_grid_lookup)+(dfg_grid_column_grid_lookup))) * dst_negative_scale_grid_lookuplookup) + (dst_negative_grid_lookuplookup))) /\ (exists ge_balance_positive_grid_lookuplookupvalue ge_balance_negative_grid_lookuplookupvalue. (((((dfg_grid_value_grid_lookup) = 2 * (ge_balance_positive_grid_lookuplookupvalue) /\ (ge_balance_negative_grid_lookuplookupvalue) = 0) \/ exists ge_signed_half_grid_lookuplookupvaluedecode. (((dfg_grid_value_grid_lookup) = 2 * ge_signed_half_grid_lookuplookupvaluedecode + 1 /\ (ge_balance_positive_grid_lookuplookupvalue) = 0) /\ (ge_balance_negative_grid_lookuplookupvalue) = S ge_signed_half_grid_lookuplookupvaluedecode))) /\ ((dst_positive_grid_lookuplookup) + ge_balance_negative_grid_lookuplookupvalue = (dst_negative_grid_lookuplookup) + ge_balance_positive_grid_lookuplookupvalue))))))))) -> ((((~((dfg_grid_row_grid_lookup)=0)) /\ (((~((dfg_grid_column_grid_lookup)=0)) /\ (exists dfg_middle_grid_lookupentry dfg_first_grid_lookupentry dfg_last_grid_lookupentry dfg_value_grid_lookupentry. (((n)=((dfg_grid_row_grid_lookup)*(dfg_grid_column_grid_lookup))*dfg_middle_grid_lookupentry) /\ (((exists dst_positive_code_grid_lookupentryfirst dst_positive_scale_grid_lookupentryfirst dst_negative_code_grid_lookupentryfirst dst_negative_scale_grid_lookupentryfirst dst_positive_grid_lookupentryfirst dst_negative_grid_lookupentryfirst. (((F) = (((((dst_positive_code_grid_lookupentryfirst) + (dst_positive_scale_grid_lookupentryfirst)) * S ((dst_positive_code_grid_lookupentryfirst) + (dst_positive_scale_grid_lookupentryfirst)) + ((dst_positive_scale_grid_lookupentryfirst) + (dst_positive_scale_grid_lookupentryfirst))) + (((dst_negative_code_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)) * S ((dst_negative_code_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)) + ((dst_negative_scale_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)))) * S ((((dst_positive_code_grid_lookupentryfirst) + (dst_positive_scale_grid_lookupentryfirst)) * S ((dst_positive_code_grid_lookupentryfirst) + (dst_positive_scale_grid_lookupentryfirst)) + ((dst_positive_scale_grid_lookupentryfirst) + (dst_positive_scale_grid_lookupentryfirst))) + (((dst_negative_code_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)) * S ((dst_negative_code_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)) + ((dst_negative_scale_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)))) + ((((dst_negative_code_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)) * S ((dst_negative_code_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)) + ((dst_negative_scale_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst))) + (((dst_negative_code_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)) * S ((dst_negative_code_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)) + ((dst_negative_scale_grid_lookupentryfirst) + (dst_negative_scale_grid_lookupentryfirst)))))) /\ (((((exists ff_h_pvs_grid_lookupentryfirstpositive. ff_h_pvs_grid_lookupentryfirstpositive + S (dst_positive_grid_lookupentryfirst) = S ((S (dfg_grid_row_grid_lookup)) * dst_positive_scale_grid_lookupentryfirst)) /\ exists ff_q_pvs_grid_lookupentryfirstpositive. dst_positive_code_grid_lookupentryfirst = ff_q_pvs_grid_lookupentryfirstpositive * S ((S (dfg_grid_row_grid_lookup)) * dst_positive_scale_grid_lookupentryfirst) + (dst_positive_grid_lookupentryfirst))) /\ (((((exists ff_h_pvs_grid_lookupentryfirstnegative. ff_h_pvs_grid_lookupentryfirstnegative + S (dst_negative_grid_lookupentryfirst) = S ((S (dfg_grid_row_grid_lookup)) * dst_negative_scale_grid_lookupentryfirst)) /\ exists ff_q_pvs_grid_lookupentryfirstnegative. dst_negative_code_grid_lookupentryfirst = ff_q_pvs_grid_lookupentryfirstnegative * S ((S (dfg_grid_row_grid_lookup)) * dst_negative_scale_grid_lookupentryfirst) + (dst_negative_grid_lookupentryfirst))) /\ (exists ge_balance_positive_grid_lookupentryfirstvalue ge_balance_negative_grid_lookupentryfirstvalue. (((((dfg_first_grid_lookupentry) = 2 * (ge_balance_positive_grid_lookupentryfirstvalue) /\ (ge_balance_negative_grid_lookupentryfirstvalue) = 0) \/ exists ge_signed_half_grid_lookupentryfirstvaluedecode. (((dfg_first_grid_lookupentry) = 2 * ge_signed_half_grid_lookupentryfirstvaluedecode + 1 /\ (ge_balance_positive_grid_lookupentryfirstvalue) = 0) /\ (ge_balance_negative_grid_lookupentryfirstvalue) = S ge_signed_half_grid_lookupentryfirstvaluedecode))) /\ ((dst_positive_grid_lookupentryfirst) + ge_balance_negative_grid_lookupentryfirstvalue = (dst_negative_grid_lookupentryfirst) + ge_balance_positive_grid_lookupentryfirstvalue))))))))) /\ (((exists dst_positive_code_grid_lookupentrylast dst_positive_scale_grid_lookupentrylast dst_negative_code_grid_lookupentrylast dst_negative_scale_grid_lookupentrylast dst_positive_grid_lookupentrylast dst_negative_grid_lookupentrylast. (((H) = (((((dst_positive_code_grid_lookupentrylast) + (dst_positive_scale_grid_lookupentrylast)) * S ((dst_positive_code_grid_lookupentrylast) + (dst_positive_scale_grid_lookupentrylast)) + ((dst_positive_scale_grid_lookupentrylast) + (dst_positive_scale_grid_lookupentrylast))) + (((dst_negative_code_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)) * S ((dst_negative_code_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)) + ((dst_negative_scale_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)))) * S ((((dst_positive_code_grid_lookupentrylast) + (dst_positive_scale_grid_lookupentrylast)) * S ((dst_positive_code_grid_lookupentrylast) + (dst_positive_scale_grid_lookupentrylast)) + ((dst_positive_scale_grid_lookupentrylast) + (dst_positive_scale_grid_lookupentrylast))) + (((dst_negative_code_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)) * S ((dst_negative_code_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)) + ((dst_negative_scale_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)))) + ((((dst_negative_code_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)) * S ((dst_negative_code_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)) + ((dst_negative_scale_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast))) + (((dst_negative_code_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)) * S ((dst_negative_code_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)) + ((dst_negative_scale_grid_lookupentrylast) + (dst_negative_scale_grid_lookupentrylast)))))) /\ (((((exists ff_h_pvs_grid_lookupentrylastpositive. ff_h_pvs_grid_lookupentrylastpositive + S (dst_positive_grid_lookupentrylast) = S ((S (dfg_grid_column_grid_lookup)) * dst_positive_scale_grid_lookupentrylast)) /\ exists ff_q_pvs_grid_lookupentrylastpositive. dst_positive_code_grid_lookupentrylast = ff_q_pvs_grid_lookupentrylastpositive * S ((S (dfg_grid_column_grid_lookup)) * dst_positive_scale_grid_lookupentrylast) + (dst_positive_grid_lookupentrylast))) /\ (((((exists ff_h_pvs_grid_lookupentrylastnegative. ff_h_pvs_grid_lookupentrylastnegative + S (dst_negative_grid_lookupentrylast) = S ((S (dfg_grid_column_grid_lookup)) * dst_negative_scale_grid_lookupentrylast)) /\ exists ff_q_pvs_grid_lookupentrylastnegative. dst_negative_code_grid_lookupentrylast = ff_q_pvs_grid_lookupentrylastnegative * S ((S (dfg_grid_column_grid_lookup)) * dst_negative_scale_grid_lookupentrylast) + (dst_negative_grid_lookupentrylast))) /\ (exists ge_balance_positive_grid_lookupentrylastvalue ge_balance_negative_grid_lookupentrylastvalue. (((((dfg_last_grid_lookupentry) = 2 * (ge_balance_positive_grid_lookupentrylastvalue) /\ (ge_balance_negative_grid_lookupentrylastvalue) = 0) \/ exists ge_signed_half_grid_lookupentrylastvaluedecode. (((dfg_last_grid_lookupentry) = 2 * ge_signed_half_grid_lookupentrylastvaluedecode + 1 /\ (ge_balance_positive_grid_lookupentrylastvalue) = 0) /\ (ge_balance_negative_grid_lookupentrylastvalue) = S ge_signed_half_grid_lookupentrylastvaluedecode))) /\ ((dst_positive_grid_lookupentrylast) + ge_balance_negative_grid_lookupentrylastvalue = (dst_negative_grid_lookupentrylast) + ge_balance_positive_grid_lookupentrylastvalue))))))))) /\ (((exists dst_positive_code_grid_lookupentrymiddle dst_positive_scale_grid_lookupentrymiddle dst_negative_code_grid_lookupentrymiddle dst_negative_scale_grid_lookupentrymiddle dst_positive_grid_lookupentrymiddle dst_negative_grid_lookupentrymiddle. (((G) = (((((dst_positive_code_grid_lookupentrymiddle) + (dst_positive_scale_grid_lookupentrymiddle)) * S ((dst_positive_code_grid_lookupentrymiddle) + (dst_positive_scale_grid_lookupentrymiddle)) + ((dst_positive_scale_grid_lookupentrymiddle) + (dst_positive_scale_grid_lookupentrymiddle))) + (((dst_negative_code_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)) * S ((dst_negative_code_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)) + ((dst_negative_scale_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)))) * S ((((dst_positive_code_grid_lookupentrymiddle) + (dst_positive_scale_grid_lookupentrymiddle)) * S ((dst_positive_code_grid_lookupentrymiddle) + (dst_positive_scale_grid_lookupentrymiddle)) + ((dst_positive_scale_grid_lookupentrymiddle) + (dst_positive_scale_grid_lookupentrymiddle))) + (((dst_negative_code_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)) * S ((dst_negative_code_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)) + ((dst_negative_scale_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)))) + ((((dst_negative_code_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)) * S ((dst_negative_code_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)) + ((dst_negative_scale_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle))) + (((dst_negative_code_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)) * S ((dst_negative_code_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)) + ((dst_negative_scale_grid_lookupentrymiddle) + (dst_negative_scale_grid_lookupentrymiddle)))))) /\ (((((exists ff_h_pvs_grid_lookupentrymiddlepositive. ff_h_pvs_grid_lookupentrymiddlepositive + S (dst_positive_grid_lookupentrymiddle) = S ((S (dfg_middle_grid_lookupentry)) * dst_positive_scale_grid_lookupentrymiddle)) /\ exists ff_q_pvs_grid_lookupentrymiddlepositive. dst_positive_code_grid_lookupentrymiddle = ff_q_pvs_grid_lookupentrymiddlepositive * S ((S (dfg_middle_grid_lookupentry)) * dst_positive_scale_grid_lookupentrymiddle) + (dst_positive_grid_lookupentrymiddle))) /\ (((((exists ff_h_pvs_grid_lookupentrymiddlenegative. ff_h_pvs_grid_lookupentrymiddlenegative + S (dst_negative_grid_lookupentrymiddle) = S ((S (dfg_middle_grid_lookupentry)) * dst_negative_scale_grid_lookupentrymiddle)) /\ exists ff_q_pvs_grid_lookupentrymiddlenegative. dst_negative_code_grid_lookupentrymiddle = ff_q_pvs_grid_lookupentrymiddlenegative * S ((S (dfg_middle_grid_lookupentry)) * dst_negative_scale_grid_lookupentrymiddle) + (dst_negative_grid_lookupentrymiddle))) /\ (exists ge_balance_positive_grid_lookupentrymiddlevalue ge_balance_negative_grid_lookupentrymiddlevalue. (((((dfg_value_grid_lookupentry) = 2 * (ge_balance_positive_grid_lookupentrymiddlevalue) /\ (ge_balance_negative_grid_lookupentrymiddlevalue) = 0) \/ exists ge_signed_half_grid_lookupentrymiddlevaluedecode. (((dfg_value_grid_lookupentry) = 2 * ge_signed_half_grid_lookupentrymiddlevaluedecode + 1 /\ (ge_balance_positive_grid_lookupentrymiddlevalue) = 0) /\ (ge_balance_negative_grid_lookupentrymiddlevalue) = S ge_signed_half_grid_lookupentrymiddlevaluedecode))) /\ ((dst_positive_grid_lookupentrymiddle) + ge_balance_negative_grid_lookupentrymiddlevalue = (dst_negative_grid_lookupentrymiddle) + ge_balance_positive_grid_lookupentrymiddlevalue))))))))) /\ (exists dfg_inner_grid_lookupentryproduct. ((exists sto_ap_grid_lookupentryproductinner sto_an_grid_lookupentryproductinner sto_bp_grid_lookupentryproductinner sto_bn_grid_lookupentryproductinner sto_cp_grid_lookupentryproductinner sto_cn_grid_lookupentryproductinner. (((((dfg_last_grid_lookupentry) = 2 * (sto_ap_grid_lookupentryproductinner) /\ (sto_an_grid_lookupentryproductinner) = 0) \/ exists ge_signed_half_grid_lookupentryproductinnerleft. (((dfg_last_grid_lookupentry) = 2 * ge_signed_half_grid_lookupentryproductinnerleft + 1 /\ (sto_ap_grid_lookupentryproductinner) = 0) /\ (sto_an_grid_lookupentryproductinner) = S ge_signed_half_grid_lookupentryproductinnerleft))) /\ ((((((dfg_value_grid_lookupentry) = 2 * (sto_bp_grid_lookupentryproductinner) /\ (sto_bn_grid_lookupentryproductinner) = 0) \/ exists ge_signed_half_grid_lookupentryproductinnerright. (((dfg_value_grid_lookupentry) = 2 * ge_signed_half_grid_lookupentryproductinnerright + 1 /\ (sto_bp_grid_lookupentryproductinner) = 0) /\ (sto_bn_grid_lookupentryproductinner) = S ge_signed_half_grid_lookupentryproductinnerright))) /\ ((((((dfg_inner_grid_lookupentryproduct) = 2 * (sto_cp_grid_lookupentryproductinner) /\ (sto_cn_grid_lookupentryproductinner) = 0) \/ exists ge_signed_half_grid_lookupentryproductinneroutput. (((dfg_inner_grid_lookupentryproduct) = 2 * ge_signed_half_grid_lookupentryproductinneroutput + 1 /\ (sto_cp_grid_lookupentryproductinner) = 0) /\ (sto_cn_grid_lookupentryproductinner) = S ge_signed_half_grid_lookupentryproductinneroutput))) /\ ((sto_ap_grid_lookupentryproductinner * sto_bp_grid_lookupentryproductinner + sto_an_grid_lookupentryproductinner * sto_bn_grid_lookupentryproductinner) + sto_cn_grid_lookupentryproductinner = (sto_ap_grid_lookupentryproductinner * sto_bn_grid_lookupentryproductinner + sto_an_grid_lookupentryproductinner * sto_bp_grid_lookupentryproductinner) + sto_cp_grid_lookupentryproductinner))))))) /\ (exists sto_ap_grid_lookupentryproductouter sto_an_grid_lookupentryproductouter sto_bp_grid_lookupentryproductouter sto_bn_grid_lookupentryproductouter sto_cp_grid_lookupentryproductouter sto_cn_grid_lookupentryproductouter. (((((dfg_first_grid_lookupentry) = 2 * (sto_ap_grid_lookupentryproductouter) /\ (sto_an_grid_lookupentryproductouter) = 0) \/ exists ge_signed_half_grid_lookupentryproductouterleft. (((dfg_first_grid_lookupentry) = 2 * ge_signed_half_grid_lookupentryproductouterleft + 1 /\ (sto_ap_grid_lookupentryproductouter) = 0) /\ (sto_an_grid_lookupentryproductouter) = S ge_signed_half_grid_lookupentryproductouterleft))) /\ ((((((dfg_inner_grid_lookupentryproduct) = 2 * (sto_bp_grid_lookupentryproductouter) /\ (sto_bn_grid_lookupentryproductouter) = 0) \/ exists ge_signed_half_grid_lookupentryproductouterright. (((dfg_inner_grid_lookupentryproduct) = 2 * ge_signed_half_grid_lookupentryproductouterright + 1 /\ (sto_bp_grid_lookupentryproductouter) = 0) /\ (sto_bn_grid_lookupentryproductouter) = S ge_signed_half_grid_lookupentryproductouterright))) /\ ((((((dfg_grid_value_grid_lookup) = 2 * (sto_cp_grid_lookupentryproductouter) /\ (sto_cn_grid_lookupentryproductouter) = 0) \/ exists ge_signed_half_grid_lookupentryproductouteroutput. (((dfg_grid_value_grid_lookup) = 2 * ge_signed_half_grid_lookupentryproductouteroutput + 1 /\ (sto_cp_grid_lookupentryproductouter) = 0) /\ (sto_cn_grid_lookupentryproductouter) = S ge_signed_half_grid_lookupentryproductouteroutput))) /\ ((sto_ap_grid_lookupentryproductouter * sto_bp_grid_lookupentryproductouter + sto_an_grid_lookupentryproductouter * sto_bn_grid_lookupentryproductouter) + sto_cn_grid_lookupentryproductouter = (sto_ap_grid_lookupentryproductouter * sto_bn_grid_lookupentryproductouter + sto_an_grid_lookupentryproductouter * sto_bp_grid_lookupentryproductouter) + sto_cp_grid_lookupentryproductouter))))))))))))))))))))) \/ ((((dfg_grid_row_grid_lookup)=0 \/ ((dfg_grid_column_grid_lookup)=0 \/ ~(exists pvs_factor_grid_lookupentryomittednondivisor. (n) = ((dfg_grid_row_grid_lookup)*(dfg_grid_column_grid_lookup)) * pvs_factor_grid_lookupentryomittednondivisor))) /\ ((dfg_grid_value_grid_lookup)=0))))))) -> (exists pvs_le_gap_grid_row_bound. pvs_le_gap_grid_row_bound + (a) = (n)) -> (exists pvs_le_gap_grid_column_bound. pvs_le_gap_grid_column_bound + (e) = (n)) -> (exists dst_positive_code_grid_lookup_value dst_positive_scale_grid_lookup_value dst_negative_code_grid_lookup_value dst_negative_scale_grid_lookup_value dst_positive_grid_lookup_value dst_negative_grid_lookup_value. (((T) = (((((dst_positive_code_grid_lookup_value) + (dst_positive_scale_grid_lookup_value)) * S ((dst_positive_code_grid_lookup_value) + (dst_positive_scale_grid_lookup_value)) + ((dst_positive_scale_grid_lookup_value) + (dst_positive_scale_grid_lookup_value))) + (((dst_negative_code_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)) * S ((dst_negative_code_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)) + ((dst_negative_scale_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)))) * S ((((dst_positive_code_grid_lookup_value) + (dst_positive_scale_grid_lookup_value)) * S ((dst_positive_code_grid_lookup_value) + (dst_positive_scale_grid_lookup_value)) + ((dst_positive_scale_grid_lookup_value) + (dst_positive_scale_grid_lookup_value))) + (((dst_negative_code_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)) * S ((dst_negative_code_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)) + ((dst_negative_scale_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)))) + ((((dst_negative_code_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)) * S ((dst_negative_code_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)) + ((dst_negative_scale_grid_lookup_value) + (dst_negative_scale_grid_lookup_value))) + (((dst_negative_code_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)) * S ((dst_negative_code_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)) + ((dst_negative_scale_grid_lookup_value) + (dst_negative_scale_grid_lookup_value)))))) /\ (((((exists ff_h_pvs_grid_lookup_valuepositive. ff_h_pvs_grid_lookup_valuepositive + S (dst_positive_grid_lookup_value) = S ((S ((S (n))*(a)+(e))) * dst_positive_scale_grid_lookup_value)) /\ exists ff_q_pvs_grid_lookup_valuepositive. dst_positive_code_grid_lookup_value = ff_q_pvs_grid_lookup_valuepositive * S ((S ((S (n))*(a)+(e))) * dst_positive_scale_grid_lookup_value) + (dst_positive_grid_lookup_value))) /\ (((((exists ff_h_pvs_grid_lookup_valuenegative. ff_h_pvs_grid_lookup_valuenegative + S (dst_negative_grid_lookup_value) = S ((S ((S (n))*(a)+(e))) * dst_negative_scale_grid_lookup_value)) /\ exists ff_q_pvs_grid_lookup_valuenegative. dst_negative_code_grid_lookup_value = ff_q_pvs_grid_lookup_valuenegative * S ((S ((S (n))*(a)+(e))) * dst_negative_scale_grid_lookup_value) + (dst_negative_grid_lookup_value))) /\ (exists ge_balance_positive_grid_lookup_valuevalue ge_balance_negative_grid_lookup_valuevalue. (((((z) = 2 * (ge_balance_positive_grid_lookup_valuevalue) /\ (ge_balance_negative_grid_lookup_valuevalue) = 0) \/ exists ge_signed_half_grid_lookup_valuevaluedecode. (((z) = 2 * ge_signed_half_grid_lookup_valuevaluedecode + 1 /\ (ge_balance_positive_grid_lookup_valuevalue) = 0) /\ (ge_balance_negative_grid_lookup_valuevalue) = S ge_signed_half_grid_lookup_valuevaluedecode))) /\ ((dst_positive_grid_lookup_value) + ge_balance_negative_grid_lookup_valuevalue = (dst_negative_grid_lookup_value) + ge_balance_positive_grid_lookup_valuevalue))))))))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_grid_lookup_result dfg_first_grid_lookup_result dfg_last_grid_lookup_result dfg_value_grid_lookup_result. (((n)=((a)*(e))*dfg_middle_grid_lookup_result) /\ (((exists dst_positive_code_grid_lookup_resultfirst dst_positive_scale_grid_lookup_resultfirst dst_negative_code_grid_lookup_resultfirst dst_negative_scale_grid_lookup_resultfirst dst_positive_grid_lookup_resultfirst dst_negative_grid_lookup_resultfirst. (((F) = (((((dst_positive_code_grid_lookup_resultfirst) + (dst_positive_scale_grid_lookup_resultfirst)) * S ((dst_positive_code_grid_lookup_resultfirst) + (dst_positive_scale_grid_lookup_resultfirst)) + ((dst_positive_scale_grid_lookup_resultfirst) + (dst_positive_scale_grid_lookup_resultfirst))) + (((dst_negative_code_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)) * S ((dst_negative_code_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)) + ((dst_negative_scale_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)))) * S ((((dst_positive_code_grid_lookup_resultfirst) + (dst_positive_scale_grid_lookup_resultfirst)) * S ((dst_positive_code_grid_lookup_resultfirst) + (dst_positive_scale_grid_lookup_resultfirst)) + ((dst_positive_scale_grid_lookup_resultfirst) + (dst_positive_scale_grid_lookup_resultfirst))) + (((dst_negative_code_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)) * S ((dst_negative_code_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)) + ((dst_negative_scale_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)))) + ((((dst_negative_code_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)) * S ((dst_negative_code_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)) + ((dst_negative_scale_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst))) + (((dst_negative_code_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)) * S ((dst_negative_code_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)) + ((dst_negative_scale_grid_lookup_resultfirst) + (dst_negative_scale_grid_lookup_resultfirst)))))) /\ (((((exists ff_h_pvs_grid_lookup_resultfirstpositive. ff_h_pvs_grid_lookup_resultfirstpositive + S (dst_positive_grid_lookup_resultfirst) = S ((S (a)) * dst_positive_scale_grid_lookup_resultfirst)) /\ exists ff_q_pvs_grid_lookup_resultfirstpositive. dst_positive_code_grid_lookup_resultfirst = ff_q_pvs_grid_lookup_resultfirstpositive * S ((S (a)) * dst_positive_scale_grid_lookup_resultfirst) + (dst_positive_grid_lookup_resultfirst))) /\ (((((exists ff_h_pvs_grid_lookup_resultfirstnegative. ff_h_pvs_grid_lookup_resultfirstnegative + S (dst_negative_grid_lookup_resultfirst) = S ((S (a)) * dst_negative_scale_grid_lookup_resultfirst)) /\ exists ff_q_pvs_grid_lookup_resultfirstnegative. dst_negative_code_grid_lookup_resultfirst = ff_q_pvs_grid_lookup_resultfirstnegative * S ((S (a)) * dst_negative_scale_grid_lookup_resultfirst) + (dst_negative_grid_lookup_resultfirst))) /\ (exists ge_balance_positive_grid_lookup_resultfirstvalue ge_balance_negative_grid_lookup_resultfirstvalue. (((((dfg_first_grid_lookup_result) = 2 * (ge_balance_positive_grid_lookup_resultfirstvalue) /\ (ge_balance_negative_grid_lookup_resultfirstvalue) = 0) \/ exists ge_signed_half_grid_lookup_resultfirstvaluedecode. (((dfg_first_grid_lookup_result) = 2 * ge_signed_half_grid_lookup_resultfirstvaluedecode + 1 /\ (ge_balance_positive_grid_lookup_resultfirstvalue) = 0) /\ (ge_balance_negative_grid_lookup_resultfirstvalue) = S ge_signed_half_grid_lookup_resultfirstvaluedecode))) /\ ((dst_positive_grid_lookup_resultfirst) + ge_balance_negative_grid_lookup_resultfirstvalue = (dst_negative_grid_lookup_resultfirst) + ge_balance_positive_grid_lookup_resultfirstvalue))))))))) /\ (((exists dst_positive_code_grid_lookup_resultlast dst_positive_scale_grid_lookup_resultlast dst_negative_code_grid_lookup_resultlast dst_negative_scale_grid_lookup_resultlast dst_positive_grid_lookup_resultlast dst_negative_grid_lookup_resultlast. (((H) = (((((dst_positive_code_grid_lookup_resultlast) + (dst_positive_scale_grid_lookup_resultlast)) * S ((dst_positive_code_grid_lookup_resultlast) + (dst_positive_scale_grid_lookup_resultlast)) + ((dst_positive_scale_grid_lookup_resultlast) + (dst_positive_scale_grid_lookup_resultlast))) + (((dst_negative_code_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)) * S ((dst_negative_code_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)) + ((dst_negative_scale_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)))) * S ((((dst_positive_code_grid_lookup_resultlast) + (dst_positive_scale_grid_lookup_resultlast)) * S ((dst_positive_code_grid_lookup_resultlast) + (dst_positive_scale_grid_lookup_resultlast)) + ((dst_positive_scale_grid_lookup_resultlast) + (dst_positive_scale_grid_lookup_resultlast))) + (((dst_negative_code_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)) * S ((dst_negative_code_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)) + ((dst_negative_scale_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)))) + ((((dst_negative_code_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)) * S ((dst_negative_code_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)) + ((dst_negative_scale_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast))) + (((dst_negative_code_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)) * S ((dst_negative_code_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)) + ((dst_negative_scale_grid_lookup_resultlast) + (dst_negative_scale_grid_lookup_resultlast)))))) /\ (((((exists ff_h_pvs_grid_lookup_resultlastpositive. ff_h_pvs_grid_lookup_resultlastpositive + S (dst_positive_grid_lookup_resultlast) = S ((S (e)) * dst_positive_scale_grid_lookup_resultlast)) /\ exists ff_q_pvs_grid_lookup_resultlastpositive. dst_positive_code_grid_lookup_resultlast = ff_q_pvs_grid_lookup_resultlastpositive * S ((S (e)) * dst_positive_scale_grid_lookup_resultlast) + (dst_positive_grid_lookup_resultlast))) /\ (((((exists ff_h_pvs_grid_lookup_resultlastnegative. ff_h_pvs_grid_lookup_resultlastnegative + S (dst_negative_grid_lookup_resultlast) = S ((S (e)) * dst_negative_scale_grid_lookup_resultlast)) /\ exists ff_q_pvs_grid_lookup_resultlastnegative. dst_negative_code_grid_lookup_resultlast = ff_q_pvs_grid_lookup_resultlastnegative * S ((S (e)) * dst_negative_scale_grid_lookup_resultlast) + (dst_negative_grid_lookup_resultlast))) /\ (exists ge_balance_positive_grid_lookup_resultlastvalue ge_balance_negative_grid_lookup_resultlastvalue. (((((dfg_last_grid_lookup_result) = 2 * (ge_balance_positive_grid_lookup_resultlastvalue) /\ (ge_balance_negative_grid_lookup_resultlastvalue) = 0) \/ exists ge_signed_half_grid_lookup_resultlastvaluedecode. (((dfg_last_grid_lookup_result) = 2 * ge_signed_half_grid_lookup_resultlastvaluedecode + 1 /\ (ge_balance_positive_grid_lookup_resultlastvalue) = 0) /\ (ge_balance_negative_grid_lookup_resultlastvalue) = S ge_signed_half_grid_lookup_resultlastvaluedecode))) /\ ((dst_positive_grid_lookup_resultlast) + ge_balance_negative_grid_lookup_resultlastvalue = (dst_negative_grid_lookup_resultlast) + ge_balance_positive_grid_lookup_resultlastvalue))))))))) /\ (((exists dst_positive_code_grid_lookup_resultmiddle dst_positive_scale_grid_lookup_resultmiddle dst_negative_code_grid_lookup_resultmiddle dst_negative_scale_grid_lookup_resultmiddle dst_positive_grid_lookup_resultmiddle dst_negative_grid_lookup_resultmiddle. (((G) = (((((dst_positive_code_grid_lookup_resultmiddle) + (dst_positive_scale_grid_lookup_resultmiddle)) * S ((dst_positive_code_grid_lookup_resultmiddle) + (dst_positive_scale_grid_lookup_resultmiddle)) + ((dst_positive_scale_grid_lookup_resultmiddle) + (dst_positive_scale_grid_lookup_resultmiddle))) + (((dst_negative_code_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)) * S ((dst_negative_code_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)) + ((dst_negative_scale_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)))) * S ((((dst_positive_code_grid_lookup_resultmiddle) + (dst_positive_scale_grid_lookup_resultmiddle)) * S ((dst_positive_code_grid_lookup_resultmiddle) + (dst_positive_scale_grid_lookup_resultmiddle)) + ((dst_positive_scale_grid_lookup_resultmiddle) + (dst_positive_scale_grid_lookup_resultmiddle))) + (((dst_negative_code_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)) * S ((dst_negative_code_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)) + ((dst_negative_scale_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)))) + ((((dst_negative_code_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)) * S ((dst_negative_code_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)) + ((dst_negative_scale_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle))) + (((dst_negative_code_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)) * S ((dst_negative_code_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)) + ((dst_negative_scale_grid_lookup_resultmiddle) + (dst_negative_scale_grid_lookup_resultmiddle)))))) /\ (((((exists ff_h_pvs_grid_lookup_resultmiddlepositive. ff_h_pvs_grid_lookup_resultmiddlepositive + S (dst_positive_grid_lookup_resultmiddle) = S ((S (dfg_middle_grid_lookup_result)) * dst_positive_scale_grid_lookup_resultmiddle)) /\ exists ff_q_pvs_grid_lookup_resultmiddlepositive. dst_positive_code_grid_lookup_resultmiddle = ff_q_pvs_grid_lookup_resultmiddlepositive * S ((S (dfg_middle_grid_lookup_result)) * dst_positive_scale_grid_lookup_resultmiddle) + (dst_positive_grid_lookup_resultmiddle))) /\ (((((exists ff_h_pvs_grid_lookup_resultmiddlenegative. ff_h_pvs_grid_lookup_resultmiddlenegative + S (dst_negative_grid_lookup_resultmiddle) = S ((S (dfg_middle_grid_lookup_result)) * dst_negative_scale_grid_lookup_resultmiddle)) /\ exists ff_q_pvs_grid_lookup_resultmiddlenegative. dst_negative_code_grid_lookup_resultmiddle = ff_q_pvs_grid_lookup_resultmiddlenegative * S ((S (dfg_middle_grid_lookup_result)) * dst_negative_scale_grid_lookup_resultmiddle) + (dst_negative_grid_lookup_resultmiddle))) /\ (exists ge_balance_positive_grid_lookup_resultmiddlevalue ge_balance_negative_grid_lookup_resultmiddlevalue. (((((dfg_value_grid_lookup_result) = 2 * (ge_balance_positive_grid_lookup_resultmiddlevalue) /\ (ge_balance_negative_grid_lookup_resultmiddlevalue) = 0) \/ exists ge_signed_half_grid_lookup_resultmiddlevaluedecode. (((dfg_value_grid_lookup_result) = 2 * ge_signed_half_grid_lookup_resultmiddlevaluedecode + 1 /\ (ge_balance_positive_grid_lookup_resultmiddlevalue) = 0) /\ (ge_balance_negative_grid_lookup_resultmiddlevalue) = S ge_signed_half_grid_lookup_resultmiddlevaluedecode))) /\ ((dst_positive_grid_lookup_resultmiddle) + ge_balance_negative_grid_lookup_resultmiddlevalue = (dst_negative_grid_lookup_resultmiddle) + ge_balance_positive_grid_lookup_resultmiddlevalue))))))))) /\ (exists dfg_inner_grid_lookup_resultproduct. ((exists sto_ap_grid_lookup_resultproductinner sto_an_grid_lookup_resultproductinner sto_bp_grid_lookup_resultproductinner sto_bn_grid_lookup_resultproductinner sto_cp_grid_lookup_resultproductinner sto_cn_grid_lookup_resultproductinner. (((((dfg_last_grid_lookup_result) = 2 * (sto_ap_grid_lookup_resultproductinner) /\ (sto_an_grid_lookup_resultproductinner) = 0) \/ exists ge_signed_half_grid_lookup_resultproductinnerleft. (((dfg_last_grid_lookup_result) = 2 * ge_signed_half_grid_lookup_resultproductinnerleft + 1 /\ (sto_ap_grid_lookup_resultproductinner) = 0) /\ (sto_an_grid_lookup_resultproductinner) = S ge_signed_half_grid_lookup_resultproductinnerleft))) /\ ((((((dfg_value_grid_lookup_result) = 2 * (sto_bp_grid_lookup_resultproductinner) /\ (sto_bn_grid_lookup_resultproductinner) = 0) \/ exists ge_signed_half_grid_lookup_resultproductinnerright. (((dfg_value_grid_lookup_result) = 2 * ge_signed_half_grid_lookup_resultproductinnerright + 1 /\ (sto_bp_grid_lookup_resultproductinner) = 0) /\ (sto_bn_grid_lookup_resultproductinner) = S ge_signed_half_grid_lookup_resultproductinnerright))) /\ ((((((dfg_inner_grid_lookup_resultproduct) = 2 * (sto_cp_grid_lookup_resultproductinner) /\ (sto_cn_grid_lookup_resultproductinner) = 0) \/ exists ge_signed_half_grid_lookup_resultproductinneroutput. (((dfg_inner_grid_lookup_resultproduct) = 2 * ge_signed_half_grid_lookup_resultproductinneroutput + 1 /\ (sto_cp_grid_lookup_resultproductinner) = 0) /\ (sto_cn_grid_lookup_resultproductinner) = S ge_signed_half_grid_lookup_resultproductinneroutput))) /\ ((sto_ap_grid_lookup_resultproductinner * sto_bp_grid_lookup_resultproductinner + sto_an_grid_lookup_resultproductinner * sto_bn_grid_lookup_resultproductinner) + sto_cn_grid_lookup_resultproductinner = (sto_ap_grid_lookup_resultproductinner * sto_bn_grid_lookup_resultproductinner + sto_an_grid_lookup_resultproductinner * sto_bp_grid_lookup_resultproductinner) + sto_cp_grid_lookup_resultproductinner))))))) /\ (exists sto_ap_grid_lookup_resultproductouter sto_an_grid_lookup_resultproductouter sto_bp_grid_lookup_resultproductouter sto_bn_grid_lookup_resultproductouter sto_cp_grid_lookup_resultproductouter sto_cn_grid_lookup_resultproductouter. (((((dfg_first_grid_lookup_result) = 2 * (sto_ap_grid_lookup_resultproductouter) /\ (sto_an_grid_lookup_resultproductouter) = 0) \/ exists ge_signed_half_grid_lookup_resultproductouterleft. (((dfg_first_grid_lookup_result) = 2 * ge_signed_half_grid_lookup_resultproductouterleft + 1 /\ (sto_ap_grid_lookup_resultproductouter) = 0) /\ (sto_an_grid_lookup_resultproductouter) = S ge_signed_half_grid_lookup_resultproductouterleft))) /\ ((((((dfg_inner_grid_lookup_resultproduct) = 2 * (sto_bp_grid_lookup_resultproductouter) /\ (sto_bn_grid_lookup_resultproductouter) = 0) \/ exists ge_signed_half_grid_lookup_resultproductouterright. (((dfg_inner_grid_lookup_resultproduct) = 2 * ge_signed_half_grid_lookup_resultproductouterright + 1 /\ (sto_bp_grid_lookup_resultproductouter) = 0) /\ (sto_bn_grid_lookup_resultproductouter) = S ge_signed_half_grid_lookup_resultproductouterright))) /\ ((((((z) = 2 * (sto_cp_grid_lookup_resultproductouter) /\ (sto_cn_grid_lookup_resultproductouter) = 0) \/ exists ge_signed_half_grid_lookup_resultproductouteroutput. (((z) = 2 * ge_signed_half_grid_lookup_resultproductouteroutput + 1 /\ (sto_cp_grid_lookup_resultproductouter) = 0) /\ (sto_cn_grid_lookup_resultproductouter) = S ge_signed_half_grid_lookup_resultproductouteroutput))) /\ ((sto_ap_grid_lookup_resultproductouter * sto_bp_grid_lookup_resultproductouter + sto_an_grid_lookup_resultproductouter * sto_bn_grid_lookup_resultproductouter) + sto_cn_grid_lookup_resultproductouter = (sto_ap_grid_lookup_resultproductouter * sto_bn_grid_lookup_resultproductouter + sto_an_grid_lookup_resultproductouter * sto_bp_grid_lookup_resultproductouter) + sto_cp_grid_lookup_resultproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_grid_lookup_resultomittednondivisor. (n) = ((a)*(e)) * pvs_factor_grid_lookup_resultomittednondivisor))) /\ ((z)=0))))