Normalization without reducibility (Q1840460)

This paper can be added to a long list of proofs for the well-known characterizations of -- strongly, weakly, head and weak head -- normalizing terms in the intersection type discipline. Motivated by the fact that Gallier has proven these characterizations in a uniform and semantical way, the author tries to use a syntactic method to prove them in a uniform way. I wonder whether this proof is correct and hope the wrong statement of Lemma 18 part 1 was a distraction of the author. The bibliography of this paper does not contain references to all original proofs, for instance Pottinger's 1980 paper in the Curry Festschrift is missing [\textit{G. Pottinger}, ``A type assignment for the strongly normalizable lambda terms'', in: J. P. Seldin et al. (eds.), To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism, Academic Press, London etc., 561-578 (1980; Zbl 0469.03006)]. Moreover other papers that prove strong normalization along similar syntactic lines are not mentioned, like van \textit{D. T. van Daalen}'s PhD thesis [The language theory of Automath, Techn. Hoegeschool Eindhoven (1980; Zbl 0422.68045)].