DirichletEntry(F,G,n,d,z)

(((~(((d))=0)) /\ (exists dc_quotient_dirichlet dc_left_dirichlet dc_right_dirichlet. ((((n))=((d))*dc_quotient_dirichlet) /\ (((exists dst_positive_code_dirichletleft dst_positive_scale_dirichletleft dst_negative_code_dirichletleft dst_negative_scale_dirichletleft dst_positive_dirichletleft dst_negative_dirichletleft. ((((F)) = (((((dst_positive_code_dirichletleft) + (dst_positive_scale_dirichletleft)) * S ((dst_positive_code_dirichletleft) + (dst_positive_scale_dirichletleft)) + ((dst_positive_scale_dirichletleft) + (dst_positive_scale_dirichletleft))) + (((dst_negative_code_dirichletleft) + (dst_negative_scale_dirichletleft)) * S ((dst_negative_code_dirichletleft) + (dst_negative_scale_dirichletleft)) + ((dst_negative_scale_dirichletleft) + (dst_negative_scale_dirichletleft)))) * S ((((dst_positive_code_dirichletleft) + (dst_positive_scale_dirichletleft)) * S ((dst_positive_code_dirichletleft) + (dst_positive_scale_dirichletleft)) + ((dst_positive_scale_dirichletleft) + (dst_positive_scale_dirichletleft))) + (((dst_negative_code_dirichletleft) + (dst_negative_scale_dirichletleft)) * S ((dst_negative_code_dirichletleft) + (dst_negative_scale_dirichletleft)) + ((dst_negative_scale_dirichletleft) + (dst_negative_scale_dirichletleft)))) + ((((dst_negative_code_dirichletleft) + (dst_negative_scale_dirichletleft)) * S ((dst_negative_code_dirichletleft) + (dst_negative_scale_dirichletleft)) + ((dst_negative_scale_dirichletleft) + (dst_negative_scale_dirichletleft))) + (((dst_negative_code_dirichletleft) + (dst_negative_scale_dirichletleft)) * S ((dst_negative_code_dirichletleft) + (dst_negative_scale_dirichletleft)) + ((dst_negative_scale_dirichletleft) + (dst_negative_scale_dirichletleft)))))) /\ (((((exists ff_h_pvs_dirichletleftpositive. ff_h_pvs_dirichletleftpositive + S (dst_positive_dirichletleft) = S ((S ((d))) * dst_positive_scale_dirichletleft)) /\ exists ff_q_pvs_dirichletleftpositive. dst_positive_code_dirichletleft = ff_q_pvs_dirichletleftpositive * S ((S ((d))) * dst_positive_scale_dirichletleft) + (dst_positive_dirichletleft))) /\ (((((exists ff_h_pvs_dirichletleftnegative. ff_h_pvs_dirichletleftnegative + S (dst_negative_dirichletleft) = S ((S ((d))) * dst_negative_scale_dirichletleft)) /\ exists ff_q_pvs_dirichletleftnegative. dst_negative_code_dirichletleft = ff_q_pvs_dirichletleftnegative * S ((S ((d))) * dst_negative_scale_dirichletleft) + (dst_negative_dirichletleft))) /\ (exists ge_balance_positive_dirichletleftvalue ge_balance_negative_dirichletleftvalue. (((((dc_left_dirichlet) = 2 * (ge_balance_positive_dirichletleftvalue) /\ (ge_balance_negative_dirichletleftvalue) = 0) \/ exists ge_signed_half_dirichletleftvaluedecode. (((dc_left_dirichlet) = 2 * ge_signed_half_dirichletleftvaluedecode + 1 /\ (ge_balance_positive_dirichletleftvalue) = 0) /\ (ge_balance_negative_dirichletleftvalue) = S ge_signed_half_dirichletleftvaluedecode))) /\ ((dst_positive_dirichletleft) + ge_balance_negative_dirichletleftvalue = (dst_negative_dirichletleft) + ge_balance_positive_dirichletleftvalue))))))))) /\ (((exists dst_positive_code_dirichletright dst_positive_scale_dirichletright dst_negative_code_dirichletright dst_negative_scale_dirichletright dst_positive_dirichletright dst_negative_dirichletright. ((((G)) = (((((dst_positive_code_dirichletright) + (dst_positive_scale_dirichletright)) * S ((dst_positive_code_dirichletright) + (dst_positive_scale_dirichletright)) + ((dst_positive_scale_dirichletright) + (dst_positive_scale_dirichletright))) + (((dst_negative_code_dirichletright) + (dst_negative_scale_dirichletright)) * S ((dst_negative_code_dirichletright) + (dst_negative_scale_dirichletright)) + ((dst_negative_scale_dirichletright) + (dst_negative_scale_dirichletright)))) * S ((((dst_positive_code_dirichletright) + (dst_positive_scale_dirichletright)) * S ((dst_positive_code_dirichletright) + (dst_positive_scale_dirichletright)) + ((dst_positive_scale_dirichletright) + (dst_positive_scale_dirichletright))) + (((dst_negative_code_dirichletright) + (dst_negative_scale_dirichletright)) * S ((dst_negative_code_dirichletright) + (dst_negative_scale_dirichletright)) + ((dst_negative_scale_dirichletright) + (dst_negative_scale_dirichletright)))) + ((((dst_negative_code_dirichletright) + (dst_negative_scale_dirichletright)) * S ((dst_negative_code_dirichletright) + (dst_negative_scale_dirichletright)) + ((dst_negative_scale_dirichletright) + (dst_negative_scale_dirichletright))) + (((dst_negative_code_dirichletright) + (dst_negative_scale_dirichletright)) * S ((dst_negative_code_dirichletright) + (dst_negative_scale_dirichletright)) + ((dst_negative_scale_dirichletright) + (dst_negative_scale_dirichletright)))))) /\ (((((exists ff_h_pvs_dirichletrightpositive. ff_h_pvs_dirichletrightpositive + S (dst_positive_dirichletright) = S ((S (dc_quotient_dirichlet)) * dst_positive_scale_dirichletright)) /\ exists ff_q_pvs_dirichletrightpositive. dst_positive_code_dirichletright = ff_q_pvs_dirichletrightpositive * S ((S (dc_quotient_dirichlet)) * dst_positive_scale_dirichletright) + (dst_positive_dirichletright))) /\ (((((exists ff_h_pvs_dirichletrightnegative. ff_h_pvs_dirichletrightnegative + S (dst_negative_dirichletright) = S ((S (dc_quotient_dirichlet)) * dst_negative_scale_dirichletright)) /\ exists ff_q_pvs_dirichletrightnegative. dst_negative_code_dirichletright = ff_q_pvs_dirichletrightnegative * S ((S (dc_quotient_dirichlet)) * dst_negative_scale_dirichletright) + (dst_negative_dirichletright))) /\ (exists ge_balance_positive_dirichletrightvalue ge_balance_negative_dirichletrightvalue. (((((dc_right_dirichlet) = 2 * (ge_balance_positive_dirichletrightvalue) /\ (ge_balance_negative_dirichletrightvalue) = 0) \/ exists ge_signed_half_dirichletrightvaluedecode. (((dc_right_dirichlet) = 2 * ge_signed_half_dirichletrightvaluedecode + 1 /\ (ge_balance_positive_dirichletrightvalue) = 0) /\ (ge_balance_negative_dirichletrightvalue) = S ge_signed_half_dirichletrightvaluedecode))) /\ ((dst_positive_dirichletright) + ge_balance_negative_dirichletrightvalue = (dst_negative_dirichletright) + ge_balance_positive_dirichletrightvalue))))))))) /\ (exists sto_ap_dirichletproduct sto_an_dirichletproduct sto_bp_dirichletproduct sto_bn_dirichletproduct sto_cp_dirichletproduct sto_cn_dirichletproduct. (((((dc_left_dirichlet) = 2 * (sto_ap_dirichletproduct) /\ (sto_an_dirichletproduct) = 0) \/ exists ge_signed_half_dirichletproductleft. (((dc_left_dirichlet) = 2 * ge_signed_half_dirichletproductleft + 1 /\ (sto_ap_dirichletproduct) = 0) /\ (sto_an_dirichletproduct) = S ge_signed_half_dirichletproductleft))) /\ ((((((dc_right_dirichlet) = 2 * (sto_bp_dirichletproduct) /\ (sto_bn_dirichletproduct) = 0) \/ exists ge_signed_half_dirichletproductright. (((dc_right_dirichlet) = 2 * ge_signed_half_dirichletproductright + 1 /\ (sto_bp_dirichletproduct) = 0) /\ (sto_bn_dirichletproduct) = S ge_signed_half_dirichletproductright))) /\ (((((((z)) = 2 * (sto_cp_dirichletproduct) /\ (sto_cn_dirichletproduct) = 0) \/ exists ge_signed_half_dirichletproductoutput. ((((z)) = 2 * ge_signed_half_dirichletproductoutput + 1 /\ (sto_cp_dirichletproduct) = 0) /\ (sto_cn_dirichletproduct) = S ge_signed_half_dirichletproductoutput))) /\ ((sto_ap_dirichletproduct * sto_bp_dirichletproduct + sto_an_dirichletproduct * sto_bn_dirichletproduct) + sto_cn_dirichletproduct = (sto_ap_dirichletproduct * sto_bn_dirichletproduct + sto_an_dirichletproduct * sto_bp_dirichletproduct) + sto_cp_dirichletproduct))))))))))))))) \/ (((((d))=0 \/ ~(exists pvs_factor_dirichletnondivisor. ((n)) = ((d)) * pvs_factor_dirichletnondivisor)) /\ (((z))=0)))

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