dirichlet_grid_column_slice

Exact expanded first-order arithmetic statement

forall F G H n T a V. (((exists dst_positive_code_dirichlet_grid_column_slice_gridtable dst_positive_scale_dirichlet_grid_column_slice_gridtable dst_negative_code_dirichlet_grid_column_slice_gridtable dst_negative_scale_dirichlet_grid_column_slice_gridtable. (((T) = (((((dst_positive_code_dirichlet_grid_column_slice_gridtable) + (dst_positive_scale_dirichlet_grid_column_slice_gridtable)) * S ((dst_positive_code_dirichlet_grid_column_slice_gridtable) + (dst_positive_scale_dirichlet_grid_column_slice_gridtable)) + ((dst_positive_scale_dirichlet_grid_column_slice_gridtable) + (dst_positive_scale_dirichlet_grid_column_slice_gridtable))) + (((dst_negative_code_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_gridtable) + (dst_positive_scale_dirichlet_grid_column_slice_gridtable)) * S ((dst_positive_code_dirichlet_grid_column_slice_gridtable) + (dst_positive_scale_dirichlet_grid_column_slice_gridtable)) + ((dst_positive_scale_dirichlet_grid_column_slice_gridtable) + (dst_positive_scale_dirichlet_grid_column_slice_gridtable))) + (((dst_negative_code_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)))) + ((((dst_negative_code_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable))) + (((dst_negative_code_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridtable) + (dst_negative_scale_dirichlet_grid_column_slice_gridtable)))))) /\ (forall dst_index_dirichlet_grid_column_slice_gridtable. (exists pvs_le_gap_dirichlet_grid_column_slice_gridtabledomain. pvs_le_gap_dirichlet_grid_column_slice_gridtabledomain + (dst_index_dirichlet_grid_column_slice_gridtable) = ((S (n))*(S (n)))) -> exists dst_positive_dirichlet_grid_column_slice_gridtable dst_negative_dirichlet_grid_column_slice_gridtable dst_value_dirichlet_grid_column_slice_gridtable. ((((exists ff_h_pvs_dirichlet_grid_column_slice_gridtableentrypositive. ff_h_pvs_dirichlet_grid_column_slice_gridtableentrypositive + S (dst_positive_dirichlet_grid_column_slice_gridtable) = S ((S (dst_index_dirichlet_grid_column_slice_gridtable)) * dst_positive_scale_dirichlet_grid_column_slice_gridtable)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_gridtableentrypositive. dst_positive_code_dirichlet_grid_column_slice_gridtable = ff_q_pvs_dirichlet_grid_column_slice_gridtableentrypositive * S ((S (dst_index_dirichlet_grid_column_slice_gridtable)) * dst_positive_scale_dirichlet_grid_column_slice_gridtable) + (dst_positive_dirichlet_grid_column_slice_gridtable))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_gridtableentrynegative. ff_h_pvs_dirichlet_grid_column_slice_gridtableentrynegative + S (dst_negative_dirichlet_grid_column_slice_gridtable) = S ((S (dst_index_dirichlet_grid_column_slice_gridtable)) * dst_negative_scale_dirichlet_grid_column_slice_gridtable)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_gridtableentrynegative. dst_negative_code_dirichlet_grid_column_slice_gridtable = ff_q_pvs_dirichlet_grid_column_slice_gridtableentrynegative * S ((S (dst_index_dirichlet_grid_column_slice_gridtable)) * dst_negative_scale_dirichlet_grid_column_slice_gridtable) + (dst_negative_dirichlet_grid_column_slice_gridtable))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_gridtableentryvalue ge_balance_negative_dirichlet_grid_column_slice_gridtableentryvalue. (((((dst_value_dirichlet_grid_column_slice_gridtable) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_gridtableentryvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_gridtableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridtableentryvaluedecode. (((dst_value_dirichlet_grid_column_slice_gridtable) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridtableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_gridtableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_gridtableentryvalue) = S ge_signed_half_dirichlet_grid_column_slice_gridtableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_gridtable) + ge_balance_negative_dirichlet_grid_column_slice_gridtableentryvalue = (dst_negative_dirichlet_grid_column_slice_gridtable) + ge_balance_positive_dirichlet_grid_column_slice_gridtableentryvalue))))))))) /\ (forall dfg_grid_row_dirichlet_grid_column_slice_grid dfg_grid_column_dirichlet_grid_column_slice_grid dfg_grid_value_dirichlet_grid_column_slice_grid. (exists pvs_le_gap_dirichlet_grid_column_slice_gridrow. pvs_le_gap_dirichlet_grid_column_slice_gridrow + (dfg_grid_row_dirichlet_grid_column_slice_grid) = (n)) -> (exists pvs_le_gap_dirichlet_grid_column_slice_gridcolumn. pvs_le_gap_dirichlet_grid_column_slice_gridcolumn + (dfg_grid_column_dirichlet_grid_column_slice_grid) = (n)) -> (exists dst_positive_code_dirichlet_grid_column_slice_gridlookup dst_positive_scale_dirichlet_grid_column_slice_gridlookup dst_negative_code_dirichlet_grid_column_slice_gridlookup dst_negative_scale_dirichlet_grid_column_slice_gridlookup dst_positive_dirichlet_grid_column_slice_gridlookup dst_negative_dirichlet_grid_column_slice_gridlookup. (((T) = (((((dst_positive_code_dirichlet_grid_column_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_column_slice_gridlookup)) * S ((dst_positive_code_dirichlet_grid_column_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_column_slice_gridlookup)) + ((dst_positive_scale_dirichlet_grid_column_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_column_slice_gridlookup))) + (((dst_negative_code_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_column_slice_gridlookup)) * S ((dst_positive_code_dirichlet_grid_column_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_column_slice_gridlookup)) + ((dst_positive_scale_dirichlet_grid_column_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_column_slice_gridlookup))) + (((dst_negative_code_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)))) + ((((dst_negative_code_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup))) + (((dst_negative_code_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_column_slice_gridlookup)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_gridlookuppositive. ff_h_pvs_dirichlet_grid_column_slice_gridlookuppositive + S (dst_positive_dirichlet_grid_column_slice_gridlookup) = S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_column_slice_grid)+(dfg_grid_column_dirichlet_grid_column_slice_grid))) * dst_positive_scale_dirichlet_grid_column_slice_gridlookup)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_gridlookuppositive. dst_positive_code_dirichlet_grid_column_slice_gridlookup = ff_q_pvs_dirichlet_grid_column_slice_gridlookuppositive * S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_column_slice_grid)+(dfg_grid_column_dirichlet_grid_column_slice_grid))) * dst_positive_scale_dirichlet_grid_column_slice_gridlookup) + (dst_positive_dirichlet_grid_column_slice_gridlookup))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_gridlookupnegative. ff_h_pvs_dirichlet_grid_column_slice_gridlookupnegative + S (dst_negative_dirichlet_grid_column_slice_gridlookup) = S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_column_slice_grid)+(dfg_grid_column_dirichlet_grid_column_slice_grid))) * dst_negative_scale_dirichlet_grid_column_slice_gridlookup)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_gridlookupnegative. dst_negative_code_dirichlet_grid_column_slice_gridlookup = ff_q_pvs_dirichlet_grid_column_slice_gridlookupnegative * S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_column_slice_grid)+(dfg_grid_column_dirichlet_grid_column_slice_grid))) * dst_negative_scale_dirichlet_grid_column_slice_gridlookup) + (dst_negative_dirichlet_grid_column_slice_gridlookup))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_gridlookupvalue ge_balance_negative_dirichlet_grid_column_slice_gridlookupvalue. (((((dfg_grid_value_dirichlet_grid_column_slice_grid) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_gridlookupvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_gridlookupvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridlookupvaluedecode. (((dfg_grid_value_dirichlet_grid_column_slice_grid) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridlookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_gridlookupvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_gridlookupvalue) = S ge_signed_half_dirichlet_grid_column_slice_gridlookupvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_gridlookup) + ge_balance_negative_dirichlet_grid_column_slice_gridlookupvalue = (dst_negative_dirichlet_grid_column_slice_gridlookup) + ge_balance_positive_dirichlet_grid_column_slice_gridlookupvalue))))))))) -> ((((~((dfg_grid_row_dirichlet_grid_column_slice_grid)=0)) /\ (((~((dfg_grid_column_dirichlet_grid_column_slice_grid)=0)) /\ (exists dfg_middle_dirichlet_grid_column_slice_gridentry dfg_first_dirichlet_grid_column_slice_gridentry dfg_last_dirichlet_grid_column_slice_gridentry dfg_value_dirichlet_grid_column_slice_gridentry. (((n)=((dfg_grid_row_dirichlet_grid_column_slice_grid)*(dfg_grid_column_dirichlet_grid_column_slice_grid))*dfg_middle_dirichlet_grid_column_slice_gridentry) /\ (((exists dst_positive_code_dirichlet_grid_column_slice_gridentryfirst dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst dst_negative_code_dirichlet_grid_column_slice_gridentryfirst dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst dst_positive_dirichlet_grid_column_slice_gridentryfirst dst_negative_dirichlet_grid_column_slice_gridentryfirst. (((F) = (((((dst_positive_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst)) * S ((dst_positive_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst)) + ((dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst))) + (((dst_negative_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst)) * S ((dst_positive_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst)) + ((dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst))) + (((dst_negative_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)))) + ((((dst_negative_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst))) + (((dst_negative_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_gridentryfirstpositive. ff_h_pvs_dirichlet_grid_column_slice_gridentryfirstpositive + S (dst_positive_dirichlet_grid_column_slice_gridentryfirst) = S ((S (dfg_grid_row_dirichlet_grid_column_slice_grid)) * dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_gridentryfirstpositive. dst_positive_code_dirichlet_grid_column_slice_gridentryfirst = ff_q_pvs_dirichlet_grid_column_slice_gridentryfirstpositive * S ((S (dfg_grid_row_dirichlet_grid_column_slice_grid)) * dst_positive_scale_dirichlet_grid_column_slice_gridentryfirst) + (dst_positive_dirichlet_grid_column_slice_gridentryfirst))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_gridentryfirstnegative. ff_h_pvs_dirichlet_grid_column_slice_gridentryfirstnegative + S (dst_negative_dirichlet_grid_column_slice_gridentryfirst) = S ((S (dfg_grid_row_dirichlet_grid_column_slice_grid)) * dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_gridentryfirstnegative. dst_negative_code_dirichlet_grid_column_slice_gridentryfirst = ff_q_pvs_dirichlet_grid_column_slice_gridentryfirstnegative * S ((S (dfg_grid_row_dirichlet_grid_column_slice_grid)) * dst_negative_scale_dirichlet_grid_column_slice_gridentryfirst) + (dst_negative_dirichlet_grid_column_slice_gridentryfirst))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_gridentryfirstvalue ge_balance_negative_dirichlet_grid_column_slice_gridentryfirstvalue. (((((dfg_first_dirichlet_grid_column_slice_gridentry) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_gridentryfirstvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_gridentryfirstvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridentryfirstvaluedecode. (((dfg_first_dirichlet_grid_column_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridentryfirstvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_gridentryfirstvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_gridentryfirstvalue) = S ge_signed_half_dirichlet_grid_column_slice_gridentryfirstvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_gridentryfirst) + ge_balance_negative_dirichlet_grid_column_slice_gridentryfirstvalue = (dst_negative_dirichlet_grid_column_slice_gridentryfirst) + ge_balance_positive_dirichlet_grid_column_slice_gridentryfirstvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_column_slice_gridentrylast dst_positive_scale_dirichlet_grid_column_slice_gridentrylast dst_negative_code_dirichlet_grid_column_slice_gridentrylast dst_negative_scale_dirichlet_grid_column_slice_gridentrylast dst_positive_dirichlet_grid_column_slice_gridentrylast dst_negative_dirichlet_grid_column_slice_gridentrylast. (((H) = (((((dst_positive_code_dirichlet_grid_column_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrylast)) * S ((dst_positive_code_dirichlet_grid_column_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrylast)) + ((dst_positive_scale_dirichlet_grid_column_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrylast))) + (((dst_negative_code_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrylast)) * S ((dst_positive_code_dirichlet_grid_column_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrylast)) + ((dst_positive_scale_dirichlet_grid_column_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrylast))) + (((dst_negative_code_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)))) + ((((dst_negative_code_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast))) + (((dst_negative_code_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_gridentrylastpositive. ff_h_pvs_dirichlet_grid_column_slice_gridentrylastpositive + S (dst_positive_dirichlet_grid_column_slice_gridentrylast) = S ((S (dfg_grid_column_dirichlet_grid_column_slice_grid)) * dst_positive_scale_dirichlet_grid_column_slice_gridentrylast)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_gridentrylastpositive. dst_positive_code_dirichlet_grid_column_slice_gridentrylast = ff_q_pvs_dirichlet_grid_column_slice_gridentrylastpositive * S ((S (dfg_grid_column_dirichlet_grid_column_slice_grid)) * dst_positive_scale_dirichlet_grid_column_slice_gridentrylast) + (dst_positive_dirichlet_grid_column_slice_gridentrylast))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_gridentrylastnegative. ff_h_pvs_dirichlet_grid_column_slice_gridentrylastnegative + S (dst_negative_dirichlet_grid_column_slice_gridentrylast) = S ((S (dfg_grid_column_dirichlet_grid_column_slice_grid)) * dst_negative_scale_dirichlet_grid_column_slice_gridentrylast)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_gridentrylastnegative. dst_negative_code_dirichlet_grid_column_slice_gridentrylast = ff_q_pvs_dirichlet_grid_column_slice_gridentrylastnegative * S ((S (dfg_grid_column_dirichlet_grid_column_slice_grid)) * dst_negative_scale_dirichlet_grid_column_slice_gridentrylast) + (dst_negative_dirichlet_grid_column_slice_gridentrylast))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_gridentrylastvalue ge_balance_negative_dirichlet_grid_column_slice_gridentrylastvalue. (((((dfg_last_dirichlet_grid_column_slice_gridentry) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_gridentrylastvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_gridentrylastvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridentrylastvaluedecode. (((dfg_last_dirichlet_grid_column_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridentrylastvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_gridentrylastvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_gridentrylastvalue) = S ge_signed_half_dirichlet_grid_column_slice_gridentrylastvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_gridentrylast) + ge_balance_negative_dirichlet_grid_column_slice_gridentrylastvalue = (dst_negative_dirichlet_grid_column_slice_gridentrylast) + ge_balance_positive_dirichlet_grid_column_slice_gridentrylastvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_column_slice_gridentrymiddle dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle dst_negative_code_dirichlet_grid_column_slice_gridentrymiddle dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle dst_positive_dirichlet_grid_column_slice_gridentrymiddle dst_negative_dirichlet_grid_column_slice_gridentrymiddle. (((G) = (((((dst_positive_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle)) * S ((dst_positive_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle)) + ((dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle))) + (((dst_negative_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle)) * S ((dst_positive_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle)) + ((dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle))) + (((dst_negative_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)))) + ((((dst_negative_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle))) + (((dst_negative_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_gridentrymiddlepositive. ff_h_pvs_dirichlet_grid_column_slice_gridentrymiddlepositive + S (dst_positive_dirichlet_grid_column_slice_gridentrymiddle) = S ((S (dfg_middle_dirichlet_grid_column_slice_gridentry)) * dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_gridentrymiddlepositive. dst_positive_code_dirichlet_grid_column_slice_gridentrymiddle = ff_q_pvs_dirichlet_grid_column_slice_gridentrymiddlepositive * S ((S (dfg_middle_dirichlet_grid_column_slice_gridentry)) * dst_positive_scale_dirichlet_grid_column_slice_gridentrymiddle) + (dst_positive_dirichlet_grid_column_slice_gridentrymiddle))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_gridentrymiddlenegative. ff_h_pvs_dirichlet_grid_column_slice_gridentrymiddlenegative + S (dst_negative_dirichlet_grid_column_slice_gridentrymiddle) = S ((S (dfg_middle_dirichlet_grid_column_slice_gridentry)) * dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_gridentrymiddlenegative. dst_negative_code_dirichlet_grid_column_slice_gridentrymiddle = ff_q_pvs_dirichlet_grid_column_slice_gridentrymiddlenegative * S ((S (dfg_middle_dirichlet_grid_column_slice_gridentry)) * dst_negative_scale_dirichlet_grid_column_slice_gridentrymiddle) + (dst_negative_dirichlet_grid_column_slice_gridentrymiddle))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_gridentrymiddlevalue ge_balance_negative_dirichlet_grid_column_slice_gridentrymiddlevalue. (((((dfg_value_dirichlet_grid_column_slice_gridentry) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_gridentrymiddlevalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_gridentrymiddlevalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridentrymiddlevaluedecode. (((dfg_value_dirichlet_grid_column_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridentrymiddlevaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_gridentrymiddlevalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_gridentrymiddlevalue) = S ge_signed_half_dirichlet_grid_column_slice_gridentrymiddlevaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_gridentrymiddle) + ge_balance_negative_dirichlet_grid_column_slice_gridentrymiddlevalue = (dst_negative_dirichlet_grid_column_slice_gridentrymiddle) + ge_balance_positive_dirichlet_grid_column_slice_gridentrymiddlevalue))))))))) /\ (exists dfg_inner_dirichlet_grid_column_slice_gridentryproduct. ((exists sto_ap_dirichlet_grid_column_slice_gridentryproductinner sto_an_dirichlet_grid_column_slice_gridentryproductinner sto_bp_dirichlet_grid_column_slice_gridentryproductinner sto_bn_dirichlet_grid_column_slice_gridentryproductinner sto_cp_dirichlet_grid_column_slice_gridentryproductinner sto_cn_dirichlet_grid_column_slice_gridentryproductinner. (((((dfg_last_dirichlet_grid_column_slice_gridentry) = 2 * (sto_ap_dirichlet_grid_column_slice_gridentryproductinner) /\ (sto_an_dirichlet_grid_column_slice_gridentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridentryproductinnerleft. (((dfg_last_dirichlet_grid_column_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridentryproductinnerleft + 1 /\ (sto_ap_dirichlet_grid_column_slice_gridentryproductinner) = 0) /\ (sto_an_dirichlet_grid_column_slice_gridentryproductinner) = S ge_signed_half_dirichlet_grid_column_slice_gridentryproductinnerleft))) /\ ((((((dfg_value_dirichlet_grid_column_slice_gridentry) = 2 * (sto_bp_dirichlet_grid_column_slice_gridentryproductinner) /\ (sto_bn_dirichlet_grid_column_slice_gridentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridentryproductinnerright. (((dfg_value_dirichlet_grid_column_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridentryproductinnerright + 1 /\ (sto_bp_dirichlet_grid_column_slice_gridentryproductinner) = 0) /\ (sto_bn_dirichlet_grid_column_slice_gridentryproductinner) = S ge_signed_half_dirichlet_grid_column_slice_gridentryproductinnerright))) /\ ((((((dfg_inner_dirichlet_grid_column_slice_gridentryproduct) = 2 * (sto_cp_dirichlet_grid_column_slice_gridentryproductinner) /\ (sto_cn_dirichlet_grid_column_slice_gridentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridentryproductinneroutput. (((dfg_inner_dirichlet_grid_column_slice_gridentryproduct) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridentryproductinneroutput + 1 /\ (sto_cp_dirichlet_grid_column_slice_gridentryproductinner) = 0) /\ (sto_cn_dirichlet_grid_column_slice_gridentryproductinner) = S ge_signed_half_dirichlet_grid_column_slice_gridentryproductinneroutput))) /\ ((sto_ap_dirichlet_grid_column_slice_gridentryproductinner * sto_bp_dirichlet_grid_column_slice_gridentryproductinner + sto_an_dirichlet_grid_column_slice_gridentryproductinner * sto_bn_dirichlet_grid_column_slice_gridentryproductinner) + sto_cn_dirichlet_grid_column_slice_gridentryproductinner = (sto_ap_dirichlet_grid_column_slice_gridentryproductinner * sto_bn_dirichlet_grid_column_slice_gridentryproductinner + sto_an_dirichlet_grid_column_slice_gridentryproductinner * sto_bp_dirichlet_grid_column_slice_gridentryproductinner) + sto_cp_dirichlet_grid_column_slice_gridentryproductinner))))))) /\ (exists sto_ap_dirichlet_grid_column_slice_gridentryproductouter sto_an_dirichlet_grid_column_slice_gridentryproductouter sto_bp_dirichlet_grid_column_slice_gridentryproductouter sto_bn_dirichlet_grid_column_slice_gridentryproductouter sto_cp_dirichlet_grid_column_slice_gridentryproductouter sto_cn_dirichlet_grid_column_slice_gridentryproductouter. (((((dfg_first_dirichlet_grid_column_slice_gridentry) = 2 * (sto_ap_dirichlet_grid_column_slice_gridentryproductouter) /\ (sto_an_dirichlet_grid_column_slice_gridentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridentryproductouterleft. (((dfg_first_dirichlet_grid_column_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridentryproductouterleft + 1 /\ (sto_ap_dirichlet_grid_column_slice_gridentryproductouter) = 0) /\ (sto_an_dirichlet_grid_column_slice_gridentryproductouter) = S ge_signed_half_dirichlet_grid_column_slice_gridentryproductouterleft))) /\ ((((((dfg_inner_dirichlet_grid_column_slice_gridentryproduct) = 2 * (sto_bp_dirichlet_grid_column_slice_gridentryproductouter) /\ (sto_bn_dirichlet_grid_column_slice_gridentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridentryproductouterright. (((dfg_inner_dirichlet_grid_column_slice_gridentryproduct) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridentryproductouterright + 1 /\ (sto_bp_dirichlet_grid_column_slice_gridentryproductouter) = 0) /\ (sto_bn_dirichlet_grid_column_slice_gridentryproductouter) = S ge_signed_half_dirichlet_grid_column_slice_gridentryproductouterright))) /\ ((((((dfg_grid_value_dirichlet_grid_column_slice_grid) = 2 * (sto_cp_dirichlet_grid_column_slice_gridentryproductouter) /\ (sto_cn_dirichlet_grid_column_slice_gridentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_gridentryproductouteroutput. (((dfg_grid_value_dirichlet_grid_column_slice_grid) = 2 * ge_signed_half_dirichlet_grid_column_slice_gridentryproductouteroutput + 1 /\ (sto_cp_dirichlet_grid_column_slice_gridentryproductouter) = 0) /\ (sto_cn_dirichlet_grid_column_slice_gridentryproductouter) = S ge_signed_half_dirichlet_grid_column_slice_gridentryproductouteroutput))) /\ ((sto_ap_dirichlet_grid_column_slice_gridentryproductouter * sto_bp_dirichlet_grid_column_slice_gridentryproductouter + sto_an_dirichlet_grid_column_slice_gridentryproductouter * sto_bn_dirichlet_grid_column_slice_gridentryproductouter) + sto_cn_dirichlet_grid_column_slice_gridentryproductouter = (sto_ap_dirichlet_grid_column_slice_gridentryproductouter * sto_bn_dirichlet_grid_column_slice_gridentryproductouter + sto_an_dirichlet_grid_column_slice_gridentryproductouter * sto_bp_dirichlet_grid_column_slice_gridentryproductouter) + sto_cp_dirichlet_grid_column_slice_gridentryproductouter))))))))))))))))))))) \/ ((((dfg_grid_row_dirichlet_grid_column_slice_grid)=0 \/ ((dfg_grid_column_dirichlet_grid_column_slice_grid)=0 \/ ~(exists pvs_factor_dirichlet_grid_column_slice_gridentryomittednondivisor. (n) = ((dfg_grid_row_dirichlet_grid_column_slice_grid)*(dfg_grid_column_dirichlet_grid_column_slice_grid)) * pvs_factor_dirichlet_grid_column_slice_gridentryomittednondivisor))) /\ ((dfg_grid_value_dirichlet_grid_column_slice_grid)=0))))))) -> (exists pvs_le_gap_dirichlet_grid_column_slice_bound. pvs_le_gap_dirichlet_grid_column_slice_bound + (a) = (n)) -> (((exists dst_positive_code_dirichlet_grid_column_slice_slicesource_table dst_positive_scale_dirichlet_grid_column_slice_slicesource_table dst_negative_code_dirichlet_grid_column_slice_slicesource_table dst_negative_scale_dirichlet_grid_column_slice_slicesource_table. (((T) = (((((dst_positive_code_dirichlet_grid_column_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_column_slice_slicesource_table)) * S ((dst_positive_code_dirichlet_grid_column_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_column_slice_slicesource_table)) + ((dst_positive_scale_dirichlet_grid_column_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_column_slice_slicesource_table))) + (((dst_negative_code_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)) * S ((dst_negative_code_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)) + ((dst_negative_scale_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_column_slice_slicesource_table)) * S ((dst_positive_code_dirichlet_grid_column_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_column_slice_slicesource_table)) + ((dst_positive_scale_dirichlet_grid_column_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_column_slice_slicesource_table))) + (((dst_negative_code_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)) * S ((dst_negative_code_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)) + ((dst_negative_scale_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)))) + ((((dst_negative_code_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)) * S ((dst_negative_code_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)) + ((dst_negative_scale_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table))) + (((dst_negative_code_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)) * S ((dst_negative_code_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)) + ((dst_negative_scale_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)))))) /\ (forall dst_index_dirichlet_grid_column_slice_slicesource_table. (exists pvs_le_gap_dirichlet_grid_column_slice_slicesource_tabledomain. pvs_le_gap_dirichlet_grid_column_slice_slicesource_tabledomain + (dst_index_dirichlet_grid_column_slice_slicesource_table) = (0)) -> exists dst_positive_dirichlet_grid_column_slice_slicesource_table dst_negative_dirichlet_grid_column_slice_slicesource_table dst_value_dirichlet_grid_column_slice_slicesource_table. ((((exists ff_h_pvs_dirichlet_grid_column_slice_slicesource_tableentrypositive. ff_h_pvs_dirichlet_grid_column_slice_slicesource_tableentrypositive + S (dst_positive_dirichlet_grid_column_slice_slicesource_table) = S ((S (dst_index_dirichlet_grid_column_slice_slicesource_table)) * dst_positive_scale_dirichlet_grid_column_slice_slicesource_table)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_slicesource_tableentrypositive. dst_positive_code_dirichlet_grid_column_slice_slicesource_table = ff_q_pvs_dirichlet_grid_column_slice_slicesource_tableentrypositive * S ((S (dst_index_dirichlet_grid_column_slice_slicesource_table)) * dst_positive_scale_dirichlet_grid_column_slice_slicesource_table) + (dst_positive_dirichlet_grid_column_slice_slicesource_table))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_slicesource_tableentrynegative. ff_h_pvs_dirichlet_grid_column_slice_slicesource_tableentrynegative + S (dst_negative_dirichlet_grid_column_slice_slicesource_table) = S ((S (dst_index_dirichlet_grid_column_slice_slicesource_table)) * dst_negative_scale_dirichlet_grid_column_slice_slicesource_table)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_slicesource_tableentrynegative. dst_negative_code_dirichlet_grid_column_slice_slicesource_table = ff_q_pvs_dirichlet_grid_column_slice_slicesource_tableentrynegative * S ((S (dst_index_dirichlet_grid_column_slice_slicesource_table)) * dst_negative_scale_dirichlet_grid_column_slice_slicesource_table) + (dst_negative_dirichlet_grid_column_slice_slicesource_table))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_slicesource_tableentryvalue ge_balance_negative_dirichlet_grid_column_slice_slicesource_tableentryvalue. (((((dst_value_dirichlet_grid_column_slice_slicesource_table) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_slicesource_tableentryvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_slicesource_tableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_slicesource_tableentryvaluedecode. (((dst_value_dirichlet_grid_column_slice_slicesource_table) = 2 * ge_signed_half_dirichlet_grid_column_slice_slicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_slicesource_tableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_slicesource_tableentryvalue) = S ge_signed_half_dirichlet_grid_column_slice_slicesource_tableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_slicesource_table) + ge_balance_negative_dirichlet_grid_column_slice_slicesource_tableentryvalue = (dst_negative_dirichlet_grid_column_slice_slicesource_table) + ge_balance_positive_dirichlet_grid_column_slice_slicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_column_slice_sliceoutput_table dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table dst_negative_code_dirichlet_grid_column_slice_sliceoutput_table dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table. (((V) = (((((dst_positive_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table)) * S ((dst_positive_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table)) + ((dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table))) + (((dst_negative_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table)) * S ((dst_positive_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table)) + ((dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table))) + (((dst_negative_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)))) + ((((dst_negative_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table))) + (((dst_negative_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)))))) /\ (forall dst_index_dirichlet_grid_column_slice_sliceoutput_table. (exists pvs_le_gap_dirichlet_grid_column_slice_sliceoutput_tabledomain. pvs_le_gap_dirichlet_grid_column_slice_sliceoutput_tabledomain + (dst_index_dirichlet_grid_column_slice_sliceoutput_table) = (S n)) -> exists dst_positive_dirichlet_grid_column_slice_sliceoutput_table dst_negative_dirichlet_grid_column_slice_sliceoutput_table dst_value_dirichlet_grid_column_slice_sliceoutput_table. ((((exists ff_h_pvs_dirichlet_grid_column_slice_sliceoutput_tableentrypositive. ff_h_pvs_dirichlet_grid_column_slice_sliceoutput_tableentrypositive + S (dst_positive_dirichlet_grid_column_slice_sliceoutput_table) = S ((S (dst_index_dirichlet_grid_column_slice_sliceoutput_table)) * dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_sliceoutput_tableentrypositive. dst_positive_code_dirichlet_grid_column_slice_sliceoutput_table = ff_q_pvs_dirichlet_grid_column_slice_sliceoutput_tableentrypositive * S ((S (dst_index_dirichlet_grid_column_slice_sliceoutput_table)) * dst_positive_scale_dirichlet_grid_column_slice_sliceoutput_table) + (dst_positive_dirichlet_grid_column_slice_sliceoutput_table))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_sliceoutput_tableentrynegative. ff_h_pvs_dirichlet_grid_column_slice_sliceoutput_tableentrynegative + S (dst_negative_dirichlet_grid_column_slice_sliceoutput_table) = S ((S (dst_index_dirichlet_grid_column_slice_sliceoutput_table)) * dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_sliceoutput_tableentrynegative. dst_negative_code_dirichlet_grid_column_slice_sliceoutput_table = ff_q_pvs_dirichlet_grid_column_slice_sliceoutput_tableentrynegative * S ((S (dst_index_dirichlet_grid_column_slice_sliceoutput_table)) * dst_negative_scale_dirichlet_grid_column_slice_sliceoutput_table) + (dst_negative_dirichlet_grid_column_slice_sliceoutput_table))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_sliceoutput_tableentryvalue ge_balance_negative_dirichlet_grid_column_slice_sliceoutput_tableentryvalue. (((((dst_value_dirichlet_grid_column_slice_sliceoutput_table) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_sliceoutput_tableentryvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_sliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_sliceoutput_tableentryvaluedecode. (((dst_value_dirichlet_grid_column_slice_sliceoutput_table) = 2 * ge_signed_half_dirichlet_grid_column_slice_sliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_sliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_sliceoutput_tableentryvalue) = S ge_signed_half_dirichlet_grid_column_slice_sliceoutput_tableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_sliceoutput_table) + ge_balance_negative_dirichlet_grid_column_slice_sliceoutput_tableentryvalue = (dst_negative_dirichlet_grid_column_slice_sliceoutput_table) + ge_balance_positive_dirichlet_grid_column_slice_sliceoutput_tableentryvalue))))))))) /\ (forall srs_index_dirichlet_grid_column_slice_slice. (exists pvs_gap_dirichlet_grid_column_slice_slicebound. pvs_gap_dirichlet_grid_column_slice_slicebound + S (srs_index_dirichlet_grid_column_slice_slice) = (S n)) -> exists srs_value_dirichlet_grid_column_slice_slice. (((exists dst_positive_code_dirichlet_grid_column_slice_sliceentrysource dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource dst_negative_code_dirichlet_grid_column_slice_sliceentrysource dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource dst_positive_dirichlet_grid_column_slice_sliceentrysource dst_negative_dirichlet_grid_column_slice_sliceentrysource. (((T) = (((((dst_positive_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource)) * S ((dst_positive_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource)) + ((dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource))) + (((dst_negative_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource)) * S ((dst_positive_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource)) + ((dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource))) + (((dst_negative_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)))) + ((((dst_negative_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource))) + (((dst_negative_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_sliceentrysourcepositive. ff_h_pvs_dirichlet_grid_column_slice_sliceentrysourcepositive + S (dst_positive_dirichlet_grid_column_slice_sliceentrysource) = S ((S (((0+1*a) + ((S n) * (srs_index_dirichlet_grid_column_slice_slice))))) * dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_sliceentrysourcepositive. dst_positive_code_dirichlet_grid_column_slice_sliceentrysource = ff_q_pvs_dirichlet_grid_column_slice_sliceentrysourcepositive * S ((S (((0+1*a) + ((S n) * (srs_index_dirichlet_grid_column_slice_slice))))) * dst_positive_scale_dirichlet_grid_column_slice_sliceentrysource) + (dst_positive_dirichlet_grid_column_slice_sliceentrysource))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_sliceentrysourcenegative. ff_h_pvs_dirichlet_grid_column_slice_sliceentrysourcenegative + S (dst_negative_dirichlet_grid_column_slice_sliceentrysource) = S ((S (((0+1*a) + ((S n) * (srs_index_dirichlet_grid_column_slice_slice))))) * dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_sliceentrysourcenegative. dst_negative_code_dirichlet_grid_column_slice_sliceentrysource = ff_q_pvs_dirichlet_grid_column_slice_sliceentrysourcenegative * S ((S (((0+1*a) + ((S n) * (srs_index_dirichlet_grid_column_slice_slice))))) * dst_negative_scale_dirichlet_grid_column_slice_sliceentrysource) + (dst_negative_dirichlet_grid_column_slice_sliceentrysource))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_sliceentrysourcevalue ge_balance_negative_dirichlet_grid_column_slice_sliceentrysourcevalue. (((((srs_value_dirichlet_grid_column_slice_slice) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_sliceentrysourcevalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_sliceentrysourcevalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_sliceentrysourcevaluedecode. (((srs_value_dirichlet_grid_column_slice_slice) = 2 * ge_signed_half_dirichlet_grid_column_slice_sliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_sliceentrysourcevalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_sliceentrysourcevalue) = S ge_signed_half_dirichlet_grid_column_slice_sliceentrysourcevaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_sliceentrysource) + ge_balance_negative_dirichlet_grid_column_slice_sliceentrysourcevalue = (dst_negative_dirichlet_grid_column_slice_sliceentrysource) + ge_balance_positive_dirichlet_grid_column_slice_sliceentrysourcevalue))))))))) /\ (exists dst_positive_code_dirichlet_grid_column_slice_sliceentryoutput dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput dst_negative_code_dirichlet_grid_column_slice_sliceentryoutput dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput dst_positive_dirichlet_grid_column_slice_sliceentryoutput dst_negative_dirichlet_grid_column_slice_sliceentryoutput. (((V) = (((((dst_positive_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput)) * S ((dst_positive_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput)) + ((dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput))) + (((dst_negative_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput)) * S ((dst_positive_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput)) + ((dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput))) + (((dst_negative_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)))) + ((((dst_negative_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput))) + (((dst_negative_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_sliceentryoutputpositive. ff_h_pvs_dirichlet_grid_column_slice_sliceentryoutputpositive + S (dst_positive_dirichlet_grid_column_slice_sliceentryoutput) = S ((S (srs_index_dirichlet_grid_column_slice_slice)) * dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_sliceentryoutputpositive. dst_positive_code_dirichlet_grid_column_slice_sliceentryoutput = ff_q_pvs_dirichlet_grid_column_slice_sliceentryoutputpositive * S ((S (srs_index_dirichlet_grid_column_slice_slice)) * dst_positive_scale_dirichlet_grid_column_slice_sliceentryoutput) + (dst_positive_dirichlet_grid_column_slice_sliceentryoutput))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_sliceentryoutputnegative. ff_h_pvs_dirichlet_grid_column_slice_sliceentryoutputnegative + S (dst_negative_dirichlet_grid_column_slice_sliceentryoutput) = S ((S (srs_index_dirichlet_grid_column_slice_slice)) * dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_sliceentryoutputnegative. dst_negative_code_dirichlet_grid_column_slice_sliceentryoutput = ff_q_pvs_dirichlet_grid_column_slice_sliceentryoutputnegative * S ((S (srs_index_dirichlet_grid_column_slice_slice)) * dst_negative_scale_dirichlet_grid_column_slice_sliceentryoutput) + (dst_negative_dirichlet_grid_column_slice_sliceentryoutput))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_sliceentryoutputvalue ge_balance_negative_dirichlet_grid_column_slice_sliceentryoutputvalue. (((((srs_value_dirichlet_grid_column_slice_slice) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_sliceentryoutputvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_sliceentryoutputvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_sliceentryoutputvaluedecode. (((srs_value_dirichlet_grid_column_slice_slice) = 2 * ge_signed_half_dirichlet_grid_column_slice_sliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_sliceentryoutputvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_sliceentryoutputvalue) = S ge_signed_half_dirichlet_grid_column_slice_sliceentryoutputvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_sliceentryoutput) + ge_balance_negative_dirichlet_grid_column_slice_sliceentryoutputvalue = (dst_negative_dirichlet_grid_column_slice_sliceentryoutput) + ge_balance_positive_dirichlet_grid_column_slice_sliceentryoutputvalue)))))))))))))))) -> (((exists dst_positive_code_dirichlet_grid_column_slice_resulttable dst_positive_scale_dirichlet_grid_column_slice_resulttable dst_negative_code_dirichlet_grid_column_slice_resulttable dst_negative_scale_dirichlet_grid_column_slice_resulttable. (((V) = (((((dst_positive_code_dirichlet_grid_column_slice_resulttable) + (dst_positive_scale_dirichlet_grid_column_slice_resulttable)) * S ((dst_positive_code_dirichlet_grid_column_slice_resulttable) + (dst_positive_scale_dirichlet_grid_column_slice_resulttable)) + ((dst_positive_scale_dirichlet_grid_column_slice_resulttable) + (dst_positive_scale_dirichlet_grid_column_slice_resulttable))) + (((dst_negative_code_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)) * S ((dst_negative_code_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)) + ((dst_negative_scale_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_resulttable) + (dst_positive_scale_dirichlet_grid_column_slice_resulttable)) * S ((dst_positive_code_dirichlet_grid_column_slice_resulttable) + (dst_positive_scale_dirichlet_grid_column_slice_resulttable)) + ((dst_positive_scale_dirichlet_grid_column_slice_resulttable) + (dst_positive_scale_dirichlet_grid_column_slice_resulttable))) + (((dst_negative_code_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)) * S ((dst_negative_code_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)) + ((dst_negative_scale_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)))) + ((((dst_negative_code_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)) * S ((dst_negative_code_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)) + ((dst_negative_scale_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable))) + (((dst_negative_code_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)) * S ((dst_negative_code_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)) + ((dst_negative_scale_dirichlet_grid_column_slice_resulttable) + (dst_negative_scale_dirichlet_grid_column_slice_resulttable)))))) /\ (forall dst_index_dirichlet_grid_column_slice_resulttable. (exists pvs_le_gap_dirichlet_grid_column_slice_resulttabledomain. pvs_le_gap_dirichlet_grid_column_slice_resulttabledomain + (dst_index_dirichlet_grid_column_slice_resulttable) = (S (n))) -> exists dst_positive_dirichlet_grid_column_slice_resulttable dst_negative_dirichlet_grid_column_slice_resulttable dst_value_dirichlet_grid_column_slice_resulttable. ((((exists ff_h_pvs_dirichlet_grid_column_slice_resulttableentrypositive. ff_h_pvs_dirichlet_grid_column_slice_resulttableentrypositive + S (dst_positive_dirichlet_grid_column_slice_resulttable) = S ((S (dst_index_dirichlet_grid_column_slice_resulttable)) * dst_positive_scale_dirichlet_grid_column_slice_resulttable)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_resulttableentrypositive. dst_positive_code_dirichlet_grid_column_slice_resulttable = ff_q_pvs_dirichlet_grid_column_slice_resulttableentrypositive * S ((S (dst_index_dirichlet_grid_column_slice_resulttable)) * dst_positive_scale_dirichlet_grid_column_slice_resulttable) + (dst_positive_dirichlet_grid_column_slice_resulttable))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_resulttableentrynegative. ff_h_pvs_dirichlet_grid_column_slice_resulttableentrynegative + S (dst_negative_dirichlet_grid_column_slice_resulttable) = S ((S (dst_index_dirichlet_grid_column_slice_resulttable)) * dst_negative_scale_dirichlet_grid_column_slice_resulttable)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_resulttableentrynegative. dst_negative_code_dirichlet_grid_column_slice_resulttable = ff_q_pvs_dirichlet_grid_column_slice_resulttableentrynegative * S ((S (dst_index_dirichlet_grid_column_slice_resulttable)) * dst_negative_scale_dirichlet_grid_column_slice_resulttable) + (dst_negative_dirichlet_grid_column_slice_resulttable))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_resulttableentryvalue ge_balance_negative_dirichlet_grid_column_slice_resulttableentryvalue. (((((dst_value_dirichlet_grid_column_slice_resulttable) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_resulttableentryvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_resulttableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resulttableentryvaluedecode. (((dst_value_dirichlet_grid_column_slice_resulttable) = 2 * ge_signed_half_dirichlet_grid_column_slice_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_resulttableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_resulttableentryvalue) = S ge_signed_half_dirichlet_grid_column_slice_resulttableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_resulttable) + ge_balance_negative_dirichlet_grid_column_slice_resulttableentryvalue = (dst_negative_dirichlet_grid_column_slice_resulttable) + ge_balance_positive_dirichlet_grid_column_slice_resulttableentryvalue))))))))) /\ (forall dfg_factor_column_dirichlet_grid_column_slice_result dfg_factor_value_dirichlet_grid_column_slice_result. (exists pvs_le_gap_dirichlet_grid_column_slice_resultbound. pvs_le_gap_dirichlet_grid_column_slice_resultbound + (dfg_factor_column_dirichlet_grid_column_slice_result) = (n)) -> (exists dst_positive_code_dirichlet_grid_column_slice_resultlookup dst_positive_scale_dirichlet_grid_column_slice_resultlookup dst_negative_code_dirichlet_grid_column_slice_resultlookup dst_negative_scale_dirichlet_grid_column_slice_resultlookup dst_positive_dirichlet_grid_column_slice_resultlookup dst_negative_dirichlet_grid_column_slice_resultlookup. (((V) = (((((dst_positive_code_dirichlet_grid_column_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_column_slice_resultlookup)) * S ((dst_positive_code_dirichlet_grid_column_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_column_slice_resultlookup)) + ((dst_positive_scale_dirichlet_grid_column_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_column_slice_resultlookup))) + (((dst_negative_code_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_column_slice_resultlookup)) * S ((dst_positive_code_dirichlet_grid_column_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_column_slice_resultlookup)) + ((dst_positive_scale_dirichlet_grid_column_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_column_slice_resultlookup))) + (((dst_negative_code_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)))) + ((((dst_negative_code_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup))) + (((dst_negative_code_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_column_slice_resultlookup)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_resultlookuppositive. ff_h_pvs_dirichlet_grid_column_slice_resultlookuppositive + S (dst_positive_dirichlet_grid_column_slice_resultlookup) = S ((S (dfg_factor_column_dirichlet_grid_column_slice_result)) * dst_positive_scale_dirichlet_grid_column_slice_resultlookup)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_resultlookuppositive. dst_positive_code_dirichlet_grid_column_slice_resultlookup = ff_q_pvs_dirichlet_grid_column_slice_resultlookuppositive * S ((S (dfg_factor_column_dirichlet_grid_column_slice_result)) * dst_positive_scale_dirichlet_grid_column_slice_resultlookup) + (dst_positive_dirichlet_grid_column_slice_resultlookup))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_resultlookupnegative. ff_h_pvs_dirichlet_grid_column_slice_resultlookupnegative + S (dst_negative_dirichlet_grid_column_slice_resultlookup) = S ((S (dfg_factor_column_dirichlet_grid_column_slice_result)) * dst_negative_scale_dirichlet_grid_column_slice_resultlookup)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_resultlookupnegative. dst_negative_code_dirichlet_grid_column_slice_resultlookup = ff_q_pvs_dirichlet_grid_column_slice_resultlookupnegative * S ((S (dfg_factor_column_dirichlet_grid_column_slice_result)) * dst_negative_scale_dirichlet_grid_column_slice_resultlookup) + (dst_negative_dirichlet_grid_column_slice_resultlookup))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_resultlookupvalue ge_balance_negative_dirichlet_grid_column_slice_resultlookupvalue. (((((dfg_factor_value_dirichlet_grid_column_slice_result) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_resultlookupvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_resultlookupvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resultlookupvaluedecode. (((dfg_factor_value_dirichlet_grid_column_slice_result) = 2 * ge_signed_half_dirichlet_grid_column_slice_resultlookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_resultlookupvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_resultlookupvalue) = S ge_signed_half_dirichlet_grid_column_slice_resultlookupvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_resultlookup) + ge_balance_negative_dirichlet_grid_column_slice_resultlookupvalue = (dst_negative_dirichlet_grid_column_slice_resultlookup) + ge_balance_positive_dirichlet_grid_column_slice_resultlookupvalue))))))))) -> ((((~((a)=0)) /\ (((~((dfg_factor_column_dirichlet_grid_column_slice_result)=0)) /\ (exists dfg_middle_dirichlet_grid_column_slice_resultentry dfg_first_dirichlet_grid_column_slice_resultentry dfg_last_dirichlet_grid_column_slice_resultentry dfg_value_dirichlet_grid_column_slice_resultentry. (((n)=((a)*(dfg_factor_column_dirichlet_grid_column_slice_result))*dfg_middle_dirichlet_grid_column_slice_resultentry) /\ (((exists dst_positive_code_dirichlet_grid_column_slice_resultentryfirst dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst dst_negative_code_dirichlet_grid_column_slice_resultentryfirst dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst dst_positive_dirichlet_grid_column_slice_resultentryfirst dst_negative_dirichlet_grid_column_slice_resultentryfirst. (((H) = (((((dst_positive_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst)) * S ((dst_positive_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst)) + ((dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst))) + (((dst_negative_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst)) * S ((dst_positive_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst)) + ((dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst))) + (((dst_negative_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)))) + ((((dst_negative_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst))) + (((dst_negative_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_resultentryfirstpositive. ff_h_pvs_dirichlet_grid_column_slice_resultentryfirstpositive + S (dst_positive_dirichlet_grid_column_slice_resultentryfirst) = S ((S (a)) * dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_resultentryfirstpositive. dst_positive_code_dirichlet_grid_column_slice_resultentryfirst = ff_q_pvs_dirichlet_grid_column_slice_resultentryfirstpositive * S ((S (a)) * dst_positive_scale_dirichlet_grid_column_slice_resultentryfirst) + (dst_positive_dirichlet_grid_column_slice_resultentryfirst))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_resultentryfirstnegative. ff_h_pvs_dirichlet_grid_column_slice_resultentryfirstnegative + S (dst_negative_dirichlet_grid_column_slice_resultentryfirst) = S ((S (a)) * dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_resultentryfirstnegative. dst_negative_code_dirichlet_grid_column_slice_resultentryfirst = ff_q_pvs_dirichlet_grid_column_slice_resultentryfirstnegative * S ((S (a)) * dst_negative_scale_dirichlet_grid_column_slice_resultentryfirst) + (dst_negative_dirichlet_grid_column_slice_resultentryfirst))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_resultentryfirstvalue ge_balance_negative_dirichlet_grid_column_slice_resultentryfirstvalue. (((((dfg_first_dirichlet_grid_column_slice_resultentry) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_resultentryfirstvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_resultentryfirstvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resultentryfirstvaluedecode. (((dfg_first_dirichlet_grid_column_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_resultentryfirstvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_resultentryfirstvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_resultentryfirstvalue) = S ge_signed_half_dirichlet_grid_column_slice_resultentryfirstvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_resultentryfirst) + ge_balance_negative_dirichlet_grid_column_slice_resultentryfirstvalue = (dst_negative_dirichlet_grid_column_slice_resultentryfirst) + ge_balance_positive_dirichlet_grid_column_slice_resultentryfirstvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_column_slice_resultentrylast dst_positive_scale_dirichlet_grid_column_slice_resultentrylast dst_negative_code_dirichlet_grid_column_slice_resultentrylast dst_negative_scale_dirichlet_grid_column_slice_resultentrylast dst_positive_dirichlet_grid_column_slice_resultentrylast dst_negative_dirichlet_grid_column_slice_resultentrylast. (((F) = (((((dst_positive_code_dirichlet_grid_column_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrylast)) * S ((dst_positive_code_dirichlet_grid_column_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrylast)) + ((dst_positive_scale_dirichlet_grid_column_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrylast))) + (((dst_negative_code_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrylast)) * S ((dst_positive_code_dirichlet_grid_column_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrylast)) + ((dst_positive_scale_dirichlet_grid_column_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrylast))) + (((dst_negative_code_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)))) + ((((dst_negative_code_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast))) + (((dst_negative_code_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_resultentrylastpositive. ff_h_pvs_dirichlet_grid_column_slice_resultentrylastpositive + S (dst_positive_dirichlet_grid_column_slice_resultentrylast) = S ((S (dfg_factor_column_dirichlet_grid_column_slice_result)) * dst_positive_scale_dirichlet_grid_column_slice_resultentrylast)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_resultentrylastpositive. dst_positive_code_dirichlet_grid_column_slice_resultentrylast = ff_q_pvs_dirichlet_grid_column_slice_resultentrylastpositive * S ((S (dfg_factor_column_dirichlet_grid_column_slice_result)) * dst_positive_scale_dirichlet_grid_column_slice_resultentrylast) + (dst_positive_dirichlet_grid_column_slice_resultentrylast))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_resultentrylastnegative. ff_h_pvs_dirichlet_grid_column_slice_resultentrylastnegative + S (dst_negative_dirichlet_grid_column_slice_resultentrylast) = S ((S (dfg_factor_column_dirichlet_grid_column_slice_result)) * dst_negative_scale_dirichlet_grid_column_slice_resultentrylast)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_resultentrylastnegative. dst_negative_code_dirichlet_grid_column_slice_resultentrylast = ff_q_pvs_dirichlet_grid_column_slice_resultentrylastnegative * S ((S (dfg_factor_column_dirichlet_grid_column_slice_result)) * dst_negative_scale_dirichlet_grid_column_slice_resultentrylast) + (dst_negative_dirichlet_grid_column_slice_resultentrylast))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_resultentrylastvalue ge_balance_negative_dirichlet_grid_column_slice_resultentrylastvalue. (((((dfg_last_dirichlet_grid_column_slice_resultentry) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_resultentrylastvalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_resultentrylastvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resultentrylastvaluedecode. (((dfg_last_dirichlet_grid_column_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_resultentrylastvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_resultentrylastvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_resultentrylastvalue) = S ge_signed_half_dirichlet_grid_column_slice_resultentrylastvaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_resultentrylast) + ge_balance_negative_dirichlet_grid_column_slice_resultentrylastvalue = (dst_negative_dirichlet_grid_column_slice_resultentrylast) + ge_balance_positive_dirichlet_grid_column_slice_resultentrylastvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_column_slice_resultentrymiddle dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle dst_negative_code_dirichlet_grid_column_slice_resultentrymiddle dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle dst_positive_dirichlet_grid_column_slice_resultentrymiddle dst_negative_dirichlet_grid_column_slice_resultentrymiddle. (((G) = (((((dst_positive_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle)) * S ((dst_positive_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle)) + ((dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle))) + (((dst_negative_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)))) * S ((((dst_positive_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle)) * S ((dst_positive_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle)) + ((dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle))) + (((dst_negative_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)))) + ((((dst_negative_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle))) + (((dst_negative_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)) * S ((dst_negative_code_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)) + ((dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_resultentrymiddlepositive. ff_h_pvs_dirichlet_grid_column_slice_resultentrymiddlepositive + S (dst_positive_dirichlet_grid_column_slice_resultentrymiddle) = S ((S (dfg_middle_dirichlet_grid_column_slice_resultentry)) * dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_resultentrymiddlepositive. dst_positive_code_dirichlet_grid_column_slice_resultentrymiddle = ff_q_pvs_dirichlet_grid_column_slice_resultentrymiddlepositive * S ((S (dfg_middle_dirichlet_grid_column_slice_resultentry)) * dst_positive_scale_dirichlet_grid_column_slice_resultentrymiddle) + (dst_positive_dirichlet_grid_column_slice_resultentrymiddle))) /\ (((((exists ff_h_pvs_dirichlet_grid_column_slice_resultentrymiddlenegative. ff_h_pvs_dirichlet_grid_column_slice_resultentrymiddlenegative + S (dst_negative_dirichlet_grid_column_slice_resultentrymiddle) = S ((S (dfg_middle_dirichlet_grid_column_slice_resultentry)) * dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle)) /\ exists ff_q_pvs_dirichlet_grid_column_slice_resultentrymiddlenegative. dst_negative_code_dirichlet_grid_column_slice_resultentrymiddle = ff_q_pvs_dirichlet_grid_column_slice_resultentrymiddlenegative * S ((S (dfg_middle_dirichlet_grid_column_slice_resultentry)) * dst_negative_scale_dirichlet_grid_column_slice_resultentrymiddle) + (dst_negative_dirichlet_grid_column_slice_resultentrymiddle))) /\ (exists ge_balance_positive_dirichlet_grid_column_slice_resultentrymiddlevalue ge_balance_negative_dirichlet_grid_column_slice_resultentrymiddlevalue. (((((dfg_value_dirichlet_grid_column_slice_resultentry) = 2 * (ge_balance_positive_dirichlet_grid_column_slice_resultentrymiddlevalue) /\ (ge_balance_negative_dirichlet_grid_column_slice_resultentrymiddlevalue) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resultentrymiddlevaluedecode. (((dfg_value_dirichlet_grid_column_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_resultentrymiddlevaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_column_slice_resultentrymiddlevalue) = 0) /\ (ge_balance_negative_dirichlet_grid_column_slice_resultentrymiddlevalue) = S ge_signed_half_dirichlet_grid_column_slice_resultentrymiddlevaluedecode))) /\ ((dst_positive_dirichlet_grid_column_slice_resultentrymiddle) + ge_balance_negative_dirichlet_grid_column_slice_resultentrymiddlevalue = (dst_negative_dirichlet_grid_column_slice_resultentrymiddle) + ge_balance_positive_dirichlet_grid_column_slice_resultentrymiddlevalue))))))))) /\ (exists dfg_inner_dirichlet_grid_column_slice_resultentryproduct. ((exists sto_ap_dirichlet_grid_column_slice_resultentryproductinner sto_an_dirichlet_grid_column_slice_resultentryproductinner sto_bp_dirichlet_grid_column_slice_resultentryproductinner sto_bn_dirichlet_grid_column_slice_resultentryproductinner sto_cp_dirichlet_grid_column_slice_resultentryproductinner sto_cn_dirichlet_grid_column_slice_resultentryproductinner. (((((dfg_last_dirichlet_grid_column_slice_resultentry) = 2 * (sto_ap_dirichlet_grid_column_slice_resultentryproductinner) /\ (sto_an_dirichlet_grid_column_slice_resultentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resultentryproductinnerleft. (((dfg_last_dirichlet_grid_column_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_resultentryproductinnerleft + 1 /\ (sto_ap_dirichlet_grid_column_slice_resultentryproductinner) = 0) /\ (sto_an_dirichlet_grid_column_slice_resultentryproductinner) = S ge_signed_half_dirichlet_grid_column_slice_resultentryproductinnerleft))) /\ ((((((dfg_value_dirichlet_grid_column_slice_resultentry) = 2 * (sto_bp_dirichlet_grid_column_slice_resultentryproductinner) /\ (sto_bn_dirichlet_grid_column_slice_resultentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resultentryproductinnerright. (((dfg_value_dirichlet_grid_column_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_resultentryproductinnerright + 1 /\ (sto_bp_dirichlet_grid_column_slice_resultentryproductinner) = 0) /\ (sto_bn_dirichlet_grid_column_slice_resultentryproductinner) = S ge_signed_half_dirichlet_grid_column_slice_resultentryproductinnerright))) /\ ((((((dfg_inner_dirichlet_grid_column_slice_resultentryproduct) = 2 * (sto_cp_dirichlet_grid_column_slice_resultentryproductinner) /\ (sto_cn_dirichlet_grid_column_slice_resultentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resultentryproductinneroutput. (((dfg_inner_dirichlet_grid_column_slice_resultentryproduct) = 2 * ge_signed_half_dirichlet_grid_column_slice_resultentryproductinneroutput + 1 /\ (sto_cp_dirichlet_grid_column_slice_resultentryproductinner) = 0) /\ (sto_cn_dirichlet_grid_column_slice_resultentryproductinner) = S ge_signed_half_dirichlet_grid_column_slice_resultentryproductinneroutput))) /\ ((sto_ap_dirichlet_grid_column_slice_resultentryproductinner * sto_bp_dirichlet_grid_column_slice_resultentryproductinner + sto_an_dirichlet_grid_column_slice_resultentryproductinner * sto_bn_dirichlet_grid_column_slice_resultentryproductinner) + sto_cn_dirichlet_grid_column_slice_resultentryproductinner = (sto_ap_dirichlet_grid_column_slice_resultentryproductinner * sto_bn_dirichlet_grid_column_slice_resultentryproductinner + sto_an_dirichlet_grid_column_slice_resultentryproductinner * sto_bp_dirichlet_grid_column_slice_resultentryproductinner) + sto_cp_dirichlet_grid_column_slice_resultentryproductinner))))))) /\ (exists sto_ap_dirichlet_grid_column_slice_resultentryproductouter sto_an_dirichlet_grid_column_slice_resultentryproductouter sto_bp_dirichlet_grid_column_slice_resultentryproductouter sto_bn_dirichlet_grid_column_slice_resultentryproductouter sto_cp_dirichlet_grid_column_slice_resultentryproductouter sto_cn_dirichlet_grid_column_slice_resultentryproductouter. (((((dfg_first_dirichlet_grid_column_slice_resultentry) = 2 * (sto_ap_dirichlet_grid_column_slice_resultentryproductouter) /\ (sto_an_dirichlet_grid_column_slice_resultentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resultentryproductouterleft. (((dfg_first_dirichlet_grid_column_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_column_slice_resultentryproductouterleft + 1 /\ (sto_ap_dirichlet_grid_column_slice_resultentryproductouter) = 0) /\ (sto_an_dirichlet_grid_column_slice_resultentryproductouter) = S ge_signed_half_dirichlet_grid_column_slice_resultentryproductouterleft))) /\ ((((((dfg_inner_dirichlet_grid_column_slice_resultentryproduct) = 2 * (sto_bp_dirichlet_grid_column_slice_resultentryproductouter) /\ (sto_bn_dirichlet_grid_column_slice_resultentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resultentryproductouterright. (((dfg_inner_dirichlet_grid_column_slice_resultentryproduct) = 2 * ge_signed_half_dirichlet_grid_column_slice_resultentryproductouterright + 1 /\ (sto_bp_dirichlet_grid_column_slice_resultentryproductouter) = 0) /\ (sto_bn_dirichlet_grid_column_slice_resultentryproductouter) = S ge_signed_half_dirichlet_grid_column_slice_resultentryproductouterright))) /\ ((((((dfg_factor_value_dirichlet_grid_column_slice_result) = 2 * (sto_cp_dirichlet_grid_column_slice_resultentryproductouter) /\ (sto_cn_dirichlet_grid_column_slice_resultentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_column_slice_resultentryproductouteroutput. (((dfg_factor_value_dirichlet_grid_column_slice_result) = 2 * ge_signed_half_dirichlet_grid_column_slice_resultentryproductouteroutput + 1 /\ (sto_cp_dirichlet_grid_column_slice_resultentryproductouter) = 0) /\ (sto_cn_dirichlet_grid_column_slice_resultentryproductouter) = S ge_signed_half_dirichlet_grid_column_slice_resultentryproductouteroutput))) /\ ((sto_ap_dirichlet_grid_column_slice_resultentryproductouter * sto_bp_dirichlet_grid_column_slice_resultentryproductouter + sto_an_dirichlet_grid_column_slice_resultentryproductouter * sto_bn_dirichlet_grid_column_slice_resultentryproductouter) + sto_cn_dirichlet_grid_column_slice_resultentryproductouter = (sto_ap_dirichlet_grid_column_slice_resultentryproductouter * sto_bn_dirichlet_grid_column_slice_resultentryproductouter + sto_an_dirichlet_grid_column_slice_resultentryproductouter * sto_bp_dirichlet_grid_column_slice_resultentryproductouter) + sto_cp_dirichlet_grid_column_slice_resultentryproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((dfg_factor_column_dirichlet_grid_column_slice_result)=0 \/ ~(exists pvs_factor_dirichlet_grid_column_slice_resultentryomittednondivisor. (n) = ((a)*(dfg_factor_column_dirichlet_grid_column_slice_result)) * pvs_factor_dirichlet_grid_column_slice_resultentryomittednondivisor))) /\ ((dfg_factor_value_dirichlet_grid_column_slice_result)=0)))))))