Lambda definition of primitive recursion

Using a fixed-point combinator, Church Boolean conditionals, a zero test, and a predecessor term, lambda-definable $g$ and $h$ giveNormal-order beta reduction evaluates only the selected conditional branch, so this term implements primitive recursion on Church numerals.

If total functions $g$ and $h$ are represented by lambda terms $G,H$, defineandAfter $j$ iterations the Church pair holds $(c_j,c_{f(\mathbf{x},j)})$, proved by mathematical induction using the defining recursion equations. Consequently $R$ represents the total primitive recursive function $f$. This statement concerns total inputs and total recursion constituents; it is not an unguarded composition theorem for arbitrary partial functions.