 These informal explications did not mention any restrictions on the sort of functions \(x,y,z,f,g,\ldots\) may be. However, the axioms above limit the applicability of the combinators to variables. Intuitively, we would like to say that given any terms, that is, any functions \(M\) and \(N\), \(\textsf{W}MN\) one-step reduces to \(MNN\) (possibly, as a subterm of another term). For example, \(M\) may be \(\textsf{K}\) and \(N\) may be \(yy\), and then \(\textsf{WK}(yy)\triangleright_1\textsf{K}(yy) (yy)\).  The latter term suggests a further one-step reduction, and indeed we might be interested in successive one-step reductions—such as those leading from \(\textsf{WK}(yy)\) to \(yy\). A way to achieve these goals is to formalize (a theory of) CL starting with the standard inequational logic but to omit the anti-symmetry rule and to add certain other axioms and rules.