dirichlet_grid_from_flat_prefix

Exact expanded first-order arithmetic statement

forall F G H n T. (((exists dst_positive_code_grid_sourcetable dst_positive_scale_grid_sourcetable dst_negative_code_grid_sourcetable dst_negative_scale_grid_sourcetable. (((T) = (((((dst_positive_code_grid_sourcetable) + (dst_positive_scale_grid_sourcetable)) * S ((dst_positive_code_grid_sourcetable) + (dst_positive_scale_grid_sourcetable)) + ((dst_positive_scale_grid_sourcetable) + (dst_positive_scale_grid_sourcetable))) + (((dst_negative_code_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)) * S ((dst_negative_code_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)) + ((dst_negative_scale_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)))) * S ((((dst_positive_code_grid_sourcetable) + (dst_positive_scale_grid_sourcetable)) * S ((dst_positive_code_grid_sourcetable) + (dst_positive_scale_grid_sourcetable)) + ((dst_positive_scale_grid_sourcetable) + (dst_positive_scale_grid_sourcetable))) + (((dst_negative_code_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)) * S ((dst_negative_code_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)) + ((dst_negative_scale_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)))) + ((((dst_negative_code_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)) * S ((dst_negative_code_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)) + ((dst_negative_scale_grid_sourcetable) + (dst_negative_scale_grid_sourcetable))) + (((dst_negative_code_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)) * S ((dst_negative_code_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)) + ((dst_negative_scale_grid_sourcetable) + (dst_negative_scale_grid_sourcetable)))))) /\ (forall dst_index_grid_sourcetable. (exists pvs_le_gap_grid_sourcetabledomain. pvs_le_gap_grid_sourcetabledomain + (dst_index_grid_sourcetable) = ((S n)*(S n))) -> exists dst_positive_grid_sourcetable dst_negative_grid_sourcetable dst_value_grid_sourcetable. ((((exists ff_h_pvs_grid_sourcetableentrypositive. ff_h_pvs_grid_sourcetableentrypositive + S (dst_positive_grid_sourcetable) = S ((S (dst_index_grid_sourcetable)) * dst_positive_scale_grid_sourcetable)) /\ exists ff_q_pvs_grid_sourcetableentrypositive. dst_positive_code_grid_sourcetable = ff_q_pvs_grid_sourcetableentrypositive * S ((S (dst_index_grid_sourcetable)) * dst_positive_scale_grid_sourcetable) + (dst_positive_grid_sourcetable))) /\ (((((exists ff_h_pvs_grid_sourcetableentrynegative. ff_h_pvs_grid_sourcetableentrynegative + S (dst_negative_grid_sourcetable) = S ((S (dst_index_grid_sourcetable)) * dst_negative_scale_grid_sourcetable)) /\ exists ff_q_pvs_grid_sourcetableentrynegative. dst_negative_code_grid_sourcetable = ff_q_pvs_grid_sourcetableentrynegative * S ((S (dst_index_grid_sourcetable)) * dst_negative_scale_grid_sourcetable) + (dst_negative_grid_sourcetable))) /\ (exists ge_balance_positive_grid_sourcetableentryvalue ge_balance_negative_grid_sourcetableentryvalue. (((((dst_value_grid_sourcetable) = 2 * (ge_balance_positive_grid_sourcetableentryvalue) /\ (ge_balance_negative_grid_sourcetableentryvalue) = 0) \/ exists ge_signed_half_grid_sourcetableentryvaluedecode. (((dst_value_grid_sourcetable) = 2 * ge_signed_half_grid_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_grid_sourcetableentryvalue) = 0) /\ (ge_balance_negative_grid_sourcetableentryvalue) = S ge_signed_half_grid_sourcetableentryvaluedecode))) /\ ((dst_positive_grid_sourcetable) + ge_balance_negative_grid_sourcetableentryvalue = (dst_negative_grid_sourcetable) + ge_balance_positive_grid_sourcetableentryvalue))))))))) /\ (forall dfg_flat_index_grid_source dfg_flat_value_grid_source. (exists pvs_le_gap_grid_sourcebound. pvs_le_gap_grid_sourcebound + (dfg_flat_index_grid_source) = ((S n)*(S n))) -> (exists dst_positive_code_grid_sourcelookup dst_positive_scale_grid_sourcelookup dst_negative_code_grid_sourcelookup dst_negative_scale_grid_sourcelookup dst_positive_grid_sourcelookup dst_negative_grid_sourcelookup. (((T) = (((((dst_positive_code_grid_sourcelookup) + (dst_positive_scale_grid_sourcelookup)) * S ((dst_positive_code_grid_sourcelookup) + (dst_positive_scale_grid_sourcelookup)) + ((dst_positive_scale_grid_sourcelookup) + (dst_positive_scale_grid_sourcelookup))) + (((dst_negative_code_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)) * S ((dst_negative_code_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)) + ((dst_negative_scale_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)))) * S ((((dst_positive_code_grid_sourcelookup) + (dst_positive_scale_grid_sourcelookup)) * S ((dst_positive_code_grid_sourcelookup) + (dst_positive_scale_grid_sourcelookup)) + ((dst_positive_scale_grid_sourcelookup) + (dst_positive_scale_grid_sourcelookup))) + (((dst_negative_code_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)) * S ((dst_negative_code_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)) + ((dst_negative_scale_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)))) + ((((dst_negative_code_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)) * S ((dst_negative_code_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)) + ((dst_negative_scale_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup))) + (((dst_negative_code_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)) * S ((dst_negative_code_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)) + ((dst_negative_scale_grid_sourcelookup) + (dst_negative_scale_grid_sourcelookup)))))) /\ (((((exists ff_h_pvs_grid_sourcelookuppositive. ff_h_pvs_grid_sourcelookuppositive + S (dst_positive_grid_sourcelookup) = S ((S (dfg_flat_index_grid_source)) * dst_positive_scale_grid_sourcelookup)) /\ exists ff_q_pvs_grid_sourcelookuppositive. dst_positive_code_grid_sourcelookup = ff_q_pvs_grid_sourcelookuppositive * S ((S (dfg_flat_index_grid_source)) * dst_positive_scale_grid_sourcelookup) + (dst_positive_grid_sourcelookup))) /\ (((((exists ff_h_pvs_grid_sourcelookupnegative. ff_h_pvs_grid_sourcelookupnegative + S (dst_negative_grid_sourcelookup) = S ((S (dfg_flat_index_grid_source)) * dst_negative_scale_grid_sourcelookup)) /\ exists ff_q_pvs_grid_sourcelookupnegative. dst_negative_code_grid_sourcelookup = ff_q_pvs_grid_sourcelookupnegative * S ((S (dfg_flat_index_grid_source)) * dst_negative_scale_grid_sourcelookup) + (dst_negative_grid_sourcelookup))) /\ (exists ge_balance_positive_grid_sourcelookupvalue ge_balance_negative_grid_sourcelookupvalue. (((((dfg_flat_value_grid_source) = 2 * (ge_balance_positive_grid_sourcelookupvalue) /\ (ge_balance_negative_grid_sourcelookupvalue) = 0) \/ exists ge_signed_half_grid_sourcelookupvaluedecode. (((dfg_flat_value_grid_source) = 2 * ge_signed_half_grid_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_grid_sourcelookupvalue) = 0) /\ (ge_balance_negative_grid_sourcelookupvalue) = S ge_signed_half_grid_sourcelookupvaluedecode))) /\ ((dst_positive_grid_sourcelookup) + ge_balance_negative_grid_sourcelookupvalue = (dst_negative_grid_sourcelookup) + ge_balance_positive_grid_sourcelookupvalue))))))))) -> (exists dfg_flat_row_grid_sourceentry dfg_flat_column_grid_sourceentry. (((dfg_flat_index_grid_source)=((S (n))*(dfg_flat_row_grid_sourceentry)+(dfg_flat_column_grid_sourceentry))) /\ (((exists pvs_gap_grid_sourceentryremainder. pvs_gap_grid_sourceentryremainder + S (dfg_flat_column_grid_sourceentry) = (S (n))) /\ ((((~((dfg_flat_row_grid_sourceentry)=0)) /\ (((~((dfg_flat_column_grid_sourceentry)=0)) /\ (exists dfg_middle_grid_sourceentrycell dfg_first_grid_sourceentrycell dfg_last_grid_sourceentrycell dfg_value_grid_sourceentrycell. (((n)=((dfg_flat_row_grid_sourceentry)*(dfg_flat_column_grid_sourceentry))*dfg_middle_grid_sourceentrycell) /\ (((exists dst_positive_code_grid_sourceentrycellfirst dst_positive_scale_grid_sourceentrycellfirst dst_negative_code_grid_sourceentrycellfirst dst_negative_scale_grid_sourceentrycellfirst dst_positive_grid_sourceentrycellfirst dst_negative_grid_sourceentrycellfirst. (((F) = (((((dst_positive_code_grid_sourceentrycellfirst) + (dst_positive_scale_grid_sourceentrycellfirst)) * S ((dst_positive_code_grid_sourceentrycellfirst) + (dst_positive_scale_grid_sourceentrycellfirst)) + ((dst_positive_scale_grid_sourceentrycellfirst) + (dst_positive_scale_grid_sourceentrycellfirst))) + (((dst_negative_code_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)) * S ((dst_negative_code_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)) + ((dst_negative_scale_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)))) * S ((((dst_positive_code_grid_sourceentrycellfirst) + (dst_positive_scale_grid_sourceentrycellfirst)) * S ((dst_positive_code_grid_sourceentrycellfirst) + (dst_positive_scale_grid_sourceentrycellfirst)) + ((dst_positive_scale_grid_sourceentrycellfirst) + (dst_positive_scale_grid_sourceentrycellfirst))) + (((dst_negative_code_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)) * S ((dst_negative_code_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)) + ((dst_negative_scale_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)))) + ((((dst_negative_code_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)) * S ((dst_negative_code_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)) + ((dst_negative_scale_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst))) + (((dst_negative_code_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)) * S ((dst_negative_code_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)) + ((dst_negative_scale_grid_sourceentrycellfirst) + (dst_negative_scale_grid_sourceentrycellfirst)))))) /\ (((((exists ff_h_pvs_grid_sourceentrycellfirstpositive. ff_h_pvs_grid_sourceentrycellfirstpositive + S (dst_positive_grid_sourceentrycellfirst) = S ((S (dfg_flat_row_grid_sourceentry)) * dst_positive_scale_grid_sourceentrycellfirst)) /\ exists ff_q_pvs_grid_sourceentrycellfirstpositive. dst_positive_code_grid_sourceentrycellfirst = ff_q_pvs_grid_sourceentrycellfirstpositive * S ((S (dfg_flat_row_grid_sourceentry)) * dst_positive_scale_grid_sourceentrycellfirst) + (dst_positive_grid_sourceentrycellfirst))) /\ (((((exists ff_h_pvs_grid_sourceentrycellfirstnegative. ff_h_pvs_grid_sourceentrycellfirstnegative + S (dst_negative_grid_sourceentrycellfirst) = S ((S (dfg_flat_row_grid_sourceentry)) * dst_negative_scale_grid_sourceentrycellfirst)) /\ exists ff_q_pvs_grid_sourceentrycellfirstnegative. dst_negative_code_grid_sourceentrycellfirst = ff_q_pvs_grid_sourceentrycellfirstnegative * S ((S (dfg_flat_row_grid_sourceentry)) * dst_negative_scale_grid_sourceentrycellfirst) + (dst_negative_grid_sourceentrycellfirst))) /\ (exists ge_balance_positive_grid_sourceentrycellfirstvalue ge_balance_negative_grid_sourceentrycellfirstvalue. (((((dfg_first_grid_sourceentrycell) = 2 * (ge_balance_positive_grid_sourceentrycellfirstvalue) /\ (ge_balance_negative_grid_sourceentrycellfirstvalue) = 0) \/ exists ge_signed_half_grid_sourceentrycellfirstvaluedecode. (((dfg_first_grid_sourceentrycell) = 2 * ge_signed_half_grid_sourceentrycellfirstvaluedecode + 1 /\ (ge_balance_positive_grid_sourceentrycellfirstvalue) = 0) /\ (ge_balance_negative_grid_sourceentrycellfirstvalue) = S ge_signed_half_grid_sourceentrycellfirstvaluedecode))) /\ ((dst_positive_grid_sourceentrycellfirst) + ge_balance_negative_grid_sourceentrycellfirstvalue = (dst_negative_grid_sourceentrycellfirst) + ge_balance_positive_grid_sourceentrycellfirstvalue))))))))) /\ (((exists dst_positive_code_grid_sourceentrycelllast dst_positive_scale_grid_sourceentrycelllast dst_negative_code_grid_sourceentrycelllast dst_negative_scale_grid_sourceentrycelllast dst_positive_grid_sourceentrycelllast dst_negative_grid_sourceentrycelllast. (((H) = (((((dst_positive_code_grid_sourceentrycelllast) + (dst_positive_scale_grid_sourceentrycelllast)) * S ((dst_positive_code_grid_sourceentrycelllast) + (dst_positive_scale_grid_sourceentrycelllast)) + ((dst_positive_scale_grid_sourceentrycelllast) + (dst_positive_scale_grid_sourceentrycelllast))) + (((dst_negative_code_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)) * S ((dst_negative_code_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)) + ((dst_negative_scale_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)))) * S ((((dst_positive_code_grid_sourceentrycelllast) + (dst_positive_scale_grid_sourceentrycelllast)) * S ((dst_positive_code_grid_sourceentrycelllast) + (dst_positive_scale_grid_sourceentrycelllast)) + ((dst_positive_scale_grid_sourceentrycelllast) + (dst_positive_scale_grid_sourceentrycelllast))) + (((dst_negative_code_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)) * S ((dst_negative_code_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)) + ((dst_negative_scale_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)))) + ((((dst_negative_code_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)) * S ((dst_negative_code_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)) + ((dst_negative_scale_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast))) + (((dst_negative_code_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)) * S ((dst_negative_code_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)) + ((dst_negative_scale_grid_sourceentrycelllast) + (dst_negative_scale_grid_sourceentrycelllast)))))) /\ (((((exists ff_h_pvs_grid_sourceentrycelllastpositive. ff_h_pvs_grid_sourceentrycelllastpositive + S (dst_positive_grid_sourceentrycelllast) = S ((S (dfg_flat_column_grid_sourceentry)) * dst_positive_scale_grid_sourceentrycelllast)) /\ exists ff_q_pvs_grid_sourceentrycelllastpositive. dst_positive_code_grid_sourceentrycelllast = ff_q_pvs_grid_sourceentrycelllastpositive * S ((S (dfg_flat_column_grid_sourceentry)) * dst_positive_scale_grid_sourceentrycelllast) + (dst_positive_grid_sourceentrycelllast))) /\ (((((exists ff_h_pvs_grid_sourceentrycelllastnegative. ff_h_pvs_grid_sourceentrycelllastnegative + S (dst_negative_grid_sourceentrycelllast) = S ((S (dfg_flat_column_grid_sourceentry)) * dst_negative_scale_grid_sourceentrycelllast)) /\ exists ff_q_pvs_grid_sourceentrycelllastnegative. dst_negative_code_grid_sourceentrycelllast = ff_q_pvs_grid_sourceentrycelllastnegative * S ((S (dfg_flat_column_grid_sourceentry)) * dst_negative_scale_grid_sourceentrycelllast) + (dst_negative_grid_sourceentrycelllast))) /\ (exists ge_balance_positive_grid_sourceentrycelllastvalue ge_balance_negative_grid_sourceentrycelllastvalue. (((((dfg_last_grid_sourceentrycell) = 2 * (ge_balance_positive_grid_sourceentrycelllastvalue) /\ (ge_balance_negative_grid_sourceentrycelllastvalue) = 0) \/ exists ge_signed_half_grid_sourceentrycelllastvaluedecode. (((dfg_last_grid_sourceentrycell) = 2 * ge_signed_half_grid_sourceentrycelllastvaluedecode + 1 /\ (ge_balance_positive_grid_sourceentrycelllastvalue) = 0) /\ (ge_balance_negative_grid_sourceentrycelllastvalue) = S ge_signed_half_grid_sourceentrycelllastvaluedecode))) /\ ((dst_positive_grid_sourceentrycelllast) + ge_balance_negative_grid_sourceentrycelllastvalue = (dst_negative_grid_sourceentrycelllast) + ge_balance_positive_grid_sourceentrycelllastvalue))))))))) /\ (((exists dst_positive_code_grid_sourceentrycellmiddle dst_positive_scale_grid_sourceentrycellmiddle dst_negative_code_grid_sourceentrycellmiddle dst_negative_scale_grid_sourceentrycellmiddle dst_positive_grid_sourceentrycellmiddle dst_negative_grid_sourceentrycellmiddle. (((G) = (((((dst_positive_code_grid_sourceentrycellmiddle) + (dst_positive_scale_grid_sourceentrycellmiddle)) * S ((dst_positive_code_grid_sourceentrycellmiddle) + (dst_positive_scale_grid_sourceentrycellmiddle)) + ((dst_positive_scale_grid_sourceentrycellmiddle) + (dst_positive_scale_grid_sourceentrycellmiddle))) + (((dst_negative_code_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)) * S ((dst_negative_code_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)) + ((dst_negative_scale_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)))) * S ((((dst_positive_code_grid_sourceentrycellmiddle) + (dst_positive_scale_grid_sourceentrycellmiddle)) * S ((dst_positive_code_grid_sourceentrycellmiddle) + (dst_positive_scale_grid_sourceentrycellmiddle)) + ((dst_positive_scale_grid_sourceentrycellmiddle) + (dst_positive_scale_grid_sourceentrycellmiddle))) + (((dst_negative_code_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)) * S ((dst_negative_code_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)) + ((dst_negative_scale_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)))) + ((((dst_negative_code_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)) * S ((dst_negative_code_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)) + ((dst_negative_scale_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle))) + (((dst_negative_code_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)) * S ((dst_negative_code_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)) + ((dst_negative_scale_grid_sourceentrycellmiddle) + (dst_negative_scale_grid_sourceentrycellmiddle)))))) /\ (((((exists ff_h_pvs_grid_sourceentrycellmiddlepositive. ff_h_pvs_grid_sourceentrycellmiddlepositive + S (dst_positive_grid_sourceentrycellmiddle) = S ((S (dfg_middle_grid_sourceentrycell)) * dst_positive_scale_grid_sourceentrycellmiddle)) /\ exists ff_q_pvs_grid_sourceentrycellmiddlepositive. dst_positive_code_grid_sourceentrycellmiddle = ff_q_pvs_grid_sourceentrycellmiddlepositive * S ((S (dfg_middle_grid_sourceentrycell)) * dst_positive_scale_grid_sourceentrycellmiddle) + (dst_positive_grid_sourceentrycellmiddle))) /\ (((((exists ff_h_pvs_grid_sourceentrycellmiddlenegative. ff_h_pvs_grid_sourceentrycellmiddlenegative + S (dst_negative_grid_sourceentrycellmiddle) = S ((S (dfg_middle_grid_sourceentrycell)) * dst_negative_scale_grid_sourceentrycellmiddle)) /\ exists ff_q_pvs_grid_sourceentrycellmiddlenegative. dst_negative_code_grid_sourceentrycellmiddle = ff_q_pvs_grid_sourceentrycellmiddlenegative * S ((S (dfg_middle_grid_sourceentrycell)) * dst_negative_scale_grid_sourceentrycellmiddle) + (dst_negative_grid_sourceentrycellmiddle))) /\ (exists ge_balance_positive_grid_sourceentrycellmiddlevalue ge_balance_negative_grid_sourceentrycellmiddlevalue. (((((dfg_value_grid_sourceentrycell) = 2 * (ge_balance_positive_grid_sourceentrycellmiddlevalue) /\ (ge_balance_negative_grid_sourceentrycellmiddlevalue) = 0) \/ exists ge_signed_half_grid_sourceentrycellmiddlevaluedecode. (((dfg_value_grid_sourceentrycell) = 2 * ge_signed_half_grid_sourceentrycellmiddlevaluedecode + 1 /\ (ge_balance_positive_grid_sourceentrycellmiddlevalue) = 0) /\ (ge_balance_negative_grid_sourceentrycellmiddlevalue) = S ge_signed_half_grid_sourceentrycellmiddlevaluedecode))) /\ ((dst_positive_grid_sourceentrycellmiddle) + ge_balance_negative_grid_sourceentrycellmiddlevalue = (dst_negative_grid_sourceentrycellmiddle) + ge_balance_positive_grid_sourceentrycellmiddlevalue))))))))) /\ (exists dfg_inner_grid_sourceentrycellproduct. ((exists sto_ap_grid_sourceentrycellproductinner sto_an_grid_sourceentrycellproductinner sto_bp_grid_sourceentrycellproductinner sto_bn_grid_sourceentrycellproductinner sto_cp_grid_sourceentrycellproductinner sto_cn_grid_sourceentrycellproductinner. (((((dfg_last_grid_sourceentrycell) = 2 * (sto_ap_grid_sourceentrycellproductinner) /\ (sto_an_grid_sourceentrycellproductinner) = 0) \/ exists ge_signed_half_grid_sourceentrycellproductinnerleft. (((dfg_last_grid_sourceentrycell) = 2 * ge_signed_half_grid_sourceentrycellproductinnerleft + 1 /\ (sto_ap_grid_sourceentrycellproductinner) = 0) /\ (sto_an_grid_sourceentrycellproductinner) = S ge_signed_half_grid_sourceentrycellproductinnerleft))) /\ ((((((dfg_value_grid_sourceentrycell) = 2 * (sto_bp_grid_sourceentrycellproductinner) /\ (sto_bn_grid_sourceentrycellproductinner) = 0) \/ exists ge_signed_half_grid_sourceentrycellproductinnerright. (((dfg_value_grid_sourceentrycell) = 2 * ge_signed_half_grid_sourceentrycellproductinnerright + 1 /\ (sto_bp_grid_sourceentrycellproductinner) = 0) /\ (sto_bn_grid_sourceentrycellproductinner) = S ge_signed_half_grid_sourceentrycellproductinnerright))) /\ ((((((dfg_inner_grid_sourceentrycellproduct) = 2 * (sto_cp_grid_sourceentrycellproductinner) /\ (sto_cn_grid_sourceentrycellproductinner) = 0) \/ exists ge_signed_half_grid_sourceentrycellproductinneroutput. (((dfg_inner_grid_sourceentrycellproduct) = 2 * ge_signed_half_grid_sourceentrycellproductinneroutput + 1 /\ (sto_cp_grid_sourceentrycellproductinner) = 0) /\ (sto_cn_grid_sourceentrycellproductinner) = S ge_signed_half_grid_sourceentrycellproductinneroutput))) /\ ((sto_ap_grid_sourceentrycellproductinner * sto_bp_grid_sourceentrycellproductinner + sto_an_grid_sourceentrycellproductinner * sto_bn_grid_sourceentrycellproductinner) + sto_cn_grid_sourceentrycellproductinner = (sto_ap_grid_sourceentrycellproductinner * sto_bn_grid_sourceentrycellproductinner + sto_an_grid_sourceentrycellproductinner * sto_bp_grid_sourceentrycellproductinner) + sto_cp_grid_sourceentrycellproductinner))))))) /\ (exists sto_ap_grid_sourceentrycellproductouter sto_an_grid_sourceentrycellproductouter sto_bp_grid_sourceentrycellproductouter sto_bn_grid_sourceentrycellproductouter sto_cp_grid_sourceentrycellproductouter sto_cn_grid_sourceentrycellproductouter. (((((dfg_first_grid_sourceentrycell) = 2 * (sto_ap_grid_sourceentrycellproductouter) /\ (sto_an_grid_sourceentrycellproductouter) = 0) \/ exists ge_signed_half_grid_sourceentrycellproductouterleft. (((dfg_first_grid_sourceentrycell) = 2 * ge_signed_half_grid_sourceentrycellproductouterleft + 1 /\ (sto_ap_grid_sourceentrycellproductouter) = 0) /\ (sto_an_grid_sourceentrycellproductouter) = S ge_signed_half_grid_sourceentrycellproductouterleft))) /\ ((((((dfg_inner_grid_sourceentrycellproduct) = 2 * (sto_bp_grid_sourceentrycellproductouter) /\ (sto_bn_grid_sourceentrycellproductouter) = 0) \/ exists ge_signed_half_grid_sourceentrycellproductouterright. (((dfg_inner_grid_sourceentrycellproduct) = 2 * ge_signed_half_grid_sourceentrycellproductouterright + 1 /\ (sto_bp_grid_sourceentrycellproductouter) = 0) /\ (sto_bn_grid_sourceentrycellproductouter) = S ge_signed_half_grid_sourceentrycellproductouterright))) /\ ((((((dfg_flat_value_grid_source) = 2 * (sto_cp_grid_sourceentrycellproductouter) /\ (sto_cn_grid_sourceentrycellproductouter) = 0) \/ exists ge_signed_half_grid_sourceentrycellproductouteroutput. (((dfg_flat_value_grid_source) = 2 * ge_signed_half_grid_sourceentrycellproductouteroutput + 1 /\ (sto_cp_grid_sourceentrycellproductouter) = 0) /\ (sto_cn_grid_sourceentrycellproductouter) = S ge_signed_half_grid_sourceentrycellproductouteroutput))) /\ ((sto_ap_grid_sourceentrycellproductouter * sto_bp_grid_sourceentrycellproductouter + sto_an_grid_sourceentrycellproductouter * sto_bn_grid_sourceentrycellproductouter) + sto_cn_grid_sourceentrycellproductouter = (sto_ap_grid_sourceentrycellproductouter * sto_bn_grid_sourceentrycellproductouter + sto_an_grid_sourceentrycellproductouter * sto_bp_grid_sourceentrycellproductouter) + sto_cp_grid_sourceentrycellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_grid_sourceentry)=0 \/ ((dfg_flat_column_grid_sourceentry)=0 \/ ~(exists pvs_factor_grid_sourceentrycellomittednondivisor. (n) = ((dfg_flat_row_grid_sourceentry)*(dfg_flat_column_grid_sourceentry)) * pvs_factor_grid_sourceentrycellomittednondivisor))) /\ ((dfg_flat_value_grid_source)=0))))))))))) -> (((exists dst_positive_code_grid_resulttable dst_positive_scale_grid_resulttable dst_negative_code_grid_resulttable dst_negative_scale_grid_resulttable. (((T) = (((((dst_positive_code_grid_resulttable) + (dst_positive_scale_grid_resulttable)) * S ((dst_positive_code_grid_resulttable) + (dst_positive_scale_grid_resulttable)) + ((dst_positive_scale_grid_resulttable) + (dst_positive_scale_grid_resulttable))) + (((dst_negative_code_grid_resulttable) + (dst_negative_scale_grid_resulttable)) * S ((dst_negative_code_grid_resulttable) + (dst_negative_scale_grid_resulttable)) + ((dst_negative_scale_grid_resulttable) + (dst_negative_scale_grid_resulttable)))) * S ((((dst_positive_code_grid_resulttable) + (dst_positive_scale_grid_resulttable)) * S ((dst_positive_code_grid_resulttable) + (dst_positive_scale_grid_resulttable)) + ((dst_positive_scale_grid_resulttable) + (dst_positive_scale_grid_resulttable))) + (((dst_negative_code_grid_resulttable) + (dst_negative_scale_grid_resulttable)) * S ((dst_negative_code_grid_resulttable) + (dst_negative_scale_grid_resulttable)) + ((dst_negative_scale_grid_resulttable) + (dst_negative_scale_grid_resulttable)))) + ((((dst_negative_code_grid_resulttable) + (dst_negative_scale_grid_resulttable)) * S ((dst_negative_code_grid_resulttable) + (dst_negative_scale_grid_resulttable)) + ((dst_negative_scale_grid_resulttable) + (dst_negative_scale_grid_resulttable))) + (((dst_negative_code_grid_resulttable) + (dst_negative_scale_grid_resulttable)) * S ((dst_negative_code_grid_resulttable) + (dst_negative_scale_grid_resulttable)) + ((dst_negative_scale_grid_resulttable) + (dst_negative_scale_grid_resulttable)))))) /\ (forall dst_index_grid_resulttable. (exists pvs_le_gap_grid_resulttabledomain. pvs_le_gap_grid_resulttabledomain + (dst_index_grid_resulttable) = ((S (n))*(S (n)))) -> exists dst_positive_grid_resulttable dst_negative_grid_resulttable dst_value_grid_resulttable. ((((exists ff_h_pvs_grid_resulttableentrypositive. ff_h_pvs_grid_resulttableentrypositive + S (dst_positive_grid_resulttable) = S ((S (dst_index_grid_resulttable)) * dst_positive_scale_grid_resulttable)) /\ exists ff_q_pvs_grid_resulttableentrypositive. dst_positive_code_grid_resulttable = ff_q_pvs_grid_resulttableentrypositive * S ((S (dst_index_grid_resulttable)) * dst_positive_scale_grid_resulttable) + (dst_positive_grid_resulttable))) /\ (((((exists ff_h_pvs_grid_resulttableentrynegative. ff_h_pvs_grid_resulttableentrynegative + S (dst_negative_grid_resulttable) = S ((S (dst_index_grid_resulttable)) * dst_negative_scale_grid_resulttable)) /\ exists ff_q_pvs_grid_resulttableentrynegative. dst_negative_code_grid_resulttable = ff_q_pvs_grid_resulttableentrynegative * S ((S (dst_index_grid_resulttable)) * dst_negative_scale_grid_resulttable) + (dst_negative_grid_resulttable))) /\ (exists ge_balance_positive_grid_resulttableentryvalue ge_balance_negative_grid_resulttableentryvalue. (((((dst_value_grid_resulttable) = 2 * (ge_balance_positive_grid_resulttableentryvalue) /\ (ge_balance_negative_grid_resulttableentryvalue) = 0) \/ exists ge_signed_half_grid_resulttableentryvaluedecode. (((dst_value_grid_resulttable) = 2 * ge_signed_half_grid_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_grid_resulttableentryvalue) = 0) /\ (ge_balance_negative_grid_resulttableentryvalue) = S ge_signed_half_grid_resulttableentryvaluedecode))) /\ ((dst_positive_grid_resulttable) + ge_balance_negative_grid_resulttableentryvalue = (dst_negative_grid_resulttable) + ge_balance_positive_grid_resulttableentryvalue))))))))) /\ (forall dfg_grid_row_grid_result dfg_grid_column_grid_result dfg_grid_value_grid_result. (exists pvs_le_gap_grid_resultrow. pvs_le_gap_grid_resultrow + (dfg_grid_row_grid_result) = (n)) -> (exists pvs_le_gap_grid_resultcolumn. pvs_le_gap_grid_resultcolumn + (dfg_grid_column_grid_result) = (n)) -> (exists dst_positive_code_grid_resultlookup dst_positive_scale_grid_resultlookup dst_negative_code_grid_resultlookup dst_negative_scale_grid_resultlookup dst_positive_grid_resultlookup dst_negative_grid_resultlookup. (((T) = (((((dst_positive_code_grid_resultlookup) + (dst_positive_scale_grid_resultlookup)) * S ((dst_positive_code_grid_resultlookup) + (dst_positive_scale_grid_resultlookup)) + ((dst_positive_scale_grid_resultlookup) + (dst_positive_scale_grid_resultlookup))) + (((dst_negative_code_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)) * S ((dst_negative_code_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)) + ((dst_negative_scale_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)))) * S ((((dst_positive_code_grid_resultlookup) + (dst_positive_scale_grid_resultlookup)) * S ((dst_positive_code_grid_resultlookup) + (dst_positive_scale_grid_resultlookup)) + ((dst_positive_scale_grid_resultlookup) + (dst_positive_scale_grid_resultlookup))) + (((dst_negative_code_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)) * S ((dst_negative_code_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)) + ((dst_negative_scale_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)))) + ((((dst_negative_code_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)) * S ((dst_negative_code_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)) + ((dst_negative_scale_grid_resultlookup) + (dst_negative_scale_grid_resultlookup))) + (((dst_negative_code_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)) * S ((dst_negative_code_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)) + ((dst_negative_scale_grid_resultlookup) + (dst_negative_scale_grid_resultlookup)))))) /\ (((((exists ff_h_pvs_grid_resultlookuppositive. ff_h_pvs_grid_resultlookuppositive + S (dst_positive_grid_resultlookup) = S ((S ((S (n))*(dfg_grid_row_grid_result)+(dfg_grid_column_grid_result))) * dst_positive_scale_grid_resultlookup)) /\ exists ff_q_pvs_grid_resultlookuppositive. dst_positive_code_grid_resultlookup = ff_q_pvs_grid_resultlookuppositive * S ((S ((S (n))*(dfg_grid_row_grid_result)+(dfg_grid_column_grid_result))) * dst_positive_scale_grid_resultlookup) + (dst_positive_grid_resultlookup))) /\ (((((exists ff_h_pvs_grid_resultlookupnegative. ff_h_pvs_grid_resultlookupnegative + S (dst_negative_grid_resultlookup) = S ((S ((S (n))*(dfg_grid_row_grid_result)+(dfg_grid_column_grid_result))) * dst_negative_scale_grid_resultlookup)) /\ exists ff_q_pvs_grid_resultlookupnegative. dst_negative_code_grid_resultlookup = ff_q_pvs_grid_resultlookupnegative * S ((S ((S (n))*(dfg_grid_row_grid_result)+(dfg_grid_column_grid_result))) * dst_negative_scale_grid_resultlookup) + (dst_negative_grid_resultlookup))) /\ (exists ge_balance_positive_grid_resultlookupvalue ge_balance_negative_grid_resultlookupvalue. (((((dfg_grid_value_grid_result) = 2 * (ge_balance_positive_grid_resultlookupvalue) /\ (ge_balance_negative_grid_resultlookupvalue) = 0) \/ exists ge_signed_half_grid_resultlookupvaluedecode. (((dfg_grid_value_grid_result) = 2 * ge_signed_half_grid_resultlookupvaluedecode + 1 /\ (ge_balance_positive_grid_resultlookupvalue) = 0) /\ (ge_balance_negative_grid_resultlookupvalue) = S ge_signed_half_grid_resultlookupvaluedecode))) /\ ((dst_positive_grid_resultlookup) + ge_balance_negative_grid_resultlookupvalue = (dst_negative_grid_resultlookup) + ge_balance_positive_grid_resultlookupvalue))))))))) -> ((((~((dfg_grid_row_grid_result)=0)) /\ (((~((dfg_grid_column_grid_result)=0)) /\ (exists dfg_middle_grid_resultentry dfg_first_grid_resultentry dfg_last_grid_resultentry dfg_value_grid_resultentry. (((n)=((dfg_grid_row_grid_result)*(dfg_grid_column_grid_result))*dfg_middle_grid_resultentry) /\ (((exists dst_positive_code_grid_resultentryfirst dst_positive_scale_grid_resultentryfirst dst_negative_code_grid_resultentryfirst dst_negative_scale_grid_resultentryfirst dst_positive_grid_resultentryfirst dst_negative_grid_resultentryfirst. (((F) = (((((dst_positive_code_grid_resultentryfirst) + (dst_positive_scale_grid_resultentryfirst)) * S ((dst_positive_code_grid_resultentryfirst) + (dst_positive_scale_grid_resultentryfirst)) + ((dst_positive_scale_grid_resultentryfirst) + (dst_positive_scale_grid_resultentryfirst))) + (((dst_negative_code_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)) * S ((dst_negative_code_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)) + ((dst_negative_scale_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)))) * S ((((dst_positive_code_grid_resultentryfirst) + (dst_positive_scale_grid_resultentryfirst)) * S ((dst_positive_code_grid_resultentryfirst) + (dst_positive_scale_grid_resultentryfirst)) + ((dst_positive_scale_grid_resultentryfirst) + (dst_positive_scale_grid_resultentryfirst))) + (((dst_negative_code_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)) * S ((dst_negative_code_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)) + ((dst_negative_scale_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)))) + ((((dst_negative_code_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)) * S ((dst_negative_code_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)) + ((dst_negative_scale_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst))) + (((dst_negative_code_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)) * S ((dst_negative_code_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)) + ((dst_negative_scale_grid_resultentryfirst) + (dst_negative_scale_grid_resultentryfirst)))))) /\ (((((exists ff_h_pvs_grid_resultentryfirstpositive. ff_h_pvs_grid_resultentryfirstpositive + S (dst_positive_grid_resultentryfirst) = S ((S (dfg_grid_row_grid_result)) * dst_positive_scale_grid_resultentryfirst)) /\ exists ff_q_pvs_grid_resultentryfirstpositive. dst_positive_code_grid_resultentryfirst = ff_q_pvs_grid_resultentryfirstpositive * S ((S (dfg_grid_row_grid_result)) * dst_positive_scale_grid_resultentryfirst) + (dst_positive_grid_resultentryfirst))) /\ (((((exists ff_h_pvs_grid_resultentryfirstnegative. ff_h_pvs_grid_resultentryfirstnegative + S (dst_negative_grid_resultentryfirst) = S ((S (dfg_grid_row_grid_result)) * dst_negative_scale_grid_resultentryfirst)) /\ exists ff_q_pvs_grid_resultentryfirstnegative. dst_negative_code_grid_resultentryfirst = ff_q_pvs_grid_resultentryfirstnegative * S ((S (dfg_grid_row_grid_result)) * dst_negative_scale_grid_resultentryfirst) + (dst_negative_grid_resultentryfirst))) /\ (exists ge_balance_positive_grid_resultentryfirstvalue ge_balance_negative_grid_resultentryfirstvalue. (((((dfg_first_grid_resultentry) = 2 * (ge_balance_positive_grid_resultentryfirstvalue) /\ (ge_balance_negative_grid_resultentryfirstvalue) = 0) \/ exists ge_signed_half_grid_resultentryfirstvaluedecode. (((dfg_first_grid_resultentry) = 2 * ge_signed_half_grid_resultentryfirstvaluedecode + 1 /\ (ge_balance_positive_grid_resultentryfirstvalue) = 0) /\ (ge_balance_negative_grid_resultentryfirstvalue) = S ge_signed_half_grid_resultentryfirstvaluedecode))) /\ ((dst_positive_grid_resultentryfirst) + ge_balance_negative_grid_resultentryfirstvalue = (dst_negative_grid_resultentryfirst) + ge_balance_positive_grid_resultentryfirstvalue))))))))) /\ (((exists dst_positive_code_grid_resultentrylast dst_positive_scale_grid_resultentrylast dst_negative_code_grid_resultentrylast dst_negative_scale_grid_resultentrylast dst_positive_grid_resultentrylast dst_negative_grid_resultentrylast. (((H) = (((((dst_positive_code_grid_resultentrylast) + (dst_positive_scale_grid_resultentrylast)) * S ((dst_positive_code_grid_resultentrylast) + (dst_positive_scale_grid_resultentrylast)) + ((dst_positive_scale_grid_resultentrylast) + (dst_positive_scale_grid_resultentrylast))) + (((dst_negative_code_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)) * S ((dst_negative_code_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)) + ((dst_negative_scale_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)))) * S ((((dst_positive_code_grid_resultentrylast) + (dst_positive_scale_grid_resultentrylast)) * S ((dst_positive_code_grid_resultentrylast) + (dst_positive_scale_grid_resultentrylast)) + ((dst_positive_scale_grid_resultentrylast) + (dst_positive_scale_grid_resultentrylast))) + (((dst_negative_code_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)) * S ((dst_negative_code_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)) + ((dst_negative_scale_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)))) + ((((dst_negative_code_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)) * S ((dst_negative_code_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)) + ((dst_negative_scale_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast))) + (((dst_negative_code_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)) * S ((dst_negative_code_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)) + ((dst_negative_scale_grid_resultentrylast) + (dst_negative_scale_grid_resultentrylast)))))) /\ (((((exists ff_h_pvs_grid_resultentrylastpositive. ff_h_pvs_grid_resultentrylastpositive + S (dst_positive_grid_resultentrylast) = S ((S (dfg_grid_column_grid_result)) * dst_positive_scale_grid_resultentrylast)) /\ exists ff_q_pvs_grid_resultentrylastpositive. dst_positive_code_grid_resultentrylast = ff_q_pvs_grid_resultentrylastpositive * S ((S (dfg_grid_column_grid_result)) * dst_positive_scale_grid_resultentrylast) + (dst_positive_grid_resultentrylast))) /\ (((((exists ff_h_pvs_grid_resultentrylastnegative. ff_h_pvs_grid_resultentrylastnegative + S (dst_negative_grid_resultentrylast) = S ((S (dfg_grid_column_grid_result)) * dst_negative_scale_grid_resultentrylast)) /\ exists ff_q_pvs_grid_resultentrylastnegative. dst_negative_code_grid_resultentrylast = ff_q_pvs_grid_resultentrylastnegative * S ((S (dfg_grid_column_grid_result)) * dst_negative_scale_grid_resultentrylast) + (dst_negative_grid_resultentrylast))) /\ (exists ge_balance_positive_grid_resultentrylastvalue ge_balance_negative_grid_resultentrylastvalue. (((((dfg_last_grid_resultentry) = 2 * (ge_balance_positive_grid_resultentrylastvalue) /\ (ge_balance_negative_grid_resultentrylastvalue) = 0) \/ exists ge_signed_half_grid_resultentrylastvaluedecode. (((dfg_last_grid_resultentry) = 2 * ge_signed_half_grid_resultentrylastvaluedecode + 1 /\ (ge_balance_positive_grid_resultentrylastvalue) = 0) /\ (ge_balance_negative_grid_resultentrylastvalue) = S ge_signed_half_grid_resultentrylastvaluedecode))) /\ ((dst_positive_grid_resultentrylast) + ge_balance_negative_grid_resultentrylastvalue = (dst_negative_grid_resultentrylast) + ge_balance_positive_grid_resultentrylastvalue))))))))) /\ (((exists dst_positive_code_grid_resultentrymiddle dst_positive_scale_grid_resultentrymiddle dst_negative_code_grid_resultentrymiddle dst_negative_scale_grid_resultentrymiddle dst_positive_grid_resultentrymiddle dst_negative_grid_resultentrymiddle. (((G) = (((((dst_positive_code_grid_resultentrymiddle) + (dst_positive_scale_grid_resultentrymiddle)) * S ((dst_positive_code_grid_resultentrymiddle) + (dst_positive_scale_grid_resultentrymiddle)) + ((dst_positive_scale_grid_resultentrymiddle) + (dst_positive_scale_grid_resultentrymiddle))) + (((dst_negative_code_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)) * S ((dst_negative_code_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)) + ((dst_negative_scale_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)))) * S ((((dst_positive_code_grid_resultentrymiddle) + (dst_positive_scale_grid_resultentrymiddle)) * S ((dst_positive_code_grid_resultentrymiddle) + (dst_positive_scale_grid_resultentrymiddle)) + ((dst_positive_scale_grid_resultentrymiddle) + (dst_positive_scale_grid_resultentrymiddle))) + (((dst_negative_code_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)) * S ((dst_negative_code_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)) + ((dst_negative_scale_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)))) + ((((dst_negative_code_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)) * S ((dst_negative_code_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)) + ((dst_negative_scale_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle))) + (((dst_negative_code_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)) * S ((dst_negative_code_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)) + ((dst_negative_scale_grid_resultentrymiddle) + (dst_negative_scale_grid_resultentrymiddle)))))) /\ (((((exists ff_h_pvs_grid_resultentrymiddlepositive. ff_h_pvs_grid_resultentrymiddlepositive + S (dst_positive_grid_resultentrymiddle) = S ((S (dfg_middle_grid_resultentry)) * dst_positive_scale_grid_resultentrymiddle)) /\ exists ff_q_pvs_grid_resultentrymiddlepositive. dst_positive_code_grid_resultentrymiddle = ff_q_pvs_grid_resultentrymiddlepositive * S ((S (dfg_middle_grid_resultentry)) * dst_positive_scale_grid_resultentrymiddle) + (dst_positive_grid_resultentrymiddle))) /\ (((((exists ff_h_pvs_grid_resultentrymiddlenegative. ff_h_pvs_grid_resultentrymiddlenegative + S (dst_negative_grid_resultentrymiddle) = S ((S (dfg_middle_grid_resultentry)) * dst_negative_scale_grid_resultentrymiddle)) /\ exists ff_q_pvs_grid_resultentrymiddlenegative. dst_negative_code_grid_resultentrymiddle = ff_q_pvs_grid_resultentrymiddlenegative * S ((S (dfg_middle_grid_resultentry)) * dst_negative_scale_grid_resultentrymiddle) + (dst_negative_grid_resultentrymiddle))) /\ (exists ge_balance_positive_grid_resultentrymiddlevalue ge_balance_negative_grid_resultentrymiddlevalue. (((((dfg_value_grid_resultentry) = 2 * (ge_balance_positive_grid_resultentrymiddlevalue) /\ (ge_balance_negative_grid_resultentrymiddlevalue) = 0) \/ exists ge_signed_half_grid_resultentrymiddlevaluedecode. (((dfg_value_grid_resultentry) = 2 * ge_signed_half_grid_resultentrymiddlevaluedecode + 1 /\ (ge_balance_positive_grid_resultentrymiddlevalue) = 0) /\ (ge_balance_negative_grid_resultentrymiddlevalue) = S ge_signed_half_grid_resultentrymiddlevaluedecode))) /\ ((dst_positive_grid_resultentrymiddle) + ge_balance_negative_grid_resultentrymiddlevalue = (dst_negative_grid_resultentrymiddle) + ge_balance_positive_grid_resultentrymiddlevalue))))))))) /\ (exists dfg_inner_grid_resultentryproduct. ((exists sto_ap_grid_resultentryproductinner sto_an_grid_resultentryproductinner sto_bp_grid_resultentryproductinner sto_bn_grid_resultentryproductinner sto_cp_grid_resultentryproductinner sto_cn_grid_resultentryproductinner. (((((dfg_last_grid_resultentry) = 2 * (sto_ap_grid_resultentryproductinner) /\ (sto_an_grid_resultentryproductinner) = 0) \/ exists ge_signed_half_grid_resultentryproductinnerleft. (((dfg_last_grid_resultentry) = 2 * ge_signed_half_grid_resultentryproductinnerleft + 1 /\ (sto_ap_grid_resultentryproductinner) = 0) /\ (sto_an_grid_resultentryproductinner) = S ge_signed_half_grid_resultentryproductinnerleft))) /\ ((((((dfg_value_grid_resultentry) = 2 * (sto_bp_grid_resultentryproductinner) /\ (sto_bn_grid_resultentryproductinner) = 0) \/ exists ge_signed_half_grid_resultentryproductinnerright. (((dfg_value_grid_resultentry) = 2 * ge_signed_half_grid_resultentryproductinnerright + 1 /\ (sto_bp_grid_resultentryproductinner) = 0) /\ (sto_bn_grid_resultentryproductinner) = S ge_signed_half_grid_resultentryproductinnerright))) /\ ((((((dfg_inner_grid_resultentryproduct) = 2 * (sto_cp_grid_resultentryproductinner) /\ (sto_cn_grid_resultentryproductinner) = 0) \/ exists ge_signed_half_grid_resultentryproductinneroutput. (((dfg_inner_grid_resultentryproduct) = 2 * ge_signed_half_grid_resultentryproductinneroutput + 1 /\ (sto_cp_grid_resultentryproductinner) = 0) /\ (sto_cn_grid_resultentryproductinner) = S ge_signed_half_grid_resultentryproductinneroutput))) /\ ((sto_ap_grid_resultentryproductinner * sto_bp_grid_resultentryproductinner + sto_an_grid_resultentryproductinner * sto_bn_grid_resultentryproductinner) + sto_cn_grid_resultentryproductinner = (sto_ap_grid_resultentryproductinner * sto_bn_grid_resultentryproductinner + sto_an_grid_resultentryproductinner * sto_bp_grid_resultentryproductinner) + sto_cp_grid_resultentryproductinner))))))) /\ (exists sto_ap_grid_resultentryproductouter sto_an_grid_resultentryproductouter sto_bp_grid_resultentryproductouter sto_bn_grid_resultentryproductouter sto_cp_grid_resultentryproductouter sto_cn_grid_resultentryproductouter. (((((dfg_first_grid_resultentry) = 2 * (sto_ap_grid_resultentryproductouter) /\ (sto_an_grid_resultentryproductouter) = 0) \/ exists ge_signed_half_grid_resultentryproductouterleft. (((dfg_first_grid_resultentry) = 2 * ge_signed_half_grid_resultentryproductouterleft + 1 /\ (sto_ap_grid_resultentryproductouter) = 0) /\ (sto_an_grid_resultentryproductouter) = S ge_signed_half_grid_resultentryproductouterleft))) /\ ((((((dfg_inner_grid_resultentryproduct) = 2 * (sto_bp_grid_resultentryproductouter) /\ (sto_bn_grid_resultentryproductouter) = 0) \/ exists ge_signed_half_grid_resultentryproductouterright. (((dfg_inner_grid_resultentryproduct) = 2 * ge_signed_half_grid_resultentryproductouterright + 1 /\ (sto_bp_grid_resultentryproductouter) = 0) /\ (sto_bn_grid_resultentryproductouter) = S ge_signed_half_grid_resultentryproductouterright))) /\ ((((((dfg_grid_value_grid_result) = 2 * (sto_cp_grid_resultentryproductouter) /\ (sto_cn_grid_resultentryproductouter) = 0) \/ exists ge_signed_half_grid_resultentryproductouteroutput. (((dfg_grid_value_grid_result) = 2 * ge_signed_half_grid_resultentryproductouteroutput + 1 /\ (sto_cp_grid_resultentryproductouter) = 0) /\ (sto_cn_grid_resultentryproductouter) = S ge_signed_half_grid_resultentryproductouteroutput))) /\ ((sto_ap_grid_resultentryproductouter * sto_bp_grid_resultentryproductouter + sto_an_grid_resultentryproductouter * sto_bn_grid_resultentryproductouter) + sto_cn_grid_resultentryproductouter = (sto_ap_grid_resultentryproductouter * sto_bn_grid_resultentryproductouter + sto_an_grid_resultentryproductouter * sto_bp_grid_resultentryproductouter) + sto_cp_grid_resultentryproductouter))))))))))))))))))))) \/ ((((dfg_grid_row_grid_result)=0 \/ ((dfg_grid_column_grid_result)=0 \/ ~(exists pvs_factor_grid_resultentryomittednondivisor. (n) = ((dfg_grid_row_grid_result)*(dfg_grid_column_grid_result)) * pvs_factor_grid_resultentryomittednondivisor))) /\ ((dfg_grid_value_grid_result)=0)))))))