DivisorTransform(N,F,G)

forall mi_index_dirichlet mi_value_dirichlet. ~(mi_index_dirichlet=0) -> (exists pvs_le_gap_dirichletbound. pvs_le_gap_dirichletbound + (mi_index_dirichlet) = ((N))) -> (exists dst_positive_code_dirichletentry dst_positive_scale_dirichletentry dst_negative_code_dirichletentry dst_negative_scale_dirichletentry dst_positive_dirichletentry dst_negative_dirichletentry. ((((G)) = (((((dst_positive_code_dirichletentry) + (dst_positive_scale_dirichletentry)) * S ((dst_positive_code_dirichletentry) + (dst_positive_scale_dirichletentry)) + ((dst_positive_scale_dirichletentry) + (dst_positive_scale_dirichletentry))) + (((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) * S ((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) + ((dst_negative_scale_dirichletentry) + (dst_negative_scale_dirichletentry)))) * S ((((dst_positive_code_dirichletentry) + (dst_positive_scale_dirichletentry)) * S ((dst_positive_code_dirichletentry) + (dst_positive_scale_dirichletentry)) + ((dst_positive_scale_dirichletentry) + (dst_positive_scale_dirichletentry))) + (((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) * S ((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) + ((dst_negative_scale_dirichletentry) + (dst_negative_scale_dirichletentry)))) + ((((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) * S ((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) + ((dst_negative_scale_dirichletentry) + (dst_negative_scale_dirichletentry))) + (((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) * S ((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) + ((dst_negative_scale_dirichletentry) + (dst_negative_scale_dirichletentry)))))) /\ (((((exists ff_h_pvs_dirichletentrypositive. ff_h_pvs_dirichletentrypositive + S (dst_positive_dirichletentry) = S ((S (mi_index_dirichlet)) * dst_positive_scale_dirichletentry)) /\ exists ff_q_pvs_dirichletentrypositive. dst_positive_code_dirichletentry = ff_q_pvs_dirichletentrypositive * S ((S (mi_index_dirichlet)) * dst_positive_scale_dirichletentry) + (dst_positive_dirichletentry))) /\ (((((exists ff_h_pvs_dirichletentrynegative. ff_h_pvs_dirichletentrynegative + S (dst_negative_dirichletentry) = S ((S (mi_index_dirichlet)) * dst_negative_scale_dirichletentry)) /\ exists ff_q_pvs_dirichletentrynegative. dst_negative_code_dirichletentry = ff_q_pvs_dirichletentrynegative * S ((S (mi_index_dirichlet)) * dst_negative_scale_dirichletentry) + (dst_negative_dirichletentry))) /\ (exists ge_balance_positive_dirichletentryvalue ge_balance_negative_dirichletentryvalue. (((((mi_value_dirichlet) = 2 * (ge_balance_positive_dirichletentryvalue) /\ (ge_balance_negative_dirichletentryvalue) = 0) \/ exists ge_signed_half_dirichletentryvaluedecode. (((mi_value_dirichlet) = 2 * ge_signed_half_dirichletentryvaluedecode + 1 /\ (ge_balance_positive_dirichletentryvalue) = 0) /\ (ge_balance_negative_dirichletentryvalue) = S ge_signed_half_dirichletentryvaluedecode))) /\ ((dst_positive_dirichletentry) + ge_balance_negative_dirichletentryvalue = (dst_negative_dirichletentry) + ge_balance_positive_dirichletentryvalue))))))))) -> (((~((mi_index_dirichlet)=0)) /\ (exists dm_mask_table_dirichletsum. ((((exists dst_positive_code_dirichletsummasktable dst_positive_scale_dirichletsummasktable dst_negative_code_dirichletsummasktable dst_negative_scale_dirichletsummasktable. (((dm_mask_table_dirichletsum) = (((((dst_positive_code_dirichletsummasktable) + (dst_positive_scale_dirichletsummasktable)) * S ((dst_positive_code_dirichletsummasktable) + (dst_positive_scale_dirichletsummasktable)) + ((dst_positive_scale_dirichletsummasktable) + (dst_positive_scale_dirichletsummasktable))) + (((dst_negative_code_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)) * S ((dst_negative_code_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)) + ((dst_negative_scale_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)))) * S ((((dst_positive_code_dirichletsummasktable) + (dst_positive_scale_dirichletsummasktable)) * S ((dst_positive_code_dirichletsummasktable) + (dst_positive_scale_dirichletsummasktable)) + ((dst_positive_scale_dirichletsummasktable) + (dst_positive_scale_dirichletsummasktable))) + (((dst_negative_code_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)) * S ((dst_negative_code_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)) + ((dst_negative_scale_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)))) + ((((dst_negative_code_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)) * S ((dst_negative_code_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)) + ((dst_negative_scale_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable))) + (((dst_negative_code_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)) * S ((dst_negative_code_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)) + ((dst_negative_scale_dirichletsummasktable) + (dst_negative_scale_dirichletsummasktable)))))) /\ (forall dst_index_dirichletsummasktable. (exists pvs_le_gap_dirichletsummasktabledomain. pvs_le_gap_dirichletsummasktabledomain + (dst_index_dirichletsummasktable) = (mi_index_dirichlet)) -> exists dst_positive_dirichletsummasktable dst_negative_dirichletsummasktable dst_value_dirichletsummasktable. ((((exists ff_h_pvs_dirichletsummasktableentrypositive. ff_h_pvs_dirichletsummasktableentrypositive + S (dst_positive_dirichletsummasktable) = S ((S (dst_index_dirichletsummasktable)) * dst_positive_scale_dirichletsummasktable)) /\ exists ff_q_pvs_dirichletsummasktableentrypositive. dst_positive_code_dirichletsummasktable = ff_q_pvs_dirichletsummasktableentrypositive * S ((S (dst_index_dirichletsummasktable)) * dst_positive_scale_dirichletsummasktable) + (dst_positive_dirichletsummasktable))) /\ (((((exists ff_h_pvs_dirichletsummasktableentrynegative. ff_h_pvs_dirichletsummasktableentrynegative + S (dst_negative_dirichletsummasktable) = S ((S (dst_index_dirichletsummasktable)) * dst_negative_scale_dirichletsummasktable)) /\ exists ff_q_pvs_dirichletsummasktableentrynegative. dst_negative_code_dirichletsummasktable = ff_q_pvs_dirichletsummasktableentrynegative * S ((S (dst_index_dirichletsummasktable)) * dst_negative_scale_dirichletsummasktable) + (dst_negative_dirichletsummasktable))) /\ (exists ge_balance_positive_dirichletsummasktableentryvalue ge_balance_negative_dirichletsummasktableentryvalue. (((((dst_value_dirichletsummasktable) = 2 * (ge_balance_positive_dirichletsummasktableentryvalue) /\ (ge_balance_negative_dirichletsummasktableentryvalue) = 0) \/ exists ge_signed_half_dirichletsummasktableentryvaluedecode. (((dst_value_dirichletsummasktable) = 2 * ge_signed_half_dirichletsummasktableentryvaluedecode + 1 /\ (ge_balance_positive_dirichletsummasktableentryvalue) = 0) /\ (ge_balance_negative_dirichletsummasktableentryvalue) = S ge_signed_half_dirichletsummasktableentryvaluedecode))) /\ ((dst_positive_dirichletsummasktable) + ge_balance_negative_dirichletsummasktableentryvalue = (dst_negative_dirichletsummasktable) + ge_balance_positive_dirichletsummasktableentryvalue))))))))) /\ (forall dm_index_dirichletsummask dm_value_dirichletsummask. (exists pvs_le_gap_dirichletsummaskdomain. pvs_le_gap_dirichletsummaskdomain + (dm_index_dirichletsummask) = (mi_index_dirichlet)) -> (exists dst_positive_code_dirichletsummasklookup dst_positive_scale_dirichletsummasklookup dst_negative_code_dirichletsummasklookup dst_negative_scale_dirichletsummasklookup dst_positive_dirichletsummasklookup dst_negative_dirichletsummasklookup. (((dm_mask_table_dirichletsum) = (((((dst_positive_code_dirichletsummasklookup) + (dst_positive_scale_dirichletsummasklookup)) * S ((dst_positive_code_dirichletsummasklookup) + (dst_positive_scale_dirichletsummasklookup)) + ((dst_positive_scale_dirichletsummasklookup) + (dst_positive_scale_dirichletsummasklookup))) + (((dst_negative_code_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)) * S ((dst_negative_code_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)) + ((dst_negative_scale_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)))) * S ((((dst_positive_code_dirichletsummasklookup) + (dst_positive_scale_dirichletsummasklookup)) * S ((dst_positive_code_dirichletsummasklookup) + (dst_positive_scale_dirichletsummasklookup)) + ((dst_positive_scale_dirichletsummasklookup) + (dst_positive_scale_dirichletsummasklookup))) + (((dst_negative_code_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)) * S ((dst_negative_code_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)) + ((dst_negative_scale_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)))) + ((((dst_negative_code_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)) * S ((dst_negative_code_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)) + ((dst_negative_scale_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup))) + (((dst_negative_code_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)) * S ((dst_negative_code_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)) + ((dst_negative_scale_dirichletsummasklookup) + (dst_negative_scale_dirichletsummasklookup)))))) /\ (((((exists ff_h_pvs_dirichletsummasklookuppositive. ff_h_pvs_dirichletsummasklookuppositive + S (dst_positive_dirichletsummasklookup) = S ((S (dm_index_dirichletsummask)) * dst_positive_scale_dirichletsummasklookup)) /\ exists ff_q_pvs_dirichletsummasklookuppositive. dst_positive_code_dirichletsummasklookup = ff_q_pvs_dirichletsummasklookuppositive * S ((S (dm_index_dirichletsummask)) * dst_positive_scale_dirichletsummasklookup) + (dst_positive_dirichletsummasklookup))) /\ (((((exists ff_h_pvs_dirichletsummasklookupnegative. ff_h_pvs_dirichletsummasklookupnegative + S (dst_negative_dirichletsummasklookup) = S ((S (dm_index_dirichletsummask)) * dst_negative_scale_dirichletsummasklookup)) /\ exists ff_q_pvs_dirichletsummasklookupnegative. dst_negative_code_dirichletsummasklookup = ff_q_pvs_dirichletsummasklookupnegative * S ((S (dm_index_dirichletsummask)) * dst_negative_scale_dirichletsummasklookup) + (dst_negative_dirichletsummasklookup))) /\ (exists ge_balance_positive_dirichletsummasklookupvalue ge_balance_negative_dirichletsummasklookupvalue. (((((dm_value_dirichletsummask) = 2 * (ge_balance_positive_dirichletsummasklookupvalue) /\ (ge_balance_negative_dirichletsummasklookupvalue) = 0) \/ exists ge_signed_half_dirichletsummasklookupvaluedecode. (((dm_value_dirichletsummask) = 2 * ge_signed_half_dirichletsummasklookupvaluedecode + 1 /\ (ge_balance_positive_dirichletsummasklookupvalue) = 0) /\ (ge_balance_negative_dirichletsummasklookupvalue) = S ge_signed_half_dirichletsummasklookupvaluedecode))) /\ ((dst_positive_dirichletsummasklookup) + ge_balance_negative_dirichletsummasklookupvalue = (dst_negative_dirichletsummasklookup) + ge_balance_positive_dirichletsummasklookupvalue))))))))) -> ((((~((dm_index_dirichletsummask)=0)) /\ (exists dm_quotient_dirichletsummaskentry. (((mi_index_dirichlet)=(dm_index_dirichletsummask)*dm_quotient_dirichletsummaskentry) /\ (exists dst_positive_code_dirichletsummaskentryinput dst_positive_scale_dirichletsummaskentryinput dst_negative_code_dirichletsummaskentryinput dst_negative_scale_dirichletsummaskentryinput dst_positive_dirichletsummaskentryinput dst_negative_dirichletsummaskentryinput. ((((F)) = (((((dst_positive_code_dirichletsummaskentryinput) + (dst_positive_scale_dirichletsummaskentryinput)) * S ((dst_positive_code_dirichletsummaskentryinput) + (dst_positive_scale_dirichletsummaskentryinput)) + ((dst_positive_scale_dirichletsummaskentryinput) + (dst_positive_scale_dirichletsummaskentryinput))) + (((dst_negative_code_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)) * S ((dst_negative_code_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)) + ((dst_negative_scale_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)))) * S ((((dst_positive_code_dirichletsummaskentryinput) + (dst_positive_scale_dirichletsummaskentryinput)) * S ((dst_positive_code_dirichletsummaskentryinput) + (dst_positive_scale_dirichletsummaskentryinput)) + ((dst_positive_scale_dirichletsummaskentryinput) + (dst_positive_scale_dirichletsummaskentryinput))) + (((dst_negative_code_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)) * S ((dst_negative_code_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)) + ((dst_negative_scale_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)))) + ((((dst_negative_code_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)) * S ((dst_negative_code_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)) + ((dst_negative_scale_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput))) + (((dst_negative_code_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)) * S ((dst_negative_code_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)) + ((dst_negative_scale_dirichletsummaskentryinput) + (dst_negative_scale_dirichletsummaskentryinput)))))) /\ (((((exists ff_h_pvs_dirichletsummaskentryinputpositive. ff_h_pvs_dirichletsummaskentryinputpositive + S (dst_positive_dirichletsummaskentryinput) = S ((S (dm_index_dirichletsummask)) * dst_positive_scale_dirichletsummaskentryinput)) /\ exists ff_q_pvs_dirichletsummaskentryinputpositive. dst_positive_code_dirichletsummaskentryinput = ff_q_pvs_dirichletsummaskentryinputpositive * S ((S (dm_index_dirichletsummask)) * dst_positive_scale_dirichletsummaskentryinput) + (dst_positive_dirichletsummaskentryinput))) /\ (((((exists ff_h_pvs_dirichletsummaskentryinputnegative. ff_h_pvs_dirichletsummaskentryinputnegative + S (dst_negative_dirichletsummaskentryinput) = S ((S (dm_index_dirichletsummask)) * dst_negative_scale_dirichletsummaskentryinput)) /\ exists ff_q_pvs_dirichletsummaskentryinputnegative. dst_negative_code_dirichletsummaskentryinput = ff_q_pvs_dirichletsummaskentryinputnegative * S ((S (dm_index_dirichletsummask)) * dst_negative_scale_dirichletsummaskentryinput) + (dst_negative_dirichletsummaskentryinput))) /\ (exists ge_balance_positive_dirichletsummaskentryinputvalue ge_balance_negative_dirichletsummaskentryinputvalue. (((((dm_value_dirichletsummask) = 2 * (ge_balance_positive_dirichletsummaskentryinputvalue) /\ (ge_balance_negative_dirichletsummaskentryinputvalue) = 0) \/ exists ge_signed_half_dirichletsummaskentryinputvaluedecode. (((dm_value_dirichletsummask) = 2 * ge_signed_half_dirichletsummaskentryinputvaluedecode + 1 /\ (ge_balance_positive_dirichletsummaskentryinputvalue) = 0) /\ (ge_balance_negative_dirichletsummaskentryinputvalue) = S ge_signed_half_dirichletsummaskentryinputvaluedecode))) /\ ((dst_positive_dirichletsummaskentryinput) + ge_balance_negative_dirichletsummaskentryinputvalue = (dst_negative_dirichletsummaskentryinput) + ge_balance_positive_dirichletsummaskentryinputvalue))))))))))))) \/ ((((dm_index_dirichletsummask)=0 \/ ~(exists pvs_factor_dirichletsummaskentrynondivisor. (mi_index_dirichlet) = (dm_index_dirichletsummask) * pvs_factor_dirichletsummaskentrynondivisor)) /\ ((dm_value_dirichletsummask)=0))))))) /\ (exists dst_positive_code_dirichletsumfold dst_positive_scale_dirichletsumfold dst_negative_code_dirichletsumfold dst_negative_scale_dirichletsumfold dst_positive_sum_dirichletsumfold dst_negative_sum_dirichletsumfold. (((dm_mask_table_dirichletsum) = (((((dst_positive_code_dirichletsumfold) + (dst_positive_scale_dirichletsumfold)) * S ((dst_positive_code_dirichletsumfold) + (dst_positive_scale_dirichletsumfold)) + ((dst_positive_scale_dirichletsumfold) + (dst_positive_scale_dirichletsumfold))) + (((dst_negative_code_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)) * S ((dst_negative_code_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)) + ((dst_negative_scale_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)))) * S ((((dst_positive_code_dirichletsumfold) + (dst_positive_scale_dirichletsumfold)) * S ((dst_positive_code_dirichletsumfold) + (dst_positive_scale_dirichletsumfold)) + ((dst_positive_scale_dirichletsumfold) + (dst_positive_scale_dirichletsumfold))) + (((dst_negative_code_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)) * S ((dst_negative_code_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)) + ((dst_negative_scale_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)))) + ((((dst_negative_code_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)) * S ((dst_negative_code_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)) + ((dst_negative_scale_dirichletsumfold) + (dst_negative_scale_dirichletsumfold))) + (((dst_negative_code_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)) * S ((dst_negative_code_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)) + ((dst_negative_scale_dirichletsumfold) + (dst_negative_scale_dirichletsumfold)))))) /\ (((exists fs_u_dst_dirichletsumfoldpositive fs_v_dst_dirichletsumfoldpositive. ((((exists fs_h_dst_dirichletsumfoldpositive_body_start. fs_h_dst_dirichletsumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichletsumfoldpositive)) /\ exists fs_q_dst_dirichletsumfoldpositive_body_start. fs_u_dst_dirichletsumfoldpositive = fs_q_dst_dirichletsumfoldpositive_body_start * S ((S (0)) * fs_v_dst_dirichletsumfoldpositive) + (0))) /\ ((((exists fs_h_dst_dirichletsumfoldpositive_body_terminal. fs_h_dst_dirichletsumfoldpositive_body_terminal + S (dst_positive_sum_dirichletsumfold) = S ((S (S (mi_index_dirichlet))) * fs_v_dst_dirichletsumfoldpositive)) /\ exists fs_q_dst_dirichletsumfoldpositive_body_terminal. fs_u_dst_dirichletsumfoldpositive = fs_q_dst_dirichletsumfoldpositive_body_terminal * S ((S (S (mi_index_dirichlet))) * fs_v_dst_dirichletsumfoldpositive) + (dst_positive_sum_dirichletsumfold))) /\ forall fs_i_dst_dirichletsumfoldpositive_body_steps. (exists fs_lt_dst_dirichletsumfoldpositive_body_steps_bound. fs_lt_dst_dirichletsumfoldpositive_body_steps_bound + S fs_i_dst_dirichletsumfoldpositive_body_steps = S (mi_index_dirichlet)) -> exists fs_a_dst_dirichletsumfoldpositive_body_steps fs_r_dst_dirichletsumfoldpositive_body_steps fs_s_dst_dirichletsumfoldpositive_body_steps. ((((exists fs_h_dst_dirichletsumfoldpositive_body_steps_summand. fs_h_dst_dirichletsumfoldpositive_body_steps_summand + S (fs_a_dst_dirichletsumfoldpositive_body_steps) = S ((S (fs_i_dst_dirichletsumfoldpositive_body_steps)) * dst_positive_scale_dirichletsumfold)) /\ exists fs_q_dst_dirichletsumfoldpositive_body_steps_summand. dst_positive_code_dirichletsumfold = fs_q_dst_dirichletsumfoldpositive_body_steps_summand * S ((S (fs_i_dst_dirichletsumfoldpositive_body_steps)) * dst_positive_scale_dirichletsumfold) + (fs_a_dst_dirichletsumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichletsumfoldpositive_body_steps_partial. fs_h_dst_dirichletsumfoldpositive_body_steps_partial + S (fs_r_dst_dirichletsumfoldpositive_body_steps) = S ((S (fs_i_dst_dirichletsumfoldpositive_body_steps)) * fs_v_dst_dirichletsumfoldpositive)) /\ exists fs_q_dst_dirichletsumfoldpositive_body_steps_partial. fs_u_dst_dirichletsumfoldpositive = fs_q_dst_dirichletsumfoldpositive_body_steps_partial * S ((S (fs_i_dst_dirichletsumfoldpositive_body_steps)) * fs_v_dst_dirichletsumfoldpositive) + (fs_r_dst_dirichletsumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichletsumfoldpositive_body_steps_successor. fs_h_dst_dirichletsumfoldpositive_body_steps_successor + S (fs_s_dst_dirichletsumfoldpositive_body_steps) = S ((S (S fs_i_dst_dirichletsumfoldpositive_body_steps)) * fs_v_dst_dirichletsumfoldpositive)) /\ exists fs_q_dst_dirichletsumfoldpositive_body_steps_successor. fs_u_dst_dirichletsumfoldpositive = fs_q_dst_dirichletsumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_dirichletsumfoldpositive_body_steps)) * fs_v_dst_dirichletsumfoldpositive) + (fs_s_dst_dirichletsumfoldpositive_body_steps))) /\ fs_s_dst_dirichletsumfoldpositive_body_steps = fs_r_dst_dirichletsumfoldpositive_body_steps + fs_a_dst_dirichletsumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_dirichletsumfoldnegative fs_v_dst_dirichletsumfoldnegative. ((((exists fs_h_dst_dirichletsumfoldnegative_body_start. fs_h_dst_dirichletsumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichletsumfoldnegative)) /\ exists fs_q_dst_dirichletsumfoldnegative_body_start. fs_u_dst_dirichletsumfoldnegative = fs_q_dst_dirichletsumfoldnegative_body_start * S ((S (0)) * fs_v_dst_dirichletsumfoldnegative) + (0))) /\ ((((exists fs_h_dst_dirichletsumfoldnegative_body_terminal. fs_h_dst_dirichletsumfoldnegative_body_terminal + S (dst_negative_sum_dirichletsumfold) = S ((S (S (mi_index_dirichlet))) * fs_v_dst_dirichletsumfoldnegative)) /\ exists fs_q_dst_dirichletsumfoldnegative_body_terminal. fs_u_dst_dirichletsumfoldnegative = fs_q_dst_dirichletsumfoldnegative_body_terminal * S ((S (S (mi_index_dirichlet))) * fs_v_dst_dirichletsumfoldnegative) + (dst_negative_sum_dirichletsumfold))) /\ forall fs_i_dst_dirichletsumfoldnegative_body_steps. (exists fs_lt_dst_dirichletsumfoldnegative_body_steps_bound. fs_lt_dst_dirichletsumfoldnegative_body_steps_bound + S fs_i_dst_dirichletsumfoldnegative_body_steps = S (mi_index_dirichlet)) -> exists fs_a_dst_dirichletsumfoldnegative_body_steps fs_r_dst_dirichletsumfoldnegative_body_steps fs_s_dst_dirichletsumfoldnegative_body_steps. ((((exists fs_h_dst_dirichletsumfoldnegative_body_steps_summand. fs_h_dst_dirichletsumfoldnegative_body_steps_summand + S (fs_a_dst_dirichletsumfoldnegative_body_steps) = S ((S (fs_i_dst_dirichletsumfoldnegative_body_steps)) * dst_negative_scale_dirichletsumfold)) /\ exists fs_q_dst_dirichletsumfoldnegative_body_steps_summand. dst_negative_code_dirichletsumfold = fs_q_dst_dirichletsumfoldnegative_body_steps_summand * S ((S (fs_i_dst_dirichletsumfoldnegative_body_steps)) * dst_negative_scale_dirichletsumfold) + (fs_a_dst_dirichletsumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichletsumfoldnegative_body_steps_partial. fs_h_dst_dirichletsumfoldnegative_body_steps_partial + S (fs_r_dst_dirichletsumfoldnegative_body_steps) = S ((S (fs_i_dst_dirichletsumfoldnegative_body_steps)) * fs_v_dst_dirichletsumfoldnegative)) /\ exists fs_q_dst_dirichletsumfoldnegative_body_steps_partial. fs_u_dst_dirichletsumfoldnegative = fs_q_dst_dirichletsumfoldnegative_body_steps_partial * S ((S (fs_i_dst_dirichletsumfoldnegative_body_steps)) * fs_v_dst_dirichletsumfoldnegative) + (fs_r_dst_dirichletsumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichletsumfoldnegative_body_steps_successor. fs_h_dst_dirichletsumfoldnegative_body_steps_successor + S (fs_s_dst_dirichletsumfoldnegative_body_steps) = S ((S (S fs_i_dst_dirichletsumfoldnegative_body_steps)) * fs_v_dst_dirichletsumfoldnegative)) /\ exists fs_q_dst_dirichletsumfoldnegative_body_steps_successor. fs_u_dst_dirichletsumfoldnegative = fs_q_dst_dirichletsumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_dirichletsumfoldnegative_body_steps)) * fs_v_dst_dirichletsumfoldnegative) + (fs_s_dst_dirichletsumfoldnegative_body_steps))) /\ fs_s_dst_dirichletsumfoldnegative_body_steps = fs_r_dst_dirichletsumfoldnegative_body_steps + fs_a_dst_dirichletsumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_dirichletsumfoldresult ge_balance_negative_dirichletsumfoldresult. (((((mi_value_dirichlet) = 2 * (ge_balance_positive_dirichletsumfoldresult) /\ (ge_balance_negative_dirichletsumfoldresult) = 0) \/ exists ge_signed_half_dirichletsumfoldresultdecode. (((mi_value_dirichlet) = 2 * ge_signed_half_dirichletsumfoldresultdecode + 1 /\ (ge_balance_positive_dirichletsumfoldresult) = 0) /\ (ge_balance_negative_dirichletsumfoldresult) = S ge_signed_half_dirichletsumfoldresultdecode))) /\ ((dst_positive_sum_dirichletsumfold) + ge_balance_negative_dirichletsumfoldresult = (dst_negative_sum_dirichletsumfold) + ge_balance_positive_dirichletsumfoldresult)))))))))))))

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