If $f$ is a total function $\mathbb N^k\to\mathbb N$, and $g$ is a total function $\mathbb N^{k+2}\to\mathbb N$, then we say that $h:\mathbb N^{k+1}\to\mathbb N$ is definable by primitive recursion from $f$ and $g$ if for all $x_1,\dots,x_k\in\mathbb N$ and $y\in\mathbb N$, \begin{align} h(x_1,\d...