DirichletGrid(F,G,H,n,T)

((exists dst_positive_code_dirichlettable dst_positive_scale_dirichlettable dst_negative_code_dirichlettable dst_negative_scale_dirichlettable. ((((T)) = (((((dst_positive_code_dirichlettable) + (dst_positive_scale_dirichlettable)) * S ((dst_positive_code_dirichlettable) + (dst_positive_scale_dirichlettable)) + ((dst_positive_scale_dirichlettable) + (dst_positive_scale_dirichlettable))) + (((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) * S ((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) + ((dst_negative_scale_dirichlettable) + (dst_negative_scale_dirichlettable)))) * S ((((dst_positive_code_dirichlettable) + (dst_positive_scale_dirichlettable)) * S ((dst_positive_code_dirichlettable) + (dst_positive_scale_dirichlettable)) + ((dst_positive_scale_dirichlettable) + (dst_positive_scale_dirichlettable))) + (((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) * S ((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) + ((dst_negative_scale_dirichlettable) + (dst_negative_scale_dirichlettable)))) + ((((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) * S ((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) + ((dst_negative_scale_dirichlettable) + (dst_negative_scale_dirichlettable))) + (((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) * S ((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) + ((dst_negative_scale_dirichlettable) + (dst_negative_scale_dirichlettable)))))) /\ (forall dst_index_dirichlettable. (exists pvs_le_gap_dirichlettabledomain. pvs_le_gap_dirichlettabledomain + (dst_index_dirichlettable) = ((S ((n)))*(S ((n))))) -> exists dst_positive_dirichlettable dst_negative_dirichlettable dst_value_dirichlettable. ((((exists ff_h_pvs_dirichlettableentrypositive. ff_h_pvs_dirichlettableentrypositive + S (dst_positive_dirichlettable) = S ((S (dst_index_dirichlettable)) * dst_positive_scale_dirichlettable)) /\ exists ff_q_pvs_dirichlettableentrypositive. dst_positive_code_dirichlettable = ff_q_pvs_dirichlettableentrypositive * S ((S (dst_index_dirichlettable)) * dst_positive_scale_dirichlettable) + (dst_positive_dirichlettable))) /\ (((((exists ff_h_pvs_dirichlettableentrynegative. ff_h_pvs_dirichlettableentrynegative + S (dst_negative_dirichlettable) = S ((S (dst_index_dirichlettable)) * dst_negative_scale_dirichlettable)) /\ exists ff_q_pvs_dirichlettableentrynegative. dst_negative_code_dirichlettable = ff_q_pvs_dirichlettableentrynegative * S ((S (dst_index_dirichlettable)) * dst_negative_scale_dirichlettable) + (dst_negative_dirichlettable))) /\ (exists ge_balance_positive_dirichlettableentryvalue ge_balance_negative_dirichlettableentryvalue. (((((dst_value_dirichlettable) = 2 * (ge_balance_positive_dirichlettableentryvalue) /\ (ge_balance_negative_dirichlettableentryvalue) = 0) \/ exists ge_signed_half_dirichlettableentryvaluedecode. (((dst_value_dirichlettable) = 2 * ge_signed_half_dirichlettableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlettableentryvalue) = 0) /\ (ge_balance_negative_dirichlettableentryvalue) = S ge_signed_half_dirichlettableentryvaluedecode))) /\ ((dst_positive_dirichlettable) + ge_balance_negative_dirichlettableentryvalue = (dst_negative_dirichlettable) + ge_balance_positive_dirichlettableentryvalue))))))))) /\ (forall dfg_grid_row_dirichlet dfg_grid_column_dirichlet dfg_grid_value_dirichlet. (exists pvs_le_gap_dirichletrow. pvs_le_gap_dirichletrow + (dfg_grid_row_dirichlet) = ((n))) -> (exists pvs_le_gap_dirichletcolumn. pvs_le_gap_dirichletcolumn + (dfg_grid_column_dirichlet) = ((n))) -> (exists dst_positive_code_dirichletlookup dst_positive_scale_dirichletlookup dst_negative_code_dirichletlookup dst_negative_scale_dirichletlookup dst_positive_dirichletlookup dst_negative_dirichletlookup. ((((T)) = (((((dst_positive_code_dirichletlookup) + (dst_positive_scale_dirichletlookup)) * S ((dst_positive_code_dirichletlookup) + (dst_positive_scale_dirichletlookup)) + ((dst_positive_scale_dirichletlookup) + (dst_positive_scale_dirichletlookup))) + (((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) * S ((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) + ((dst_negative_scale_dirichletlookup) + (dst_negative_scale_dirichletlookup)))) * S ((((dst_positive_code_dirichletlookup) + (dst_positive_scale_dirichletlookup)) * S ((dst_positive_code_dirichletlookup) + (dst_positive_scale_dirichletlookup)) + ((dst_positive_scale_dirichletlookup) + (dst_positive_scale_dirichletlookup))) + (((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) * S ((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) + ((dst_negative_scale_dirichletlookup) + (dst_negative_scale_dirichletlookup)))) + ((((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) * S ((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) + ((dst_negative_scale_dirichletlookup) + (dst_negative_scale_dirichletlookup))) + (((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) * S ((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) + ((dst_negative_scale_dirichletlookup) + (dst_negative_scale_dirichletlookup)))))) /\ (((((exists ff_h_pvs_dirichletlookuppositive. ff_h_pvs_dirichletlookuppositive + S (dst_positive_dirichletlookup) = S ((S ((S ((n)))*(dfg_grid_row_dirichlet)+(dfg_grid_column_dirichlet))) * dst_positive_scale_dirichletlookup)) /\ exists ff_q_pvs_dirichletlookuppositive. dst_positive_code_dirichletlookup = ff_q_pvs_dirichletlookuppositive * S ((S ((S ((n)))*(dfg_grid_row_dirichlet)+(dfg_grid_column_dirichlet))) * dst_positive_scale_dirichletlookup) + (dst_positive_dirichletlookup))) /\ (((((exists ff_h_pvs_dirichletlookupnegative. ff_h_pvs_dirichletlookupnegative + S (dst_negative_dirichletlookup) = S ((S ((S ((n)))*(dfg_grid_row_dirichlet)+(dfg_grid_column_dirichlet))) * dst_negative_scale_dirichletlookup)) /\ exists ff_q_pvs_dirichletlookupnegative. dst_negative_code_dirichletlookup = ff_q_pvs_dirichletlookupnegative * S ((S ((S ((n)))*(dfg_grid_row_dirichlet)+(dfg_grid_column_dirichlet))) * dst_negative_scale_dirichletlookup) + (dst_negative_dirichletlookup))) /\ (exists ge_balance_positive_dirichletlookupvalue ge_balance_negative_dirichletlookupvalue. (((((dfg_grid_value_dirichlet) = 2 * (ge_balance_positive_dirichletlookupvalue) /\ (ge_balance_negative_dirichletlookupvalue) = 0) \/ exists ge_signed_half_dirichletlookupvaluedecode. (((dfg_grid_value_dirichlet) = 2 * ge_signed_half_dirichletlookupvaluedecode + 1 /\ (ge_balance_positive_dirichletlookupvalue) = 0) /\ (ge_balance_negative_dirichletlookupvalue) = S ge_signed_half_dirichletlookupvaluedecode))) /\ ((dst_positive_dirichletlookup) + ge_balance_negative_dirichletlookupvalue = (dst_negative_dirichletlookup) + ge_balance_positive_dirichletlookupvalue))))))))) -> ((((~((dfg_grid_row_dirichlet)=0)) /\ (((~((dfg_grid_column_dirichlet)=0)) /\ (exists dfg_middle_dirichletentry dfg_first_dirichletentry dfg_last_dirichletentry dfg_value_dirichletentry. ((((n))=((dfg_grid_row_dirichlet)*(dfg_grid_column_dirichlet))*dfg_middle_dirichletentry) /\ (((exists dst_positive_code_dirichletentryfirst dst_positive_scale_dirichletentryfirst dst_negative_code_dirichletentryfirst dst_negative_scale_dirichletentryfirst dst_positive_dirichletentryfirst dst_negative_dirichletentryfirst. ((((F)) = (((((dst_positive_code_dirichletentryfirst) + (dst_positive_scale_dirichletentryfirst)) * S ((dst_positive_code_dirichletentryfirst) + (dst_positive_scale_dirichletentryfirst)) + ((dst_positive_scale_dirichletentryfirst) + (dst_positive_scale_dirichletentryfirst))) + (((dst_negative_code_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)) * S ((dst_negative_code_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)) + ((dst_negative_scale_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)))) * S ((((dst_positive_code_dirichletentryfirst) + (dst_positive_scale_dirichletentryfirst)) * S ((dst_positive_code_dirichletentryfirst) + (dst_positive_scale_dirichletentryfirst)) + ((dst_positive_scale_dirichletentryfirst) + (dst_positive_scale_dirichletentryfirst))) + (((dst_negative_code_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)) * S ((dst_negative_code_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)) + ((dst_negative_scale_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)))) + ((((dst_negative_code_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)) * S ((dst_negative_code_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)) + ((dst_negative_scale_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst))) + (((dst_negative_code_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)) * S ((dst_negative_code_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)) + ((dst_negative_scale_dirichletentryfirst) + (dst_negative_scale_dirichletentryfirst)))))) /\ (((((exists ff_h_pvs_dirichletentryfirstpositive. ff_h_pvs_dirichletentryfirstpositive + S (dst_positive_dirichletentryfirst) = S ((S (dfg_grid_row_dirichlet)) * dst_positive_scale_dirichletentryfirst)) /\ exists ff_q_pvs_dirichletentryfirstpositive. dst_positive_code_dirichletentryfirst = ff_q_pvs_dirichletentryfirstpositive * S ((S (dfg_grid_row_dirichlet)) * dst_positive_scale_dirichletentryfirst) + (dst_positive_dirichletentryfirst))) /\ (((((exists ff_h_pvs_dirichletentryfirstnegative. ff_h_pvs_dirichletentryfirstnegative + S (dst_negative_dirichletentryfirst) = S ((S (dfg_grid_row_dirichlet)) * dst_negative_scale_dirichletentryfirst)) /\ exists ff_q_pvs_dirichletentryfirstnegative. dst_negative_code_dirichletentryfirst = ff_q_pvs_dirichletentryfirstnegative * S ((S (dfg_grid_row_dirichlet)) * dst_negative_scale_dirichletentryfirst) + (dst_negative_dirichletentryfirst))) /\ (exists ge_balance_positive_dirichletentryfirstvalue ge_balance_negative_dirichletentryfirstvalue. (((((dfg_first_dirichletentry) = 2 * (ge_balance_positive_dirichletentryfirstvalue) /\ (ge_balance_negative_dirichletentryfirstvalue) = 0) \/ exists ge_signed_half_dirichletentryfirstvaluedecode. (((dfg_first_dirichletentry) = 2 * ge_signed_half_dirichletentryfirstvaluedecode + 1 /\ (ge_balance_positive_dirichletentryfirstvalue) = 0) /\ (ge_balance_negative_dirichletentryfirstvalue) = S ge_signed_half_dirichletentryfirstvaluedecode))) /\ ((dst_positive_dirichletentryfirst) + ge_balance_negative_dirichletentryfirstvalue = (dst_negative_dirichletentryfirst) + ge_balance_positive_dirichletentryfirstvalue))))))))) /\ (((exists dst_positive_code_dirichletentrylast dst_positive_scale_dirichletentrylast dst_negative_code_dirichletentrylast dst_negative_scale_dirichletentrylast dst_positive_dirichletentrylast dst_negative_dirichletentrylast. ((((H)) = (((((dst_positive_code_dirichletentrylast) + (dst_positive_scale_dirichletentrylast)) * S ((dst_positive_code_dirichletentrylast) + (dst_positive_scale_dirichletentrylast)) + ((dst_positive_scale_dirichletentrylast) + (dst_positive_scale_dirichletentrylast))) + (((dst_negative_code_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)) * S ((dst_negative_code_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)) + ((dst_negative_scale_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)))) * S ((((dst_positive_code_dirichletentrylast) + (dst_positive_scale_dirichletentrylast)) * S ((dst_positive_code_dirichletentrylast) + (dst_positive_scale_dirichletentrylast)) + ((dst_positive_scale_dirichletentrylast) + (dst_positive_scale_dirichletentrylast))) + (((dst_negative_code_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)) * S ((dst_negative_code_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)) + ((dst_negative_scale_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)))) + ((((dst_negative_code_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)) * S ((dst_negative_code_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)) + ((dst_negative_scale_dirichletentrylast) + (dst_negative_scale_dirichletentrylast))) + (((dst_negative_code_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)) * S ((dst_negative_code_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)) + ((dst_negative_scale_dirichletentrylast) + (dst_negative_scale_dirichletentrylast)))))) /\ (((((exists ff_h_pvs_dirichletentrylastpositive. ff_h_pvs_dirichletentrylastpositive + S (dst_positive_dirichletentrylast) = S ((S (dfg_grid_column_dirichlet)) * dst_positive_scale_dirichletentrylast)) /\ exists ff_q_pvs_dirichletentrylastpositive. dst_positive_code_dirichletentrylast = ff_q_pvs_dirichletentrylastpositive * S ((S (dfg_grid_column_dirichlet)) * dst_positive_scale_dirichletentrylast) + (dst_positive_dirichletentrylast))) /\ (((((exists ff_h_pvs_dirichletentrylastnegative. ff_h_pvs_dirichletentrylastnegative + S (dst_negative_dirichletentrylast) = S ((S (dfg_grid_column_dirichlet)) * dst_negative_scale_dirichletentrylast)) /\ exists ff_q_pvs_dirichletentrylastnegative. dst_negative_code_dirichletentrylast = ff_q_pvs_dirichletentrylastnegative * S ((S (dfg_grid_column_dirichlet)) * dst_negative_scale_dirichletentrylast) + (dst_negative_dirichletentrylast))) /\ (exists ge_balance_positive_dirichletentrylastvalue ge_balance_negative_dirichletentrylastvalue. (((((dfg_last_dirichletentry) = 2 * (ge_balance_positive_dirichletentrylastvalue) /\ (ge_balance_negative_dirichletentrylastvalue) = 0) \/ exists ge_signed_half_dirichletentrylastvaluedecode. (((dfg_last_dirichletentry) = 2 * ge_signed_half_dirichletentrylastvaluedecode + 1 /\ (ge_balance_positive_dirichletentrylastvalue) = 0) /\ (ge_balance_negative_dirichletentrylastvalue) = S ge_signed_half_dirichletentrylastvaluedecode))) /\ ((dst_positive_dirichletentrylast) + ge_balance_negative_dirichletentrylastvalue = (dst_negative_dirichletentrylast) + ge_balance_positive_dirichletentrylastvalue))))))))) /\ (((exists dst_positive_code_dirichletentrymiddle dst_positive_scale_dirichletentrymiddle dst_negative_code_dirichletentrymiddle dst_negative_scale_dirichletentrymiddle dst_positive_dirichletentrymiddle dst_negative_dirichletentrymiddle. ((((G)) = (((((dst_positive_code_dirichletentrymiddle) + (dst_positive_scale_dirichletentrymiddle)) * S ((dst_positive_code_dirichletentrymiddle) + (dst_positive_scale_dirichletentrymiddle)) + ((dst_positive_scale_dirichletentrymiddle) + (dst_positive_scale_dirichletentrymiddle))) + (((dst_negative_code_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)) * S ((dst_negative_code_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)) + ((dst_negative_scale_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)))) * S ((((dst_positive_code_dirichletentrymiddle) + (dst_positive_scale_dirichletentrymiddle)) * S ((dst_positive_code_dirichletentrymiddle) + (dst_positive_scale_dirichletentrymiddle)) + ((dst_positive_scale_dirichletentrymiddle) + (dst_positive_scale_dirichletentrymiddle))) + (((dst_negative_code_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)) * S ((dst_negative_code_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)) + ((dst_negative_scale_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)))) + ((((dst_negative_code_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)) * S ((dst_negative_code_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)) + ((dst_negative_scale_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle))) + (((dst_negative_code_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)) * S ((dst_negative_code_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)) + ((dst_negative_scale_dirichletentrymiddle) + (dst_negative_scale_dirichletentrymiddle)))))) /\ (((((exists ff_h_pvs_dirichletentrymiddlepositive. ff_h_pvs_dirichletentrymiddlepositive + S (dst_positive_dirichletentrymiddle) = S ((S (dfg_middle_dirichletentry)) * dst_positive_scale_dirichletentrymiddle)) /\ exists ff_q_pvs_dirichletentrymiddlepositive. dst_positive_code_dirichletentrymiddle = ff_q_pvs_dirichletentrymiddlepositive * S ((S (dfg_middle_dirichletentry)) * dst_positive_scale_dirichletentrymiddle) + (dst_positive_dirichletentrymiddle))) /\ (((((exists ff_h_pvs_dirichletentrymiddlenegative. ff_h_pvs_dirichletentrymiddlenegative + S (dst_negative_dirichletentrymiddle) = S ((S (dfg_middle_dirichletentry)) * dst_negative_scale_dirichletentrymiddle)) /\ exists ff_q_pvs_dirichletentrymiddlenegative. dst_negative_code_dirichletentrymiddle = ff_q_pvs_dirichletentrymiddlenegative * S ((S (dfg_middle_dirichletentry)) * dst_negative_scale_dirichletentrymiddle) + (dst_negative_dirichletentrymiddle))) /\ (exists ge_balance_positive_dirichletentrymiddlevalue ge_balance_negative_dirichletentrymiddlevalue. (((((dfg_value_dirichletentry) = 2 * (ge_balance_positive_dirichletentrymiddlevalue) /\ (ge_balance_negative_dirichletentrymiddlevalue) = 0) \/ exists ge_signed_half_dirichletentrymiddlevaluedecode. (((dfg_value_dirichletentry) = 2 * ge_signed_half_dirichletentrymiddlevaluedecode + 1 /\ (ge_balance_positive_dirichletentrymiddlevalue) = 0) /\ (ge_balance_negative_dirichletentrymiddlevalue) = S ge_signed_half_dirichletentrymiddlevaluedecode))) /\ ((dst_positive_dirichletentrymiddle) + ge_balance_negative_dirichletentrymiddlevalue = (dst_negative_dirichletentrymiddle) + ge_balance_positive_dirichletentrymiddlevalue))))))))) /\ (exists dfg_inner_dirichletentryproduct. ((exists sto_ap_dirichletentryproductinner sto_an_dirichletentryproductinner sto_bp_dirichletentryproductinner sto_bn_dirichletentryproductinner sto_cp_dirichletentryproductinner sto_cn_dirichletentryproductinner. (((((dfg_last_dirichletentry) = 2 * (sto_ap_dirichletentryproductinner) /\ (sto_an_dirichletentryproductinner) = 0) \/ exists ge_signed_half_dirichletentryproductinnerleft. (((dfg_last_dirichletentry) = 2 * ge_signed_half_dirichletentryproductinnerleft + 1 /\ (sto_ap_dirichletentryproductinner) = 0) /\ (sto_an_dirichletentryproductinner) = S ge_signed_half_dirichletentryproductinnerleft))) /\ ((((((dfg_value_dirichletentry) = 2 * (sto_bp_dirichletentryproductinner) /\ (sto_bn_dirichletentryproductinner) = 0) \/ exists ge_signed_half_dirichletentryproductinnerright. (((dfg_value_dirichletentry) = 2 * ge_signed_half_dirichletentryproductinnerright + 1 /\ (sto_bp_dirichletentryproductinner) = 0) /\ (sto_bn_dirichletentryproductinner) = S ge_signed_half_dirichletentryproductinnerright))) /\ ((((((dfg_inner_dirichletentryproduct) = 2 * (sto_cp_dirichletentryproductinner) /\ (sto_cn_dirichletentryproductinner) = 0) \/ exists ge_signed_half_dirichletentryproductinneroutput. (((dfg_inner_dirichletentryproduct) = 2 * ge_signed_half_dirichletentryproductinneroutput + 1 /\ (sto_cp_dirichletentryproductinner) = 0) /\ (sto_cn_dirichletentryproductinner) = S ge_signed_half_dirichletentryproductinneroutput))) /\ ((sto_ap_dirichletentryproductinner * sto_bp_dirichletentryproductinner + sto_an_dirichletentryproductinner * sto_bn_dirichletentryproductinner) + sto_cn_dirichletentryproductinner = (sto_ap_dirichletentryproductinner * sto_bn_dirichletentryproductinner + sto_an_dirichletentryproductinner * sto_bp_dirichletentryproductinner) + sto_cp_dirichletentryproductinner))))))) /\ (exists sto_ap_dirichletentryproductouter sto_an_dirichletentryproductouter sto_bp_dirichletentryproductouter sto_bn_dirichletentryproductouter sto_cp_dirichletentryproductouter sto_cn_dirichletentryproductouter. (((((dfg_first_dirichletentry) = 2 * (sto_ap_dirichletentryproductouter) /\ (sto_an_dirichletentryproductouter) = 0) \/ exists ge_signed_half_dirichletentryproductouterleft. (((dfg_first_dirichletentry) = 2 * ge_signed_half_dirichletentryproductouterleft + 1 /\ (sto_ap_dirichletentryproductouter) = 0) /\ (sto_an_dirichletentryproductouter) = S ge_signed_half_dirichletentryproductouterleft))) /\ ((((((dfg_inner_dirichletentryproduct) = 2 * (sto_bp_dirichletentryproductouter) /\ (sto_bn_dirichletentryproductouter) = 0) \/ exists ge_signed_half_dirichletentryproductouterright. (((dfg_inner_dirichletentryproduct) = 2 * ge_signed_half_dirichletentryproductouterright + 1 /\ (sto_bp_dirichletentryproductouter) = 0) /\ (sto_bn_dirichletentryproductouter) = S ge_signed_half_dirichletentryproductouterright))) /\ ((((((dfg_grid_value_dirichlet) = 2 * (sto_cp_dirichletentryproductouter) /\ (sto_cn_dirichletentryproductouter) = 0) \/ exists ge_signed_half_dirichletentryproductouteroutput. (((dfg_grid_value_dirichlet) = 2 * ge_signed_half_dirichletentryproductouteroutput + 1 /\ (sto_cp_dirichletentryproductouter) = 0) /\ (sto_cn_dirichletentryproductouter) = S ge_signed_half_dirichletentryproductouteroutput))) /\ ((sto_ap_dirichletentryproductouter * sto_bp_dirichletentryproductouter + sto_an_dirichletentryproductouter * sto_bn_dirichletentryproductouter) + sto_cn_dirichletentryproductouter = (sto_ap_dirichletentryproductouter * sto_bn_dirichletentryproductouter + sto_an_dirichletentryproductouter * sto_bp_dirichletentryproductouter) + sto_cp_dirichletentryproductouter))))))))))))))))))))) \/ ((((dfg_grid_row_dirichlet)=0 \/ ((dfg_grid_column_dirichlet)=0 \/ ~(exists pvs_factor_dirichletentryomittednondivisor. ((n)) = ((dfg_grid_row_dirichlet)*(dfg_grid_column_dirichlet)) * pvs_factor_dirichletentryomittednondivisor))) /\ ((dfg_grid_value_dirichlet)=0))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.