On Strong Normalization of Explicit Substitution Calculi (Short Note)

摘要

We present a counterexample to the strong normalization - alsocalled termination - of the underlying calculus of explicitsubstitution of lambda-tau. This problem was open.