DirichletTable(N,F,G,H)

((exists dst_positive_code_dirichletleft dst_positive_scale_dirichletleft dst_negative_code_dirichletleft dst_negative_scale_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)))))) /\ (forall dst_index_dirichletleft. (exists pvs_le_gap_dirichletleftdomain. pvs_le_gap_dirichletleftdomain + (dst_index_dirichletleft) = ((N))) -> exists dst_positive_dirichletleft dst_negative_dirichletleft dst_value_dirichletleft. ((((exists ff_h_pvs_dirichletleftentrypositive. ff_h_pvs_dirichletleftentrypositive + S (dst_positive_dirichletleft) = S ((S (dst_index_dirichletleft)) * dst_positive_scale_dirichletleft)) /\ exists ff_q_pvs_dirichletleftentrypositive. dst_positive_code_dirichletleft = ff_q_pvs_dirichletleftentrypositive * S ((S (dst_index_dirichletleft)) * dst_positive_scale_dirichletleft) + (dst_positive_dirichletleft))) /\ (((((exists ff_h_pvs_dirichletleftentrynegative. ff_h_pvs_dirichletleftentrynegative + S (dst_negative_dirichletleft) = S ((S (dst_index_dirichletleft)) * dst_negative_scale_dirichletleft)) /\ exists ff_q_pvs_dirichletleftentrynegative. dst_negative_code_dirichletleft = ff_q_pvs_dirichletleftentrynegative * S ((S (dst_index_dirichletleft)) * dst_negative_scale_dirichletleft) + (dst_negative_dirichletleft))) /\ (exists ge_balance_positive_dirichletleftentryvalue ge_balance_negative_dirichletleftentryvalue. (((((dst_value_dirichletleft) = 2 * (ge_balance_positive_dirichletleftentryvalue) /\ (ge_balance_negative_dirichletleftentryvalue) = 0) \/ exists ge_signed_half_dirichletleftentryvaluedecode. (((dst_value_dirichletleft) = 2 * ge_signed_half_dirichletleftentryvaluedecode + 1 /\ (ge_balance_positive_dirichletleftentryvalue) = 0) /\ (ge_balance_negative_dirichletleftentryvalue) = S ge_signed_half_dirichletleftentryvaluedecode))) /\ ((dst_positive_dirichletleft) + ge_balance_negative_dirichletleftentryvalue = (dst_negative_dirichletleft) + ge_balance_positive_dirichletleftentryvalue))))))))) /\ (((exists dst_positive_code_dirichletright dst_positive_scale_dirichletright dst_negative_code_dirichletright dst_negative_scale_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)))))) /\ (forall dst_index_dirichletright. (exists pvs_le_gap_dirichletrightdomain. pvs_le_gap_dirichletrightdomain + (dst_index_dirichletright) = ((N))) -> exists dst_positive_dirichletright dst_negative_dirichletright dst_value_dirichletright. ((((exists ff_h_pvs_dirichletrightentrypositive. ff_h_pvs_dirichletrightentrypositive + S (dst_positive_dirichletright) = S ((S (dst_index_dirichletright)) * dst_positive_scale_dirichletright)) /\ exists ff_q_pvs_dirichletrightentrypositive. dst_positive_code_dirichletright = ff_q_pvs_dirichletrightentrypositive * S ((S (dst_index_dirichletright)) * dst_positive_scale_dirichletright) + (dst_positive_dirichletright))) /\ (((((exists ff_h_pvs_dirichletrightentrynegative. ff_h_pvs_dirichletrightentrynegative + S (dst_negative_dirichletright) = S ((S (dst_index_dirichletright)) * dst_negative_scale_dirichletright)) /\ exists ff_q_pvs_dirichletrightentrynegative. dst_negative_code_dirichletright = ff_q_pvs_dirichletrightentrynegative * S ((S (dst_index_dirichletright)) * dst_negative_scale_dirichletright) + (dst_negative_dirichletright))) /\ (exists ge_balance_positive_dirichletrightentryvalue ge_balance_negative_dirichletrightentryvalue. (((((dst_value_dirichletright) = 2 * (ge_balance_positive_dirichletrightentryvalue) /\ (ge_balance_negative_dirichletrightentryvalue) = 0) \/ exists ge_signed_half_dirichletrightentryvaluedecode. (((dst_value_dirichletright) = 2 * ge_signed_half_dirichletrightentryvaluedecode + 1 /\ (ge_balance_positive_dirichletrightentryvalue) = 0) /\ (ge_balance_negative_dirichletrightentryvalue) = S ge_signed_half_dirichletrightentryvaluedecode))) /\ ((dst_positive_dirichletright) + ge_balance_negative_dirichletrightentryvalue = (dst_negative_dirichletright) + ge_balance_positive_dirichletrightentryvalue))))))))) /\ (((exists dst_positive_code_dirichlettable dst_positive_scale_dirichlettable dst_negative_code_dirichlettable dst_negative_scale_dirichlettable. ((((H)) = (((((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) = ((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 dc_input_dirichlet dc_output_dirichlet. ~(dc_input_dirichlet=0) -> (exists pvs_le_gap_dirichletdomain. pvs_le_gap_dirichletdomain + (dc_input_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. ((((H)) = (((((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_input_dirichlet)) * dst_positive_scale_dirichletlookup)) /\ exists ff_q_pvs_dirichletlookuppositive. dst_positive_code_dirichletlookup = ff_q_pvs_dirichletlookuppositive * S ((S (dc_input_dirichlet)) * dst_positive_scale_dirichletlookup) + (dst_positive_dirichletlookup))) /\ (((((exists ff_h_pvs_dirichletlookupnegative. ff_h_pvs_dirichletlookupnegative + S (dst_negative_dirichletlookup) = S ((S (dc_input_dirichlet)) * dst_negative_scale_dirichletlookup)) /\ exists ff_q_pvs_dirichletlookupnegative. dst_negative_code_dirichletlookup = ff_q_pvs_dirichletlookupnegative * S ((S (dc_input_dirichlet)) * dst_negative_scale_dirichletlookup) + (dst_negative_dirichletlookup))) /\ (exists ge_balance_positive_dirichletlookupvalue ge_balance_negative_dirichletlookupvalue. (((((dc_output_dirichlet) = 2 * (ge_balance_positive_dirichletlookupvalue) /\ (ge_balance_negative_dirichletlookupvalue) = 0) \/ exists ge_signed_half_dirichletlookupvaluedecode. (((dc_output_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_input_dirichlet)=0)) /\ (exists dc_mask_dirichletvalue. ((((exists dst_positive_code_dirichletvaluemasktable dst_positive_scale_dirichletvaluemasktable dst_negative_code_dirichletvaluemasktable dst_negative_scale_dirichletvaluemasktable. (((dc_mask_dirichletvalue) = (((((dst_positive_code_dirichletvaluemasktable) + (dst_positive_scale_dirichletvaluemasktable)) * S ((dst_positive_code_dirichletvaluemasktable) + (dst_positive_scale_dirichletvaluemasktable)) + ((dst_positive_scale_dirichletvaluemasktable) + (dst_positive_scale_dirichletvaluemasktable))) + (((dst_negative_code_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)) * S ((dst_negative_code_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)) + ((dst_negative_scale_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)))) * S ((((dst_positive_code_dirichletvaluemasktable) + (dst_positive_scale_dirichletvaluemasktable)) * S ((dst_positive_code_dirichletvaluemasktable) + (dst_positive_scale_dirichletvaluemasktable)) + ((dst_positive_scale_dirichletvaluemasktable) + (dst_positive_scale_dirichletvaluemasktable))) + (((dst_negative_code_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)) * S ((dst_negative_code_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)) + ((dst_negative_scale_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)))) + ((((dst_negative_code_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)) * S ((dst_negative_code_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)) + ((dst_negative_scale_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable))) + (((dst_negative_code_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)) * S ((dst_negative_code_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)) + ((dst_negative_scale_dirichletvaluemasktable) + (dst_negative_scale_dirichletvaluemasktable)))))) /\ (forall dst_index_dirichletvaluemasktable. (exists pvs_le_gap_dirichletvaluemasktabledomain. pvs_le_gap_dirichletvaluemasktabledomain + (dst_index_dirichletvaluemasktable) = (dc_input_dirichlet)) -> exists dst_positive_dirichletvaluemasktable dst_negative_dirichletvaluemasktable dst_value_dirichletvaluemasktable. ((((exists ff_h_pvs_dirichletvaluemasktableentrypositive. ff_h_pvs_dirichletvaluemasktableentrypositive + S (dst_positive_dirichletvaluemasktable) = S ((S (dst_index_dirichletvaluemasktable)) * dst_positive_scale_dirichletvaluemasktable)) /\ exists ff_q_pvs_dirichletvaluemasktableentrypositive. dst_positive_code_dirichletvaluemasktable = ff_q_pvs_dirichletvaluemasktableentrypositive * S ((S (dst_index_dirichletvaluemasktable)) * dst_positive_scale_dirichletvaluemasktable) + (dst_positive_dirichletvaluemasktable))) /\ (((((exists ff_h_pvs_dirichletvaluemasktableentrynegative. ff_h_pvs_dirichletvaluemasktableentrynegative + S (dst_negative_dirichletvaluemasktable) = S ((S (dst_index_dirichletvaluemasktable)) * dst_negative_scale_dirichletvaluemasktable)) /\ exists ff_q_pvs_dirichletvaluemasktableentrynegative. dst_negative_code_dirichletvaluemasktable = ff_q_pvs_dirichletvaluemasktableentrynegative * S ((S (dst_index_dirichletvaluemasktable)) * dst_negative_scale_dirichletvaluemasktable) + (dst_negative_dirichletvaluemasktable))) /\ (exists ge_balance_positive_dirichletvaluemasktableentryvalue ge_balance_negative_dirichletvaluemasktableentryvalue. (((((dst_value_dirichletvaluemasktable) = 2 * (ge_balance_positive_dirichletvaluemasktableentryvalue) /\ (ge_balance_negative_dirichletvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_dirichletvaluemasktableentryvaluedecode. (((dst_value_dirichletvaluemasktable) = 2 * ge_signed_half_dirichletvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_dirichletvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_dirichletvaluemasktableentryvalue) = S ge_signed_half_dirichletvaluemasktableentryvaluedecode))) /\ ((dst_positive_dirichletvaluemasktable) + ge_balance_negative_dirichletvaluemasktableentryvalue = (dst_negative_dirichletvaluemasktable) + ge_balance_positive_dirichletvaluemasktableentryvalue))))))))) /\ (forall dc_index_dirichletvaluemask dc_value_dirichletvaluemask. (exists pvs_le_gap_dirichletvaluemaskdomain. pvs_le_gap_dirichletvaluemaskdomain + (dc_index_dirichletvaluemask) = (dc_input_dirichlet)) -> (exists dst_positive_code_dirichletvaluemasklookup dst_positive_scale_dirichletvaluemasklookup dst_negative_code_dirichletvaluemasklookup dst_negative_scale_dirichletvaluemasklookup dst_positive_dirichletvaluemasklookup dst_negative_dirichletvaluemasklookup. (((dc_mask_dirichletvalue) = (((((dst_positive_code_dirichletvaluemasklookup) + (dst_positive_scale_dirichletvaluemasklookup)) * S ((dst_positive_code_dirichletvaluemasklookup) + (dst_positive_scale_dirichletvaluemasklookup)) + ((dst_positive_scale_dirichletvaluemasklookup) + (dst_positive_scale_dirichletvaluemasklookup))) + (((dst_negative_code_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)) * S ((dst_negative_code_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)) + ((dst_negative_scale_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)))) * S ((((dst_positive_code_dirichletvaluemasklookup) + (dst_positive_scale_dirichletvaluemasklookup)) * S ((dst_positive_code_dirichletvaluemasklookup) + (dst_positive_scale_dirichletvaluemasklookup)) + ((dst_positive_scale_dirichletvaluemasklookup) + (dst_positive_scale_dirichletvaluemasklookup))) + (((dst_negative_code_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)) * S ((dst_negative_code_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)) + ((dst_negative_scale_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)))) + ((((dst_negative_code_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)) * S ((dst_negative_code_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)) + ((dst_negative_scale_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup))) + (((dst_negative_code_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)) * S ((dst_negative_code_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)) + ((dst_negative_scale_dirichletvaluemasklookup) + (dst_negative_scale_dirichletvaluemasklookup)))))) /\ (((((exists ff_h_pvs_dirichletvaluemasklookuppositive. ff_h_pvs_dirichletvaluemasklookuppositive + S (dst_positive_dirichletvaluemasklookup) = S ((S (dc_index_dirichletvaluemask)) * dst_positive_scale_dirichletvaluemasklookup)) /\ exists ff_q_pvs_dirichletvaluemasklookuppositive. dst_positive_code_dirichletvaluemasklookup = ff_q_pvs_dirichletvaluemasklookuppositive * S ((S (dc_index_dirichletvaluemask)) * dst_positive_scale_dirichletvaluemasklookup) + (dst_positive_dirichletvaluemasklookup))) /\ (((((exists ff_h_pvs_dirichletvaluemasklookupnegative. ff_h_pvs_dirichletvaluemasklookupnegative + S (dst_negative_dirichletvaluemasklookup) = S ((S (dc_index_dirichletvaluemask)) * dst_negative_scale_dirichletvaluemasklookup)) /\ exists ff_q_pvs_dirichletvaluemasklookupnegative. dst_negative_code_dirichletvaluemasklookup = ff_q_pvs_dirichletvaluemasklookupnegative * S ((S (dc_index_dirichletvaluemask)) * dst_negative_scale_dirichletvaluemasklookup) + (dst_negative_dirichletvaluemasklookup))) /\ (exists ge_balance_positive_dirichletvaluemasklookupvalue ge_balance_negative_dirichletvaluemasklookupvalue. (((((dc_value_dirichletvaluemask) = 2 * (ge_balance_positive_dirichletvaluemasklookupvalue) /\ (ge_balance_negative_dirichletvaluemasklookupvalue) = 0) \/ exists ge_signed_half_dirichletvaluemasklookupvaluedecode. (((dc_value_dirichletvaluemask) = 2 * ge_signed_half_dirichletvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_dirichletvaluemasklookupvalue) = 0) /\ (ge_balance_negative_dirichletvaluemasklookupvalue) = S ge_signed_half_dirichletvaluemasklookupvaluedecode))) /\ ((dst_positive_dirichletvaluemasklookup) + ge_balance_negative_dirichletvaluemasklookupvalue = (dst_negative_dirichletvaluemasklookup) + ge_balance_positive_dirichletvaluemasklookupvalue))))))))) -> ((((~((dc_index_dirichletvaluemask)=0)) /\ (exists dc_quotient_dirichletvaluemaskentry dc_left_dirichletvaluemaskentry dc_right_dirichletvaluemaskentry. (((dc_input_dirichlet)=(dc_index_dirichletvaluemask)*dc_quotient_dirichletvaluemaskentry) /\ (((exists dst_positive_code_dirichletvaluemaskentryleft dst_positive_scale_dirichletvaluemaskentryleft dst_negative_code_dirichletvaluemaskentryleft dst_negative_scale_dirichletvaluemaskentryleft dst_positive_dirichletvaluemaskentryleft dst_negative_dirichletvaluemaskentryleft. ((((F)) = (((((dst_positive_code_dirichletvaluemaskentryleft) + (dst_positive_scale_dirichletvaluemaskentryleft)) * S ((dst_positive_code_dirichletvaluemaskentryleft) + (dst_positive_scale_dirichletvaluemaskentryleft)) + ((dst_positive_scale_dirichletvaluemaskentryleft) + (dst_positive_scale_dirichletvaluemaskentryleft))) + (((dst_negative_code_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)) * S ((dst_negative_code_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)) + ((dst_negative_scale_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)))) * S ((((dst_positive_code_dirichletvaluemaskentryleft) + (dst_positive_scale_dirichletvaluemaskentryleft)) * S ((dst_positive_code_dirichletvaluemaskentryleft) + (dst_positive_scale_dirichletvaluemaskentryleft)) + ((dst_positive_scale_dirichletvaluemaskentryleft) + (dst_positive_scale_dirichletvaluemaskentryleft))) + (((dst_negative_code_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)) * S ((dst_negative_code_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)) + ((dst_negative_scale_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)))) + ((((dst_negative_code_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)) * S ((dst_negative_code_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)) + ((dst_negative_scale_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft))) + (((dst_negative_code_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)) * S ((dst_negative_code_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)) + ((dst_negative_scale_dirichletvaluemaskentryleft) + (dst_negative_scale_dirichletvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_dirichletvaluemaskentryleftpositive. ff_h_pvs_dirichletvaluemaskentryleftpositive + S (dst_positive_dirichletvaluemaskentryleft) = S ((S (dc_index_dirichletvaluemask)) * dst_positive_scale_dirichletvaluemaskentryleft)) /\ exists ff_q_pvs_dirichletvaluemaskentryleftpositive. dst_positive_code_dirichletvaluemaskentryleft = ff_q_pvs_dirichletvaluemaskentryleftpositive * S ((S (dc_index_dirichletvaluemask)) * dst_positive_scale_dirichletvaluemaskentryleft) + (dst_positive_dirichletvaluemaskentryleft))) /\ (((((exists ff_h_pvs_dirichletvaluemaskentryleftnegative. ff_h_pvs_dirichletvaluemaskentryleftnegative + S (dst_negative_dirichletvaluemaskentryleft) = S ((S (dc_index_dirichletvaluemask)) * dst_negative_scale_dirichletvaluemaskentryleft)) /\ exists ff_q_pvs_dirichletvaluemaskentryleftnegative. dst_negative_code_dirichletvaluemaskentryleft = ff_q_pvs_dirichletvaluemaskentryleftnegative * S ((S (dc_index_dirichletvaluemask)) * dst_negative_scale_dirichletvaluemaskentryleft) + (dst_negative_dirichletvaluemaskentryleft))) /\ (exists ge_balance_positive_dirichletvaluemaskentryleftvalue ge_balance_negative_dirichletvaluemaskentryleftvalue. (((((dc_left_dirichletvaluemaskentry) = 2 * (ge_balance_positive_dirichletvaluemaskentryleftvalue) /\ (ge_balance_negative_dirichletvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_dirichletvaluemaskentryleftvaluedecode. (((dc_left_dirichletvaluemaskentry) = 2 * ge_signed_half_dirichletvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_dirichletvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_dirichletvaluemaskentryleftvalue) = S ge_signed_half_dirichletvaluemaskentryleftvaluedecode))) /\ ((dst_positive_dirichletvaluemaskentryleft) + ge_balance_negative_dirichletvaluemaskentryleftvalue = (dst_negative_dirichletvaluemaskentryleft) + ge_balance_positive_dirichletvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_dirichletvaluemaskentryright dst_positive_scale_dirichletvaluemaskentryright dst_negative_code_dirichletvaluemaskentryright dst_negative_scale_dirichletvaluemaskentryright dst_positive_dirichletvaluemaskentryright dst_negative_dirichletvaluemaskentryright. ((((G)) = (((((dst_positive_code_dirichletvaluemaskentryright) + (dst_positive_scale_dirichletvaluemaskentryright)) * S ((dst_positive_code_dirichletvaluemaskentryright) + (dst_positive_scale_dirichletvaluemaskentryright)) + ((dst_positive_scale_dirichletvaluemaskentryright) + (dst_positive_scale_dirichletvaluemaskentryright))) + (((dst_negative_code_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)) * S ((dst_negative_code_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)) + ((dst_negative_scale_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)))) * S ((((dst_positive_code_dirichletvaluemaskentryright) + (dst_positive_scale_dirichletvaluemaskentryright)) * S ((dst_positive_code_dirichletvaluemaskentryright) + (dst_positive_scale_dirichletvaluemaskentryright)) + ((dst_positive_scale_dirichletvaluemaskentryright) + (dst_positive_scale_dirichletvaluemaskentryright))) + (((dst_negative_code_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)) * S ((dst_negative_code_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)) + ((dst_negative_scale_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)))) + ((((dst_negative_code_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)) * S ((dst_negative_code_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)) + ((dst_negative_scale_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright))) + (((dst_negative_code_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)) * S ((dst_negative_code_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)) + ((dst_negative_scale_dirichletvaluemaskentryright) + (dst_negative_scale_dirichletvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_dirichletvaluemaskentryrightpositive. ff_h_pvs_dirichletvaluemaskentryrightpositive + S (dst_positive_dirichletvaluemaskentryright) = S ((S (dc_quotient_dirichletvaluemaskentry)) * dst_positive_scale_dirichletvaluemaskentryright)) /\ exists ff_q_pvs_dirichletvaluemaskentryrightpositive. dst_positive_code_dirichletvaluemaskentryright = ff_q_pvs_dirichletvaluemaskentryrightpositive * S ((S (dc_quotient_dirichletvaluemaskentry)) * dst_positive_scale_dirichletvaluemaskentryright) + (dst_positive_dirichletvaluemaskentryright))) /\ (((((exists ff_h_pvs_dirichletvaluemaskentryrightnegative. ff_h_pvs_dirichletvaluemaskentryrightnegative + S (dst_negative_dirichletvaluemaskentryright) = S ((S (dc_quotient_dirichletvaluemaskentry)) * dst_negative_scale_dirichletvaluemaskentryright)) /\ exists ff_q_pvs_dirichletvaluemaskentryrightnegative. dst_negative_code_dirichletvaluemaskentryright = ff_q_pvs_dirichletvaluemaskentryrightnegative * S ((S (dc_quotient_dirichletvaluemaskentry)) * dst_negative_scale_dirichletvaluemaskentryright) + (dst_negative_dirichletvaluemaskentryright))) /\ (exists ge_balance_positive_dirichletvaluemaskentryrightvalue ge_balance_negative_dirichletvaluemaskentryrightvalue. (((((dc_right_dirichletvaluemaskentry) = 2 * (ge_balance_positive_dirichletvaluemaskentryrightvalue) /\ (ge_balance_negative_dirichletvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_dirichletvaluemaskentryrightvaluedecode. (((dc_right_dirichletvaluemaskentry) = 2 * ge_signed_half_dirichletvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_dirichletvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_dirichletvaluemaskentryrightvalue) = S ge_signed_half_dirichletvaluemaskentryrightvaluedecode))) /\ ((dst_positive_dirichletvaluemaskentryright) + ge_balance_negative_dirichletvaluemaskentryrightvalue = (dst_negative_dirichletvaluemaskentryright) + ge_balance_positive_dirichletvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_dirichletvaluemaskentryproduct sto_an_dirichletvaluemaskentryproduct sto_bp_dirichletvaluemaskentryproduct sto_bn_dirichletvaluemaskentryproduct sto_cp_dirichletvaluemaskentryproduct sto_cn_dirichletvaluemaskentryproduct. (((((dc_left_dirichletvaluemaskentry) = 2 * (sto_ap_dirichletvaluemaskentryproduct) /\ (sto_an_dirichletvaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichletvaluemaskentryproductleft. (((dc_left_dirichletvaluemaskentry) = 2 * ge_signed_half_dirichletvaluemaskentryproductleft + 1 /\ (sto_ap_dirichletvaluemaskentryproduct) = 0) /\ (sto_an_dirichletvaluemaskentryproduct) = S ge_signed_half_dirichletvaluemaskentryproductleft))) /\ ((((((dc_right_dirichletvaluemaskentry) = 2 * (sto_bp_dirichletvaluemaskentryproduct) /\ (sto_bn_dirichletvaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichletvaluemaskentryproductright. (((dc_right_dirichletvaluemaskentry) = 2 * ge_signed_half_dirichletvaluemaskentryproductright + 1 /\ (sto_bp_dirichletvaluemaskentryproduct) = 0) /\ (sto_bn_dirichletvaluemaskentryproduct) = S ge_signed_half_dirichletvaluemaskentryproductright))) /\ ((((((dc_value_dirichletvaluemask) = 2 * (sto_cp_dirichletvaluemaskentryproduct) /\ (sto_cn_dirichletvaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichletvaluemaskentryproductoutput. (((dc_value_dirichletvaluemask) = 2 * ge_signed_half_dirichletvaluemaskentryproductoutput + 1 /\ (sto_cp_dirichletvaluemaskentryproduct) = 0) /\ (sto_cn_dirichletvaluemaskentryproduct) = S ge_signed_half_dirichletvaluemaskentryproductoutput))) /\ ((sto_ap_dirichletvaluemaskentryproduct * sto_bp_dirichletvaluemaskentryproduct + sto_an_dirichletvaluemaskentryproduct * sto_bn_dirichletvaluemaskentryproduct) + sto_cn_dirichletvaluemaskentryproduct = (sto_ap_dirichletvaluemaskentryproduct * sto_bn_dirichletvaluemaskentryproduct + sto_an_dirichletvaluemaskentryproduct * sto_bp_dirichletvaluemaskentryproduct) + sto_cp_dirichletvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_dirichletvaluemask)=0 \/ ~(exists pvs_factor_dirichletvaluemaskentrynondivisor. (dc_input_dirichlet) = (dc_index_dirichletvaluemask) * pvs_factor_dirichletvaluemaskentrynondivisor)) /\ ((dc_value_dirichletvaluemask)=0))))))) /\ (exists dst_positive_code_dirichletvaluefold dst_positive_scale_dirichletvaluefold dst_negative_code_dirichletvaluefold dst_negative_scale_dirichletvaluefold dst_positive_sum_dirichletvaluefold dst_negative_sum_dirichletvaluefold. (((dc_mask_dirichletvalue) = (((((dst_positive_code_dirichletvaluefold) + (dst_positive_scale_dirichletvaluefold)) * S ((dst_positive_code_dirichletvaluefold) + (dst_positive_scale_dirichletvaluefold)) + ((dst_positive_scale_dirichletvaluefold) + (dst_positive_scale_dirichletvaluefold))) + (((dst_negative_code_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)) * S ((dst_negative_code_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)) + ((dst_negative_scale_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)))) * S ((((dst_positive_code_dirichletvaluefold) + (dst_positive_scale_dirichletvaluefold)) * S ((dst_positive_code_dirichletvaluefold) + (dst_positive_scale_dirichletvaluefold)) + ((dst_positive_scale_dirichletvaluefold) + (dst_positive_scale_dirichletvaluefold))) + (((dst_negative_code_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)) * S ((dst_negative_code_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)) + ((dst_negative_scale_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)))) + ((((dst_negative_code_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)) * S ((dst_negative_code_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)) + ((dst_negative_scale_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold))) + (((dst_negative_code_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)) * S ((dst_negative_code_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)) + ((dst_negative_scale_dirichletvaluefold) + (dst_negative_scale_dirichletvaluefold)))))) /\ (((exists fs_u_dst_dirichletvaluefoldpositive fs_v_dst_dirichletvaluefoldpositive. ((((exists fs_h_dst_dirichletvaluefoldpositive_body_start. fs_h_dst_dirichletvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichletvaluefoldpositive)) /\ exists fs_q_dst_dirichletvaluefoldpositive_body_start. fs_u_dst_dirichletvaluefoldpositive = fs_q_dst_dirichletvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_dirichletvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_dirichletvaluefoldpositive_body_terminal. fs_h_dst_dirichletvaluefoldpositive_body_terminal + S (dst_positive_sum_dirichletvaluefold) = S ((S (S (dc_input_dirichlet))) * fs_v_dst_dirichletvaluefoldpositive)) /\ exists fs_q_dst_dirichletvaluefoldpositive_body_terminal. fs_u_dst_dirichletvaluefoldpositive = fs_q_dst_dirichletvaluefoldpositive_body_terminal * S ((S (S (dc_input_dirichlet))) * fs_v_dst_dirichletvaluefoldpositive) + (dst_positive_sum_dirichletvaluefold))) /\ forall fs_i_dst_dirichletvaluefoldpositive_body_steps. (exists fs_lt_dst_dirichletvaluefoldpositive_body_steps_bound. fs_lt_dst_dirichletvaluefoldpositive_body_steps_bound + S fs_i_dst_dirichletvaluefoldpositive_body_steps = S (dc_input_dirichlet)) -> exists fs_a_dst_dirichletvaluefoldpositive_body_steps fs_r_dst_dirichletvaluefoldpositive_body_steps fs_s_dst_dirichletvaluefoldpositive_body_steps. ((((exists fs_h_dst_dirichletvaluefoldpositive_body_steps_summand. fs_h_dst_dirichletvaluefoldpositive_body_steps_summand + S (fs_a_dst_dirichletvaluefoldpositive_body_steps) = S ((S (fs_i_dst_dirichletvaluefoldpositive_body_steps)) * dst_positive_scale_dirichletvaluefold)) /\ exists fs_q_dst_dirichletvaluefoldpositive_body_steps_summand. dst_positive_code_dirichletvaluefold = fs_q_dst_dirichletvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_dirichletvaluefoldpositive_body_steps)) * dst_positive_scale_dirichletvaluefold) + (fs_a_dst_dirichletvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichletvaluefoldpositive_body_steps_partial. fs_h_dst_dirichletvaluefoldpositive_body_steps_partial + S (fs_r_dst_dirichletvaluefoldpositive_body_steps) = S ((S (fs_i_dst_dirichletvaluefoldpositive_body_steps)) * fs_v_dst_dirichletvaluefoldpositive)) /\ exists fs_q_dst_dirichletvaluefoldpositive_body_steps_partial. fs_u_dst_dirichletvaluefoldpositive = fs_q_dst_dirichletvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_dirichletvaluefoldpositive_body_steps)) * fs_v_dst_dirichletvaluefoldpositive) + (fs_r_dst_dirichletvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichletvaluefoldpositive_body_steps_successor. fs_h_dst_dirichletvaluefoldpositive_body_steps_successor + S (fs_s_dst_dirichletvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_dirichletvaluefoldpositive_body_steps)) * fs_v_dst_dirichletvaluefoldpositive)) /\ exists fs_q_dst_dirichletvaluefoldpositive_body_steps_successor. fs_u_dst_dirichletvaluefoldpositive = fs_q_dst_dirichletvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_dirichletvaluefoldpositive_body_steps)) * fs_v_dst_dirichletvaluefoldpositive) + (fs_s_dst_dirichletvaluefoldpositive_body_steps))) /\ fs_s_dst_dirichletvaluefoldpositive_body_steps = fs_r_dst_dirichletvaluefoldpositive_body_steps + fs_a_dst_dirichletvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_dirichletvaluefoldnegative fs_v_dst_dirichletvaluefoldnegative. ((((exists fs_h_dst_dirichletvaluefoldnegative_body_start. fs_h_dst_dirichletvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichletvaluefoldnegative)) /\ exists fs_q_dst_dirichletvaluefoldnegative_body_start. fs_u_dst_dirichletvaluefoldnegative = fs_q_dst_dirichletvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_dirichletvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_dirichletvaluefoldnegative_body_terminal. fs_h_dst_dirichletvaluefoldnegative_body_terminal + S (dst_negative_sum_dirichletvaluefold) = S ((S (S (dc_input_dirichlet))) * fs_v_dst_dirichletvaluefoldnegative)) /\ exists fs_q_dst_dirichletvaluefoldnegative_body_terminal. fs_u_dst_dirichletvaluefoldnegative = fs_q_dst_dirichletvaluefoldnegative_body_terminal * S ((S (S (dc_input_dirichlet))) * fs_v_dst_dirichletvaluefoldnegative) + (dst_negative_sum_dirichletvaluefold))) /\ forall fs_i_dst_dirichletvaluefoldnegative_body_steps. (exists fs_lt_dst_dirichletvaluefoldnegative_body_steps_bound. fs_lt_dst_dirichletvaluefoldnegative_body_steps_bound + S fs_i_dst_dirichletvaluefoldnegative_body_steps = S (dc_input_dirichlet)) -> exists fs_a_dst_dirichletvaluefoldnegative_body_steps fs_r_dst_dirichletvaluefoldnegative_body_steps fs_s_dst_dirichletvaluefoldnegative_body_steps. ((((exists fs_h_dst_dirichletvaluefoldnegative_body_steps_summand. fs_h_dst_dirichletvaluefoldnegative_body_steps_summand + S (fs_a_dst_dirichletvaluefoldnegative_body_steps) = S ((S (fs_i_dst_dirichletvaluefoldnegative_body_steps)) * dst_negative_scale_dirichletvaluefold)) /\ exists fs_q_dst_dirichletvaluefoldnegative_body_steps_summand. dst_negative_code_dirichletvaluefold = fs_q_dst_dirichletvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_dirichletvaluefoldnegative_body_steps)) * dst_negative_scale_dirichletvaluefold) + (fs_a_dst_dirichletvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichletvaluefoldnegative_body_steps_partial. fs_h_dst_dirichletvaluefoldnegative_body_steps_partial + S (fs_r_dst_dirichletvaluefoldnegative_body_steps) = S ((S (fs_i_dst_dirichletvaluefoldnegative_body_steps)) * fs_v_dst_dirichletvaluefoldnegative)) /\ exists fs_q_dst_dirichletvaluefoldnegative_body_steps_partial. fs_u_dst_dirichletvaluefoldnegative = fs_q_dst_dirichletvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_dirichletvaluefoldnegative_body_steps)) * fs_v_dst_dirichletvaluefoldnegative) + (fs_r_dst_dirichletvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichletvaluefoldnegative_body_steps_successor. fs_h_dst_dirichletvaluefoldnegative_body_steps_successor + S (fs_s_dst_dirichletvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_dirichletvaluefoldnegative_body_steps)) * fs_v_dst_dirichletvaluefoldnegative)) /\ exists fs_q_dst_dirichletvaluefoldnegative_body_steps_successor. fs_u_dst_dirichletvaluefoldnegative = fs_q_dst_dirichletvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_dirichletvaluefoldnegative_body_steps)) * fs_v_dst_dirichletvaluefoldnegative) + (fs_s_dst_dirichletvaluefoldnegative_body_steps))) /\ fs_s_dst_dirichletvaluefoldnegative_body_steps = fs_r_dst_dirichletvaluefoldnegative_body_steps + fs_a_dst_dirichletvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_dirichletvaluefoldresult ge_balance_negative_dirichletvaluefoldresult. (((((dc_output_dirichlet) = 2 * (ge_balance_positive_dirichletvaluefoldresult) /\ (ge_balance_negative_dirichletvaluefoldresult) = 0) \/ exists ge_signed_half_dirichletvaluefoldresultdecode. (((dc_output_dirichlet) = 2 * ge_signed_half_dirichletvaluefoldresultdecode + 1 /\ (ge_balance_positive_dirichletvaluefoldresult) = 0) /\ (ge_balance_negative_dirichletvaluefoldresult) = S ge_signed_half_dirichletvaluefoldresultdecode))) /\ ((dst_positive_sum_dirichletvaluefold) + ge_balance_negative_dirichletvaluefoldresult = (dst_negative_sum_dirichletvaluefold) + ge_balance_positive_dirichletvaluefoldresult)))))))))))))))))))

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