We write \(f(c) = \R(c,d,xy.e)\) for the function which is defined by primitive recursion on the natural number \(c\) with base case \(d\) and step function \(xy.e\) (or alternatively \(\lambda xy.e\)) which maps the value \(y\) for the previous number \(x {:} \N\) to the value for \(\s(x)\). Note that \(\R\) is a new variable-binding operator: the variables \(x\) and \(y\) become bound in \(e\).