KroneckerDeltaTable(N,E)

((exists dst_positive_code_dirichlettable dst_positive_scale_dirichlettable dst_negative_code_dirichlettable dst_negative_scale_dirichlettable. ((((E)) = (((((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 du_index_dirichlet du_value_dirichlet. ~(du_index_dirichlet=0) -> (exists pvs_le_gap_dirichletbound. pvs_le_gap_dirichletbound + (du_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. ((((E)) = (((((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 (du_index_dirichlet)) * dst_positive_scale_dirichletentry)) /\ exists ff_q_pvs_dirichletentrypositive. dst_positive_code_dirichletentry = ff_q_pvs_dirichletentrypositive * S ((S (du_index_dirichlet)) * dst_positive_scale_dirichletentry) + (dst_positive_dirichletentry))) /\ (((((exists ff_h_pvs_dirichletentrynegative. ff_h_pvs_dirichletentrynegative + S (dst_negative_dirichletentry) = S ((S (du_index_dirichlet)) * dst_negative_scale_dirichletentry)) /\ exists ff_q_pvs_dirichletentrynegative. dst_negative_code_dirichletentry = ff_q_pvs_dirichletentrynegative * S ((S (du_index_dirichlet)) * dst_negative_scale_dirichletentry) + (dst_negative_dirichletentry))) /\ (exists ge_balance_positive_dirichletentryvalue ge_balance_negative_dirichletentryvalue. (((((du_value_dirichlet) = 2 * (ge_balance_positive_dirichletentryvalue) /\ (ge_balance_negative_dirichletentryvalue) = 0) \/ exists ge_signed_half_dirichletentryvaluedecode. (((du_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))))))))) -> ((((du_index_dirichlet)=1 -> (du_value_dirichlet)=2) /\ (~((du_index_dirichlet)=1) -> (du_value_dirichlet)=0)))))

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