Predecessor function
= Predecessor function
{title2=$\operatorname{pred}$}
The predecessor function on the nonnegative integers is $\operatorname{pred}(0)=0$ and $\operatorname{pred}(n+1)=n$. This is a <primitive recursive function> by primitive recursion from the zero and projection functions.