DF0016 — dirichlet_grid_column_slice

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 + 1 · a,S n,S n) → DirichletFactorRow(H,G,F,n,a,V)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ArithAt(F,i,z) · 1 ArithSlice(F,G,o,s,l) · 1 DirichletGrid(F,G,H,n,T) · 1 DirichletFactorRow(F,G,H,n,a,V) · 1 Le(a,b) · 1

Actual proof prerequisites

signed_rectangular_slice_lookup · checked external prerequisite succ_le_succ · checked external prerequisite zero_add · checked external prerequisite one_mul · checked external prerequisite dirichlet_grid_table_lookup add_comm · checked external prerequisite dirichlet_grid_entry_transpose

Original expanded first-order 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)))))))

Complete tactic proof in conservative notation

All 66 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

66 script commands · 11 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 (2)

dirichlet grid entry transpose dirichlet grid table lookup

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

L1
intro F
L2
intro G
L3
intro H
L4
intro n
L5
intro T
L6
intro a
L7
intro V
L8
intro hg
L9
intro ha
L10
intro hs

02Separate the logical casesL11–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L11
split
L12
cases hs
L13
cases hs_right

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

Work with arbitrary variables or the premises of the current implication.

L15
intro e
L16
intro z
L17
intro he
L18
intro hz

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 + 1 · a + S n · e,z)Definitions: ArithAt(T,0 + 1 · a + S n · 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+1*a)
L23
specialize signed_rectangular_slice_lookup (S n)
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

Instantiate or apply named facts and discharge the corresponding proof obligations.

L29
specialize succ_le_succ (e)
L30
specialize succ_le_succ (n)
L31
apply succ_le_succ
L32
exact he
L33
exact hz

07Establish hindexL34–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply zero add.

L34
have hindex : (0+1*a)+(S n)*e=(S (n))*(e)+(a)
L35
trans a+(S n)*e
L36
congr
L37
trans 1*a
L38
apply zero_add
L39
apply one_mul
L40
refl
L41
apply add_comm
L42
rewrite hindex at hl
L43
rewrite hindex at hl

08Calculate and transport equalitiesL44–45

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L44
rewrite hindex at hl
L45
rewrite hindex at hl

09Use earlier factsL46–55

Instantiate or apply named facts and discharge the corresponding proof obligations.

L46
specialize dirichlet_grid_entry_transpose (F)
L47
specialize dirichlet_grid_entry_transpose (G)
L48
specialize dirichlet_grid_entry_transpose (H)
L49
specialize dirichlet_grid_entry_transpose (n)
L50
specialize dirichlet_grid_entry_transpose (e)
L51
specialize dirichlet_grid_entry_transpose (a)
L52
specialize dirichlet_grid_entry_transpose (z)
L53
apply dirichlet_grid_entry_transpose
L54
specialize dirichlet_grid_table_lookup (F)
L55
specialize dirichlet_grid_table_lookup (G)

10Use earlier factsL56–65

Instantiate or apply named facts and discharge the corresponding proof obligations.

L56
specialize dirichlet_grid_table_lookup (H)
L57
specialize dirichlet_grid_table_lookup (n)
L58
specialize dirichlet_grid_table_lookup (T)
L59
specialize dirichlet_grid_table_lookup (e)
L60
specialize dirichlet_grid_table_lookup (a)
L61
specialize dirichlet_grid_table_lookup (z)
L62
apply dirichlet_grid_table_lookup
L63
exact hg
L64
exact he
L65
exact ha

11Use earlier factsL66–66

Instantiate or apply named facts and discharge the corresponding proof obligations.

L66
exact hl

Library-wide reading audit

Original defined command ledger · 66 lines

0001intro F
0002intro G
0003intro H
0004intro n
0005intro T
0006intro a
0007intro V
0008intro hg
0009intro ha
0010intro hs
0011split
0012cases hs
0013cases hs_right
0014exact hs_right_left
0015intro e
0016intro z
0017intro he
0018intro hz
0019have hl : ArithAt(T,0 + 1 · a + S n · e,z)
0020specialize signed_rectangular_slice_lookup (T)
0021specialize signed_rectangular_slice_lookup (V)
0022specialize signed_rectangular_slice_lookup (0+1*a)
0023specialize signed_rectangular_slice_lookup (S n)
0024specialize signed_rectangular_slice_lookup (S n)
0025specialize signed_rectangular_slice_lookup (e)
0026specialize signed_rectangular_slice_lookup (z)
0027apply signed_rectangular_slice_lookup
0028exact hs
0029specialize succ_le_succ (e)
0030specialize succ_le_succ (n)
0031apply succ_le_succ
0032exact he
0033exact hz
0034have hindex : (0+1*a)+(S n)*e=(S (n))*(e)+(a)
0035trans a+(S n)*e
0036congr
0037trans 1*a
0038apply zero_add
0039apply one_mul
0040refl
0041apply add_comm
0042rewrite hindex at hl
0043rewrite hindex at hl
0044rewrite hindex at hl
0045rewrite hindex at hl
0046specialize dirichlet_grid_entry_transpose (F)
0047specialize dirichlet_grid_entry_transpose (G)
0048specialize dirichlet_grid_entry_transpose (H)
0049specialize dirichlet_grid_entry_transpose (n)
0050specialize dirichlet_grid_entry_transpose (e)
0051specialize dirichlet_grid_entry_transpose (a)
0052specialize dirichlet_grid_entry_transpose (z)
0053apply dirichlet_grid_entry_transpose
0054specialize dirichlet_grid_table_lookup (F)
0055specialize dirichlet_grid_table_lookup (G)
0056specialize dirichlet_grid_table_lookup (H)
0057specialize dirichlet_grid_table_lookup (n)
0058specialize dirichlet_grid_table_lookup (T)
0059specialize dirichlet_grid_table_lookup (e)
0060specialize dirichlet_grid_table_lookup (a)
0061specialize dirichlet_grid_table_lookup (z)
0062apply dirichlet_grid_table_lookup
0063exact hg
0064exact he
0065exact ha
0066exact hl