DirichletGridEntry(F,G,H,n,a,e,z)

(((~(((a))=0)) /\ (((~(((e))=0)) /\ (exists dfg_middle_dirichlet dfg_first_dirichlet dfg_last_dirichlet dfg_value_dirichlet. ((((n))=(((a))*((e)))*dfg_middle_dirichlet) /\ (((exists dst_positive_code_dirichletfirst dst_positive_scale_dirichletfirst dst_negative_code_dirichletfirst dst_negative_scale_dirichletfirst dst_positive_dirichletfirst dst_negative_dirichletfirst. ((((F)) = (((((dst_positive_code_dirichletfirst) + (dst_positive_scale_dirichletfirst)) * S ((dst_positive_code_dirichletfirst) + (dst_positive_scale_dirichletfirst)) + ((dst_positive_scale_dirichletfirst) + (dst_positive_scale_dirichletfirst))) + (((dst_negative_code_dirichletfirst) + (dst_negative_scale_dirichletfirst)) * S ((dst_negative_code_dirichletfirst) + (dst_negative_scale_dirichletfirst)) + ((dst_negative_scale_dirichletfirst) + (dst_negative_scale_dirichletfirst)))) * S ((((dst_positive_code_dirichletfirst) + (dst_positive_scale_dirichletfirst)) * S ((dst_positive_code_dirichletfirst) + (dst_positive_scale_dirichletfirst)) + ((dst_positive_scale_dirichletfirst) + (dst_positive_scale_dirichletfirst))) + (((dst_negative_code_dirichletfirst) + (dst_negative_scale_dirichletfirst)) * S ((dst_negative_code_dirichletfirst) + (dst_negative_scale_dirichletfirst)) + ((dst_negative_scale_dirichletfirst) + (dst_negative_scale_dirichletfirst)))) + ((((dst_negative_code_dirichletfirst) + (dst_negative_scale_dirichletfirst)) * S ((dst_negative_code_dirichletfirst) + (dst_negative_scale_dirichletfirst)) + ((dst_negative_scale_dirichletfirst) + (dst_negative_scale_dirichletfirst))) + (((dst_negative_code_dirichletfirst) + (dst_negative_scale_dirichletfirst)) * S ((dst_negative_code_dirichletfirst) + (dst_negative_scale_dirichletfirst)) + ((dst_negative_scale_dirichletfirst) + (dst_negative_scale_dirichletfirst)))))) /\ (((((exists ff_h_pvs_dirichletfirstpositive. ff_h_pvs_dirichletfirstpositive + S (dst_positive_dirichletfirst) = S ((S ((a))) * dst_positive_scale_dirichletfirst)) /\ exists ff_q_pvs_dirichletfirstpositive. dst_positive_code_dirichletfirst = ff_q_pvs_dirichletfirstpositive * S ((S ((a))) * dst_positive_scale_dirichletfirst) + (dst_positive_dirichletfirst))) /\ (((((exists ff_h_pvs_dirichletfirstnegative. ff_h_pvs_dirichletfirstnegative + S (dst_negative_dirichletfirst) = S ((S ((a))) * dst_negative_scale_dirichletfirst)) /\ exists ff_q_pvs_dirichletfirstnegative. dst_negative_code_dirichletfirst = ff_q_pvs_dirichletfirstnegative * S ((S ((a))) * dst_negative_scale_dirichletfirst) + (dst_negative_dirichletfirst))) /\ (exists ge_balance_positive_dirichletfirstvalue ge_balance_negative_dirichletfirstvalue. (((((dfg_first_dirichlet) = 2 * (ge_balance_positive_dirichletfirstvalue) /\ (ge_balance_negative_dirichletfirstvalue) = 0) \/ exists ge_signed_half_dirichletfirstvaluedecode. (((dfg_first_dirichlet) = 2 * ge_signed_half_dirichletfirstvaluedecode + 1 /\ (ge_balance_positive_dirichletfirstvalue) = 0) /\ (ge_balance_negative_dirichletfirstvalue) = S ge_signed_half_dirichletfirstvaluedecode))) /\ ((dst_positive_dirichletfirst) + ge_balance_negative_dirichletfirstvalue = (dst_negative_dirichletfirst) + ge_balance_positive_dirichletfirstvalue))))))))) /\ (((exists dst_positive_code_dirichletlast dst_positive_scale_dirichletlast dst_negative_code_dirichletlast dst_negative_scale_dirichletlast dst_positive_dirichletlast dst_negative_dirichletlast. ((((H)) = (((((dst_positive_code_dirichletlast) + (dst_positive_scale_dirichletlast)) * S ((dst_positive_code_dirichletlast) + (dst_positive_scale_dirichletlast)) + ((dst_positive_scale_dirichletlast) + (dst_positive_scale_dirichletlast))) + (((dst_negative_code_dirichletlast) + (dst_negative_scale_dirichletlast)) * S ((dst_negative_code_dirichletlast) + (dst_negative_scale_dirichletlast)) + ((dst_negative_scale_dirichletlast) + (dst_negative_scale_dirichletlast)))) * S ((((dst_positive_code_dirichletlast) + (dst_positive_scale_dirichletlast)) * S ((dst_positive_code_dirichletlast) + (dst_positive_scale_dirichletlast)) + ((dst_positive_scale_dirichletlast) + (dst_positive_scale_dirichletlast))) + (((dst_negative_code_dirichletlast) + (dst_negative_scale_dirichletlast)) * S ((dst_negative_code_dirichletlast) + (dst_negative_scale_dirichletlast)) + ((dst_negative_scale_dirichletlast) + (dst_negative_scale_dirichletlast)))) + ((((dst_negative_code_dirichletlast) + (dst_negative_scale_dirichletlast)) * S ((dst_negative_code_dirichletlast) + (dst_negative_scale_dirichletlast)) + ((dst_negative_scale_dirichletlast) + (dst_negative_scale_dirichletlast))) + (((dst_negative_code_dirichletlast) + (dst_negative_scale_dirichletlast)) * S ((dst_negative_code_dirichletlast) + (dst_negative_scale_dirichletlast)) + ((dst_negative_scale_dirichletlast) + (dst_negative_scale_dirichletlast)))))) /\ (((((exists ff_h_pvs_dirichletlastpositive. ff_h_pvs_dirichletlastpositive + S (dst_positive_dirichletlast) = S ((S ((e))) * dst_positive_scale_dirichletlast)) /\ exists ff_q_pvs_dirichletlastpositive. dst_positive_code_dirichletlast = ff_q_pvs_dirichletlastpositive * S ((S ((e))) * dst_positive_scale_dirichletlast) + (dst_positive_dirichletlast))) /\ (((((exists ff_h_pvs_dirichletlastnegative. ff_h_pvs_dirichletlastnegative + S (dst_negative_dirichletlast) = S ((S ((e))) * dst_negative_scale_dirichletlast)) /\ exists ff_q_pvs_dirichletlastnegative. dst_negative_code_dirichletlast = ff_q_pvs_dirichletlastnegative * S ((S ((e))) * dst_negative_scale_dirichletlast) + (dst_negative_dirichletlast))) /\ (exists ge_balance_positive_dirichletlastvalue ge_balance_negative_dirichletlastvalue. (((((dfg_last_dirichlet) = 2 * (ge_balance_positive_dirichletlastvalue) /\ (ge_balance_negative_dirichletlastvalue) = 0) \/ exists ge_signed_half_dirichletlastvaluedecode. (((dfg_last_dirichlet) = 2 * ge_signed_half_dirichletlastvaluedecode + 1 /\ (ge_balance_positive_dirichletlastvalue) = 0) /\ (ge_balance_negative_dirichletlastvalue) = S ge_signed_half_dirichletlastvaluedecode))) /\ ((dst_positive_dirichletlast) + ge_balance_negative_dirichletlastvalue = (dst_negative_dirichletlast) + ge_balance_positive_dirichletlastvalue))))))))) /\ (((exists dst_positive_code_dirichletmiddle dst_positive_scale_dirichletmiddle dst_negative_code_dirichletmiddle dst_negative_scale_dirichletmiddle dst_positive_dirichletmiddle dst_negative_dirichletmiddle. ((((G)) = (((((dst_positive_code_dirichletmiddle) + (dst_positive_scale_dirichletmiddle)) * S ((dst_positive_code_dirichletmiddle) + (dst_positive_scale_dirichletmiddle)) + ((dst_positive_scale_dirichletmiddle) + (dst_positive_scale_dirichletmiddle))) + (((dst_negative_code_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)) * S ((dst_negative_code_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)) + ((dst_negative_scale_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)))) * S ((((dst_positive_code_dirichletmiddle) + (dst_positive_scale_dirichletmiddle)) * S ((dst_positive_code_dirichletmiddle) + (dst_positive_scale_dirichletmiddle)) + ((dst_positive_scale_dirichletmiddle) + (dst_positive_scale_dirichletmiddle))) + (((dst_negative_code_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)) * S ((dst_negative_code_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)) + ((dst_negative_scale_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)))) + ((((dst_negative_code_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)) * S ((dst_negative_code_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)) + ((dst_negative_scale_dirichletmiddle) + (dst_negative_scale_dirichletmiddle))) + (((dst_negative_code_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)) * S ((dst_negative_code_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)) + ((dst_negative_scale_dirichletmiddle) + (dst_negative_scale_dirichletmiddle)))))) /\ (((((exists ff_h_pvs_dirichletmiddlepositive. ff_h_pvs_dirichletmiddlepositive + S (dst_positive_dirichletmiddle) = S ((S (dfg_middle_dirichlet)) * dst_positive_scale_dirichletmiddle)) /\ exists ff_q_pvs_dirichletmiddlepositive. dst_positive_code_dirichletmiddle = ff_q_pvs_dirichletmiddlepositive * S ((S (dfg_middle_dirichlet)) * dst_positive_scale_dirichletmiddle) + (dst_positive_dirichletmiddle))) /\ (((((exists ff_h_pvs_dirichletmiddlenegative. ff_h_pvs_dirichletmiddlenegative + S (dst_negative_dirichletmiddle) = S ((S (dfg_middle_dirichlet)) * dst_negative_scale_dirichletmiddle)) /\ exists ff_q_pvs_dirichletmiddlenegative. dst_negative_code_dirichletmiddle = ff_q_pvs_dirichletmiddlenegative * S ((S (dfg_middle_dirichlet)) * dst_negative_scale_dirichletmiddle) + (dst_negative_dirichletmiddle))) /\ (exists ge_balance_positive_dirichletmiddlevalue ge_balance_negative_dirichletmiddlevalue. (((((dfg_value_dirichlet) = 2 * (ge_balance_positive_dirichletmiddlevalue) /\ (ge_balance_negative_dirichletmiddlevalue) = 0) \/ exists ge_signed_half_dirichletmiddlevaluedecode. (((dfg_value_dirichlet) = 2 * ge_signed_half_dirichletmiddlevaluedecode + 1 /\ (ge_balance_positive_dirichletmiddlevalue) = 0) /\ (ge_balance_negative_dirichletmiddlevalue) = S ge_signed_half_dirichletmiddlevaluedecode))) /\ ((dst_positive_dirichletmiddle) + ge_balance_negative_dirichletmiddlevalue = (dst_negative_dirichletmiddle) + ge_balance_positive_dirichletmiddlevalue))))))))) /\ (exists dfg_inner_dirichletproduct. ((exists sto_ap_dirichletproductinner sto_an_dirichletproductinner sto_bp_dirichletproductinner sto_bn_dirichletproductinner sto_cp_dirichletproductinner sto_cn_dirichletproductinner. (((((dfg_last_dirichlet) = 2 * (sto_ap_dirichletproductinner) /\ (sto_an_dirichletproductinner) = 0) \/ exists ge_signed_half_dirichletproductinnerleft. (((dfg_last_dirichlet) = 2 * ge_signed_half_dirichletproductinnerleft + 1 /\ (sto_ap_dirichletproductinner) = 0) /\ (sto_an_dirichletproductinner) = S ge_signed_half_dirichletproductinnerleft))) /\ ((((((dfg_value_dirichlet) = 2 * (sto_bp_dirichletproductinner) /\ (sto_bn_dirichletproductinner) = 0) \/ exists ge_signed_half_dirichletproductinnerright. (((dfg_value_dirichlet) = 2 * ge_signed_half_dirichletproductinnerright + 1 /\ (sto_bp_dirichletproductinner) = 0) /\ (sto_bn_dirichletproductinner) = S ge_signed_half_dirichletproductinnerright))) /\ ((((((dfg_inner_dirichletproduct) = 2 * (sto_cp_dirichletproductinner) /\ (sto_cn_dirichletproductinner) = 0) \/ exists ge_signed_half_dirichletproductinneroutput. (((dfg_inner_dirichletproduct) = 2 * ge_signed_half_dirichletproductinneroutput + 1 /\ (sto_cp_dirichletproductinner) = 0) /\ (sto_cn_dirichletproductinner) = S ge_signed_half_dirichletproductinneroutput))) /\ ((sto_ap_dirichletproductinner * sto_bp_dirichletproductinner + sto_an_dirichletproductinner * sto_bn_dirichletproductinner) + sto_cn_dirichletproductinner = (sto_ap_dirichletproductinner * sto_bn_dirichletproductinner + sto_an_dirichletproductinner * sto_bp_dirichletproductinner) + sto_cp_dirichletproductinner))))))) /\ (exists sto_ap_dirichletproductouter sto_an_dirichletproductouter sto_bp_dirichletproductouter sto_bn_dirichletproductouter sto_cp_dirichletproductouter sto_cn_dirichletproductouter. (((((dfg_first_dirichlet) = 2 * (sto_ap_dirichletproductouter) /\ (sto_an_dirichletproductouter) = 0) \/ exists ge_signed_half_dirichletproductouterleft. (((dfg_first_dirichlet) = 2 * ge_signed_half_dirichletproductouterleft + 1 /\ (sto_ap_dirichletproductouter) = 0) /\ (sto_an_dirichletproductouter) = S ge_signed_half_dirichletproductouterleft))) /\ ((((((dfg_inner_dirichletproduct) = 2 * (sto_bp_dirichletproductouter) /\ (sto_bn_dirichletproductouter) = 0) \/ exists ge_signed_half_dirichletproductouterright. (((dfg_inner_dirichletproduct) = 2 * ge_signed_half_dirichletproductouterright + 1 /\ (sto_bp_dirichletproductouter) = 0) /\ (sto_bn_dirichletproductouter) = S ge_signed_half_dirichletproductouterright))) /\ (((((((z)) = 2 * (sto_cp_dirichletproductouter) /\ (sto_cn_dirichletproductouter) = 0) \/ exists ge_signed_half_dirichletproductouteroutput. ((((z)) = 2 * ge_signed_half_dirichletproductouteroutput + 1 /\ (sto_cp_dirichletproductouter) = 0) /\ (sto_cn_dirichletproductouter) = S ge_signed_half_dirichletproductouteroutput))) /\ ((sto_ap_dirichletproductouter * sto_bp_dirichletproductouter + sto_an_dirichletproductouter * sto_bn_dirichletproductouter) + sto_cn_dirichletproductouter = (sto_ap_dirichletproductouter * sto_bn_dirichletproductouter + sto_an_dirichletproductouter * sto_bp_dirichletproductouter) + sto_cp_dirichletproductouter))))))))))))))))))))) \/ (((((a))=0 \/ (((e))=0 \/ ~(exists pvs_factor_dirichletomittednondivisor. ((n)) = (((a))*((e))) * pvs_factor_dirichletomittednondivisor))) /\ (((z))=0)))

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