Theorem: Function Obtained by Substitution from URM Computable Functions

Let the functions $f: \N^t \to \N, g_1: \N^k \to \N, g_2: \N^k \to \N, \ldots, g_t: \N^k \to \N$ all be URM computable functions.
Let $h: \N^k \to \N$ be defined from $f, g_1, g_2, \ldots, g_t$ by substitution.
Then $h$ is also URM computable.

Proof:
From the definition:
:$\map h {n_1, n_2, \ldots, n_k} = \map f {\map {g_1} {n_1, n_2, \ldots, n_k}, \map {g_2} {n_1, n_2, \ldots, n_k}, \ldots, \map {g_t} {n_1, n_2, \ldots, n_k} }$
Let $P, Q_1, Q_2, \ldots, Q_t$ be normalized URM programs which compute $f, g_1, g_2, \ldots, g_t$ respectively.
Let $\map u = \max \set {\map \rho P, \map \rho {Q_1}, \map \rho {Q_2}, \ldots, \map \rho {Q_t} }$.
Let $s_j = \map \lambda {Q_j}$ be the number of basic instructions in $Q_j$ for $1 \le j \le t$.
Hence:
:registers $R_{u + 1}, R_{u + 2}, \ldots, R_{u + k}$ can be used to hold a copy of the input $\tuple {n_1, n_2, \ldots, n_k}$ so it can be guaranteed not to be accidentally overwritten by any operations performed by any of $P, Q_1, Q_2, \ldots, Q_t$
:registers $R_{u + k + 1}, R_{u + k + 2}, \ldots, R_{u + k + t}$ can be used to hold copies of the outputs of each of $Q_1, Q_2, \ldots, Q_t$ so they also can be guaranteed not to be accidentally overwritten by any operations performed by any of $P, Q_1, Q_2, \ldots, Q_t$.
The following algorithm can be followed to create a URM program $H$ to compute $h$.
It is assumed that:
:the input is in $R_1, R_2, \ldots, R_k$
:each of $P, Q_1, Q_2, \ldots, Q_t$ are written so as to start at line $1$.
{| border="1"
|-
! align="right" | Step !!
! align="left" | Process
! align="left" | Notes
|-
| align="right" | $1$ ||
| align="left" | Append a Block Copy Program $\map C {1, u + 1, k}$ to $H$<ref>$H$, at this point, is a null URM program. After this step $\map \lambda H = k$.</ref>.
| This stores the input somewhere safe so it can be accessed again later.
|-
| align="right" | $2$ ||
| align="left" | Set $i = 1$.
| This counts how many times we iterate through the following loop.
|-
| align="right" | $3$ ||
| align="left" | Calculate $l = \map \lambda H$.
| This is the length of $H$ so far.
|-
| align="right" | $4$ ||
| align="left" | Append a Block Copy Program $\map C {u + 1, 1, k}$ to $H$.
| This restores the input that we saved in step $1$ so it will be ready for program $Q_i$<ref>The first time through $H$, this step is technically unneeded, as $R_1, R_2, \ldots, R_k$ already contains the input. However, performing this step in ''all'' cases keeps the algorithm simpler and more modular. It's a programmer thing.</ref>.
|-
| align="right" | $5$ ||
| align="left" | Increment the <tt>Jump</tt>s in $Q_i$ by $l$ lines<ref>To '''increment the <tt>Jump</tt>s by $r$''' for any normalized URM program is done by changing all <tt>Jump</tt>s of the form $\map J {m, n, q}$ to $\map J {m, n, q + r}$.</ref>. Call this amended version $Q_i'$.
| As $Q_i$ was written so as to start from line 1, we need to move all the <tt>Jump</tt>s so as to point to the same lines relative to the start of $Q_i'$.
|-
| align="right" | $6$ ||
| align="left" | Append $Q_i'$ to $H$.
| So $\map \lambda H$ increases by $s_i$.
|-
| align="right" | $7$ ||
| align="left" | Append the command $\map C {1, u + k + i}$ to $H$.
| This stores the output of $Q_i'$ in a safe place where it won't get overwritten by something else.
|-
| align="right" | $8$ ||
| align="left" | Add $1$ to $i$.
| 
|-
| align="right" | $9$ ||
| align="left" | Is $i \le t$? If so, go to step $3$. Otherwise, continue to the next step.
|
|-
| align="right" | $10$ ||
| align="left" | Append the Block Copy Program $\map C {u + k + 1, 1, t}$ to $H$.
| This copies the outputs of $Q_1, Q_2, \ldots, Q_t$ back into $R_1, R_2, \ldots, R_t$ ready to be the input to program $P$.
|-
| align="right" | $11$ ||
| align="left" | Calculate $l = \map \lambda H$.
| This is the length of $H$ so far.
|-
| align="right" | $12$ ||
| align="left" | Increment the <tt>Jump</tt>s in $P$ by $l$ lines. Call this amended version $P'$.
|
|-
| align="right" | $13$ ||
| align="left" | Append $P'$ to $H$.
| At this point, $\ds \map \lambda H = k + \sum_{j \mathop = 1}^t \paren {k + s_j + 1} + t + \map \lambda P$.
|}
It can easily be determined that $H$ computes $h$.
Hence $h$ is URM computable.
{{qed}}