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.

Studies of Program Constructs (acm F.3.3), Mathematical Logic (acm F.4.1)
Combinatory logic and lambda-calculus (msc 03B40), Inductive definability (msc 03D70)
CWI
Department of Computer Science [CS]

van Raamsdonk, F, & Severi, P. (1995). On normalisation. Department of Computer Science [CS]. CWI.