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
∀ N. ∀ F. ∀ G. ∀ H. ∀ U. ∀ n. ∀ T. ∀ R. ArithTable(N,F) → DirichletTable(N,H,G,U) → ¬n = 0 → Le(n,N) → DirichletGrid(F,G,H,n,T) → ArithRowSums(T,R,0,S n,1,S n,S n) → DirichletPrefix(F,U,n,n,R)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall N F G H U n T R. (exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_outer_input dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_outer_input dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input. (((F) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_outer_input. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_outer_inputdomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_outer_inputdomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_outer_input) = (N)) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_outer_input dst_negative_dirichlet_grid_row_sums_convolution_prefix_outer_input dst_value_dirichlet_grid_row_sums_convolution_prefix_outer_input. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_outer_inputentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_outer_inputentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_outer_input) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_outer_input)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_outer_inputentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_outer_input = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_outer_inputentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_outer_input)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_outer_input))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_outer_inputentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_outer_inputentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_outer_input) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_outer_input)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_outer_inputentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_outer_input = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_outer_inputentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_outer_input)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_outer_input) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_outer_input))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_outer_input) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_outer_input) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_outer_input) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_outer_input) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_outer_inputentryvalue))))))))) -> (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft. (((H) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftdomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftdomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) = (N)) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableleft) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableleftentryvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright. (((G) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableright. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightdomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightdomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) = (N)) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableright dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableright dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tableright. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableright))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tableright = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tableright)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableright))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tableright) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablerightentryvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable. (((U) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tabletabledomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tabletabledomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) = (N)) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tabletable) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tabletableentryvalue))))))))) /\ (forall dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table dc_output_dirichlet_grid_row_sums_convolution_prefix_inner_table. ~(dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table=0) -> (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tabledomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tabledomain + (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table) = (N)) -> (exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup. (((U) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookuppositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookuppositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) = S ((S (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookuppositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookuppositive * S ((S (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) = S ((S (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupnegative * S ((S (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvalue. (((((dc_output_dirichlet_grid_row_sums_convolution_prefix_inner_table) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvaluedecode. (((dc_output_dirichlet_grid_row_sums_convolution_prefix_inner_table) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookup) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablelookupvalue))))))))) -> (((~((dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table)=0)) /\ (exists dc_mask_dirichlet_grid_row_sums_convolution_prefix_inner_tablevalue. ((((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable. (((dc_mask_dirichlet_grid_row_sums_convolution_prefix_inner_tablevalue) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktabledomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktabledomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) = (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table)) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktable) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasktableentryvalue))))))))) /\ (forall dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask dc_value_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskdomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskdomain + (dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask) = (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table)) -> (exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup. (((dc_mask_dirichlet_grid_row_sums_convolution_prefix_inner_tablevalue) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookuppositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookuppositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) = S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookuppositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookuppositive * S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) = S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupnegative * S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvalue. (((((dc_value_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvaluedecode. (((dc_value_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookup) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemasklookupvalue))))))))) -> ((((~((dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)=0)) /\ (exists dc_quotient_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry dc_left_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry dc_right_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry. (((dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table)=(dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)*dc_quotient_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft. (((H) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftpositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftpositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) = S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftpositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftpositive * S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) = S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftnegative * S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvalue. (((((dc_left_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvaluedecode. (((dc_left_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleft) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright. (((G) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightpositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightpositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) = S ((S (dc_quotient_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightpositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightpositive * S ((S (dc_quotient_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) = S ((S (dc_quotient_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightnegative * S ((S (dc_quotient_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvalue. (((((dc_right_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvaluedecode. (((dc_right_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryright) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryrightvalue))))))))) /\ (exists sto_ap_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct sto_an_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct sto_bp_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct sto_bn_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct sto_cp_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct sto_cn_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct. (((((dc_left_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry) = 2 * (sto_ap_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) /\ (sto_an_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproductleft. (((dc_left_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproductleft + 1 /\ (sto_ap_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) = 0) /\ (sto_an_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproductleft))) /\ ((((((dc_right_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry) = 2 * (sto_bp_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) /\ (sto_bn_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproductright. (((dc_right_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproductright + 1 /\ (sto_bp_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) = 0) /\ (sto_bn_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproductright))) /\ ((((((dc_value_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask) = 2 * (sto_cp_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) /\ (sto_cn_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproductoutput. (((dc_value_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproductoutput + 1 /\ (sto_cp_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) = 0) /\ (sto_cn_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproductoutput))) /\ ((sto_ap_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct * sto_bp_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct + sto_an_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct * sto_bn_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) + sto_cn_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct = (sto_ap_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct * sto_bn_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct + sto_an_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct * sto_bp_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct) + sto_cp_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentryproduct))))))))))))))) \/ ((((dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)=0 \/ ~(exists pvs_factor_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentrynondivisor. (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table) = (dc_index_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask) * pvs_factor_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemaskentrynondivisor)) /\ ((dc_value_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluemask)=0))))))) /\ (exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold dst_positive_sum_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold dst_negative_sum_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold. (((dc_mask_dirichlet_grid_row_sums_convolution_prefix_inner_tablevalue) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)))))) /\ (((exists fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive. ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_start. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_start. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_terminal. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_terminal + S (dst_positive_sum_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) = S ((S (S (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table))) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_terminal. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_terminal * S ((S (S (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table))) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive) + (dst_positive_sum_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold))) /\ forall fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps. (exists fs_lt_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_bound. fs_lt_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_bound + S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps = S (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table)) -> exists fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps. ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_summand. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_summand + S (fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps) = S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_summand. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_partial. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_partial + S (fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps) = S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_partial. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive) + (fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_successor. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_successor + S (fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps) = S ((S (S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_successor. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive) + (fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps))) /\ fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps = fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps + fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative. ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_start. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_start. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_terminal. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_terminal + S (dst_negative_sum_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) = S ((S (S (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table))) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_terminal. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_terminal * S ((S (S (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table))) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative) + (dst_negative_sum_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold))) /\ forall fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps. (exists fs_lt_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_bound. fs_lt_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_bound + S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps = S (dc_input_dirichlet_grid_row_sums_convolution_prefix_inner_table)) -> exists fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps. ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_summand. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_summand + S (fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps) = S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_summand. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + (fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_partial. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_partial + S (fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps) = S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_partial. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative) + (fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_successor. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_successor + S (fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps) = S ((S (S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_successor. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative) + (fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps))) /\ fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps = fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps + fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresult ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresult. (((((dc_output_dirichlet_grid_row_sums_convolution_prefix_inner_table) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresult) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresult) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresultdecode. (((dc_output_dirichlet_grid_row_sums_convolution_prefix_inner_table) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresultdecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresult) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresult) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresultdecode))) /\ ((dst_positive_sum_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresult = (dst_negative_sum_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefold) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_inner_tablevaluefoldresult)))))))))))))))))))) -> ~(n=0) -> (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_domain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_domain + (n) = (N)) -> (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridtable dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridtable dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable. (((T) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_gridtable. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_gridtabledomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_gridtabledomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_gridtable) = ((S (n))*(S (n)))) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridtable dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridtable dst_value_dirichlet_grid_row_sums_convolution_prefix_gridtable. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridtableentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridtableentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridtable) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_gridtable)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridtableentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridtable = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridtableentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_gridtable)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridtable))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridtableentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridtableentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridtable) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_gridtable)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridtableentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridtable = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridtableentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_gridtable)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridtable) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridtable))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_gridtable) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_gridtable) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridtable) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridtable) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridtableentryvalue))))))))) /\ (forall dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid dfg_grid_value_dirichlet_grid_row_sums_convolution_prefix_grid. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_gridrow. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_gridrow + (dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid) = (n)) -> (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_gridcolumn. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_gridcolumn + (dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid) = (n)) -> (exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridlookup dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridlookup. (((T) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridlookuppositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridlookuppositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridlookup) = S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)+(dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid))) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridlookuppositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridlookuppositive * S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)+(dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid))) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridlookup))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridlookupnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridlookupnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridlookup) = S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)+(dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid))) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridlookupnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridlookup = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridlookupnegative * S ((S ((S (n))*(dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)+(dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid))) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridlookup))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridlookupvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridlookupvalue. (((((dfg_grid_value_dirichlet_grid_row_sums_convolution_prefix_grid) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridlookupvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridlookupvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridlookupvaluedecode. (((dfg_grid_value_dirichlet_grid_row_sums_convolution_prefix_grid) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridlookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridlookupvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridlookupvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridlookupvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridlookupvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridlookup) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridlookupvalue))))))))) -> ((((~((dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)=0)) /\ (((~((dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid)=0)) /\ (exists dfg_middle_dirichlet_grid_row_sums_convolution_prefix_gridentry dfg_first_dirichlet_grid_row_sums_convolution_prefix_gridentry dfg_last_dirichlet_grid_row_sums_convolution_prefix_gridentry dfg_value_dirichlet_grid_row_sums_convolution_prefix_gridentry. (((n)=((dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)*(dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid))*dfg_middle_dirichlet_grid_row_sums_convolution_prefix_gridentry) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst. (((F) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstpositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstpositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) = S ((S (dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstpositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstpositive * S ((S (dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) = S ((S (dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstnegative * S ((S (dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvalue. (((((dfg_first_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvaluedecode. (((dfg_first_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentryfirst) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentryfirstvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrylast dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrylast. (((H) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrylastpositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrylastpositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) = S ((S (dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrylastpositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrylastpositive * S ((S (dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrylast))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrylastnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrylastnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) = S ((S (dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrylastnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrylast = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrylastnegative * S ((S (dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrylast))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvalue. (((((dfg_last_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvaluedecode. (((dfg_last_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrylast) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrylastvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle. (((G) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlepositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlepositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) = S ((S (dfg_middle_dirichlet_grid_row_sums_convolution_prefix_gridentry)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlepositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlepositive * S ((S (dfg_middle_dirichlet_grid_row_sums_convolution_prefix_gridentry)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlenegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlenegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) = S ((S (dfg_middle_dirichlet_grid_row_sums_convolution_prefix_gridentry)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlenegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlenegative * S ((S (dfg_middle_dirichlet_grid_row_sums_convolution_prefix_gridentry)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevalue. (((((dfg_value_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevaluedecode. (((dfg_value_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddle) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_gridentrymiddlevalue))))))))) /\ (exists dfg_inner_dirichlet_grid_row_sums_convolution_prefix_gridentryproduct. ((exists sto_ap_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner sto_an_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner sto_bp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner sto_bn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner sto_cp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner sto_cn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner. (((((dfg_last_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * (sto_ap_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) /\ (sto_an_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinnerleft. (((dfg_last_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinnerleft + 1 /\ (sto_ap_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) = 0) /\ (sto_an_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinnerleft))) /\ ((((((dfg_value_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * (sto_bp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) /\ (sto_bn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinnerright. (((dfg_value_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinnerright + 1 /\ (sto_bp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) = 0) /\ (sto_bn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinnerright))) /\ ((((((dfg_inner_dirichlet_grid_row_sums_convolution_prefix_gridentryproduct) = 2 * (sto_cp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) /\ (sto_cn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinneroutput. (((dfg_inner_dirichlet_grid_row_sums_convolution_prefix_gridentryproduct) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinneroutput + 1 /\ (sto_cp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) = 0) /\ (sto_cn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinneroutput))) /\ ((sto_ap_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner * sto_bp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner + sto_an_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner * sto_bn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) + sto_cn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner = (sto_ap_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner * sto_bn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner + sto_an_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner * sto_bp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner) + sto_cp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductinner))))))) /\ (exists sto_ap_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter sto_an_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter sto_bp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter sto_bn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter sto_cp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter sto_cn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter. (((((dfg_first_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * (sto_ap_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) /\ (sto_an_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouterleft. (((dfg_first_dirichlet_grid_row_sums_convolution_prefix_gridentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouterleft + 1 /\ (sto_ap_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) = 0) /\ (sto_an_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouterleft))) /\ ((((((dfg_inner_dirichlet_grid_row_sums_convolution_prefix_gridentryproduct) = 2 * (sto_bp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) /\ (sto_bn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouterright. (((dfg_inner_dirichlet_grid_row_sums_convolution_prefix_gridentryproduct) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouterright + 1 /\ (sto_bp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) = 0) /\ (sto_bn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouterright))) /\ ((((((dfg_grid_value_dirichlet_grid_row_sums_convolution_prefix_grid) = 2 * (sto_cp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) /\ (sto_cn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouteroutput. (((dfg_grid_value_dirichlet_grid_row_sums_convolution_prefix_grid) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouteroutput + 1 /\ (sto_cp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) = 0) /\ (sto_cn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouteroutput))) /\ ((sto_ap_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter * sto_bp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter + sto_an_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter * sto_bn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) + sto_cn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter = (sto_ap_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter * sto_bn_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter + sto_an_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter * sto_bp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter) + sto_cp_dirichlet_grid_row_sums_convolution_prefix_gridentryproductouter))))))))))))))))))))) \/ ((((dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)=0 \/ ((dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid)=0 \/ ~(exists pvs_factor_dirichlet_grid_row_sums_convolution_prefix_gridentryomittednondivisor. (n) = ((dfg_grid_row_dirichlet_grid_row_sums_convolution_prefix_grid)*(dfg_grid_column_dirichlet_grid_row_sums_convolution_prefix_grid)) * pvs_factor_dirichlet_grid_row_sums_convolution_prefix_gridentryomittednondivisor))) /\ ((dfg_grid_value_dirichlet_grid_row_sums_convolution_prefix_grid)=0))))))) -> (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table. (((T) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_rowssource_table. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_rowssource_tabledomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_rowssource_tabledomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) = (0)) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowssource_table dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowssource_table dst_value_dirichlet_grid_row_sums_convolution_prefix_rowssource_table. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowssource_table))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowssource_table = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowssource_table)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowssource_table))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowssource_table) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table. (((R) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tabledomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tabledomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) = (S n)) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table dst_value_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrow_table) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrow_tableentryvalue))))))))) /\ (forall srt_index_dirichlet_grid_row_sums_convolution_prefix_rows. (exists pvs_gap_dirichlet_grid_row_sums_convolution_prefix_rowsbound. pvs_gap_dirichlet_grid_row_sums_convolution_prefix_rowsbound + S (srt_index_dirichlet_grid_row_sums_convolution_prefix_rows) = (S n)) -> exists srt_value_dirichlet_grid_row_sums_convolution_prefix_rows. (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry. (((R) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) = S ((S (srt_index_dirichlet_grid_row_sums_convolution_prefix_rows)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowentrypositive * S ((S (srt_index_dirichlet_grid_row_sums_convolution_prefix_rows)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) = S ((S (srt_index_dirichlet_grid_row_sums_convolution_prefix_rows)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowentrynegative * S ((S (srt_index_dirichlet_grid_row_sums_convolution_prefix_rows)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvalue. (((((srt_value_dirichlet_grid_row_sums_convolution_prefix_rows) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvaluedecode. (((srt_value_dirichlet_grid_row_sums_convolution_prefix_rows) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowentry) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowentryvalue))))))))) /\ (exists srs_slice_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sum. ((((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table. (((T) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tabledomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tabledomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table dst_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_table) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table. (((srs_slice_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sum) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tabledomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) = (S n)) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table dst_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_table) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice. (exists pvs_gap_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicebound. pvs_gap_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslicebound + S (srs_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice) = (S n)) -> exists srs_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice. (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource. (((T) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcepositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((S n) * (srt_index_dirichlet_grid_row_sums_convolution_prefix_rows)))) + ((1) * (srs_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice))))) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcepositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcepositive * S ((S (((((0) + ((S n) * (srt_index_dirichlet_grid_row_sums_convolution_prefix_rows)))) + ((1) * (srs_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice))))) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcenegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((S n) * (srt_index_dirichlet_grid_row_sums_convolution_prefix_rows)))) + ((1) * (srs_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice))))) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcenegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcenegative * S ((S (((((0) + ((S n) * (srt_index_dirichlet_grid_row_sums_convolution_prefix_rows)))) + ((1) * (srs_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice))))) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevalue. (((((srs_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysource) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput. (((srs_slice_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sum) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputpositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) = S ((S (srs_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputpositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) = S ((S (srs_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvalue. (((((srs_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumslice) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutput) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum dst_positive_sum_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum dst_negative_sum_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum. (((srs_slice_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sum) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive. ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_start. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_start. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_terminal. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) = S ((S (S n)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_terminal. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_terminal * S ((S (S n)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive) + (dst_positive_sum_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum))) /\ forall fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps = S n) -> exists fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive) + (fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive) + (fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps = fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps + fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative. ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_start. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_start. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_terminal. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) = S ((S (S n)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_terminal. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_terminal * S ((S (S n)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative) + (dst_negative_sum_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum))) /\ forall fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps = S n) -> exists fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + (fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative) + (fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative = fs_q_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative) + (fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps = fs_r_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps + fs_a_dst_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresult ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresult. (((((srt_value_dirichlet_grid_row_sums_convolution_prefix_rows) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresult) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresultdecode. (((srt_value_dirichlet_grid_row_sums_convolution_prefix_rows) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresult) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresult = (dst_negative_sum_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsum) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_rowsrowrow_sumsumresult)))))))))))))))))) -> (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resulttable dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resulttable dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable. (((R) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)))))) /\ (forall dst_index_dirichlet_grid_row_sums_convolution_prefix_resulttable. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_resulttabledomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_resulttabledomain + (dst_index_dirichlet_grid_row_sums_convolution_prefix_resulttable) = (n)) -> exists dst_positive_dirichlet_grid_row_sums_convolution_prefix_resulttable dst_negative_dirichlet_grid_row_sums_convolution_prefix_resulttable dst_value_dirichlet_grid_row_sums_convolution_prefix_resulttable. ((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resulttableentrypositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resulttableentrypositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_resulttable) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_resulttable)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resulttableentrypositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resulttable = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resulttableentrypositive * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_resulttable)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_resulttable))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resulttableentrynegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resulttableentrynegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resulttable) = S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_resulttable)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resulttableentrynegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resulttable = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resulttableentrynegative * S ((S (dst_index_dirichlet_grid_row_sums_convolution_prefix_resulttable)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resulttable) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resulttable))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvalue. (((((dst_value_dirichlet_grid_row_sums_convolution_prefix_resulttable) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvaluedecode. (((dst_value_dirichlet_grid_row_sums_convolution_prefix_resulttable) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_resulttable) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resulttable) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resulttableentryvalue))))))))) /\ (forall dc_index_dirichlet_grid_row_sums_convolution_prefix_result dc_value_dirichlet_grid_row_sums_convolution_prefix_result. (exists pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_resultdomain. pvs_le_gap_dirichlet_grid_row_sums_convolution_prefix_resultdomain + (dc_index_dirichlet_grid_row_sums_convolution_prefix_result) = (n)) -> (exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultlookup dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultlookup. (((R) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultlookuppositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultlookuppositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultlookup) = S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_result)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultlookuppositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultlookuppositive * S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_result)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultlookup))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultlookupnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultlookupnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultlookup) = S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_result)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultlookupnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultlookup = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultlookupnegative * S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_result)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultlookup))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultlookupvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultlookupvalue. (((((dc_value_dirichlet_grid_row_sums_convolution_prefix_result) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultlookupvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultlookupvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultlookupvaluedecode. (((dc_value_dirichlet_grid_row_sums_convolution_prefix_result) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultlookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultlookupvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultlookupvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultlookupvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultlookupvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultlookup) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultlookupvalue))))))))) -> ((((~((dc_index_dirichlet_grid_row_sums_convolution_prefix_result)=0)) /\ (exists dc_quotient_dirichlet_grid_row_sums_convolution_prefix_resultentry dc_left_dirichlet_grid_row_sums_convolution_prefix_resultentry dc_right_dirichlet_grid_row_sums_convolution_prefix_resultentry. (((n)=(dc_index_dirichlet_grid_row_sums_convolution_prefix_result)*dc_quotient_dirichlet_grid_row_sums_convolution_prefix_resultentry) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryleft dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryleft. (((F) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryleftpositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryleftpositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) = S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_result)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryleftpositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryleftpositive * S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_result)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryleft))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryleftnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryleftnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) = S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_result)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryleftnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryleft = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryleftnegative * S ((S (dc_index_dirichlet_grid_row_sums_convolution_prefix_result)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryleft))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvalue. (((((dc_left_dirichlet_grid_row_sums_convolution_prefix_resultentry) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvaluedecode. (((dc_left_dirichlet_grid_row_sums_convolution_prefix_resultentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryleft) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryleftvalue))))))))) /\ (((exists dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryright dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryright. (((U) = (((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)))) * S ((((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) * S ((dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) + ((dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)))) + ((((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright))) + (((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) * S ((dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) + ((dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)))))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryrightpositive. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryrightpositive + S (dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryright) = S ((S (dc_quotient_dirichlet_grid_row_sums_convolution_prefix_resultentry)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryrightpositive. dst_positive_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryrightpositive * S ((S (dc_quotient_dirichlet_grid_row_sums_convolution_prefix_resultentry)) * dst_positive_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryright))) /\ (((((exists ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryrightnegative. ff_h_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryrightnegative + S (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryright) = S ((S (dc_quotient_dirichlet_grid_row_sums_convolution_prefix_resultentry)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright)) /\ exists ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryrightnegative. dst_negative_code_dirichlet_grid_row_sums_convolution_prefix_resultentryright = ff_q_pvs_dirichlet_grid_row_sums_convolution_prefix_resultentryrightnegative * S ((S (dc_quotient_dirichlet_grid_row_sums_convolution_prefix_resultentry)) * dst_negative_scale_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryright))) /\ (exists ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvalue ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvalue. (((((dc_right_dirichlet_grid_row_sums_convolution_prefix_resultentry) = 2 * (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvalue) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvalue) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvaluedecode. (((dc_right_dirichlet_grid_row_sums_convolution_prefix_resultentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvaluedecode + 1 /\ (ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvalue) = 0) /\ (ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvalue) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvaluedecode))) /\ ((dst_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + ge_balance_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvalue = (dst_negative_dirichlet_grid_row_sums_convolution_prefix_resultentryright) + ge_balance_positive_dirichlet_grid_row_sums_convolution_prefix_resultentryrightvalue))))))))) /\ (exists sto_ap_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct sto_an_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct sto_bp_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct sto_bn_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct sto_cp_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct sto_cn_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct. (((((dc_left_dirichlet_grid_row_sums_convolution_prefix_resultentry) = 2 * (sto_ap_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) /\ (sto_an_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryproductleft. (((dc_left_dirichlet_grid_row_sums_convolution_prefix_resultentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryproductleft + 1 /\ (sto_ap_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) = 0) /\ (sto_an_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryproductleft))) /\ ((((((dc_right_dirichlet_grid_row_sums_convolution_prefix_resultentry) = 2 * (sto_bp_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) /\ (sto_bn_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryproductright. (((dc_right_dirichlet_grid_row_sums_convolution_prefix_resultentry) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryproductright + 1 /\ (sto_bp_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) = 0) /\ (sto_bn_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryproductright))) /\ ((((((dc_value_dirichlet_grid_row_sums_convolution_prefix_result) = 2 * (sto_cp_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) /\ (sto_cn_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) = 0) \/ exists ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryproductoutput. (((dc_value_dirichlet_grid_row_sums_convolution_prefix_result) = 2 * ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryproductoutput + 1 /\ (sto_cp_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) = 0) /\ (sto_cn_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) = S ge_signed_half_dirichlet_grid_row_sums_convolution_prefix_resultentryproductoutput))) /\ ((sto_ap_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct * sto_bp_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct + sto_an_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct * sto_bn_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) + sto_cn_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct = (sto_ap_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct * sto_bn_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct + sto_an_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct * sto_bp_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct) + sto_cp_dirichlet_grid_row_sums_convolution_prefix_resultentryproduct))))))))))))))) \/ ((((dc_index_dirichlet_grid_row_sums_convolution_prefix_result)=0 \/ ~(exists pvs_factor_dirichlet_grid_row_sums_convolution_prefix_resultentrynondivisor. (n) = (dc_index_dirichlet_grid_row_sums_convolution_prefix_result) * pvs_factor_dirichlet_grid_row_sums_convolution_prefix_resultentrynondivisor)) /\ ((dc_value_dirichlet_grid_row_sums_convolution_prefix_result)=0)))))))Complete tactic proof in conservative notation
All 72 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
72 script commands · 13 reading checkpoints · 1 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)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–14
03Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
split
04Use earlier factsL16–19
05Separate the logical casesL20–21
06Use earlier factsL22–22
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L22
exact hr_right_left
07Fix variables and assumptionsL23–26
08Establish hsL27–36
Establish this local claim before using it. It is not an additional assumption.
- L27
have hs : SignedSliceSum(T,0 + S n · a,1,S n,z)Definitions: SignedSliceSum(T,0 + S n · a,1,S n,z)Original native command in the exact edition - L28
specialize signed_rectangular_row_sums_lookup (T) - L29
specialize signed_rectangular_row_sums_lookup (R) - L30
specialize signed_rectangular_row_sums_lookup (0) - L31
specialize signed_rectangular_row_sums_lookup (S n) - L32
specialize signed_rectangular_row_sums_lookup (1) - L33
specialize signed_rectangular_row_sums_lookup (S n) - L34
specialize signed_rectangular_row_sums_lookup (S n) - L35
specialize signed_rectangular_row_sums_lookup (a) - L36
specialize signed_rectangular_row_sums_lookup (z)
09Use earlier factsL37–43
10Separate the logical casesL44–45
11Use earlier factsL46–55
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L46
specialize dirichlet_factor_row_nested_entry (N) - L47
specialize dirichlet_factor_row_nested_entry (F) - L48
specialize dirichlet_factor_row_nested_entry (G) - L49
specialize dirichlet_factor_row_nested_entry (H) - L50
specialize dirichlet_factor_row_nested_entry (U) - L51
specialize dirichlet_factor_row_nested_entry (n) - L52
specialize dirichlet_factor_row_nested_entry (a) - L53
specialize dirichlet_factor_row_nested_entry (x) - L54
specialize dirichlet_factor_row_nested_entry (z) - L55
apply dirichlet_factor_row_nested_entry
12Use earlier factsL56–65
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 72 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro H - 0005
intro U - 0006
intro n - 0007
intro T - 0008
intro R - 0009
intro hF - 0010
intro hU - 0011
intro hn - 0012
intro hnN - 0013
intro hg - 0014
intro hr - 0015
split - 0016
specialize signed_table_domain_resize (S n) - 0017
specialize signed_table_domain_resize (n) - 0018
specialize signed_table_domain_resize (R) - 0019
apply signed_table_domain_resize - 0020
cases hr - 0021
cases hr_right - 0022
exact hr_right_left - 0023
intro a - 0024
intro z - 0025
intro ha - 0026
intro hz - 0027
have hs : SignedSliceSum(T,0 + S n · a,1,S n,z) - 0028
specialize signed_rectangular_row_sums_lookup (T) - 0029
specialize signed_rectangular_row_sums_lookup (R) - 0030
specialize signed_rectangular_row_sums_lookup (0) - 0031
specialize signed_rectangular_row_sums_lookup (S n) - 0032
specialize signed_rectangular_row_sums_lookup (1) - 0033
specialize signed_rectangular_row_sums_lookup (S n) - 0034
specialize signed_rectangular_row_sums_lookup (S n) - 0035
specialize signed_rectangular_row_sums_lookup (a) - 0036
specialize signed_rectangular_row_sums_lookup (z) - 0037
apply signed_rectangular_row_sums_lookup - 0038
exact hr - 0039
specialize succ_le_succ (a) - 0040
specialize succ_le_succ (n) - 0041
apply succ_le_succ - 0042
exact ha - 0043
exact hz - 0044
cases hs - 0045
cases hs_witness - 0046
specialize dirichlet_factor_row_nested_entry (N) - 0047
specialize dirichlet_factor_row_nested_entry (F) - 0048
specialize dirichlet_factor_row_nested_entry (G) - 0049
specialize dirichlet_factor_row_nested_entry (H) - 0050
specialize dirichlet_factor_row_nested_entry (U) - 0051
specialize dirichlet_factor_row_nested_entry (n) - 0052
specialize dirichlet_factor_row_nested_entry (a) - 0053
specialize dirichlet_factor_row_nested_entry (x) - 0054
specialize dirichlet_factor_row_nested_entry (z) - 0055
apply dirichlet_factor_row_nested_entry - 0056
exact hF - 0057
exact hU - 0058
exact hn - 0059
exact hnN - 0060
exact ha - 0061
specialize dirichlet_grid_row_slice (F) - 0062
specialize dirichlet_grid_row_slice (G) - 0063
specialize dirichlet_grid_row_slice (H) - 0064
specialize dirichlet_grid_row_slice (n) - 0065
specialize dirichlet_grid_row_slice (T) - 0066
specialize dirichlet_grid_row_slice (a) - 0067
specialize dirichlet_grid_row_slice (x) - 0068
apply dirichlet_grid_row_slice - 0069
exact hg - 0070
exact ha - 0071
exact hs_witness_left - 0072
exact hs_witness_right