 Using this definition, it is possible to λ-define functions over the positive integers. A function F of one positive integer is λ-definable if we can find a λ-formula F, such that if \(F(m) = n\) and m and n are λ-formulas standing for the integers m and n, then the λ-formula \(\{\mathbf{F}\} (\mathbf{m})\) can be converted to n by applying the conversion rules of λ-calculus. Thus, for example, the successor function S, first introduced by Church, can be λ-defined as follows: 