DirichletPrefix(F,G,n,l,M)

((exists dst_positive_code_dirichlettable dst_positive_scale_dirichlettable dst_negative_code_dirichlettable dst_negative_scale_dirichlettable. ((((M)) = (((((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) = ((l))) -> 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 dc_index_dirichlet dc_value_dirichlet. (exists pvs_le_gap_dirichletdomain. pvs_le_gap_dirichletdomain + (dc_index_dirichlet) = ((l))) -> (exists dst_positive_code_dirichletlookup dst_positive_scale_dirichletlookup dst_negative_code_dirichletlookup dst_negative_scale_dirichletlookup dst_positive_dirichletlookup dst_negative_dirichletlookup. ((((M)) = (((((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 (dc_index_dirichlet)) * dst_positive_scale_dirichletlookup)) /\ exists ff_q_pvs_dirichletlookuppositive. dst_positive_code_dirichletlookup = ff_q_pvs_dirichletlookuppositive * S ((S (dc_index_dirichlet)) * dst_positive_scale_dirichletlookup) + (dst_positive_dirichletlookup))) /\ (((((exists ff_h_pvs_dirichletlookupnegative. ff_h_pvs_dirichletlookupnegative + S (dst_negative_dirichletlookup) = S ((S (dc_index_dirichlet)) * dst_negative_scale_dirichletlookup)) /\ exists ff_q_pvs_dirichletlookupnegative. dst_negative_code_dirichletlookup = ff_q_pvs_dirichletlookupnegative * S ((S (dc_index_dirichlet)) * dst_negative_scale_dirichletlookup) + (dst_negative_dirichletlookup))) /\ (exists ge_balance_positive_dirichletlookupvalue ge_balance_negative_dirichletlookupvalue. (((((dc_value_dirichlet) = 2 * (ge_balance_positive_dirichletlookupvalue) /\ (ge_balance_negative_dirichletlookupvalue) = 0) \/ exists ge_signed_half_dirichletlookupvaluedecode. (((dc_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))))))))) -> ((((~((dc_index_dirichlet)=0)) /\ (exists dc_quotient_dirichletentry dc_left_dirichletentry dc_right_dirichletentry. ((((n))=(dc_index_dirichlet)*dc_quotient_dirichletentry) /\ (((exists dst_positive_code_dirichletentryleft dst_positive_scale_dirichletentryleft dst_negative_code_dirichletentryleft dst_negative_scale_dirichletentryleft dst_positive_dirichletentryleft dst_negative_dirichletentryleft. ((((F)) = (((((dst_positive_code_dirichletentryleft) + (dst_positive_scale_dirichletentryleft)) * S ((dst_positive_code_dirichletentryleft) + (dst_positive_scale_dirichletentryleft)) + ((dst_positive_scale_dirichletentryleft) + (dst_positive_scale_dirichletentryleft))) + (((dst_negative_code_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)) * S ((dst_negative_code_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)) + ((dst_negative_scale_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)))) * S ((((dst_positive_code_dirichletentryleft) + (dst_positive_scale_dirichletentryleft)) * S ((dst_positive_code_dirichletentryleft) + (dst_positive_scale_dirichletentryleft)) + ((dst_positive_scale_dirichletentryleft) + (dst_positive_scale_dirichletentryleft))) + (((dst_negative_code_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)) * S ((dst_negative_code_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)) + ((dst_negative_scale_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)))) + ((((dst_negative_code_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)) * S ((dst_negative_code_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)) + ((dst_negative_scale_dirichletentryleft) + (dst_negative_scale_dirichletentryleft))) + (((dst_negative_code_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)) * S ((dst_negative_code_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)) + ((dst_negative_scale_dirichletentryleft) + (dst_negative_scale_dirichletentryleft)))))) /\ (((((exists ff_h_pvs_dirichletentryleftpositive. ff_h_pvs_dirichletentryleftpositive + S (dst_positive_dirichletentryleft) = S ((S (dc_index_dirichlet)) * dst_positive_scale_dirichletentryleft)) /\ exists ff_q_pvs_dirichletentryleftpositive. dst_positive_code_dirichletentryleft = ff_q_pvs_dirichletentryleftpositive * S ((S (dc_index_dirichlet)) * dst_positive_scale_dirichletentryleft) + (dst_positive_dirichletentryleft))) /\ (((((exists ff_h_pvs_dirichletentryleftnegative. ff_h_pvs_dirichletentryleftnegative + S (dst_negative_dirichletentryleft) = S ((S (dc_index_dirichlet)) * dst_negative_scale_dirichletentryleft)) /\ exists ff_q_pvs_dirichletentryleftnegative. dst_negative_code_dirichletentryleft = ff_q_pvs_dirichletentryleftnegative * S ((S (dc_index_dirichlet)) * dst_negative_scale_dirichletentryleft) + (dst_negative_dirichletentryleft))) /\ (exists ge_balance_positive_dirichletentryleftvalue ge_balance_negative_dirichletentryleftvalue. (((((dc_left_dirichletentry) = 2 * (ge_balance_positive_dirichletentryleftvalue) /\ (ge_balance_negative_dirichletentryleftvalue) = 0) \/ exists ge_signed_half_dirichletentryleftvaluedecode. (((dc_left_dirichletentry) = 2 * ge_signed_half_dirichletentryleftvaluedecode + 1 /\ (ge_balance_positive_dirichletentryleftvalue) = 0) /\ (ge_balance_negative_dirichletentryleftvalue) = S ge_signed_half_dirichletentryleftvaluedecode))) /\ ((dst_positive_dirichletentryleft) + ge_balance_negative_dirichletentryleftvalue = (dst_negative_dirichletentryleft) + ge_balance_positive_dirichletentryleftvalue))))))))) /\ (((exists dst_positive_code_dirichletentryright dst_positive_scale_dirichletentryright dst_negative_code_dirichletentryright dst_negative_scale_dirichletentryright dst_positive_dirichletentryright dst_negative_dirichletentryright. ((((G)) = (((((dst_positive_code_dirichletentryright) + (dst_positive_scale_dirichletentryright)) * S ((dst_positive_code_dirichletentryright) + (dst_positive_scale_dirichletentryright)) + ((dst_positive_scale_dirichletentryright) + (dst_positive_scale_dirichletentryright))) + (((dst_negative_code_dirichletentryright) + (dst_negative_scale_dirichletentryright)) * S ((dst_negative_code_dirichletentryright) + (dst_negative_scale_dirichletentryright)) + ((dst_negative_scale_dirichletentryright) + (dst_negative_scale_dirichletentryright)))) * S ((((dst_positive_code_dirichletentryright) + (dst_positive_scale_dirichletentryright)) * S ((dst_positive_code_dirichletentryright) + (dst_positive_scale_dirichletentryright)) + ((dst_positive_scale_dirichletentryright) + (dst_positive_scale_dirichletentryright))) + (((dst_negative_code_dirichletentryright) + (dst_negative_scale_dirichletentryright)) * S ((dst_negative_code_dirichletentryright) + (dst_negative_scale_dirichletentryright)) + ((dst_negative_scale_dirichletentryright) + (dst_negative_scale_dirichletentryright)))) + ((((dst_negative_code_dirichletentryright) + (dst_negative_scale_dirichletentryright)) * S ((dst_negative_code_dirichletentryright) + (dst_negative_scale_dirichletentryright)) + ((dst_negative_scale_dirichletentryright) + (dst_negative_scale_dirichletentryright))) + (((dst_negative_code_dirichletentryright) + (dst_negative_scale_dirichletentryright)) * S ((dst_negative_code_dirichletentryright) + (dst_negative_scale_dirichletentryright)) + ((dst_negative_scale_dirichletentryright) + (dst_negative_scale_dirichletentryright)))))) /\ (((((exists ff_h_pvs_dirichletentryrightpositive. ff_h_pvs_dirichletentryrightpositive + S (dst_positive_dirichletentryright) = S ((S (dc_quotient_dirichletentry)) * dst_positive_scale_dirichletentryright)) /\ exists ff_q_pvs_dirichletentryrightpositive. dst_positive_code_dirichletentryright = ff_q_pvs_dirichletentryrightpositive * S ((S (dc_quotient_dirichletentry)) * dst_positive_scale_dirichletentryright) + (dst_positive_dirichletentryright))) /\ (((((exists ff_h_pvs_dirichletentryrightnegative. ff_h_pvs_dirichletentryrightnegative + S (dst_negative_dirichletentryright) = S ((S (dc_quotient_dirichletentry)) * dst_negative_scale_dirichletentryright)) /\ exists ff_q_pvs_dirichletentryrightnegative. dst_negative_code_dirichletentryright = ff_q_pvs_dirichletentryrightnegative * S ((S (dc_quotient_dirichletentry)) * dst_negative_scale_dirichletentryright) + (dst_negative_dirichletentryright))) /\ (exists ge_balance_positive_dirichletentryrightvalue ge_balance_negative_dirichletentryrightvalue. (((((dc_right_dirichletentry) = 2 * (ge_balance_positive_dirichletentryrightvalue) /\ (ge_balance_negative_dirichletentryrightvalue) = 0) \/ exists ge_signed_half_dirichletentryrightvaluedecode. (((dc_right_dirichletentry) = 2 * ge_signed_half_dirichletentryrightvaluedecode + 1 /\ (ge_balance_positive_dirichletentryrightvalue) = 0) /\ (ge_balance_negative_dirichletentryrightvalue) = S ge_signed_half_dirichletentryrightvaluedecode))) /\ ((dst_positive_dirichletentryright) + ge_balance_negative_dirichletentryrightvalue = (dst_negative_dirichletentryright) + ge_balance_positive_dirichletentryrightvalue))))))))) /\ (exists sto_ap_dirichletentryproduct sto_an_dirichletentryproduct sto_bp_dirichletentryproduct sto_bn_dirichletentryproduct sto_cp_dirichletentryproduct sto_cn_dirichletentryproduct. (((((dc_left_dirichletentry) = 2 * (sto_ap_dirichletentryproduct) /\ (sto_an_dirichletentryproduct) = 0) \/ exists ge_signed_half_dirichletentryproductleft. (((dc_left_dirichletentry) = 2 * ge_signed_half_dirichletentryproductleft + 1 /\ (sto_ap_dirichletentryproduct) = 0) /\ (sto_an_dirichletentryproduct) = S ge_signed_half_dirichletentryproductleft))) /\ ((((((dc_right_dirichletentry) = 2 * (sto_bp_dirichletentryproduct) /\ (sto_bn_dirichletentryproduct) = 0) \/ exists ge_signed_half_dirichletentryproductright. (((dc_right_dirichletentry) = 2 * ge_signed_half_dirichletentryproductright + 1 /\ (sto_bp_dirichletentryproduct) = 0) /\ (sto_bn_dirichletentryproduct) = S ge_signed_half_dirichletentryproductright))) /\ ((((((dc_value_dirichlet) = 2 * (sto_cp_dirichletentryproduct) /\ (sto_cn_dirichletentryproduct) = 0) \/ exists ge_signed_half_dirichletentryproductoutput. (((dc_value_dirichlet) = 2 * ge_signed_half_dirichletentryproductoutput + 1 /\ (sto_cp_dirichletentryproduct) = 0) /\ (sto_cn_dirichletentryproduct) = S ge_signed_half_dirichletentryproductoutput))) /\ ((sto_ap_dirichletentryproduct * sto_bp_dirichletentryproduct + sto_an_dirichletentryproduct * sto_bn_dirichletentryproduct) + sto_cn_dirichletentryproduct = (sto_ap_dirichletentryproduct * sto_bn_dirichletentryproduct + sto_an_dirichletentryproduct * sto_bp_dirichletentryproduct) + sto_cp_dirichletentryproduct))))))))))))))) \/ ((((dc_index_dirichlet)=0 \/ ~(exists pvs_factor_dirichletentrynondivisor. ((n)) = (dc_index_dirichlet) * pvs_factor_dirichletentrynondivisor)) /\ ((dc_value_dirichlet)=0))))))

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