\begin{definition}[Definition:Basic Primitive Recursive Function/Successor Function]
The '''successor function''' $\Succ: \N \to \N$ is a basic primitive recursive function, defined as:
:$\forall n \in \N: \map \Succ n = n + 1$
It is URM computable by a single-instruction URM program.
Category:Definitions/Mathematical Logic
Category:Definitions/Primitive Recursive Functions
\end{definition}