DirichletSum(F,G,n,z)

((~(((n))=0)) /\ (exists dc_mask_dirichlet. ((((exists dst_positive_code_dirichletmasktable dst_positive_scale_dirichletmasktable dst_negative_code_dirichletmasktable dst_negative_scale_dirichletmasktable. (((dc_mask_dirichlet) = (((((dst_positive_code_dirichletmasktable) + (dst_positive_scale_dirichletmasktable)) * S ((dst_positive_code_dirichletmasktable) + (dst_positive_scale_dirichletmasktable)) + ((dst_positive_scale_dirichletmasktable) + (dst_positive_scale_dirichletmasktable))) + (((dst_negative_code_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)) * S ((dst_negative_code_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)) + ((dst_negative_scale_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)))) * S ((((dst_positive_code_dirichletmasktable) + (dst_positive_scale_dirichletmasktable)) * S ((dst_positive_code_dirichletmasktable) + (dst_positive_scale_dirichletmasktable)) + ((dst_positive_scale_dirichletmasktable) + (dst_positive_scale_dirichletmasktable))) + (((dst_negative_code_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)) * S ((dst_negative_code_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)) + ((dst_negative_scale_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)))) + ((((dst_negative_code_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)) * S ((dst_negative_code_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)) + ((dst_negative_scale_dirichletmasktable) + (dst_negative_scale_dirichletmasktable))) + (((dst_negative_code_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)) * S ((dst_negative_code_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)) + ((dst_negative_scale_dirichletmasktable) + (dst_negative_scale_dirichletmasktable)))))) /\ (forall dst_index_dirichletmasktable. (exists pvs_le_gap_dirichletmasktabledomain. pvs_le_gap_dirichletmasktabledomain + (dst_index_dirichletmasktable) = ((n))) -> exists dst_positive_dirichletmasktable dst_negative_dirichletmasktable dst_value_dirichletmasktable. ((((exists ff_h_pvs_dirichletmasktableentrypositive. ff_h_pvs_dirichletmasktableentrypositive + S (dst_positive_dirichletmasktable) = S ((S (dst_index_dirichletmasktable)) * dst_positive_scale_dirichletmasktable)) /\ exists ff_q_pvs_dirichletmasktableentrypositive. dst_positive_code_dirichletmasktable = ff_q_pvs_dirichletmasktableentrypositive * S ((S (dst_index_dirichletmasktable)) * dst_positive_scale_dirichletmasktable) + (dst_positive_dirichletmasktable))) /\ (((((exists ff_h_pvs_dirichletmasktableentrynegative. ff_h_pvs_dirichletmasktableentrynegative + S (dst_negative_dirichletmasktable) = S ((S (dst_index_dirichletmasktable)) * dst_negative_scale_dirichletmasktable)) /\ exists ff_q_pvs_dirichletmasktableentrynegative. dst_negative_code_dirichletmasktable = ff_q_pvs_dirichletmasktableentrynegative * S ((S (dst_index_dirichletmasktable)) * dst_negative_scale_dirichletmasktable) + (dst_negative_dirichletmasktable))) /\ (exists ge_balance_positive_dirichletmasktableentryvalue ge_balance_negative_dirichletmasktableentryvalue. (((((dst_value_dirichletmasktable) = 2 * (ge_balance_positive_dirichletmasktableentryvalue) /\ (ge_balance_negative_dirichletmasktableentryvalue) = 0) \/ exists ge_signed_half_dirichletmasktableentryvaluedecode. (((dst_value_dirichletmasktable) = 2 * ge_signed_half_dirichletmasktableentryvaluedecode + 1 /\ (ge_balance_positive_dirichletmasktableentryvalue) = 0) /\ (ge_balance_negative_dirichletmasktableentryvalue) = S ge_signed_half_dirichletmasktableentryvaluedecode))) /\ ((dst_positive_dirichletmasktable) + ge_balance_negative_dirichletmasktableentryvalue = (dst_negative_dirichletmasktable) + ge_balance_positive_dirichletmasktableentryvalue))))))))) /\ (forall dc_index_dirichletmask dc_value_dirichletmask. (exists pvs_le_gap_dirichletmaskdomain. pvs_le_gap_dirichletmaskdomain + (dc_index_dirichletmask) = ((n))) -> (exists dst_positive_code_dirichletmasklookup dst_positive_scale_dirichletmasklookup dst_negative_code_dirichletmasklookup dst_negative_scale_dirichletmasklookup dst_positive_dirichletmasklookup dst_negative_dirichletmasklookup. (((dc_mask_dirichlet) = (((((dst_positive_code_dirichletmasklookup) + (dst_positive_scale_dirichletmasklookup)) * S ((dst_positive_code_dirichletmasklookup) + (dst_positive_scale_dirichletmasklookup)) + ((dst_positive_scale_dirichletmasklookup) + (dst_positive_scale_dirichletmasklookup))) + (((dst_negative_code_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)) * S ((dst_negative_code_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)) + ((dst_negative_scale_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)))) * S ((((dst_positive_code_dirichletmasklookup) + (dst_positive_scale_dirichletmasklookup)) * S ((dst_positive_code_dirichletmasklookup) + (dst_positive_scale_dirichletmasklookup)) + ((dst_positive_scale_dirichletmasklookup) + (dst_positive_scale_dirichletmasklookup))) + (((dst_negative_code_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)) * S ((dst_negative_code_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)) + ((dst_negative_scale_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)))) + ((((dst_negative_code_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)) * S ((dst_negative_code_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)) + ((dst_negative_scale_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup))) + (((dst_negative_code_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)) * S ((dst_negative_code_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)) + ((dst_negative_scale_dirichletmasklookup) + (dst_negative_scale_dirichletmasklookup)))))) /\ (((((exists ff_h_pvs_dirichletmasklookuppositive. ff_h_pvs_dirichletmasklookuppositive + S (dst_positive_dirichletmasklookup) = S ((S (dc_index_dirichletmask)) * dst_positive_scale_dirichletmasklookup)) /\ exists ff_q_pvs_dirichletmasklookuppositive. dst_positive_code_dirichletmasklookup = ff_q_pvs_dirichletmasklookuppositive * S ((S (dc_index_dirichletmask)) * dst_positive_scale_dirichletmasklookup) + (dst_positive_dirichletmasklookup))) /\ (((((exists ff_h_pvs_dirichletmasklookupnegative. ff_h_pvs_dirichletmasklookupnegative + S (dst_negative_dirichletmasklookup) = S ((S (dc_index_dirichletmask)) * dst_negative_scale_dirichletmasklookup)) /\ exists ff_q_pvs_dirichletmasklookupnegative. dst_negative_code_dirichletmasklookup = ff_q_pvs_dirichletmasklookupnegative * S ((S (dc_index_dirichletmask)) * dst_negative_scale_dirichletmasklookup) + (dst_negative_dirichletmasklookup))) /\ (exists ge_balance_positive_dirichletmasklookupvalue ge_balance_negative_dirichletmasklookupvalue. (((((dc_value_dirichletmask) = 2 * (ge_balance_positive_dirichletmasklookupvalue) /\ (ge_balance_negative_dirichletmasklookupvalue) = 0) \/ exists ge_signed_half_dirichletmasklookupvaluedecode. (((dc_value_dirichletmask) = 2 * ge_signed_half_dirichletmasklookupvaluedecode + 1 /\ (ge_balance_positive_dirichletmasklookupvalue) = 0) /\ (ge_balance_negative_dirichletmasklookupvalue) = S ge_signed_half_dirichletmasklookupvaluedecode))) /\ ((dst_positive_dirichletmasklookup) + ge_balance_negative_dirichletmasklookupvalue = (dst_negative_dirichletmasklookup) + ge_balance_positive_dirichletmasklookupvalue))))))))) -> ((((~((dc_index_dirichletmask)=0)) /\ (exists dc_quotient_dirichletmaskentry dc_left_dirichletmaskentry dc_right_dirichletmaskentry. ((((n))=(dc_index_dirichletmask)*dc_quotient_dirichletmaskentry) /\ (((exists dst_positive_code_dirichletmaskentryleft dst_positive_scale_dirichletmaskentryleft dst_negative_code_dirichletmaskentryleft dst_negative_scale_dirichletmaskentryleft dst_positive_dirichletmaskentryleft dst_negative_dirichletmaskentryleft. ((((F)) = (((((dst_positive_code_dirichletmaskentryleft) + (dst_positive_scale_dirichletmaskentryleft)) * S ((dst_positive_code_dirichletmaskentryleft) + (dst_positive_scale_dirichletmaskentryleft)) + ((dst_positive_scale_dirichletmaskentryleft) + (dst_positive_scale_dirichletmaskentryleft))) + (((dst_negative_code_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)) * S ((dst_negative_code_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)) + ((dst_negative_scale_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)))) * S ((((dst_positive_code_dirichletmaskentryleft) + (dst_positive_scale_dirichletmaskentryleft)) * S ((dst_positive_code_dirichletmaskentryleft) + (dst_positive_scale_dirichletmaskentryleft)) + ((dst_positive_scale_dirichletmaskentryleft) + (dst_positive_scale_dirichletmaskentryleft))) + (((dst_negative_code_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)) * S ((dst_negative_code_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)) + ((dst_negative_scale_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)))) + ((((dst_negative_code_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)) * S ((dst_negative_code_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)) + ((dst_negative_scale_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft))) + (((dst_negative_code_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)) * S ((dst_negative_code_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)) + ((dst_negative_scale_dirichletmaskentryleft) + (dst_negative_scale_dirichletmaskentryleft)))))) /\ (((((exists ff_h_pvs_dirichletmaskentryleftpositive. ff_h_pvs_dirichletmaskentryleftpositive + S (dst_positive_dirichletmaskentryleft) = S ((S (dc_index_dirichletmask)) * dst_positive_scale_dirichletmaskentryleft)) /\ exists ff_q_pvs_dirichletmaskentryleftpositive. dst_positive_code_dirichletmaskentryleft = ff_q_pvs_dirichletmaskentryleftpositive * S ((S (dc_index_dirichletmask)) * dst_positive_scale_dirichletmaskentryleft) + (dst_positive_dirichletmaskentryleft))) /\ (((((exists ff_h_pvs_dirichletmaskentryleftnegative. ff_h_pvs_dirichletmaskentryleftnegative + S (dst_negative_dirichletmaskentryleft) = S ((S (dc_index_dirichletmask)) * dst_negative_scale_dirichletmaskentryleft)) /\ exists ff_q_pvs_dirichletmaskentryleftnegative. dst_negative_code_dirichletmaskentryleft = ff_q_pvs_dirichletmaskentryleftnegative * S ((S (dc_index_dirichletmask)) * dst_negative_scale_dirichletmaskentryleft) + (dst_negative_dirichletmaskentryleft))) /\ (exists ge_balance_positive_dirichletmaskentryleftvalue ge_balance_negative_dirichletmaskentryleftvalue. (((((dc_left_dirichletmaskentry) = 2 * (ge_balance_positive_dirichletmaskentryleftvalue) /\ (ge_balance_negative_dirichletmaskentryleftvalue) = 0) \/ exists ge_signed_half_dirichletmaskentryleftvaluedecode. (((dc_left_dirichletmaskentry) = 2 * ge_signed_half_dirichletmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_dirichletmaskentryleftvalue) = 0) /\ (ge_balance_negative_dirichletmaskentryleftvalue) = S ge_signed_half_dirichletmaskentryleftvaluedecode))) /\ ((dst_positive_dirichletmaskentryleft) + ge_balance_negative_dirichletmaskentryleftvalue = (dst_negative_dirichletmaskentryleft) + ge_balance_positive_dirichletmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_dirichletmaskentryright dst_positive_scale_dirichletmaskentryright dst_negative_code_dirichletmaskentryright dst_negative_scale_dirichletmaskentryright dst_positive_dirichletmaskentryright dst_negative_dirichletmaskentryright. ((((G)) = (((((dst_positive_code_dirichletmaskentryright) + (dst_positive_scale_dirichletmaskentryright)) * S ((dst_positive_code_dirichletmaskentryright) + (dst_positive_scale_dirichletmaskentryright)) + ((dst_positive_scale_dirichletmaskentryright) + (dst_positive_scale_dirichletmaskentryright))) + (((dst_negative_code_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)) * S ((dst_negative_code_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)) + ((dst_negative_scale_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)))) * S ((((dst_positive_code_dirichletmaskentryright) + (dst_positive_scale_dirichletmaskentryright)) * S ((dst_positive_code_dirichletmaskentryright) + (dst_positive_scale_dirichletmaskentryright)) + ((dst_positive_scale_dirichletmaskentryright) + (dst_positive_scale_dirichletmaskentryright))) + (((dst_negative_code_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)) * S ((dst_negative_code_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)) + ((dst_negative_scale_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)))) + ((((dst_negative_code_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)) * S ((dst_negative_code_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)) + ((dst_negative_scale_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright))) + (((dst_negative_code_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)) * S ((dst_negative_code_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)) + ((dst_negative_scale_dirichletmaskentryright) + (dst_negative_scale_dirichletmaskentryright)))))) /\ (((((exists ff_h_pvs_dirichletmaskentryrightpositive. ff_h_pvs_dirichletmaskentryrightpositive + S (dst_positive_dirichletmaskentryright) = S ((S (dc_quotient_dirichletmaskentry)) * dst_positive_scale_dirichletmaskentryright)) /\ exists ff_q_pvs_dirichletmaskentryrightpositive. dst_positive_code_dirichletmaskentryright = ff_q_pvs_dirichletmaskentryrightpositive * S ((S (dc_quotient_dirichletmaskentry)) * dst_positive_scale_dirichletmaskentryright) + (dst_positive_dirichletmaskentryright))) /\ (((((exists ff_h_pvs_dirichletmaskentryrightnegative. ff_h_pvs_dirichletmaskentryrightnegative + S (dst_negative_dirichletmaskentryright) = S ((S (dc_quotient_dirichletmaskentry)) * dst_negative_scale_dirichletmaskentryright)) /\ exists ff_q_pvs_dirichletmaskentryrightnegative. dst_negative_code_dirichletmaskentryright = ff_q_pvs_dirichletmaskentryrightnegative * S ((S (dc_quotient_dirichletmaskentry)) * dst_negative_scale_dirichletmaskentryright) + (dst_negative_dirichletmaskentryright))) /\ (exists ge_balance_positive_dirichletmaskentryrightvalue ge_balance_negative_dirichletmaskentryrightvalue. (((((dc_right_dirichletmaskentry) = 2 * (ge_balance_positive_dirichletmaskentryrightvalue) /\ (ge_balance_negative_dirichletmaskentryrightvalue) = 0) \/ exists ge_signed_half_dirichletmaskentryrightvaluedecode. (((dc_right_dirichletmaskentry) = 2 * ge_signed_half_dirichletmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_dirichletmaskentryrightvalue) = 0) /\ (ge_balance_negative_dirichletmaskentryrightvalue) = S ge_signed_half_dirichletmaskentryrightvaluedecode))) /\ ((dst_positive_dirichletmaskentryright) + ge_balance_negative_dirichletmaskentryrightvalue = (dst_negative_dirichletmaskentryright) + ge_balance_positive_dirichletmaskentryrightvalue))))))))) /\ (exists sto_ap_dirichletmaskentryproduct sto_an_dirichletmaskentryproduct sto_bp_dirichletmaskentryproduct sto_bn_dirichletmaskentryproduct sto_cp_dirichletmaskentryproduct sto_cn_dirichletmaskentryproduct. (((((dc_left_dirichletmaskentry) = 2 * (sto_ap_dirichletmaskentryproduct) /\ (sto_an_dirichletmaskentryproduct) = 0) \/ exists ge_signed_half_dirichletmaskentryproductleft. (((dc_left_dirichletmaskentry) = 2 * ge_signed_half_dirichletmaskentryproductleft + 1 /\ (sto_ap_dirichletmaskentryproduct) = 0) /\ (sto_an_dirichletmaskentryproduct) = S ge_signed_half_dirichletmaskentryproductleft))) /\ ((((((dc_right_dirichletmaskentry) = 2 * (sto_bp_dirichletmaskentryproduct) /\ (sto_bn_dirichletmaskentryproduct) = 0) \/ exists ge_signed_half_dirichletmaskentryproductright. (((dc_right_dirichletmaskentry) = 2 * ge_signed_half_dirichletmaskentryproductright + 1 /\ (sto_bp_dirichletmaskentryproduct) = 0) /\ (sto_bn_dirichletmaskentryproduct) = S ge_signed_half_dirichletmaskentryproductright))) /\ ((((((dc_value_dirichletmask) = 2 * (sto_cp_dirichletmaskentryproduct) /\ (sto_cn_dirichletmaskentryproduct) = 0) \/ exists ge_signed_half_dirichletmaskentryproductoutput. (((dc_value_dirichletmask) = 2 * ge_signed_half_dirichletmaskentryproductoutput + 1 /\ (sto_cp_dirichletmaskentryproduct) = 0) /\ (sto_cn_dirichletmaskentryproduct) = S ge_signed_half_dirichletmaskentryproductoutput))) /\ ((sto_ap_dirichletmaskentryproduct * sto_bp_dirichletmaskentryproduct + sto_an_dirichletmaskentryproduct * sto_bn_dirichletmaskentryproduct) + sto_cn_dirichletmaskentryproduct = (sto_ap_dirichletmaskentryproduct * sto_bn_dirichletmaskentryproduct + sto_an_dirichletmaskentryproduct * sto_bp_dirichletmaskentryproduct) + sto_cp_dirichletmaskentryproduct))))))))))))))) \/ ((((dc_index_dirichletmask)=0 \/ ~(exists pvs_factor_dirichletmaskentrynondivisor. ((n)) = (dc_index_dirichletmask) * pvs_factor_dirichletmaskentrynondivisor)) /\ ((dc_value_dirichletmask)=0))))))) /\ (exists dst_positive_code_dirichletfold dst_positive_scale_dirichletfold dst_negative_code_dirichletfold dst_negative_scale_dirichletfold dst_positive_sum_dirichletfold dst_negative_sum_dirichletfold. (((dc_mask_dirichlet) = (((((dst_positive_code_dirichletfold) + (dst_positive_scale_dirichletfold)) * S ((dst_positive_code_dirichletfold) + (dst_positive_scale_dirichletfold)) + ((dst_positive_scale_dirichletfold) + (dst_positive_scale_dirichletfold))) + (((dst_negative_code_dirichletfold) + (dst_negative_scale_dirichletfold)) * S ((dst_negative_code_dirichletfold) + (dst_negative_scale_dirichletfold)) + ((dst_negative_scale_dirichletfold) + (dst_negative_scale_dirichletfold)))) * S ((((dst_positive_code_dirichletfold) + (dst_positive_scale_dirichletfold)) * S ((dst_positive_code_dirichletfold) + (dst_positive_scale_dirichletfold)) + ((dst_positive_scale_dirichletfold) + (dst_positive_scale_dirichletfold))) + (((dst_negative_code_dirichletfold) + (dst_negative_scale_dirichletfold)) * S ((dst_negative_code_dirichletfold) + (dst_negative_scale_dirichletfold)) + ((dst_negative_scale_dirichletfold) + (dst_negative_scale_dirichletfold)))) + ((((dst_negative_code_dirichletfold) + (dst_negative_scale_dirichletfold)) * S ((dst_negative_code_dirichletfold) + (dst_negative_scale_dirichletfold)) + ((dst_negative_scale_dirichletfold) + (dst_negative_scale_dirichletfold))) + (((dst_negative_code_dirichletfold) + (dst_negative_scale_dirichletfold)) * S ((dst_negative_code_dirichletfold) + (dst_negative_scale_dirichletfold)) + ((dst_negative_scale_dirichletfold) + (dst_negative_scale_dirichletfold)))))) /\ (((exists fs_u_dst_dirichletfoldpositive fs_v_dst_dirichletfoldpositive. ((((exists fs_h_dst_dirichletfoldpositive_body_start. fs_h_dst_dirichletfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichletfoldpositive)) /\ exists fs_q_dst_dirichletfoldpositive_body_start. fs_u_dst_dirichletfoldpositive = fs_q_dst_dirichletfoldpositive_body_start * S ((S (0)) * fs_v_dst_dirichletfoldpositive) + (0))) /\ ((((exists fs_h_dst_dirichletfoldpositive_body_terminal. fs_h_dst_dirichletfoldpositive_body_terminal + S (dst_positive_sum_dirichletfold) = S ((S (S ((n)))) * fs_v_dst_dirichletfoldpositive)) /\ exists fs_q_dst_dirichletfoldpositive_body_terminal. fs_u_dst_dirichletfoldpositive = fs_q_dst_dirichletfoldpositive_body_terminal * S ((S (S ((n)))) * fs_v_dst_dirichletfoldpositive) + (dst_positive_sum_dirichletfold))) /\ forall fs_i_dst_dirichletfoldpositive_body_steps. (exists fs_lt_dst_dirichletfoldpositive_body_steps_bound. fs_lt_dst_dirichletfoldpositive_body_steps_bound + S fs_i_dst_dirichletfoldpositive_body_steps = S ((n))) -> exists fs_a_dst_dirichletfoldpositive_body_steps fs_r_dst_dirichletfoldpositive_body_steps fs_s_dst_dirichletfoldpositive_body_steps. ((((exists fs_h_dst_dirichletfoldpositive_body_steps_summand. fs_h_dst_dirichletfoldpositive_body_steps_summand + S (fs_a_dst_dirichletfoldpositive_body_steps) = S ((S (fs_i_dst_dirichletfoldpositive_body_steps)) * dst_positive_scale_dirichletfold)) /\ exists fs_q_dst_dirichletfoldpositive_body_steps_summand. dst_positive_code_dirichletfold = fs_q_dst_dirichletfoldpositive_body_steps_summand * S ((S (fs_i_dst_dirichletfoldpositive_body_steps)) * dst_positive_scale_dirichletfold) + (fs_a_dst_dirichletfoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichletfoldpositive_body_steps_partial. fs_h_dst_dirichletfoldpositive_body_steps_partial + S (fs_r_dst_dirichletfoldpositive_body_steps) = S ((S (fs_i_dst_dirichletfoldpositive_body_steps)) * fs_v_dst_dirichletfoldpositive)) /\ exists fs_q_dst_dirichletfoldpositive_body_steps_partial. fs_u_dst_dirichletfoldpositive = fs_q_dst_dirichletfoldpositive_body_steps_partial * S ((S (fs_i_dst_dirichletfoldpositive_body_steps)) * fs_v_dst_dirichletfoldpositive) + (fs_r_dst_dirichletfoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichletfoldpositive_body_steps_successor. fs_h_dst_dirichletfoldpositive_body_steps_successor + S (fs_s_dst_dirichletfoldpositive_body_steps) = S ((S (S fs_i_dst_dirichletfoldpositive_body_steps)) * fs_v_dst_dirichletfoldpositive)) /\ exists fs_q_dst_dirichletfoldpositive_body_steps_successor. fs_u_dst_dirichletfoldpositive = fs_q_dst_dirichletfoldpositive_body_steps_successor * S ((S (S fs_i_dst_dirichletfoldpositive_body_steps)) * fs_v_dst_dirichletfoldpositive) + (fs_s_dst_dirichletfoldpositive_body_steps))) /\ fs_s_dst_dirichletfoldpositive_body_steps = fs_r_dst_dirichletfoldpositive_body_steps + fs_a_dst_dirichletfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_dirichletfoldnegative fs_v_dst_dirichletfoldnegative. ((((exists fs_h_dst_dirichletfoldnegative_body_start. fs_h_dst_dirichletfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichletfoldnegative)) /\ exists fs_q_dst_dirichletfoldnegative_body_start. fs_u_dst_dirichletfoldnegative = fs_q_dst_dirichletfoldnegative_body_start * S ((S (0)) * fs_v_dst_dirichletfoldnegative) + (0))) /\ ((((exists fs_h_dst_dirichletfoldnegative_body_terminal. fs_h_dst_dirichletfoldnegative_body_terminal + S (dst_negative_sum_dirichletfold) = S ((S (S ((n)))) * fs_v_dst_dirichletfoldnegative)) /\ exists fs_q_dst_dirichletfoldnegative_body_terminal. fs_u_dst_dirichletfoldnegative = fs_q_dst_dirichletfoldnegative_body_terminal * S ((S (S ((n)))) * fs_v_dst_dirichletfoldnegative) + (dst_negative_sum_dirichletfold))) /\ forall fs_i_dst_dirichletfoldnegative_body_steps. (exists fs_lt_dst_dirichletfoldnegative_body_steps_bound. fs_lt_dst_dirichletfoldnegative_body_steps_bound + S fs_i_dst_dirichletfoldnegative_body_steps = S ((n))) -> exists fs_a_dst_dirichletfoldnegative_body_steps fs_r_dst_dirichletfoldnegative_body_steps fs_s_dst_dirichletfoldnegative_body_steps. ((((exists fs_h_dst_dirichletfoldnegative_body_steps_summand. fs_h_dst_dirichletfoldnegative_body_steps_summand + S (fs_a_dst_dirichletfoldnegative_body_steps) = S ((S (fs_i_dst_dirichletfoldnegative_body_steps)) * dst_negative_scale_dirichletfold)) /\ exists fs_q_dst_dirichletfoldnegative_body_steps_summand. dst_negative_code_dirichletfold = fs_q_dst_dirichletfoldnegative_body_steps_summand * S ((S (fs_i_dst_dirichletfoldnegative_body_steps)) * dst_negative_scale_dirichletfold) + (fs_a_dst_dirichletfoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichletfoldnegative_body_steps_partial. fs_h_dst_dirichletfoldnegative_body_steps_partial + S (fs_r_dst_dirichletfoldnegative_body_steps) = S ((S (fs_i_dst_dirichletfoldnegative_body_steps)) * fs_v_dst_dirichletfoldnegative)) /\ exists fs_q_dst_dirichletfoldnegative_body_steps_partial. fs_u_dst_dirichletfoldnegative = fs_q_dst_dirichletfoldnegative_body_steps_partial * S ((S (fs_i_dst_dirichletfoldnegative_body_steps)) * fs_v_dst_dirichletfoldnegative) + (fs_r_dst_dirichletfoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichletfoldnegative_body_steps_successor. fs_h_dst_dirichletfoldnegative_body_steps_successor + S (fs_s_dst_dirichletfoldnegative_body_steps) = S ((S (S fs_i_dst_dirichletfoldnegative_body_steps)) * fs_v_dst_dirichletfoldnegative)) /\ exists fs_q_dst_dirichletfoldnegative_body_steps_successor. fs_u_dst_dirichletfoldnegative = fs_q_dst_dirichletfoldnegative_body_steps_successor * S ((S (S fs_i_dst_dirichletfoldnegative_body_steps)) * fs_v_dst_dirichletfoldnegative) + (fs_s_dst_dirichletfoldnegative_body_steps))) /\ fs_s_dst_dirichletfoldnegative_body_steps = fs_r_dst_dirichletfoldnegative_body_steps + fs_a_dst_dirichletfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_dirichletfoldresult ge_balance_negative_dirichletfoldresult. ((((((z)) = 2 * (ge_balance_positive_dirichletfoldresult) /\ (ge_balance_negative_dirichletfoldresult) = 0) \/ exists ge_signed_half_dirichletfoldresultdecode. ((((z)) = 2 * ge_signed_half_dirichletfoldresultdecode + 1 /\ (ge_balance_positive_dirichletfoldresult) = 0) /\ (ge_balance_negative_dirichletfoldresult) = S ge_signed_half_dirichletfoldresultdecode))) /\ ((dst_positive_sum_dirichletfold) + ge_balance_negative_dirichletfoldresult = (dst_negative_sum_dirichletfold) + ge_balance_positive_dirichletfoldresult))))))))))))

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