ABSTRACT
We have so far described relations on CL-terms by, first, specifying operations on terms, and then by applying a closure to that operation. For example, we started with B1 , which is defined as the replacement of a redex by its reduct in a term, and then we defined Bw as the reflexive transitive closure of the B1 relation. Such an approach is quite satisfactory, moreover, it turned out to be useful in proving various theorems, in defining combinators for special purposes or in comparing CL-terms to Λ -terms.
