Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Every grid, slice, row sum and intermediate table is constructed. Retained cells have witnessed n=(a*e)*c and value F(a)*(H(e)*G(c)). The flat endpoint is unused. Table associativity includes N=0 and compares only positive values, not encodings. Full G009 remains broader.
Exact theorem in conservative defined notation
∀ F. ∀ G. ∀ H. ∀ n. ∀ T. ∀ a. ∀ V. DirichletGrid(F,G,H,n,T) → Le(a,n) → ArithSlice(T,V,0 + S n · a,1,S n) → DirichletFactorRow(F,G,H,n,a,V)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall F G H n T a V. (((exists dst_positive_code_dirichlet_grid_row_slice_gridtable dst_positive_scale_dirichlet_grid_row_slice_gridtable dst_negative_code_dirichlet_grid_row_slice_gridtable dst_negative_scale_dirichlet_grid_row_slice_gridtable. (((T) = (((((dst_positive_code_dirichlet_grid_row_slice_gridtable) + (dst_positive_scale_dirichlet_grid_row_slice_gridtable)) * S ((dst_positive_code_dirichlet_grid_row_slice_gridtable) + (dst_positive_scale_dirichlet_grid_row_slice_gridtable)) + ((dst_positive_scale_dirichlet_grid_row_slice_gridtable) + (dst_positive_scale_dirichlet_grid_row_slice_gridtable))) + (((dst_negative_code_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_gridtable) + (dst_positive_scale_dirichlet_grid_row_slice_gridtable)) * S ((dst_positive_code_dirichlet_grid_row_slice_gridtable) + (dst_positive_scale_dirichlet_grid_row_slice_gridtable)) + ((dst_positive_scale_dirichlet_grid_row_slice_gridtable) + (dst_positive_scale_dirichlet_grid_row_slice_gridtable))) + (((dst_negative_code_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)))) + ((((dst_negative_code_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable))) + (((dst_negative_code_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridtable) + (dst_negative_scale_dirichlet_grid_row_slice_gridtable)))))) /\ (forall dst_index_dirichlet_grid_row_slice_gridtable. (exists pvs_le_gap_dirichlet_grid_row_slice_gridtabledomain. pvs_le_gap_dirichlet_grid_row_slice_gridtabledomain + (dst_index_dirichlet_grid_row_slice_gridtable) = ((S (n))*(S (n)))) -> exists dst_positive_dirichlet_grid_row_slice_gridtable dst_negative_dirichlet_grid_row_slice_gridtable dst_value_dirichlet_grid_row_slice_gridtable. ((((exists ff_h_pvs_dirichlet_grid_row_slice_gridtableentrypositive. ff_h_pvs_dirichlet_grid_row_slice_gridtableentrypositive + S (dst_positive_dirichlet_grid_row_slice_gridtable) = S ((S (dst_index_dirichlet_grid_row_slice_gridtable)) * dst_positive_scale_dirichlet_grid_row_slice_gridtable)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_gridtableentrypositive. dst_positive_code_dirichlet_grid_row_slice_gridtable = ff_q_pvs_dirichlet_grid_row_slice_gridtableentrypositive * S ((S (dst_index_dirichlet_grid_row_slice_gridtable)) * dst_positive_scale_dirichlet_grid_row_slice_gridtable) + (dst_positive_dirichlet_grid_row_slice_gridtable))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_gridtableentrynegative. ff_h_pvs_dirichlet_grid_row_slice_gridtableentrynegative + S (dst_negative_dirichlet_grid_row_slice_gridtable) = S ((S (dst_index_dirichlet_grid_row_slice_gridtable)) * dst_negative_scale_dirichlet_grid_row_slice_gridtable)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_gridtableentrynegative. dst_negative_code_dirichlet_grid_row_slice_gridtable = ff_q_pvs_dirichlet_grid_row_slice_gridtableentrynegative * S ((S (dst_index_dirichlet_grid_row_slice_gridtable)) * dst_negative_scale_dirichlet_grid_row_slice_gridtable) + (dst_negative_dirichlet_grid_row_slice_gridtable))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_gridtableentryvalue ge_balance_negative_dirichlet_grid_row_slice_gridtableentryvalue. (((((dst_value_dirichlet_grid_row_slice_gridtable) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_gridtableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_gridtableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridtableentryvaluedecode. (((dst_value_dirichlet_grid_row_slice_gridtable) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridtableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_gridtableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_gridtableentryvalue) = S ge_signed_half_dirichlet_grid_row_slice_gridtableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_gridtable) + ge_balance_negative_dirichlet_grid_row_slice_gridtableentryvalue = (dst_negative_dirichlet_grid_row_slice_gridtable) + ge_balance_positive_dirichlet_grid_row_slice_gridtableentryvalue))))))))) /\ (forall dfg_grid_row_dirichlet_grid_row_slice_grid dfg_grid_column_dirichlet_grid_row_slice_grid dfg_grid_value_dirichlet_grid_row_slice_grid. (exists pvs_le_gap_dirichlet_grid_row_slice_gridrow. pvs_le_gap_dirichlet_grid_row_slice_gridrow + (dfg_grid_row_dirichlet_grid_row_slice_grid) = (n)) -> (exists pvs_le_gap_dirichlet_grid_row_slice_gridcolumn. pvs_le_gap_dirichlet_grid_row_slice_gridcolumn + (dfg_grid_column_dirichlet_grid_row_slice_grid) = (n)) -> (exists dst_positive_code_dirichlet_grid_row_slice_gridlookup dst_positive_scale_dirichlet_grid_row_slice_gridlookup dst_negative_code_dirichlet_grid_row_slice_gridlookup dst_negative_scale_dirichlet_grid_row_slice_gridlookup dst_positive_dirichlet_grid_row_slice_gridlookup dst_negative_dirichlet_grid_row_slice_gridlookup. (((T) = (((((dst_positive_code_dirichlet_grid_row_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_row_slice_gridlookup)) * S ((dst_positive_code_dirichlet_grid_row_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_row_slice_gridlookup)) + ((dst_positive_scale_dirichlet_grid_row_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_row_slice_gridlookup))) + (((dst_negative_code_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_row_slice_gridlookup)) * S ((dst_positive_code_dirichlet_grid_row_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_row_slice_gridlookup)) + ((dst_positive_scale_dirichlet_grid_row_slice_gridlookup) + (dst_positive_scale_dirichlet_grid_row_slice_gridlookup))) + (((dst_negative_code_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)))) + ((((dst_negative_code_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup))) + (((dst_negative_code_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridlookup) + (dst_negative_scale_dirichlet_grid_row_slice_gridlookup)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_gridlookuppositive. ff_h_pvs_dirichlet_grid_row_slice_gridlookuppositive + S (dst_positive_dirichlet_grid_row_slice_gridlookup) = S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_row_slice_grid)+(dfg_grid_column_dirichlet_grid_row_slice_grid))) * dst_positive_scale_dirichlet_grid_row_slice_gridlookup)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_gridlookuppositive. dst_positive_code_dirichlet_grid_row_slice_gridlookup = ff_q_pvs_dirichlet_grid_row_slice_gridlookuppositive * S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_row_slice_grid)+(dfg_grid_column_dirichlet_grid_row_slice_grid))) * dst_positive_scale_dirichlet_grid_row_slice_gridlookup) + (dst_positive_dirichlet_grid_row_slice_gridlookup))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_gridlookupnegative. ff_h_pvs_dirichlet_grid_row_slice_gridlookupnegative + S (dst_negative_dirichlet_grid_row_slice_gridlookup) = S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_row_slice_grid)+(dfg_grid_column_dirichlet_grid_row_slice_grid))) * dst_negative_scale_dirichlet_grid_row_slice_gridlookup)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_gridlookupnegative. dst_negative_code_dirichlet_grid_row_slice_gridlookup = ff_q_pvs_dirichlet_grid_row_slice_gridlookupnegative * S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_row_slice_grid)+(dfg_grid_column_dirichlet_grid_row_slice_grid))) * dst_negative_scale_dirichlet_grid_row_slice_gridlookup) + (dst_negative_dirichlet_grid_row_slice_gridlookup))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_gridlookupvalue ge_balance_negative_dirichlet_grid_row_slice_gridlookupvalue. (((((dfg_grid_value_dirichlet_grid_row_slice_grid) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_gridlookupvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_gridlookupvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridlookupvaluedecode. (((dfg_grid_value_dirichlet_grid_row_slice_grid) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridlookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_gridlookupvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_gridlookupvalue) = S ge_signed_half_dirichlet_grid_row_slice_gridlookupvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_gridlookup) + ge_balance_negative_dirichlet_grid_row_slice_gridlookupvalue = (dst_negative_dirichlet_grid_row_slice_gridlookup) + ge_balance_positive_dirichlet_grid_row_slice_gridlookupvalue))))))))) -> ((((~((dfg_grid_row_dirichlet_grid_row_slice_grid)=0)) /\ (((~((dfg_grid_column_dirichlet_grid_row_slice_grid)=0)) /\ (exists dfg_middle_dirichlet_grid_row_slice_gridentry dfg_first_dirichlet_grid_row_slice_gridentry dfg_last_dirichlet_grid_row_slice_gridentry dfg_value_dirichlet_grid_row_slice_gridentry. (((n)=((dfg_grid_row_dirichlet_grid_row_slice_grid)*(dfg_grid_column_dirichlet_grid_row_slice_grid))*dfg_middle_dirichlet_grid_row_slice_gridentry) /\ (((exists dst_positive_code_dirichlet_grid_row_slice_gridentryfirst dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst dst_negative_code_dirichlet_grid_row_slice_gridentryfirst dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst dst_positive_dirichlet_grid_row_slice_gridentryfirst dst_negative_dirichlet_grid_row_slice_gridentryfirst. (((F) = (((((dst_positive_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst)) * S ((dst_positive_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst)) + ((dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst))) + (((dst_negative_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst)) * S ((dst_positive_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst)) + ((dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst))) + (((dst_negative_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)))) + ((((dst_negative_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst))) + (((dst_negative_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_gridentryfirstpositive. ff_h_pvs_dirichlet_grid_row_slice_gridentryfirstpositive + S (dst_positive_dirichlet_grid_row_slice_gridentryfirst) = S ((S (dfg_grid_row_dirichlet_grid_row_slice_grid)) * dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_gridentryfirstpositive. dst_positive_code_dirichlet_grid_row_slice_gridentryfirst = ff_q_pvs_dirichlet_grid_row_slice_gridentryfirstpositive * S ((S (dfg_grid_row_dirichlet_grid_row_slice_grid)) * dst_positive_scale_dirichlet_grid_row_slice_gridentryfirst) + (dst_positive_dirichlet_grid_row_slice_gridentryfirst))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_gridentryfirstnegative. ff_h_pvs_dirichlet_grid_row_slice_gridentryfirstnegative + S (dst_negative_dirichlet_grid_row_slice_gridentryfirst) = S ((S (dfg_grid_row_dirichlet_grid_row_slice_grid)) * dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_gridentryfirstnegative. dst_negative_code_dirichlet_grid_row_slice_gridentryfirst = ff_q_pvs_dirichlet_grid_row_slice_gridentryfirstnegative * S ((S (dfg_grid_row_dirichlet_grid_row_slice_grid)) * dst_negative_scale_dirichlet_grid_row_slice_gridentryfirst) + (dst_negative_dirichlet_grid_row_slice_gridentryfirst))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_gridentryfirstvalue ge_balance_negative_dirichlet_grid_row_slice_gridentryfirstvalue. (((((dfg_first_dirichlet_grid_row_slice_gridentry) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_gridentryfirstvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_gridentryfirstvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridentryfirstvaluedecode. (((dfg_first_dirichlet_grid_row_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridentryfirstvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_gridentryfirstvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_gridentryfirstvalue) = S ge_signed_half_dirichlet_grid_row_slice_gridentryfirstvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_gridentryfirst) + ge_balance_negative_dirichlet_grid_row_slice_gridentryfirstvalue = (dst_negative_dirichlet_grid_row_slice_gridentryfirst) + ge_balance_positive_dirichlet_grid_row_slice_gridentryfirstvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_slice_gridentrylast dst_positive_scale_dirichlet_grid_row_slice_gridentrylast dst_negative_code_dirichlet_grid_row_slice_gridentrylast dst_negative_scale_dirichlet_grid_row_slice_gridentrylast dst_positive_dirichlet_grid_row_slice_gridentrylast dst_negative_dirichlet_grid_row_slice_gridentrylast. (((H) = (((((dst_positive_code_dirichlet_grid_row_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrylast)) * S ((dst_positive_code_dirichlet_grid_row_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrylast)) + ((dst_positive_scale_dirichlet_grid_row_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrylast))) + (((dst_negative_code_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrylast)) * S ((dst_positive_code_dirichlet_grid_row_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrylast)) + ((dst_positive_scale_dirichlet_grid_row_slice_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrylast))) + (((dst_negative_code_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)))) + ((((dst_negative_code_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast))) + (((dst_negative_code_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_gridentrylastpositive. ff_h_pvs_dirichlet_grid_row_slice_gridentrylastpositive + S (dst_positive_dirichlet_grid_row_slice_gridentrylast) = S ((S (dfg_grid_column_dirichlet_grid_row_slice_grid)) * dst_positive_scale_dirichlet_grid_row_slice_gridentrylast)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_gridentrylastpositive. dst_positive_code_dirichlet_grid_row_slice_gridentrylast = ff_q_pvs_dirichlet_grid_row_slice_gridentrylastpositive * S ((S (dfg_grid_column_dirichlet_grid_row_slice_grid)) * dst_positive_scale_dirichlet_grid_row_slice_gridentrylast) + (dst_positive_dirichlet_grid_row_slice_gridentrylast))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_gridentrylastnegative. ff_h_pvs_dirichlet_grid_row_slice_gridentrylastnegative + S (dst_negative_dirichlet_grid_row_slice_gridentrylast) = S ((S (dfg_grid_column_dirichlet_grid_row_slice_grid)) * dst_negative_scale_dirichlet_grid_row_slice_gridentrylast)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_gridentrylastnegative. dst_negative_code_dirichlet_grid_row_slice_gridentrylast = ff_q_pvs_dirichlet_grid_row_slice_gridentrylastnegative * S ((S (dfg_grid_column_dirichlet_grid_row_slice_grid)) * dst_negative_scale_dirichlet_grid_row_slice_gridentrylast) + (dst_negative_dirichlet_grid_row_slice_gridentrylast))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_gridentrylastvalue ge_balance_negative_dirichlet_grid_row_slice_gridentrylastvalue. (((((dfg_last_dirichlet_grid_row_slice_gridentry) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_gridentrylastvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_gridentrylastvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridentrylastvaluedecode. (((dfg_last_dirichlet_grid_row_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridentrylastvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_gridentrylastvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_gridentrylastvalue) = S ge_signed_half_dirichlet_grid_row_slice_gridentrylastvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_gridentrylast) + ge_balance_negative_dirichlet_grid_row_slice_gridentrylastvalue = (dst_negative_dirichlet_grid_row_slice_gridentrylast) + ge_balance_positive_dirichlet_grid_row_slice_gridentrylastvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_slice_gridentrymiddle dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle dst_negative_code_dirichlet_grid_row_slice_gridentrymiddle dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle dst_positive_dirichlet_grid_row_slice_gridentrymiddle dst_negative_dirichlet_grid_row_slice_gridentrymiddle. (((G) = (((((dst_positive_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle)) * S ((dst_positive_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle)) + ((dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle))) + (((dst_negative_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle)) * S ((dst_positive_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle)) + ((dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle))) + (((dst_negative_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)))) + ((((dst_negative_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle))) + (((dst_negative_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_gridentrymiddlepositive. ff_h_pvs_dirichlet_grid_row_slice_gridentrymiddlepositive + S (dst_positive_dirichlet_grid_row_slice_gridentrymiddle) = S ((S (dfg_middle_dirichlet_grid_row_slice_gridentry)) * dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_gridentrymiddlepositive. dst_positive_code_dirichlet_grid_row_slice_gridentrymiddle = ff_q_pvs_dirichlet_grid_row_slice_gridentrymiddlepositive * S ((S (dfg_middle_dirichlet_grid_row_slice_gridentry)) * dst_positive_scale_dirichlet_grid_row_slice_gridentrymiddle) + (dst_positive_dirichlet_grid_row_slice_gridentrymiddle))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_gridentrymiddlenegative. ff_h_pvs_dirichlet_grid_row_slice_gridentrymiddlenegative + S (dst_negative_dirichlet_grid_row_slice_gridentrymiddle) = S ((S (dfg_middle_dirichlet_grid_row_slice_gridentry)) * dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_gridentrymiddlenegative. dst_negative_code_dirichlet_grid_row_slice_gridentrymiddle = ff_q_pvs_dirichlet_grid_row_slice_gridentrymiddlenegative * S ((S (dfg_middle_dirichlet_grid_row_slice_gridentry)) * dst_negative_scale_dirichlet_grid_row_slice_gridentrymiddle) + (dst_negative_dirichlet_grid_row_slice_gridentrymiddle))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_gridentrymiddlevalue ge_balance_negative_dirichlet_grid_row_slice_gridentrymiddlevalue. (((((dfg_value_dirichlet_grid_row_slice_gridentry) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_gridentrymiddlevalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_gridentrymiddlevalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridentrymiddlevaluedecode. (((dfg_value_dirichlet_grid_row_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridentrymiddlevaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_gridentrymiddlevalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_gridentrymiddlevalue) = S ge_signed_half_dirichlet_grid_row_slice_gridentrymiddlevaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_gridentrymiddle) + ge_balance_negative_dirichlet_grid_row_slice_gridentrymiddlevalue = (dst_negative_dirichlet_grid_row_slice_gridentrymiddle) + ge_balance_positive_dirichlet_grid_row_slice_gridentrymiddlevalue))))))))) /\ (exists dfg_inner_dirichlet_grid_row_slice_gridentryproduct. ((exists sto_ap_dirichlet_grid_row_slice_gridentryproductinner sto_an_dirichlet_grid_row_slice_gridentryproductinner sto_bp_dirichlet_grid_row_slice_gridentryproductinner sto_bn_dirichlet_grid_row_slice_gridentryproductinner sto_cp_dirichlet_grid_row_slice_gridentryproductinner sto_cn_dirichlet_grid_row_slice_gridentryproductinner. (((((dfg_last_dirichlet_grid_row_slice_gridentry) = 2 * (sto_ap_dirichlet_grid_row_slice_gridentryproductinner) /\ (sto_an_dirichlet_grid_row_slice_gridentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridentryproductinnerleft. (((dfg_last_dirichlet_grid_row_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridentryproductinnerleft + 1 /\ (sto_ap_dirichlet_grid_row_slice_gridentryproductinner) = 0) /\ (sto_an_dirichlet_grid_row_slice_gridentryproductinner) = S ge_signed_half_dirichlet_grid_row_slice_gridentryproductinnerleft))) /\ ((((((dfg_value_dirichlet_grid_row_slice_gridentry) = 2 * (sto_bp_dirichlet_grid_row_slice_gridentryproductinner) /\ (sto_bn_dirichlet_grid_row_slice_gridentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridentryproductinnerright. (((dfg_value_dirichlet_grid_row_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridentryproductinnerright + 1 /\ (sto_bp_dirichlet_grid_row_slice_gridentryproductinner) = 0) /\ (sto_bn_dirichlet_grid_row_slice_gridentryproductinner) = S ge_signed_half_dirichlet_grid_row_slice_gridentryproductinnerright))) /\ ((((((dfg_inner_dirichlet_grid_row_slice_gridentryproduct) = 2 * (sto_cp_dirichlet_grid_row_slice_gridentryproductinner) /\ (sto_cn_dirichlet_grid_row_slice_gridentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridentryproductinneroutput. (((dfg_inner_dirichlet_grid_row_slice_gridentryproduct) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridentryproductinneroutput + 1 /\ (sto_cp_dirichlet_grid_row_slice_gridentryproductinner) = 0) /\ (sto_cn_dirichlet_grid_row_slice_gridentryproductinner) = S ge_signed_half_dirichlet_grid_row_slice_gridentryproductinneroutput))) /\ ((sto_ap_dirichlet_grid_row_slice_gridentryproductinner * sto_bp_dirichlet_grid_row_slice_gridentryproductinner + sto_an_dirichlet_grid_row_slice_gridentryproductinner * sto_bn_dirichlet_grid_row_slice_gridentryproductinner) + sto_cn_dirichlet_grid_row_slice_gridentryproductinner = (sto_ap_dirichlet_grid_row_slice_gridentryproductinner * sto_bn_dirichlet_grid_row_slice_gridentryproductinner + sto_an_dirichlet_grid_row_slice_gridentryproductinner * sto_bp_dirichlet_grid_row_slice_gridentryproductinner) + sto_cp_dirichlet_grid_row_slice_gridentryproductinner))))))) /\ (exists sto_ap_dirichlet_grid_row_slice_gridentryproductouter sto_an_dirichlet_grid_row_slice_gridentryproductouter sto_bp_dirichlet_grid_row_slice_gridentryproductouter sto_bn_dirichlet_grid_row_slice_gridentryproductouter sto_cp_dirichlet_grid_row_slice_gridentryproductouter sto_cn_dirichlet_grid_row_slice_gridentryproductouter. (((((dfg_first_dirichlet_grid_row_slice_gridentry) = 2 * (sto_ap_dirichlet_grid_row_slice_gridentryproductouter) /\ (sto_an_dirichlet_grid_row_slice_gridentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridentryproductouterleft. (((dfg_first_dirichlet_grid_row_slice_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridentryproductouterleft + 1 /\ (sto_ap_dirichlet_grid_row_slice_gridentryproductouter) = 0) /\ (sto_an_dirichlet_grid_row_slice_gridentryproductouter) = S ge_signed_half_dirichlet_grid_row_slice_gridentryproductouterleft))) /\ ((((((dfg_inner_dirichlet_grid_row_slice_gridentryproduct) = 2 * (sto_bp_dirichlet_grid_row_slice_gridentryproductouter) /\ (sto_bn_dirichlet_grid_row_slice_gridentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridentryproductouterright. (((dfg_inner_dirichlet_grid_row_slice_gridentryproduct) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridentryproductouterright + 1 /\ (sto_bp_dirichlet_grid_row_slice_gridentryproductouter) = 0) /\ (sto_bn_dirichlet_grid_row_slice_gridentryproductouter) = S ge_signed_half_dirichlet_grid_row_slice_gridentryproductouterright))) /\ ((((((dfg_grid_value_dirichlet_grid_row_slice_grid) = 2 * (sto_cp_dirichlet_grid_row_slice_gridentryproductouter) /\ (sto_cn_dirichlet_grid_row_slice_gridentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_gridentryproductouteroutput. (((dfg_grid_value_dirichlet_grid_row_slice_grid) = 2 * ge_signed_half_dirichlet_grid_row_slice_gridentryproductouteroutput + 1 /\ (sto_cp_dirichlet_grid_row_slice_gridentryproductouter) = 0) /\ (sto_cn_dirichlet_grid_row_slice_gridentryproductouter) = S ge_signed_half_dirichlet_grid_row_slice_gridentryproductouteroutput))) /\ ((sto_ap_dirichlet_grid_row_slice_gridentryproductouter * sto_bp_dirichlet_grid_row_slice_gridentryproductouter + sto_an_dirichlet_grid_row_slice_gridentryproductouter * sto_bn_dirichlet_grid_row_slice_gridentryproductouter) + sto_cn_dirichlet_grid_row_slice_gridentryproductouter = (sto_ap_dirichlet_grid_row_slice_gridentryproductouter * sto_bn_dirichlet_grid_row_slice_gridentryproductouter + sto_an_dirichlet_grid_row_slice_gridentryproductouter * sto_bp_dirichlet_grid_row_slice_gridentryproductouter) + sto_cp_dirichlet_grid_row_slice_gridentryproductouter))))))))))))))))))))) \/ ((((dfg_grid_row_dirichlet_grid_row_slice_grid)=0 \/ ((dfg_grid_column_dirichlet_grid_row_slice_grid)=0 \/ ~(exists pvs_factor_dirichlet_grid_row_slice_gridentryomittednondivisor. (n) = ((dfg_grid_row_dirichlet_grid_row_slice_grid)*(dfg_grid_column_dirichlet_grid_row_slice_grid)) * pvs_factor_dirichlet_grid_row_slice_gridentryomittednondivisor))) /\ ((dfg_grid_value_dirichlet_grid_row_slice_grid)=0))))))) -> (exists pvs_le_gap_dirichlet_grid_row_slice_bound. pvs_le_gap_dirichlet_grid_row_slice_bound + (a) = (n)) -> (((exists dst_positive_code_dirichlet_grid_row_slice_slicesource_table dst_positive_scale_dirichlet_grid_row_slice_slicesource_table dst_negative_code_dirichlet_grid_row_slice_slicesource_table dst_negative_scale_dirichlet_grid_row_slice_slicesource_table. (((T) = (((((dst_positive_code_dirichlet_grid_row_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_row_slice_slicesource_table)) * S ((dst_positive_code_dirichlet_grid_row_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_row_slice_slicesource_table)) + ((dst_positive_scale_dirichlet_grid_row_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_row_slice_slicesource_table))) + (((dst_negative_code_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)) * S ((dst_negative_code_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)) + ((dst_negative_scale_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_row_slice_slicesource_table)) * S ((dst_positive_code_dirichlet_grid_row_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_row_slice_slicesource_table)) + ((dst_positive_scale_dirichlet_grid_row_slice_slicesource_table) + (dst_positive_scale_dirichlet_grid_row_slice_slicesource_table))) + (((dst_negative_code_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)) * S ((dst_negative_code_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)) + ((dst_negative_scale_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)))) + ((((dst_negative_code_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)) * S ((dst_negative_code_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)) + ((dst_negative_scale_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table))) + (((dst_negative_code_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)) * S ((dst_negative_code_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)) + ((dst_negative_scale_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)))))) /\ (forall dst_index_dirichlet_grid_row_slice_slicesource_table. (exists pvs_le_gap_dirichlet_grid_row_slice_slicesource_tabledomain. pvs_le_gap_dirichlet_grid_row_slice_slicesource_tabledomain + (dst_index_dirichlet_grid_row_slice_slicesource_table) = (0)) -> exists dst_positive_dirichlet_grid_row_slice_slicesource_table dst_negative_dirichlet_grid_row_slice_slicesource_table dst_value_dirichlet_grid_row_slice_slicesource_table. ((((exists ff_h_pvs_dirichlet_grid_row_slice_slicesource_tableentrypositive. ff_h_pvs_dirichlet_grid_row_slice_slicesource_tableentrypositive + S (dst_positive_dirichlet_grid_row_slice_slicesource_table) = S ((S (dst_index_dirichlet_grid_row_slice_slicesource_table)) * dst_positive_scale_dirichlet_grid_row_slice_slicesource_table)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_slicesource_tableentrypositive. dst_positive_code_dirichlet_grid_row_slice_slicesource_table = ff_q_pvs_dirichlet_grid_row_slice_slicesource_tableentrypositive * S ((S (dst_index_dirichlet_grid_row_slice_slicesource_table)) * dst_positive_scale_dirichlet_grid_row_slice_slicesource_table) + (dst_positive_dirichlet_grid_row_slice_slicesource_table))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_slicesource_tableentrynegative. ff_h_pvs_dirichlet_grid_row_slice_slicesource_tableentrynegative + S (dst_negative_dirichlet_grid_row_slice_slicesource_table) = S ((S (dst_index_dirichlet_grid_row_slice_slicesource_table)) * dst_negative_scale_dirichlet_grid_row_slice_slicesource_table)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_slicesource_tableentrynegative. dst_negative_code_dirichlet_grid_row_slice_slicesource_table = ff_q_pvs_dirichlet_grid_row_slice_slicesource_tableentrynegative * S ((S (dst_index_dirichlet_grid_row_slice_slicesource_table)) * dst_negative_scale_dirichlet_grid_row_slice_slicesource_table) + (dst_negative_dirichlet_grid_row_slice_slicesource_table))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_slicesource_tableentryvalue ge_balance_negative_dirichlet_grid_row_slice_slicesource_tableentryvalue. (((((dst_value_dirichlet_grid_row_slice_slicesource_table) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_slicesource_tableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_slicesource_tableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_slicesource_tableentryvaluedecode. (((dst_value_dirichlet_grid_row_slice_slicesource_table) = 2 * ge_signed_half_dirichlet_grid_row_slice_slicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_slicesource_tableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_slicesource_tableentryvalue) = S ge_signed_half_dirichlet_grid_row_slice_slicesource_tableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_slicesource_table) + ge_balance_negative_dirichlet_grid_row_slice_slicesource_tableentryvalue = (dst_negative_dirichlet_grid_row_slice_slicesource_table) + ge_balance_positive_dirichlet_grid_row_slice_slicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_slice_sliceoutput_table dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table dst_negative_code_dirichlet_grid_row_slice_sliceoutput_table dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table. (((V) = (((((dst_positive_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table)) * S ((dst_positive_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table)) + ((dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table))) + (((dst_negative_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table)) * S ((dst_positive_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table)) + ((dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table))) + (((dst_negative_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)))) + ((((dst_negative_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table))) + (((dst_negative_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)))))) /\ (forall dst_index_dirichlet_grid_row_slice_sliceoutput_table. (exists pvs_le_gap_dirichlet_grid_row_slice_sliceoutput_tabledomain. pvs_le_gap_dirichlet_grid_row_slice_sliceoutput_tabledomain + (dst_index_dirichlet_grid_row_slice_sliceoutput_table) = (S n)) -> exists dst_positive_dirichlet_grid_row_slice_sliceoutput_table dst_negative_dirichlet_grid_row_slice_sliceoutput_table dst_value_dirichlet_grid_row_slice_sliceoutput_table. ((((exists ff_h_pvs_dirichlet_grid_row_slice_sliceoutput_tableentrypositive. ff_h_pvs_dirichlet_grid_row_slice_sliceoutput_tableentrypositive + S (dst_positive_dirichlet_grid_row_slice_sliceoutput_table) = S ((S (dst_index_dirichlet_grid_row_slice_sliceoutput_table)) * dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_sliceoutput_tableentrypositive. dst_positive_code_dirichlet_grid_row_slice_sliceoutput_table = ff_q_pvs_dirichlet_grid_row_slice_sliceoutput_tableentrypositive * S ((S (dst_index_dirichlet_grid_row_slice_sliceoutput_table)) * dst_positive_scale_dirichlet_grid_row_slice_sliceoutput_table) + (dst_positive_dirichlet_grid_row_slice_sliceoutput_table))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_sliceoutput_tableentrynegative. ff_h_pvs_dirichlet_grid_row_slice_sliceoutput_tableentrynegative + S (dst_negative_dirichlet_grid_row_slice_sliceoutput_table) = S ((S (dst_index_dirichlet_grid_row_slice_sliceoutput_table)) * dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_sliceoutput_tableentrynegative. dst_negative_code_dirichlet_grid_row_slice_sliceoutput_table = ff_q_pvs_dirichlet_grid_row_slice_sliceoutput_tableentrynegative * S ((S (dst_index_dirichlet_grid_row_slice_sliceoutput_table)) * dst_negative_scale_dirichlet_grid_row_slice_sliceoutput_table) + (dst_negative_dirichlet_grid_row_slice_sliceoutput_table))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_sliceoutput_tableentryvalue ge_balance_negative_dirichlet_grid_row_slice_sliceoutput_tableentryvalue. (((((dst_value_dirichlet_grid_row_slice_sliceoutput_table) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_sliceoutput_tableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_sliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_sliceoutput_tableentryvaluedecode. (((dst_value_dirichlet_grid_row_slice_sliceoutput_table) = 2 * ge_signed_half_dirichlet_grid_row_slice_sliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_sliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_sliceoutput_tableentryvalue) = S ge_signed_half_dirichlet_grid_row_slice_sliceoutput_tableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_sliceoutput_table) + ge_balance_negative_dirichlet_grid_row_slice_sliceoutput_tableentryvalue = (dst_negative_dirichlet_grid_row_slice_sliceoutput_table) + ge_balance_positive_dirichlet_grid_row_slice_sliceoutput_tableentryvalue))))))))) /\ (forall srs_index_dirichlet_grid_row_slice_slice. (exists pvs_gap_dirichlet_grid_row_slice_slicebound. pvs_gap_dirichlet_grid_row_slice_slicebound + S (srs_index_dirichlet_grid_row_slice_slice) = (S n)) -> exists srs_value_dirichlet_grid_row_slice_slice. (((exists dst_positive_code_dirichlet_grid_row_slice_sliceentrysource dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource dst_negative_code_dirichlet_grid_row_slice_sliceentrysource dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource dst_positive_dirichlet_grid_row_slice_sliceentrysource dst_negative_dirichlet_grid_row_slice_sliceentrysource. (((T) = (((((dst_positive_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource)) * S ((dst_positive_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource)) + ((dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource))) + (((dst_negative_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource)) * S ((dst_positive_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource)) + ((dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource))) + (((dst_negative_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)))) + ((((dst_negative_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource))) + (((dst_negative_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_sliceentrysourcepositive. ff_h_pvs_dirichlet_grid_row_slice_sliceentrysourcepositive + S (dst_positive_dirichlet_grid_row_slice_sliceentrysource) = S ((S (((0+(S n)*a) + ((1) * (srs_index_dirichlet_grid_row_slice_slice))))) * dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_sliceentrysourcepositive. dst_positive_code_dirichlet_grid_row_slice_sliceentrysource = ff_q_pvs_dirichlet_grid_row_slice_sliceentrysourcepositive * S ((S (((0+(S n)*a) + ((1) * (srs_index_dirichlet_grid_row_slice_slice))))) * dst_positive_scale_dirichlet_grid_row_slice_sliceentrysource) + (dst_positive_dirichlet_grid_row_slice_sliceentrysource))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_sliceentrysourcenegative. ff_h_pvs_dirichlet_grid_row_slice_sliceentrysourcenegative + S (dst_negative_dirichlet_grid_row_slice_sliceentrysource) = S ((S (((0+(S n)*a) + ((1) * (srs_index_dirichlet_grid_row_slice_slice))))) * dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_sliceentrysourcenegative. dst_negative_code_dirichlet_grid_row_slice_sliceentrysource = ff_q_pvs_dirichlet_grid_row_slice_sliceentrysourcenegative * S ((S (((0+(S n)*a) + ((1) * (srs_index_dirichlet_grid_row_slice_slice))))) * dst_negative_scale_dirichlet_grid_row_slice_sliceentrysource) + (dst_negative_dirichlet_grid_row_slice_sliceentrysource))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_sliceentrysourcevalue ge_balance_negative_dirichlet_grid_row_slice_sliceentrysourcevalue. (((((srs_value_dirichlet_grid_row_slice_slice) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_sliceentrysourcevalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_sliceentrysourcevalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_sliceentrysourcevaluedecode. (((srs_value_dirichlet_grid_row_slice_slice) = 2 * ge_signed_half_dirichlet_grid_row_slice_sliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_sliceentrysourcevalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_sliceentrysourcevalue) = S ge_signed_half_dirichlet_grid_row_slice_sliceentrysourcevaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_sliceentrysource) + ge_balance_negative_dirichlet_grid_row_slice_sliceentrysourcevalue = (dst_negative_dirichlet_grid_row_slice_sliceentrysource) + ge_balance_positive_dirichlet_grid_row_slice_sliceentrysourcevalue))))))))) /\ (exists dst_positive_code_dirichlet_grid_row_slice_sliceentryoutput dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput dst_negative_code_dirichlet_grid_row_slice_sliceentryoutput dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput dst_positive_dirichlet_grid_row_slice_sliceentryoutput dst_negative_dirichlet_grid_row_slice_sliceentryoutput. (((V) = (((((dst_positive_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput)) * S ((dst_positive_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput)) + ((dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput))) + (((dst_negative_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput)) * S ((dst_positive_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput)) + ((dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput))) + (((dst_negative_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)))) + ((((dst_negative_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput))) + (((dst_negative_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_sliceentryoutputpositive. ff_h_pvs_dirichlet_grid_row_slice_sliceentryoutputpositive + S (dst_positive_dirichlet_grid_row_slice_sliceentryoutput) = S ((S (srs_index_dirichlet_grid_row_slice_slice)) * dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_sliceentryoutputpositive. dst_positive_code_dirichlet_grid_row_slice_sliceentryoutput = ff_q_pvs_dirichlet_grid_row_slice_sliceentryoutputpositive * S ((S (srs_index_dirichlet_grid_row_slice_slice)) * dst_positive_scale_dirichlet_grid_row_slice_sliceentryoutput) + (dst_positive_dirichlet_grid_row_slice_sliceentryoutput))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_sliceentryoutputnegative. ff_h_pvs_dirichlet_grid_row_slice_sliceentryoutputnegative + S (dst_negative_dirichlet_grid_row_slice_sliceentryoutput) = S ((S (srs_index_dirichlet_grid_row_slice_slice)) * dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_sliceentryoutputnegative. dst_negative_code_dirichlet_grid_row_slice_sliceentryoutput = ff_q_pvs_dirichlet_grid_row_slice_sliceentryoutputnegative * S ((S (srs_index_dirichlet_grid_row_slice_slice)) * dst_negative_scale_dirichlet_grid_row_slice_sliceentryoutput) + (dst_negative_dirichlet_grid_row_slice_sliceentryoutput))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_sliceentryoutputvalue ge_balance_negative_dirichlet_grid_row_slice_sliceentryoutputvalue. (((((srs_value_dirichlet_grid_row_slice_slice) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_sliceentryoutputvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_sliceentryoutputvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_sliceentryoutputvaluedecode. (((srs_value_dirichlet_grid_row_slice_slice) = 2 * ge_signed_half_dirichlet_grid_row_slice_sliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_sliceentryoutputvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_sliceentryoutputvalue) = S ge_signed_half_dirichlet_grid_row_slice_sliceentryoutputvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_sliceentryoutput) + ge_balance_negative_dirichlet_grid_row_slice_sliceentryoutputvalue = (dst_negative_dirichlet_grid_row_slice_sliceentryoutput) + ge_balance_positive_dirichlet_grid_row_slice_sliceentryoutputvalue)))))))))))))))) -> (((exists dst_positive_code_dirichlet_grid_row_slice_resulttable dst_positive_scale_dirichlet_grid_row_slice_resulttable dst_negative_code_dirichlet_grid_row_slice_resulttable dst_negative_scale_dirichlet_grid_row_slice_resulttable. (((V) = (((((dst_positive_code_dirichlet_grid_row_slice_resulttable) + (dst_positive_scale_dirichlet_grid_row_slice_resulttable)) * S ((dst_positive_code_dirichlet_grid_row_slice_resulttable) + (dst_positive_scale_dirichlet_grid_row_slice_resulttable)) + ((dst_positive_scale_dirichlet_grid_row_slice_resulttable) + (dst_positive_scale_dirichlet_grid_row_slice_resulttable))) + (((dst_negative_code_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)) * S ((dst_negative_code_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)) + ((dst_negative_scale_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_resulttable) + (dst_positive_scale_dirichlet_grid_row_slice_resulttable)) * S ((dst_positive_code_dirichlet_grid_row_slice_resulttable) + (dst_positive_scale_dirichlet_grid_row_slice_resulttable)) + ((dst_positive_scale_dirichlet_grid_row_slice_resulttable) + (dst_positive_scale_dirichlet_grid_row_slice_resulttable))) + (((dst_negative_code_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)) * S ((dst_negative_code_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)) + ((dst_negative_scale_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)))) + ((((dst_negative_code_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)) * S ((dst_negative_code_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)) + ((dst_negative_scale_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable))) + (((dst_negative_code_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)) * S ((dst_negative_code_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)) + ((dst_negative_scale_dirichlet_grid_row_slice_resulttable) + (dst_negative_scale_dirichlet_grid_row_slice_resulttable)))))) /\ (forall dst_index_dirichlet_grid_row_slice_resulttable. (exists pvs_le_gap_dirichlet_grid_row_slice_resulttabledomain. pvs_le_gap_dirichlet_grid_row_slice_resulttabledomain + (dst_index_dirichlet_grid_row_slice_resulttable) = (S (n))) -> exists dst_positive_dirichlet_grid_row_slice_resulttable dst_negative_dirichlet_grid_row_slice_resulttable dst_value_dirichlet_grid_row_slice_resulttable. ((((exists ff_h_pvs_dirichlet_grid_row_slice_resulttableentrypositive. ff_h_pvs_dirichlet_grid_row_slice_resulttableentrypositive + S (dst_positive_dirichlet_grid_row_slice_resulttable) = S ((S (dst_index_dirichlet_grid_row_slice_resulttable)) * dst_positive_scale_dirichlet_grid_row_slice_resulttable)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_resulttableentrypositive. dst_positive_code_dirichlet_grid_row_slice_resulttable = ff_q_pvs_dirichlet_grid_row_slice_resulttableentrypositive * S ((S (dst_index_dirichlet_grid_row_slice_resulttable)) * dst_positive_scale_dirichlet_grid_row_slice_resulttable) + (dst_positive_dirichlet_grid_row_slice_resulttable))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_resulttableentrynegative. ff_h_pvs_dirichlet_grid_row_slice_resulttableentrynegative + S (dst_negative_dirichlet_grid_row_slice_resulttable) = S ((S (dst_index_dirichlet_grid_row_slice_resulttable)) * dst_negative_scale_dirichlet_grid_row_slice_resulttable)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_resulttableentrynegative. dst_negative_code_dirichlet_grid_row_slice_resulttable = ff_q_pvs_dirichlet_grid_row_slice_resulttableentrynegative * S ((S (dst_index_dirichlet_grid_row_slice_resulttable)) * dst_negative_scale_dirichlet_grid_row_slice_resulttable) + (dst_negative_dirichlet_grid_row_slice_resulttable))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_resulttableentryvalue ge_balance_negative_dirichlet_grid_row_slice_resulttableentryvalue. (((((dst_value_dirichlet_grid_row_slice_resulttable) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_resulttableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_resulttableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resulttableentryvaluedecode. (((dst_value_dirichlet_grid_row_slice_resulttable) = 2 * ge_signed_half_dirichlet_grid_row_slice_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_resulttableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_resulttableentryvalue) = S ge_signed_half_dirichlet_grid_row_slice_resulttableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_resulttable) + ge_balance_negative_dirichlet_grid_row_slice_resulttableentryvalue = (dst_negative_dirichlet_grid_row_slice_resulttable) + ge_balance_positive_dirichlet_grid_row_slice_resulttableentryvalue))))))))) /\ (forall dfg_factor_column_dirichlet_grid_row_slice_result dfg_factor_value_dirichlet_grid_row_slice_result. (exists pvs_le_gap_dirichlet_grid_row_slice_resultbound. pvs_le_gap_dirichlet_grid_row_slice_resultbound + (dfg_factor_column_dirichlet_grid_row_slice_result) = (n)) -> (exists dst_positive_code_dirichlet_grid_row_slice_resultlookup dst_positive_scale_dirichlet_grid_row_slice_resultlookup dst_negative_code_dirichlet_grid_row_slice_resultlookup dst_negative_scale_dirichlet_grid_row_slice_resultlookup dst_positive_dirichlet_grid_row_slice_resultlookup dst_negative_dirichlet_grid_row_slice_resultlookup. (((V) = (((((dst_positive_code_dirichlet_grid_row_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_row_slice_resultlookup)) * S ((dst_positive_code_dirichlet_grid_row_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_row_slice_resultlookup)) + ((dst_positive_scale_dirichlet_grid_row_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_row_slice_resultlookup))) + (((dst_negative_code_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_row_slice_resultlookup)) * S ((dst_positive_code_dirichlet_grid_row_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_row_slice_resultlookup)) + ((dst_positive_scale_dirichlet_grid_row_slice_resultlookup) + (dst_positive_scale_dirichlet_grid_row_slice_resultlookup))) + (((dst_negative_code_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)))) + ((((dst_negative_code_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup))) + (((dst_negative_code_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultlookup) + (dst_negative_scale_dirichlet_grid_row_slice_resultlookup)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_resultlookuppositive. ff_h_pvs_dirichlet_grid_row_slice_resultlookuppositive + S (dst_positive_dirichlet_grid_row_slice_resultlookup) = S ((S (dfg_factor_column_dirichlet_grid_row_slice_result)) * dst_positive_scale_dirichlet_grid_row_slice_resultlookup)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_resultlookuppositive. dst_positive_code_dirichlet_grid_row_slice_resultlookup = ff_q_pvs_dirichlet_grid_row_slice_resultlookuppositive * S ((S (dfg_factor_column_dirichlet_grid_row_slice_result)) * dst_positive_scale_dirichlet_grid_row_slice_resultlookup) + (dst_positive_dirichlet_grid_row_slice_resultlookup))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_resultlookupnegative. ff_h_pvs_dirichlet_grid_row_slice_resultlookupnegative + S (dst_negative_dirichlet_grid_row_slice_resultlookup) = S ((S (dfg_factor_column_dirichlet_grid_row_slice_result)) * dst_negative_scale_dirichlet_grid_row_slice_resultlookup)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_resultlookupnegative. dst_negative_code_dirichlet_grid_row_slice_resultlookup = ff_q_pvs_dirichlet_grid_row_slice_resultlookupnegative * S ((S (dfg_factor_column_dirichlet_grid_row_slice_result)) * dst_negative_scale_dirichlet_grid_row_slice_resultlookup) + (dst_negative_dirichlet_grid_row_slice_resultlookup))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_resultlookupvalue ge_balance_negative_dirichlet_grid_row_slice_resultlookupvalue. (((((dfg_factor_value_dirichlet_grid_row_slice_result) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_resultlookupvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_resultlookupvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resultlookupvaluedecode. (((dfg_factor_value_dirichlet_grid_row_slice_result) = 2 * ge_signed_half_dirichlet_grid_row_slice_resultlookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_resultlookupvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_resultlookupvalue) = S ge_signed_half_dirichlet_grid_row_slice_resultlookupvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_resultlookup) + ge_balance_negative_dirichlet_grid_row_slice_resultlookupvalue = (dst_negative_dirichlet_grid_row_slice_resultlookup) + ge_balance_positive_dirichlet_grid_row_slice_resultlookupvalue))))))))) -> ((((~((a)=0)) /\ (((~((dfg_factor_column_dirichlet_grid_row_slice_result)=0)) /\ (exists dfg_middle_dirichlet_grid_row_slice_resultentry dfg_first_dirichlet_grid_row_slice_resultentry dfg_last_dirichlet_grid_row_slice_resultentry dfg_value_dirichlet_grid_row_slice_resultentry. (((n)=((a)*(dfg_factor_column_dirichlet_grid_row_slice_result))*dfg_middle_dirichlet_grid_row_slice_resultentry) /\ (((exists dst_positive_code_dirichlet_grid_row_slice_resultentryfirst dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst dst_negative_code_dirichlet_grid_row_slice_resultentryfirst dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst dst_positive_dirichlet_grid_row_slice_resultentryfirst dst_negative_dirichlet_grid_row_slice_resultentryfirst. (((F) = (((((dst_positive_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst)) * S ((dst_positive_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst)) + ((dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst))) + (((dst_negative_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst)) * S ((dst_positive_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst)) + ((dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst) + (dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst))) + (((dst_negative_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)))) + ((((dst_negative_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst))) + (((dst_negative_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_resultentryfirstpositive. ff_h_pvs_dirichlet_grid_row_slice_resultentryfirstpositive + S (dst_positive_dirichlet_grid_row_slice_resultentryfirst) = S ((S (a)) * dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_resultentryfirstpositive. dst_positive_code_dirichlet_grid_row_slice_resultentryfirst = ff_q_pvs_dirichlet_grid_row_slice_resultentryfirstpositive * S ((S (a)) * dst_positive_scale_dirichlet_grid_row_slice_resultentryfirst) + (dst_positive_dirichlet_grid_row_slice_resultentryfirst))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_resultentryfirstnegative. ff_h_pvs_dirichlet_grid_row_slice_resultentryfirstnegative + S (dst_negative_dirichlet_grid_row_slice_resultentryfirst) = S ((S (a)) * dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_resultentryfirstnegative. dst_negative_code_dirichlet_grid_row_slice_resultentryfirst = ff_q_pvs_dirichlet_grid_row_slice_resultentryfirstnegative * S ((S (a)) * dst_negative_scale_dirichlet_grid_row_slice_resultentryfirst) + (dst_negative_dirichlet_grid_row_slice_resultentryfirst))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_resultentryfirstvalue ge_balance_negative_dirichlet_grid_row_slice_resultentryfirstvalue. (((((dfg_first_dirichlet_grid_row_slice_resultentry) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_resultentryfirstvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_resultentryfirstvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resultentryfirstvaluedecode. (((dfg_first_dirichlet_grid_row_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_resultentryfirstvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_resultentryfirstvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_resultentryfirstvalue) = S ge_signed_half_dirichlet_grid_row_slice_resultentryfirstvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_resultentryfirst) + ge_balance_negative_dirichlet_grid_row_slice_resultentryfirstvalue = (dst_negative_dirichlet_grid_row_slice_resultentryfirst) + ge_balance_positive_dirichlet_grid_row_slice_resultentryfirstvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_slice_resultentrylast dst_positive_scale_dirichlet_grid_row_slice_resultentrylast dst_negative_code_dirichlet_grid_row_slice_resultentrylast dst_negative_scale_dirichlet_grid_row_slice_resultentrylast dst_positive_dirichlet_grid_row_slice_resultentrylast dst_negative_dirichlet_grid_row_slice_resultentrylast. (((H) = (((((dst_positive_code_dirichlet_grid_row_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrylast)) * S ((dst_positive_code_dirichlet_grid_row_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrylast)) + ((dst_positive_scale_dirichlet_grid_row_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrylast))) + (((dst_negative_code_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrylast)) * S ((dst_positive_code_dirichlet_grid_row_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrylast)) + ((dst_positive_scale_dirichlet_grid_row_slice_resultentrylast) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrylast))) + (((dst_negative_code_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)))) + ((((dst_negative_code_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast))) + (((dst_negative_code_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_resultentrylastpositive. ff_h_pvs_dirichlet_grid_row_slice_resultentrylastpositive + S (dst_positive_dirichlet_grid_row_slice_resultentrylast) = S ((S (dfg_factor_column_dirichlet_grid_row_slice_result)) * dst_positive_scale_dirichlet_grid_row_slice_resultentrylast)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_resultentrylastpositive. dst_positive_code_dirichlet_grid_row_slice_resultentrylast = ff_q_pvs_dirichlet_grid_row_slice_resultentrylastpositive * S ((S (dfg_factor_column_dirichlet_grid_row_slice_result)) * dst_positive_scale_dirichlet_grid_row_slice_resultentrylast) + (dst_positive_dirichlet_grid_row_slice_resultentrylast))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_resultentrylastnegative. ff_h_pvs_dirichlet_grid_row_slice_resultentrylastnegative + S (dst_negative_dirichlet_grid_row_slice_resultentrylast) = S ((S (dfg_factor_column_dirichlet_grid_row_slice_result)) * dst_negative_scale_dirichlet_grid_row_slice_resultentrylast)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_resultentrylastnegative. dst_negative_code_dirichlet_grid_row_slice_resultentrylast = ff_q_pvs_dirichlet_grid_row_slice_resultentrylastnegative * S ((S (dfg_factor_column_dirichlet_grid_row_slice_result)) * dst_negative_scale_dirichlet_grid_row_slice_resultentrylast) + (dst_negative_dirichlet_grid_row_slice_resultentrylast))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_resultentrylastvalue ge_balance_negative_dirichlet_grid_row_slice_resultentrylastvalue. (((((dfg_last_dirichlet_grid_row_slice_resultentry) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_resultentrylastvalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_resultentrylastvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resultentrylastvaluedecode. (((dfg_last_dirichlet_grid_row_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_resultentrylastvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_resultentrylastvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_resultentrylastvalue) = S ge_signed_half_dirichlet_grid_row_slice_resultentrylastvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_resultentrylast) + ge_balance_negative_dirichlet_grid_row_slice_resultentrylastvalue = (dst_negative_dirichlet_grid_row_slice_resultentrylast) + ge_balance_positive_dirichlet_grid_row_slice_resultentrylastvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_slice_resultentrymiddle dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle dst_negative_code_dirichlet_grid_row_slice_resultentrymiddle dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle dst_positive_dirichlet_grid_row_slice_resultentrymiddle dst_negative_dirichlet_grid_row_slice_resultentrymiddle. (((G) = (((((dst_positive_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle)) * S ((dst_positive_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle)) + ((dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle))) + (((dst_negative_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)))) * S ((((dst_positive_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle)) * S ((dst_positive_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle)) + ((dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle) + (dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle))) + (((dst_negative_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)))) + ((((dst_negative_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle))) + (((dst_negative_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_resultentrymiddlepositive. ff_h_pvs_dirichlet_grid_row_slice_resultentrymiddlepositive + S (dst_positive_dirichlet_grid_row_slice_resultentrymiddle) = S ((S (dfg_middle_dirichlet_grid_row_slice_resultentry)) * dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_resultentrymiddlepositive. dst_positive_code_dirichlet_grid_row_slice_resultentrymiddle = ff_q_pvs_dirichlet_grid_row_slice_resultentrymiddlepositive * S ((S (dfg_middle_dirichlet_grid_row_slice_resultentry)) * dst_positive_scale_dirichlet_grid_row_slice_resultentrymiddle) + (dst_positive_dirichlet_grid_row_slice_resultentrymiddle))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_slice_resultentrymiddlenegative. ff_h_pvs_dirichlet_grid_row_slice_resultentrymiddlenegative + S (dst_negative_dirichlet_grid_row_slice_resultentrymiddle) = S ((S (dfg_middle_dirichlet_grid_row_slice_resultentry)) * dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle)) /\ exists ff_q_pvs_dirichlet_grid_row_slice_resultentrymiddlenegative. dst_negative_code_dirichlet_grid_row_slice_resultentrymiddle = ff_q_pvs_dirichlet_grid_row_slice_resultentrymiddlenegative * S ((S (dfg_middle_dirichlet_grid_row_slice_resultentry)) * dst_negative_scale_dirichlet_grid_row_slice_resultentrymiddle) + (dst_negative_dirichlet_grid_row_slice_resultentrymiddle))) /\ (exists ge_balance_positive_dirichlet_grid_row_slice_resultentrymiddlevalue ge_balance_negative_dirichlet_grid_row_slice_resultentrymiddlevalue. (((((dfg_value_dirichlet_grid_row_slice_resultentry) = 2 * (ge_balance_positive_dirichlet_grid_row_slice_resultentrymiddlevalue) /\ (ge_balance_negative_dirichlet_grid_row_slice_resultentrymiddlevalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resultentrymiddlevaluedecode. (((dfg_value_dirichlet_grid_row_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_resultentrymiddlevaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_slice_resultentrymiddlevalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_slice_resultentrymiddlevalue) = S ge_signed_half_dirichlet_grid_row_slice_resultentrymiddlevaluedecode))) /\ ((dst_positive_dirichlet_grid_row_slice_resultentrymiddle) + ge_balance_negative_dirichlet_grid_row_slice_resultentrymiddlevalue = (dst_negative_dirichlet_grid_row_slice_resultentrymiddle) + ge_balance_positive_dirichlet_grid_row_slice_resultentrymiddlevalue))))))))) /\ (exists dfg_inner_dirichlet_grid_row_slice_resultentryproduct. ((exists sto_ap_dirichlet_grid_row_slice_resultentryproductinner sto_an_dirichlet_grid_row_slice_resultentryproductinner sto_bp_dirichlet_grid_row_slice_resultentryproductinner sto_bn_dirichlet_grid_row_slice_resultentryproductinner sto_cp_dirichlet_grid_row_slice_resultentryproductinner sto_cn_dirichlet_grid_row_slice_resultentryproductinner. (((((dfg_last_dirichlet_grid_row_slice_resultentry) = 2 * (sto_ap_dirichlet_grid_row_slice_resultentryproductinner) /\ (sto_an_dirichlet_grid_row_slice_resultentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resultentryproductinnerleft. (((dfg_last_dirichlet_grid_row_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_resultentryproductinnerleft + 1 /\ (sto_ap_dirichlet_grid_row_slice_resultentryproductinner) = 0) /\ (sto_an_dirichlet_grid_row_slice_resultentryproductinner) = S ge_signed_half_dirichlet_grid_row_slice_resultentryproductinnerleft))) /\ ((((((dfg_value_dirichlet_grid_row_slice_resultentry) = 2 * (sto_bp_dirichlet_grid_row_slice_resultentryproductinner) /\ (sto_bn_dirichlet_grid_row_slice_resultentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resultentryproductinnerright. (((dfg_value_dirichlet_grid_row_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_resultentryproductinnerright + 1 /\ (sto_bp_dirichlet_grid_row_slice_resultentryproductinner) = 0) /\ (sto_bn_dirichlet_grid_row_slice_resultentryproductinner) = S ge_signed_half_dirichlet_grid_row_slice_resultentryproductinnerright))) /\ ((((((dfg_inner_dirichlet_grid_row_slice_resultentryproduct) = 2 * (sto_cp_dirichlet_grid_row_slice_resultentryproductinner) /\ (sto_cn_dirichlet_grid_row_slice_resultentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resultentryproductinneroutput. (((dfg_inner_dirichlet_grid_row_slice_resultentryproduct) = 2 * ge_signed_half_dirichlet_grid_row_slice_resultentryproductinneroutput + 1 /\ (sto_cp_dirichlet_grid_row_slice_resultentryproductinner) = 0) /\ (sto_cn_dirichlet_grid_row_slice_resultentryproductinner) = S ge_signed_half_dirichlet_grid_row_slice_resultentryproductinneroutput))) /\ ((sto_ap_dirichlet_grid_row_slice_resultentryproductinner * sto_bp_dirichlet_grid_row_slice_resultentryproductinner + sto_an_dirichlet_grid_row_slice_resultentryproductinner * sto_bn_dirichlet_grid_row_slice_resultentryproductinner) + sto_cn_dirichlet_grid_row_slice_resultentryproductinner = (sto_ap_dirichlet_grid_row_slice_resultentryproductinner * sto_bn_dirichlet_grid_row_slice_resultentryproductinner + sto_an_dirichlet_grid_row_slice_resultentryproductinner * sto_bp_dirichlet_grid_row_slice_resultentryproductinner) + sto_cp_dirichlet_grid_row_slice_resultentryproductinner))))))) /\ (exists sto_ap_dirichlet_grid_row_slice_resultentryproductouter sto_an_dirichlet_grid_row_slice_resultentryproductouter sto_bp_dirichlet_grid_row_slice_resultentryproductouter sto_bn_dirichlet_grid_row_slice_resultentryproductouter sto_cp_dirichlet_grid_row_slice_resultentryproductouter sto_cn_dirichlet_grid_row_slice_resultentryproductouter. (((((dfg_first_dirichlet_grid_row_slice_resultentry) = 2 * (sto_ap_dirichlet_grid_row_slice_resultentryproductouter) /\ (sto_an_dirichlet_grid_row_slice_resultentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resultentryproductouterleft. (((dfg_first_dirichlet_grid_row_slice_resultentry) = 2 * ge_signed_half_dirichlet_grid_row_slice_resultentryproductouterleft + 1 /\ (sto_ap_dirichlet_grid_row_slice_resultentryproductouter) = 0) /\ (sto_an_dirichlet_grid_row_slice_resultentryproductouter) = S ge_signed_half_dirichlet_grid_row_slice_resultentryproductouterleft))) /\ ((((((dfg_inner_dirichlet_grid_row_slice_resultentryproduct) = 2 * (sto_bp_dirichlet_grid_row_slice_resultentryproductouter) /\ (sto_bn_dirichlet_grid_row_slice_resultentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resultentryproductouterright. (((dfg_inner_dirichlet_grid_row_slice_resultentryproduct) = 2 * ge_signed_half_dirichlet_grid_row_slice_resultentryproductouterright + 1 /\ (sto_bp_dirichlet_grid_row_slice_resultentryproductouter) = 0) /\ (sto_bn_dirichlet_grid_row_slice_resultentryproductouter) = S ge_signed_half_dirichlet_grid_row_slice_resultentryproductouterright))) /\ ((((((dfg_factor_value_dirichlet_grid_row_slice_result) = 2 * (sto_cp_dirichlet_grid_row_slice_resultentryproductouter) /\ (sto_cn_dirichlet_grid_row_slice_resultentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_row_slice_resultentryproductouteroutput. (((dfg_factor_value_dirichlet_grid_row_slice_result) = 2 * ge_signed_half_dirichlet_grid_row_slice_resultentryproductouteroutput + 1 /\ (sto_cp_dirichlet_grid_row_slice_resultentryproductouter) = 0) /\ (sto_cn_dirichlet_grid_row_slice_resultentryproductouter) = S ge_signed_half_dirichlet_grid_row_slice_resultentryproductouteroutput))) /\ ((sto_ap_dirichlet_grid_row_slice_resultentryproductouter * sto_bp_dirichlet_grid_row_slice_resultentryproductouter + sto_an_dirichlet_grid_row_slice_resultentryproductouter * sto_bn_dirichlet_grid_row_slice_resultentryproductouter) + sto_cn_dirichlet_grid_row_slice_resultentryproductouter = (sto_ap_dirichlet_grid_row_slice_resultentryproductouter * sto_bn_dirichlet_grid_row_slice_resultentryproductouter + sto_an_dirichlet_grid_row_slice_resultentryproductouter * sto_bp_dirichlet_grid_row_slice_resultentryproductouter) + sto_cp_dirichlet_grid_row_slice_resultentryproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((dfg_factor_column_dirichlet_grid_row_slice_result)=0 \/ ~(exists pvs_factor_dirichlet_grid_row_slice_resultentryomittednondivisor. (n) = ((a)*(dfg_factor_column_dirichlet_grid_row_slice_result)) * pvs_factor_dirichlet_grid_row_slice_resultentryomittednondivisor))) /\ ((dfg_factor_value_dirichlet_grid_row_slice_result)=0)))))))Complete tactic proof in conservative notation
All 54 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
54 script commands · 9 reading checkpoints · 2 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Separate the logical casesL11–13
03Use earlier factsL14–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
exact hs_right_left
04Fix variables and assumptionsL15–18
05Establish hlL19–28
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed rectangular slice lookup.
- L19
have hl : ArithAt(T,0 + S n · a + 1 · e,z)Definitions: ArithAt(T,0 + S n · a + 1 · e,z)Original native command in the exact edition - L20
specialize signed_rectangular_slice_lookup (T) - L21
specialize signed_rectangular_slice_lookup (V) - L22
specialize signed_rectangular_slice_lookup (0+(S n)*a) - L23
specialize signed_rectangular_slice_lookup (1) - L24
specialize signed_rectangular_slice_lookup (S n) - L25
specialize signed_rectangular_slice_lookup (e) - L26
specialize signed_rectangular_slice_lookup (z) - L27
apply signed_rectangular_slice_lookup - L28
exact hs
06Use earlier factsL29–33
07Establish hindexL34–43
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply zero add.
08Use earlier factsL44–53
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L44
specialize dirichlet_grid_table_lookup (H) - L45
specialize dirichlet_grid_table_lookup (n) - L46
specialize dirichlet_grid_table_lookup (T) - L47
specialize dirichlet_grid_table_lookup (a) - L48
specialize dirichlet_grid_table_lookup (e) - L49
specialize dirichlet_grid_table_lookup (z) - L50
apply dirichlet_grid_table_lookup - L51
exact hg - L52
exact ha - L53
exact he
09Use earlier factsL54–54
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L54
exact hl
Original defined command ledger · 54 lines
- 0001
intro F - 0002
intro G - 0003
intro H - 0004
intro n - 0005
intro T - 0006
intro a - 0007
intro V - 0008
intro hg - 0009
intro ha - 0010
intro hs - 0011
split - 0012
cases hs - 0013
cases hs_right - 0014
exact hs_right_left - 0015
intro e - 0016
intro z - 0017
intro he - 0018
intro hz - 0019
have hl : ArithAt(T,0 + S n · a + 1 · e,z) - 0020
specialize signed_rectangular_slice_lookup (T) - 0021
specialize signed_rectangular_slice_lookup (V) - 0022
specialize signed_rectangular_slice_lookup (0+(S n)*a) - 0023
specialize signed_rectangular_slice_lookup (1) - 0024
specialize signed_rectangular_slice_lookup (S n) - 0025
specialize signed_rectangular_slice_lookup (e) - 0026
specialize signed_rectangular_slice_lookup (z) - 0027
apply signed_rectangular_slice_lookup - 0028
exact hs - 0029
specialize succ_le_succ (e) - 0030
specialize succ_le_succ (n) - 0031
apply succ_le_succ - 0032
exact he - 0033
exact hz - 0034
have hindex : (0+(S n)*a)+(1)*e=(S (n))*(a)+(e) - 0035
congr - 0036
apply zero_add - 0037
apply one_mul - 0038
rewrite hindex at hl - 0039
rewrite hindex at hl - 0040
rewrite hindex at hl - 0041
rewrite hindex at hl - 0042
specialize dirichlet_grid_table_lookup (F) - 0043
specialize dirichlet_grid_table_lookup (G) - 0044
specialize dirichlet_grid_table_lookup (H) - 0045
specialize dirichlet_grid_table_lookup (n) - 0046
specialize dirichlet_grid_table_lookup (T) - 0047
specialize dirichlet_grid_table_lookup (a) - 0048
specialize dirichlet_grid_table_lookup (e) - 0049
specialize dirichlet_grid_table_lookup (z) - 0050
apply dirichlet_grid_table_lookup - 0051
exact hg - 0052
exact ha - 0053
exact he - 0054
exact hl