dirichlet_grid_table_exists

forall F G H n. (exists dst_positive_code_grid_F dst_positive_scale_grid_F dst_negative_code_grid_F dst_negative_scale_grid_F. (((F) = (((((dst_positive_code_grid_F) + (dst_positive_scale_grid_F)) * S ((dst_positive_code_grid_F) + (dst_positive_scale_grid_F)) + ((dst_positive_scale_grid_F) + (dst_positive_scale_grid_F))) + (((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) * S ((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) + ((dst_negative_scale_grid_F) + (dst_negative_scale_grid_F)))) * S ((((dst_positive_code_grid_F) + (dst_positive_scale_grid_F)) * S ((dst_positive_code_grid_F) + (dst_positive_scale_grid_F)) + ((dst_positive_scale_grid_F) + (dst_positive_scale_grid_F))) + (((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) * S ((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) + ((dst_negative_scale_grid_F) + (dst_negative_scale_grid_F)))) + ((((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) * S ((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) + ((dst_negative_scale_grid_F) + (dst_negative_scale_grid_F))) + (((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) * S ((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) + ((dst_negative_scale_grid_F) + (dst_negative_scale_grid_F)))))) /\ (forall dst_index_grid_F. (exists pvs_le_gap_grid_Fdomain. pvs_le_gap_grid_Fdomain + (dst_index_grid_F) = (0)) -> exists dst_positive_grid_F dst_negative_grid_F dst_value_grid_F. ((((exists ff_h_pvs_grid_Fentrypositive. ff_h_pvs_grid_Fentrypositive + S (dst_positive_grid_F) = S ((S (dst_index_grid_F)) * dst_positive_scale_grid_F)) /\ exists ff_q_pvs_grid_Fentrypositive. dst_positive_code_grid_F = ff_q_pvs_grid_Fentrypositive * S ((S (dst_index_grid_F)) * dst_positive_scale_grid_F) + (dst_positive_grid_F))) /\ (((((exists ff_h_pvs_grid_Fentrynegative. ff_h_pvs_grid_Fentrynegative + S (dst_negative_grid_F) = S ((S (dst_index_grid_F)) * dst_negative_scale_grid_F)) /\ exists ff_q_pvs_grid_Fentrynegative. dst_negative_code_grid_F = ff_q_pvs_grid_Fentrynegative * S ((S (dst_index_grid_F)) * dst_negative_scale_grid_F) + (dst_negative_grid_F))) /\ (exists ge_balance_positive_grid_Fentryvalue ge_balance_negative_grid_Fentryvalue. (((((dst_value_grid_F) = 2 * (ge_balance_positive_grid_Fentryvalue) /\ (ge_balance_negative_grid_Fentryvalue) = 0) \/ exists ge_signed_half_grid_Fentryvaluedecode. (((dst_value_grid_F) = 2 * ge_signed_half_grid_Fentryvaluedecode + 1 /\ (ge_balance_positive_grid_Fentryvalue) = 0) /\ (ge_balance_negative_grid_Fentryvalue) = S ge_signed_half_grid_Fentryvaluedecode))) /\ ((dst_positive_grid_F) + ge_balance_negative_grid_Fentryvalue = (dst_negative_grid_F) + ge_balance_positive_grid_Fentryvalue))))))))) -> (exists dst_positive_code_grid_G dst_positive_scale_grid_G dst_negative_code_grid_G dst_negative_scale_grid_G. (((G) = (((((dst_positive_code_grid_G) + (dst_positive_scale_grid_G)) * S ((dst_positive_code_grid_G) + (dst_positive_scale_grid_G)) + ((dst_positive_scale_grid_G) + (dst_positive_scale_grid_G))) + (((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) * S ((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) + ((dst_negative_scale_grid_G) + (dst_negative_scale_grid_G)))) * S ((((dst_positive_code_grid_G) + (dst_positive_scale_grid_G)) * S ((dst_positive_code_grid_G) + (dst_positive_scale_grid_G)) + ((dst_positive_scale_grid_G) + (dst_positive_scale_grid_G))) + (((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) * S ((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) + ((dst_negative_scale_grid_G) + (dst_negative_scale_grid_G)))) + ((((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) * S ((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) + ((dst_negative_scale_grid_G) + (dst_negative_scale_grid_G))) + (((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) * S ((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) + ((dst_negative_scale_grid_G) + (dst_negative_scale_grid_G)))))) /\ (forall dst_index_grid_G. (exists pvs_le_gap_grid_Gdomain. pvs_le_gap_grid_Gdomain + (dst_index_grid_G) = (0)) -> exists dst_positive_grid_G dst_negative_grid_G dst_value_grid_G. ((((exists ff_h_pvs_grid_Gentrypositive. ff_h_pvs_grid_Gentrypositive + S (dst_positive_grid_G) = S ((S (dst_index_grid_G)) * dst_positive_scale_grid_G)) /\ exists ff_q_pvs_grid_Gentrypositive. dst_positive_code_grid_G = ff_q_pvs_grid_Gentrypositive * S ((S (dst_index_grid_G)) * dst_positive_scale_grid_G) + (dst_positive_grid_G))) /\ (((((exists ff_h_pvs_grid_Gentrynegative. ff_h_pvs_grid_Gentrynegative + S (dst_negative_grid_G) = S ((S (dst_index_grid_G)) * dst_negative_scale_grid_G)) /\ exists ff_q_pvs_grid_Gentrynegative. dst_negative_code_grid_G = ff_q_pvs_grid_Gentrynegative * S ((S (dst_index_grid_G)) * dst_negative_scale_grid_G) + (dst_negative_grid_G))) /\ (exists ge_balance_positive_grid_Gentryvalue ge_balance_negative_grid_Gentryvalue. (((((dst_value_grid_G) = 2 * (ge_balance_positive_grid_Gentryvalue) /\ (ge_balance_negative_grid_Gentryvalue) = 0) \/ exists ge_signed_half_grid_Gentryvaluedecode. (((dst_value_grid_G) = 2 * ge_signed_half_grid_Gentryvaluedecode + 1 /\ (ge_balance_positive_grid_Gentryvalue) = 0) /\ (ge_balance_negative_grid_Gentryvalue) = S ge_signed_half_grid_Gentryvaluedecode))) /\ ((dst_positive_grid_G) + ge_balance_negative_grid_Gentryvalue = (dst_negative_grid_G) + ge_balance_positive_grid_Gentryvalue))))))))) -> (exists dst_positive_code_grid_H dst_positive_scale_grid_H dst_negative_code_grid_H dst_negative_scale_grid_H. (((H) = (((((dst_positive_code_grid_H) + (dst_positive_scale_grid_H)) * S ((dst_positive_code_grid_H) + (dst_positive_scale_grid_H)) + ((dst_positive_scale_grid_H) + (dst_positive_scale_grid_H))) + (((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) * S ((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) + ((dst_negative_scale_grid_H) + (dst_negative_scale_grid_H)))) * S ((((dst_positive_code_grid_H) + (dst_positive_scale_grid_H)) * S ((dst_positive_code_grid_H) + (dst_positive_scale_grid_H)) + ((dst_positive_scale_grid_H) + (dst_positive_scale_grid_H))) + (((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) * S ((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) + ((dst_negative_scale_grid_H) + (dst_negative_scale_grid_H)))) + ((((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) * S ((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) + ((dst_negative_scale_grid_H) + (dst_negative_scale_grid_H))) + (((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) * S ((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) + ((dst_negative_scale_grid_H) + (dst_negative_scale_grid_H)))))) /\ (forall dst_index_grid_H. (exists pvs_le_gap_grid_Hdomain. pvs_le_gap_grid_Hdomain + (dst_index_grid_H) = (0)) -> exists dst_positive_grid_H dst_negative_grid_H dst_value_grid_H. ((((exists ff_h_pvs_grid_Hentrypositive. ff_h_pvs_grid_Hentrypositive + S (dst_positive_grid_H) = S ((S (dst_index_grid_H)) * dst_positive_scale_grid_H)) /\ exists ff_q_pvs_grid_Hentrypositive. dst_positive_code_grid_H = ff_q_pvs_grid_Hentrypositive * S ((S (dst_index_grid_H)) * dst_positive_scale_grid_H) + (dst_positive_grid_H))) /\ (((((exists ff_h_pvs_grid_Hentrynegative. ff_h_pvs_grid_Hentrynegative + S (dst_negative_grid_H) = S ((S (dst_index_grid_H)) * dst_negative_scale_grid_H)) /\ exists ff_q_pvs_grid_Hentrynegative. dst_negative_code_grid_H = ff_q_pvs_grid_Hentrynegative * S ((S (dst_index_grid_H)) * dst_negative_scale_grid_H) + (dst_negative_grid_H))) /\ (exists ge_balance_positive_grid_Hentryvalue ge_balance_negative_grid_Hentryvalue. (((((dst_value_grid_H) = 2 * (ge_balance_positive_grid_Hentryvalue) /\ (ge_balance_negative_grid_Hentryvalue) = 0) \/ exists ge_signed_half_grid_Hentryvaluedecode. (((dst_value_grid_H) = 2 * ge_signed_half_grid_Hentryvaluedecode + 1 /\ (ge_balance_positive_grid_Hentryvalue) = 0) /\ (ge_balance_negative_grid_Hentryvalue) = S ge_signed_half_grid_Hentryvaluedecode))) /\ ((dst_positive_grid_H) + ge_balance_negative_grid_Hentryvalue = (dst_negative_grid_H) + ge_balance_positive_grid_Hentryvalue))))))))) -> exists T. (((exists dst_positive_code_grid_totaltable dst_positive_scale_grid_totaltable dst_negative_code_grid_totaltable dst_negative_scale_grid_totaltable. (((T) = (((((dst_positive_code_grid_totaltable) + (dst_positive_scale_grid_totaltable)) * S ((dst_positive_code_grid_totaltable) + (dst_positive_scale_grid_totaltable)) + ((dst_positive_scale_grid_totaltable) + (dst_positive_scale_grid_totaltable))) + (((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) * S ((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) + ((dst_negative_scale_grid_totaltable) + (dst_negative_scale_grid_totaltable)))) * S ((((dst_positive_code_grid_totaltable) + (dst_positive_scale_grid_totaltable)) * S ((dst_positive_code_grid_totaltable) + (dst_positive_scale_grid_totaltable)) + ((dst_positive_scale_grid_totaltable) + (dst_positive_scale_grid_totaltable))) + (((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) * S ((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) + ((dst_negative_scale_grid_totaltable) + (dst_negative_scale_grid_totaltable)))) + ((((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) * S ((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) + ((dst_negative_scale_grid_totaltable) + (dst_negative_scale_grid_totaltable))) + (((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) * S ((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) + ((dst_negative_scale_grid_totaltable) + (dst_negative_scale_grid_totaltable)))))) /\ (forall dst_index_grid_totaltable. (exists pvs_le_gap_grid_totaltabledomain. pvs_le_gap_grid_totaltabledomain + (dst_index_grid_totaltable) = ((S (n))*(S (n)))) -> exists dst_positive_grid_totaltable dst_negative_grid_totaltable dst_value_grid_totaltable. ((((exists ff_h_pvs_grid_totaltableentrypositive. ff_h_pvs_grid_totaltableentrypositive + S (dst_positive_grid_totaltable) = S ((S (dst_index_grid_totaltable)) * dst_positive_scale_grid_totaltable)) /\ exists ff_q_pvs_grid_totaltableentrypositive. dst_positive_code_grid_totaltable = ff_q_pvs_grid_totaltableentrypositive * S ((S (dst_index_grid_totaltable)) * dst_positive_scale_grid_totaltable) + (dst_positive_grid_totaltable))) /\ (((((exists ff_h_pvs_grid_totaltableentrynegative. ff_h_pvs_grid_totaltableentrynegative + S (dst_negative_grid_totaltable) = S ((S (dst_index_grid_totaltable)) * dst_negative_scale_grid_totaltable)) /\ exists ff_q_pvs_grid_totaltableentrynegative. dst_negative_code_grid_totaltable = ff_q_pvs_grid_totaltableentrynegative * S ((S (dst_index_grid_totaltable)) * dst_negative_scale_grid_totaltable) + (dst_negative_grid_totaltable))) /\ (exists ge_balance_positive_grid_totaltableentryvalue ge_balance_negative_grid_totaltableentryvalue. (((((dst_value_grid_totaltable) = 2 * (ge_balance_positive_grid_totaltableentryvalue) /\ (ge_balance_negative_grid_totaltableentryvalue) = 0) \/ exists ge_signed_half_grid_totaltableentryvaluedecode. (((dst_value_grid_totaltable) = 2 * ge_signed_half_grid_totaltableentryvaluedecode + 1 /\ (ge_balance_positive_grid_totaltableentryvalue) = 0) /\ (ge_balance_negative_grid_totaltableentryvalue) = S ge_signed_half_grid_totaltableentryvaluedecode))) /\ ((dst_positive_grid_totaltable) + ge_balance_negative_grid_totaltableentryvalue = (dst_negative_grid_totaltable) + ge_balance_positive_grid_totaltableentryvalue))))))))) /\ (forall dfg_grid_row_grid_total dfg_grid_column_grid_total dfg_grid_value_grid_total. (exists pvs_le_gap_grid_totalrow. pvs_le_gap_grid_totalrow + (dfg_grid_row_grid_total) = (n)) -> (exists pvs_le_gap_grid_totalcolumn. pvs_le_gap_grid_totalcolumn + (dfg_grid_column_grid_total) = (n)) -> (exists dst_positive_code_grid_totallookup dst_positive_scale_grid_totallookup dst_negative_code_grid_totallookup dst_negative_scale_grid_totallookup dst_positive_grid_totallookup dst_negative_grid_totallookup. (((T) = (((((dst_positive_code_grid_totallookup) + (dst_positive_scale_grid_totallookup)) * S ((dst_positive_code_grid_totallookup) + (dst_positive_scale_grid_totallookup)) + ((dst_positive_scale_grid_totallookup) + (dst_positive_scale_grid_totallookup))) + (((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) * S ((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) + ((dst_negative_scale_grid_totallookup) + (dst_negative_scale_grid_totallookup)))) * S ((((dst_positive_code_grid_totallookup) + (dst_positive_scale_grid_totallookup)) * S ((dst_positive_code_grid_totallookup) + (dst_positive_scale_grid_totallookup)) + ((dst_positive_scale_grid_totallookup) + (dst_positive_scale_grid_totallookup))) + (((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) * S ((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) + ((dst_negative_scale_grid_totallookup) + (dst_negative_scale_grid_totallookup)))) + ((((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) * S ((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) + ((dst_negative_scale_grid_totallookup) + (dst_negative_scale_grid_totallookup))) + (((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) * S ((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) + ((dst_negative_scale_grid_totallookup) + (dst_negative_scale_grid_totallookup)))))) /\ (((((exists ff_h_pvs_grid_totallookuppositive. ff_h_pvs_grid_totallookuppositive + S (dst_positive_grid_totallookup) = S ((S ((S (n))*(dfg_grid_row_grid_total)+(dfg_grid_column_grid_total))) * dst_positive_scale_grid_totallookup)) /\ exists ff_q_pvs_grid_totallookuppositive. dst_positive_code_grid_totallookup = ff_q_pvs_grid_totallookuppositive * S ((S ((S (n))*(dfg_grid_row_grid_total)+(dfg_grid_column_grid_total))) * dst_positive_scale_grid_totallookup) + (dst_positive_grid_totallookup))) /\ (((((exists ff_h_pvs_grid_totallookupnegative. ff_h_pvs_grid_totallookupnegative + S (dst_negative_grid_totallookup) = S ((S ((S (n))*(dfg_grid_row_grid_total)+(dfg_grid_column_grid_total))) * dst_negative_scale_grid_totallookup)) /\ exists ff_q_pvs_grid_totallookupnegative. dst_negative_code_grid_totallookup = ff_q_pvs_grid_totallookupnegative * S ((S ((S (n))*(dfg_grid_row_grid_total)+(dfg_grid_column_grid_total))) * dst_negative_scale_grid_totallookup) + (dst_negative_grid_totallookup))) /\ (exists ge_balance_positive_grid_totallookupvalue ge_balance_negative_grid_totallookupvalue. (((((dfg_grid_value_grid_total) = 2 * (ge_balance_positive_grid_totallookupvalue) /\ (ge_balance_negative_grid_totallookupvalue) = 0) \/ exists ge_signed_half_grid_totallookupvaluedecode. (((dfg_grid_value_grid_total) = 2 * ge_signed_half_grid_totallookupvaluedecode + 1 /\ (ge_balance_positive_grid_totallookupvalue) = 0) /\ (ge_balance_negative_grid_totallookupvalue) = S ge_signed_half_grid_totallookupvaluedecode))) /\ ((dst_positive_grid_totallookup) + ge_balance_negative_grid_totallookupvalue = (dst_negative_grid_totallookup) + ge_balance_positive_grid_totallookupvalue))))))))) -> ((((~((dfg_grid_row_grid_total)=0)) /\ (((~((dfg_grid_column_grid_total)=0)) /\ (exists dfg_middle_grid_totalentry dfg_first_grid_totalentry dfg_last_grid_totalentry dfg_value_grid_totalentry. (((n)=((dfg_grid_row_grid_total)*(dfg_grid_column_grid_total))*dfg_middle_grid_totalentry) /\ (((exists dst_positive_code_grid_totalentryfirst dst_positive_scale_grid_totalentryfirst dst_negative_code_grid_totalentryfirst dst_negative_scale_grid_totalentryfirst dst_positive_grid_totalentryfirst dst_negative_grid_totalentryfirst. (((F) = (((((dst_positive_code_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst)) * S ((dst_positive_code_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst)) + ((dst_positive_scale_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst))) + (((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) * S ((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) + ((dst_negative_scale_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)))) * S ((((dst_positive_code_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst)) * S ((dst_positive_code_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst)) + ((dst_positive_scale_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst))) + (((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) * S ((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) + ((dst_negative_scale_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)))) + ((((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) * S ((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) + ((dst_negative_scale_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst))) + (((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) * S ((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) + ((dst_negative_scale_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)))))) /\ (((((exists ff_h_pvs_grid_totalentryfirstpositive. ff_h_pvs_grid_totalentryfirstpositive + S (dst_positive_grid_totalentryfirst) = S ((S (dfg_grid_row_grid_total)) * dst_positive_scale_grid_totalentryfirst)) /\ exists ff_q_pvs_grid_totalentryfirstpositive. dst_positive_code_grid_totalentryfirst = ff_q_pvs_grid_totalentryfirstpositive * S ((S (dfg_grid_row_grid_total)) * dst_positive_scale_grid_totalentryfirst) + (dst_positive_grid_totalentryfirst))) /\ (((((exists ff_h_pvs_grid_totalentryfirstnegative. ff_h_pvs_grid_totalentryfirstnegative + S (dst_negative_grid_totalentryfirst) = S ((S (dfg_grid_row_grid_total)) * dst_negative_scale_grid_totalentryfirst)) /\ exists ff_q_pvs_grid_totalentryfirstnegative. dst_negative_code_grid_totalentryfirst = ff_q_pvs_grid_totalentryfirstnegative * S ((S (dfg_grid_row_grid_total)) * dst_negative_scale_grid_totalentryfirst) + (dst_negative_grid_totalentryfirst))) /\ (exists ge_balance_positive_grid_totalentryfirstvalue ge_balance_negative_grid_totalentryfirstvalue. (((((dfg_first_grid_totalentry) = 2 * (ge_balance_positive_grid_totalentryfirstvalue) /\ (ge_balance_negative_grid_totalentryfirstvalue) = 0) \/ exists ge_signed_half_grid_totalentryfirstvaluedecode. (((dfg_first_grid_totalentry) = 2 * ge_signed_half_grid_totalentryfirstvaluedecode + 1 /\ (ge_balance_positive_grid_totalentryfirstvalue) = 0) /\ (ge_balance_negative_grid_totalentryfirstvalue) = S ge_signed_half_grid_totalentryfirstvaluedecode))) /\ ((dst_positive_grid_totalentryfirst) + ge_balance_negative_grid_totalentryfirstvalue = (dst_negative_grid_totalentryfirst) + ge_balance_positive_grid_totalentryfirstvalue))))))))) /\ (((exists dst_positive_code_grid_totalentrylast dst_positive_scale_grid_totalentrylast dst_negative_code_grid_totalentrylast dst_negative_scale_grid_totalentrylast dst_positive_grid_totalentrylast dst_negative_grid_totalentrylast. (((H) = (((((dst_positive_code_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast)) * S ((dst_positive_code_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast)) + ((dst_positive_scale_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast))) + (((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) * S ((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) + ((dst_negative_scale_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)))) * S ((((dst_positive_code_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast)) * S ((dst_positive_code_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast)) + ((dst_positive_scale_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast))) + (((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) * S ((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) + ((dst_negative_scale_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)))) + ((((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) * S ((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) + ((dst_negative_scale_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast))) + (((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) * S ((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) + ((dst_negative_scale_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)))))) /\ (((((exists ff_h_pvs_grid_totalentrylastpositive. ff_h_pvs_grid_totalentrylastpositive + S (dst_positive_grid_totalentrylast) = S ((S (dfg_grid_column_grid_total)) * dst_positive_scale_grid_totalentrylast)) /\ exists ff_q_pvs_grid_totalentrylastpositive. dst_positive_code_grid_totalentrylast = ff_q_pvs_grid_totalentrylastpositive * S ((S (dfg_grid_column_grid_total)) * dst_positive_scale_grid_totalentrylast) + (dst_positive_grid_totalentrylast))) /\ (((((exists ff_h_pvs_grid_totalentrylastnegative. ff_h_pvs_grid_totalentrylastnegative + S (dst_negative_grid_totalentrylast) = S ((S (dfg_grid_column_grid_total)) * dst_negative_scale_grid_totalentrylast)) /\ exists ff_q_pvs_grid_totalentrylastnegative. dst_negative_code_grid_totalentrylast = ff_q_pvs_grid_totalentrylastnegative * S ((S (dfg_grid_column_grid_total)) * dst_negative_scale_grid_totalentrylast) + (dst_negative_grid_totalentrylast))) /\ (exists ge_balance_positive_grid_totalentrylastvalue ge_balance_negative_grid_totalentrylastvalue. (((((dfg_last_grid_totalentry) = 2 * (ge_balance_positive_grid_totalentrylastvalue) /\ (ge_balance_negative_grid_totalentrylastvalue) = 0) \/ exists ge_signed_half_grid_totalentrylastvaluedecode. (((dfg_last_grid_totalentry) = 2 * ge_signed_half_grid_totalentrylastvaluedecode + 1 /\ (ge_balance_positive_grid_totalentrylastvalue) = 0) /\ (ge_balance_negative_grid_totalentrylastvalue) = S ge_signed_half_grid_totalentrylastvaluedecode))) /\ ((dst_positive_grid_totalentrylast) + ge_balance_negative_grid_totalentrylastvalue = (dst_negative_grid_totalentrylast) + ge_balance_positive_grid_totalentrylastvalue))))))))) /\ (((exists dst_positive_code_grid_totalentrymiddle dst_positive_scale_grid_totalentrymiddle dst_negative_code_grid_totalentrymiddle dst_negative_scale_grid_totalentrymiddle dst_positive_grid_totalentrymiddle dst_negative_grid_totalentrymiddle. (((G) = (((((dst_positive_code_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle)) * S ((dst_positive_code_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle)) + ((dst_positive_scale_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle))) + (((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) * S ((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) + ((dst_negative_scale_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)))) * S ((((dst_positive_code_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle)) * S ((dst_positive_code_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle)) + ((dst_positive_scale_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle))) + (((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) * S ((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) + ((dst_negative_scale_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)))) + ((((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) * S ((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) + ((dst_negative_scale_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle))) + (((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) * S ((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) + ((dst_negative_scale_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)))))) /\ (((((exists ff_h_pvs_grid_totalentrymiddlepositive. ff_h_pvs_grid_totalentrymiddlepositive + S (dst_positive_grid_totalentrymiddle) = S ((S (dfg_middle_grid_totalentry)) * dst_positive_scale_grid_totalentrymiddle)) /\ exists ff_q_pvs_grid_totalentrymiddlepositive. dst_positive_code_grid_totalentrymiddle = ff_q_pvs_grid_totalentrymiddlepositive * S ((S (dfg_middle_grid_totalentry)) * dst_positive_scale_grid_totalentrymiddle) + (dst_positive_grid_totalentrymiddle))) /\ (((((exists ff_h_pvs_grid_totalentrymiddlenegative. ff_h_pvs_grid_totalentrymiddlenegative + S (dst_negative_grid_totalentrymiddle) = S ((S (dfg_middle_grid_totalentry)) * dst_negative_scale_grid_totalentrymiddle)) /\ exists ff_q_pvs_grid_totalentrymiddlenegative. dst_negative_code_grid_totalentrymiddle = ff_q_pvs_grid_totalentrymiddlenegative * S ((S (dfg_middle_grid_totalentry)) * dst_negative_scale_grid_totalentrymiddle) + (dst_negative_grid_totalentrymiddle))) /\ (exists ge_balance_positive_grid_totalentrymiddlevalue ge_balance_negative_grid_totalentrymiddlevalue. (((((dfg_value_grid_totalentry) = 2 * (ge_balance_positive_grid_totalentrymiddlevalue) /\ (ge_balance_negative_grid_totalentrymiddlevalue) = 0) \/ exists ge_signed_half_grid_totalentrymiddlevaluedecode. (((dfg_value_grid_totalentry) = 2 * ge_signed_half_grid_totalentrymiddlevaluedecode + 1 /\ (ge_balance_positive_grid_totalentrymiddlevalue) = 0) /\ (ge_balance_negative_grid_totalentrymiddlevalue) = S ge_signed_half_grid_totalentrymiddlevaluedecode))) /\ ((dst_positive_grid_totalentrymiddle) + ge_balance_negative_grid_totalentrymiddlevalue = (dst_negative_grid_totalentrymiddle) + ge_balance_positive_grid_totalentrymiddlevalue))))))))) /\ (exists dfg_inner_grid_totalentryproduct. ((exists sto_ap_grid_totalentryproductinner sto_an_grid_totalentryproductinner sto_bp_grid_totalentryproductinner sto_bn_grid_totalentryproductinner sto_cp_grid_totalentryproductinner sto_cn_grid_totalentryproductinner. (((((dfg_last_grid_totalentry) = 2 * (sto_ap_grid_totalentryproductinner) /\ (sto_an_grid_totalentryproductinner) = 0) \/ exists ge_signed_half_grid_totalentryproductinnerleft. (((dfg_last_grid_totalentry) = 2 * ge_signed_half_grid_totalentryproductinnerleft + 1 /\ (sto_ap_grid_totalentryproductinner) = 0) /\ (sto_an_grid_totalentryproductinner) = S ge_signed_half_grid_totalentryproductinnerleft))) /\ ((((((dfg_value_grid_totalentry) = 2 * (sto_bp_grid_totalentryproductinner) /\ (sto_bn_grid_totalentryproductinner) = 0) \/ exists ge_signed_half_grid_totalentryproductinnerright. (((dfg_value_grid_totalentry) = 2 * ge_signed_half_grid_totalentryproductinnerright + 1 /\ (sto_bp_grid_totalentryproductinner) = 0) /\ (sto_bn_grid_totalentryproductinner) = S ge_signed_half_grid_totalentryproductinnerright))) /\ ((((((dfg_inner_grid_totalentryproduct) = 2 * (sto_cp_grid_totalentryproductinner) /\ (sto_cn_grid_totalentryproductinner) = 0) \/ exists ge_signed_half_grid_totalentryproductinneroutput. (((dfg_inner_grid_totalentryproduct) = 2 * ge_signed_half_grid_totalentryproductinneroutput + 1 /\ (sto_cp_grid_totalentryproductinner) = 0) /\ (sto_cn_grid_totalentryproductinner) = S ge_signed_half_grid_totalentryproductinneroutput))) /\ ((sto_ap_grid_totalentryproductinner * sto_bp_grid_totalentryproductinner + sto_an_grid_totalentryproductinner * sto_bn_grid_totalentryproductinner) + sto_cn_grid_totalentryproductinner = (sto_ap_grid_totalentryproductinner * sto_bn_grid_totalentryproductinner + sto_an_grid_totalentryproductinner * sto_bp_grid_totalentryproductinner) + sto_cp_grid_totalentryproductinner))))))) /\ (exists sto_ap_grid_totalentryproductouter sto_an_grid_totalentryproductouter sto_bp_grid_totalentryproductouter sto_bn_grid_totalentryproductouter sto_cp_grid_totalentryproductouter sto_cn_grid_totalentryproductouter. (((((dfg_first_grid_totalentry) = 2 * (sto_ap_grid_totalentryproductouter) /\ (sto_an_grid_totalentryproductouter) = 0) \/ exists ge_signed_half_grid_totalentryproductouterleft. (((dfg_first_grid_totalentry) = 2 * ge_signed_half_grid_totalentryproductouterleft + 1 /\ (sto_ap_grid_totalentryproductouter) = 0) /\ (sto_an_grid_totalentryproductouter) = S ge_signed_half_grid_totalentryproductouterleft))) /\ ((((((dfg_inner_grid_totalentryproduct) = 2 * (sto_bp_grid_totalentryproductouter) /\ (sto_bn_grid_totalentryproductouter) = 0) \/ exists ge_signed_half_grid_totalentryproductouterright. (((dfg_inner_grid_totalentryproduct) = 2 * ge_signed_half_grid_totalentryproductouterright + 1 /\ (sto_bp_grid_totalentryproductouter) = 0) /\ (sto_bn_grid_totalentryproductouter) = S ge_signed_half_grid_totalentryproductouterright))) /\ ((((((dfg_grid_value_grid_total) = 2 * (sto_cp_grid_totalentryproductouter) /\ (sto_cn_grid_totalentryproductouter) = 0) \/ exists ge_signed_half_grid_totalentryproductouteroutput. (((dfg_grid_value_grid_total) = 2 * ge_signed_half_grid_totalentryproductouteroutput + 1 /\ (sto_cp_grid_totalentryproductouter) = 0) /\ (sto_cn_grid_totalentryproductouter) = S ge_signed_half_grid_totalentryproductouteroutput))) /\ ((sto_ap_grid_totalentryproductouter * sto_bp_grid_totalentryproductouter + sto_an_grid_totalentryproductouter * sto_bn_grid_totalentryproductouter) + sto_cn_grid_totalentryproductouter = (sto_ap_grid_totalentryproductouter * sto_bn_grid_totalentryproductouter + sto_an_grid_totalentryproductouter * sto_bp_grid_totalentryproductouter) + sto_cp_grid_totalentryproductouter))))))))))))))))))))) \/ ((((dfg_grid_row_grid_total)=0 \/ ((dfg_grid_column_grid_total)=0 \/ ~(exists pvs_factor_grid_totalentryomittednondivisor. (n) = ((dfg_grid_row_grid_total)*(dfg_grid_column_grid_total)) * pvs_factor_grid_totalentryomittednondivisor))) /\ ((dfg_grid_value_grid_total)=0)))))))