[proofplan] We construct $g$ as the composition of three computable pieces. First, an *input validation* stage parses $v$ as $\operatorname{code}(M)$ of a register machine with some arity $k$, and $u$ as $\operatorname{code}(w)$ of a $k$-tuple of words; if either parse fails or arities mismatch, the stage enters a divergent loop, which correctly realises the "$\uparrow$" branch of the specification. Second, a *halting-step minimiser* computes the least step count $v_0$ at which $M$ has reached its halt state on input $w$: this uses minimisation applied to the step-test function $f'(v, u, y) = a$ if the state field of the configuration code $h(v, u, y)$ equals $\operatorname{code}(q_H)$ and $\varepsilon$ otherwise — where $h$ is the [configuration function](/theorems/1818). The function $f'$ is computable (it combines the computable $h$ with a fixed word-equality test), minimisation of a computable function is computable by [Recursive Implies Computable](/theorems/1817), and minimisation diverges iff $M$ does not halt on $w$, matching the specification. Third, an *output-extraction* stage calls $h(v, u, v_0)$ to obtain the halting configuration, then extracts the contents of register $0$ (the conventional output register) from its register block. Combined, these three computable pieces yield a computable $g$. [/proofplan]

[step:Fix notation for the software principle's output function] Let $\mathbb{W} = \Sigma^*$ with fixed alphabet $\Sigma$ and fixed separators $\sharp, |$ as in the proof of [Computability of the Configuration Function](/theorems/1818). For a register machine $M$ of arity $k$ and input tuple $w \in \mathbb{W}^k$, write $f_{M, k}(w)$ for the partial function computed by $M$ — i.e., $f_{M, k}(w)$ is the contents of register $0$ at the first moment $M$ reaches state $q_H$ (its halt state) started on inputs $w$ loaded into registers $0, \ldots, k - 1$ and all other registers empty; it is undefined if $M$ never halts on $w$. We want to show that the function \begin{align*} g : \mathbb{W}^2 &\rightharpoonup \mathbb{W}, \\ (v, u) &\mapsto \begin{cases} f_{M, k}(w) & \text{if } v = \operatorname{code}(M) \text{ for a valid } k\text{-ary machine } M \text{ and } u = \operatorname{code}(w) \text{ for } w \in \mathbb{W}^k, \\ \uparrow & \text{otherwise}, \end{cases} \end{align*} is computable. Informally, $g$ is a universal interpreter: given an encoded program $v$ and an encoded input $u$, it runs the program on the input. Let $h : \mathbb{W}^3 \rightharpoonup \mathbb{W}$ be the configuration function of [Computability of the Configuration Function](/theorems/1818): $h(v, u, y) = \operatorname{code}(C(M, w, \#y))$ when $v, u$ encode a valid machine and input tuple, and $h(v, u, y) \uparrow$ otherwise. Here $\#y$ is the course's step-count convention (equal to $|y|$; see Step 2 of the proof of [Computability of the Configuration Function](/theorems/1818)). [/step]

[step:Define the halting-step witness function via minimisation] Define an auxiliary function \begin{align*} f' : \mathbb{W}^3 &\rightharpoonup \mathbb{W}, \\ (v, u, y) &\mapsto \begin{cases} \varepsilon & \text{if } h(v, u, y) \downarrow \text{ and the state field of } h(v, u, y) \text{ equals } \operatorname{code}(q_{H, v}), \\ a & \text{if } h(v, u, y) \downarrow \text{ and the state field of } h(v, u, y) \ne \operatorname{code}(q_{H, v}), \\ \uparrow & \text{if } h(v, u, y) \uparrow, \end{cases} \end{align*} where $q_{H, v}$ is the halt state of the machine encoded by $v$ (and $\operatorname{code}(q_{H, v})$ is readable from $v$). Note: we swapped the roles of $\varepsilon$ and $a$ relative to a naive halting indicator, because our minimisation operator $\mu$ searches for the shortlex-least $y$ with $f'(v, u, y) = \varepsilon$, and we want to minimise over halting steps. [claim:$f'$ is computable] Given computable $h$ (from [Computability of the Configuration Function](/theorems/1818)), we construct a register machine $M_{f'}$ that, on input $(v, u, y)$: (a) Runs $M_h$ on $(v, u, y)$, obtaining configuration code $c$ in a scratch register; if $M_h$ diverges, $M_{f'}$ diverges (matching the "undefined" case). (b) Extracts the state field of $c$ (the prefix before the first $|$) into a scratch register $R_\text{st}$, using the left-to-right scan with separator detection already described in Step 3 of the proof of [Truncated Computation Function](/theorems/1819). (c) Extracts $\operatorname{code}(q_{H, v})$ from $v$ (here $v$ must first be restored from a master copy, having been destructively consumed by $M_h$). Parsing $v$ to locate the halt-state sub-field is a fixed regular operation on $v$: scan for the "halt state" marker in the standard encoding format, and copy the following sub-word into a scratch register $R_\text{halt}$. If parsing $v$ fails, this mirrors the "malformed $v$" failure that $M_h$ would have already triggered in (a) via divergence; but for robustness, if parsing reaches end-of-input without finding the halt-state marker, enter a divergent loop. (d) Compare $R_\text{st}$ to $R_\text{halt}$ letter-by-letter: this is a word-equality test, a computable finite operation as in Step 4 of the proof of [Computability of the Configuration Function](/theorems/1818). If equal, write $\varepsilon$ to register $0$ (erase register $0$) and halt; if not equal, write $a$ to register $0$ and halt. Each step is a bounded sequence of register operations or a finite call to a computable sub-machine. Hence $M_{f'}$ computes $f'$, and $f'$ is computable. [/claim] Define \begin{align*} h' : \mathbb{W}^2 &\rightharpoonup \mathbb{W}, \\ (v, u) &\mapsto (\mu f')(v, u) = \min\{y \in \mathbb{W} : f'(v, u, y) = \varepsilon \text{ and } f'(v, u, y') \downarrow \text{ for all } y' < y\}, \end{align*} where $<$ is the shortlex order and $\min$ is the shortlex-least element (well-defined by the well-orderedness of $(\mathbb{W}, <)$ from [Shortlex Order and Computable Successor](/theorems/1815)). [claim:$h'$ is computable, and $h'(v, u)$ is defined iff $(v, u)$ encodes a valid machine-and-input pair such that the encoded machine halts on the encoded input] Computability: $h'$ is the minimisation $\mu f'$ of the computable function $f'$ (previous claim). By closure of computable functions under minimisation (L3 of [Recursive Implies Computable](/theorems/1817)), $h'$ is computable. Definedness: we analyse when $(\mu f')(v, u)$ is defined. - If $(v, u)$ does not encode a valid machine-and-input pair, then $h(v, u, \varepsilon) \uparrow$, so $f'(v, u, \varepsilon) \uparrow$. The minimisation fails the "defined at all $y' < y$" clause at the very first step $y' = \varepsilon$, so $(\mu f')(v, u) \uparrow$. - If $(v, u) = (\operatorname{code}(M), \operatorname{code}(w))$ with $M$ of arity $k$ and $w \in \mathbb{W}^k$, then by the specification of $h$, $h(v, u, y) \downarrow$ for every $y \in \mathbb{W}$, with $h(v, u, y) = \operatorname{code}(C(M, w, |y|))$. Therefore $f'(v, u, y) \downarrow$ for every $y$, and $f'(v, u, y) = \varepsilon$ iff $C(M, w, |y|)$ is in state $q_H$. So: - If $M$ halts on $w$, let $n^\star$ be the least step count at which $M$ reaches $q_H$ (so $C(M, w, n^\star)$ is in state $q_H$ and $C(M, w, n) \ne q_H$ for $n < n^\star$, where by "the configuration after $n < n^\star$ steps is not in state $q_H$" we mean the running state, not the adopted "stay after halt" convention — but since $n^\star$ is minimal, no earlier $n$ is in state $q_H$ under either interpretation). The set $\{y \in \mathbb{W} : |y| = n^\star\}$ consists of words of length $n^\star$; among these, the shortlex-least is $a_0^{n^\star}$ where $a_0$ is the shortlex-minimum letter. Smaller $y$ (in shortlex order) have $|y| < n^\star$, for which $f'(v, u, y) = a \ne \varepsilon$; the shortlex-least $y$ at which $f' = \varepsilon$ is $a_0^{n^\star}$. Hence $h'(v, u) = a_0^{n^\star}$. - If $M$ does not halt on $w$, then $C(M, w, n)$ is not in state $q_H$ for any $n$, so $f'(v, u, y) = a$ for every $y$. The minimum set is empty, so $(\mu f')(v, u) \uparrow$, i.e. $h'(v, u) \uparrow$. Hence $h'(v, u) \downarrow$ iff $(v, u)$ encodes a valid pair and $M$ halts on $w$; moreover, when defined, $|h'(v, u)|$ equals the first halting step count $n^\star$. [/claim] [/step]

[step:Extract the output from the halting configuration] Define \begin{align*} \text{ext}_0 : \mathbb{W} &\rightharpoonup \mathbb{W}, \\ c &\mapsto \begin{cases} r_0 & \text{if } c = \operatorname{code}(q) \cdot | \cdot \sharp r_0 \sharp r_1 \sharp \cdots \sharp r_{N-1} \sharp \text{ for some } q, r_0, \ldots, r_{N-1}, N, \\ \uparrow & \text{otherwise}, \end{cases} \end{align*} the function that extracts register $0$'s contents from a configuration code. [claim:$\text{ext}_0$ is computable] We construct a register machine $M_\text{ext}$ with input register $0$ holding $c$: (a) Scan $c$ left-to-right (using the reversal trick) until the first $|$ is encountered; discard all preceding letters and the $|$ itself. If end-of-input is reached without encountering $|$, enter a divergent loop (input is malformed, matching $\text{ext}_0(c) \uparrow$). (b) Now we are positioned just after the $|$ in the scan. The next letter should be a $\sharp$ (opening the register block). Read it and verify; if not $\sharp$, diverge (malformed). After consuming this $\sharp$, we are at the start of $r_0$. (c) Copy letters into the output register $0$ (after erasing it) until the next $\sharp$ is encountered; this $\sharp$ terminates $r_0$. Discard the terminating $\sharp$ and halt. If input $c$ is well-formed, steps (a)–(c) correctly extract $r_0$ and place it in register $0$. If $c$ is ill-formed, divergence is achieved by one of the explicit checks. Hence $\text{ext}_0$ is computable. [/claim] [/step]

[step:Assemble $g$ from the computable pieces and conclude] Define \begin{align*} g : \mathbb{W}^2 &\rightharpoonup \mathbb{W}, \\ (v, u) &\mapsto \text{ext}_0(h(v, u, h'(v, u))). \end{align*} We show this matches the specification of the theorem, and that it is computable. *Matching the specification.* Three cases. - If $(v, u)$ does not encode a valid machine-input pair: by Step 2, $h'(v, u) \uparrow$. The composition $\text{ext}_0(h(v, u, h'(v, u)))$ is therefore undefined (the inner call $h'$ diverges), matching the "$\uparrow$" branch of $g$. - If $(v, u) = (\operatorname{code}(M), \operatorname{code}(w))$ with $M$ halting on $w$: by Step 2, $h'(v, u) = y_0$ for some $y_0 \in \mathbb{W}$ with $|y_0| = n^\star$, the first halting step count. Then $h(v, u, y_0) = \operatorname{code}(C(M, w, n^\star))$, the halting configuration code. By the convention defining $f_{M, k}$, $f_{M, k}(w)$ equals the register-$0$ contents of this configuration, which is $\text{ext}_0(\operatorname{code}(C(M, w, n^\star))) = r_0$ at step $n^\star$. Hence $g(v, u) = f_{M, k}(w)$. - If $(v, u) = (\operatorname{code}(M), \operatorname{code}(w))$ with $M$ not halting on $w$: by Step 2, $h'(v, u) \uparrow$, so $g(v, u) \uparrow$, matching $f_{M, k}(w) \uparrow$ (the convention that $M$'s computed function is undefined when $M$ does not halt). In all three cases, $g$ matches the specification. *Computability.* The function $g$ is the composition of three computable functions $h'$, $h$, and $\text{ext}_0$: \begin{align*} g &= \text{ext}_0 \circ (h \circ (\pi_1^2, \pi_2^2, h')), \end{align*} where $\pi_i^2$ are projections $\mathbb{W}^2 \to \mathbb{W}$. Each of $h$ (by [Computability of the Configuration Function](/theorems/1818)), $h'$ (by Step 2), $\text{ext}_0$ (by Step 3), and the projections (basic functions, computable by Step 3 of the proof of [Recursive Implies Computable](/theorems/1817)) is computable. By L1 of the proof of [Recursive Implies Computable](/theorems/1817) (closure of computable functions under composition), $g$ is computable. Equivalently, one can exhibit an explicit register machine computing $g$ by concatenating the machines $M_{h'}$, $M_h$, and $M_\text{ext}$ with master copies of $v$ and $u$ preserved between phases, as in the concatenation construction of the L1 proof. Divergence in $M_{h'}$ propagates to divergence of the composite (because its output is needed as input to the next phase); halting produces the value $y_0 = h'(v, u)$, which is then fed (along with restored $v, u$) into $M_h$, producing $c = h(v, u, y_0)$; which is finally fed into $M_\text{ext}$, producing the desired output. Hence $g$ is computable. [/step]