Reducibility Strikes Again, I!

In these notes, we prove some general theorems for establishing properties of untyped λ-terms, using a variant of the reducibility method. These theorems apply to (pure) λ-terms typable in the systems of conjunctive types DΩ and D. As applications, we give simple proofs of the characterizations of the terms having head-normal forms, of the normalizable terms, and of the strongly normalizing terms. We also give a characterization of the terms having weak head-normal forms. This last result appears to be new