The set $F_{n}$ of primitive recursive function symbols of arity $n$ can be defined inductively as:
\begin{align} & Z, \text{Succ} \in F_{1} & \\ &\pi_{j}^{n} \in F_{n} \quad \text{for each} \quad j=1,\dots, n \\ &\text{If} \quad f \in F_{n} \quad \text{and} \quad g_{1},\dots, g_{n} \in F_{m}, \text{then} \circ_{n}^{m}[f,g_{1},\dots,g_{n}]\in F_{m} & \\ &\text{If} \quad f \in F_{n+2} \quad \text{and} \quad g \in F_{n}, \text{then} \quad \text{Rec}^{n}[f,g]\in F_{n+1} & \end{align}
$A$ is defined to be the smallest set such that:
- $0 \in A$
- If $x \in A$ then $S(x)\in A$
- If $x_{1},\dots,x_{n} \in A$, $n\geq 1$ and $f \in F_{n}$ then $f(x_{1},\dots,x_{n}) \in A$.
The interpretation is then considered a function $f \in F_{n}, [[f]]\mathbb{N}^{n} \to \mathbb{N}$ such that: \begin{array}[lr] [[Z]](k)&=& 0 \\ [[\text{Succ}]](k) &= &k+1 \\ [[\pi_{j}^{n}]](k_{1},\dots,k_{n}) &= &k_{j} \\ [[\circ_{n}^{m}[f,g_{1},\dots,g_{n}]]](k_{1},\dots,k_{m}) &= &[[f]]([[g_{1}]](k_{1},\dots,k_{m}),\dots, [[g_{n}]](k_{1},\dots, k_{m})) \\ [[\text{Rec}^{n}[f,g]]](k_{1},\dots,k_{n},0) &= & [[g]](k_{1},\dots,k_{n}) \\ [[\text{Rec}^{n}[f,g]]](k_{1},\dots,k_{n},m+1) &= & [[f]](k_{1},\dots,k_{n},m,[[\text{Rec}^{n}[f,g]]](k_{1},\dots,k_{n},m) \end{array} The terms in $A$ are defined as:
- $[[0]]=0$
- $S[[t]]=[[t]]+1$
- $[[f(t_{1},\dots,t_{n})]]=[[f]]([[t_{1}]],\dots,[[t_{n}]])$
Finally, the computational relation $\leadsto$ is inductively defined: \begin{equation} \frac{c \in C}{c \leadsto c}(a) \quad \frac{x \in A}{Z(x) \leadsto 0} (b) \quad \frac{x \in A}{\text{Succ}(x) \leadsto S(x)}(c) \quad \frac{x_{j} \leadsto z}{\pi_{j}^{n}(x_{1},\dots,x_{n}) \leadsto z}(d) \tag{1}\end{equation}
\begin{equation} \frac{f(g_{1}(x_{1},\dots,x_{m}),\dots,g_{n}(x_{1},\dots,x_{m})) \leadsto z}{\circ_{n}^{m}[f,g_{1},\dots,g_{n}](x_{1},\dots,x_{m}) \leadsto z} \tag{2} \end{equation}
\begin{equation} \frac{y \leadsto 0 \quad g(x_{1},\dots,x_{n}) \leadsto z}{\text{Rec}^{n}[f,g](x_{1},\dots,x_{n},y) \leadsto z} \tag{3} \end{equation}
\begin{equation} \frac{y \leadsto S(u) \quad f(x_{1},\dots,x_{n},u,\text{Rec}^{n}[f,g](x_{1},\dots,x_{n},u)) \leadsto z}{\text{Rec}^{n}[f,g](x_{1},\dots,x_{n},y) \leadsto z} \tag{4}\end{equation}
The question now is to show by induction on derivations $s \leadsto t$ that for all terms $s,t \in A$, that if $s \leadsto t$ then $[[s]]=[[t]]$.