The s-m-n theorem

Define the functions $s_m^n$ recursively from the binary map of [L1]: $s_0^n(e):=e,$ and $s_{m+1}^n(e,a_1,\dots ,a_{m+1}):=s(s_m^{n+1}(e,a_1,\dots ,a_m),a_{m+1})\mathrm{.}$ Because $s$ is total computable and composition preserves total computability, each $s_m^n$ is total computable.

We prove the defining identity from [L2] by induction on $m$. For $m=0$, step 1.1 gives $s_0^n(e)=e$, so the statement is immediate. Assume it holds for $m$. Then for every input tuple $b_1,\dots ,b_n$, ${\phi }_{s_{m+1}^n(e,a_1,\dots ,a_{m+1})}({\mathrm{Inp}}_n(b_1,\dots ,b_n))$ $\simeq {\phi }_{s_m^{n+1}(e,a_1,\dots ,a_m)}(<mi\; mathvariant="normal">⌜</mi>a_{m+1},{\mathrm{Inp}}_n(b_1,\dots ,b_n){<mi\; mathvariant="normal">⌝</mi>}_{\mathrm{s}\mathrm{e}\mathrm{q}})$ by [L1]. By the definition in [L2], that inner code is exactly ${\mathrm{Inp}}_{n+1}(a_{m+1},b_1,\dots ,b_n)\mathrm{.}$ The induction hypothesis therefore turns the right-hand side into ${\phi }_e({\mathrm{Inp}}_{m+n+1}(a_1,\dots ,a_m,a_{m+1},b_1,\dots ,b_n))\mathrm{.}$ So the required identity also holds for $m+1$.

Therefore for every $m,n$ the recursively defined $s_m^n$ is a parameter-specialization function.