 Of course, it is not necessary to define various numerical functions by simulating their recursive definitions. As we saw above in the case of the first representation of numbers, we might just happen to have the right terms such as \(\textsf{BS}(\textsf{BB})\) and \(\textsf{B}\), that behave as the target functions do on numbers. That is, an equally good way to define arithmetic functions is to simply list some terms and then show that they behave as expected. However, once it has been shown that the basic primitive recursive functions together with recursion and minimization can be emulated in CL, we have got not only a nice collection of arithmetic functions in the form of combinators to work with, but also a proof that combinatory logic is sufficiently expressive to formalize all partial recursive functions. Indeed, the remaining steps of such a proof can be carried out in CL, though the details are beyond the scope of this entry.