####
On Normalisation

F. van Raamsdonk and P. Severi

CWI technical report CS-R9545

Abstract:
Using a characterisation of strongly normalising $\lambda$-terms, we give new and simple proofs of the following:
all developments and superdevelopments are finite,
a certain rewrite strategy is perpetual,
a certain rewrite strategy is maximal and thus perpetual,
simply typed $\lambda$-calculus is strongly normalising.