[proofplan] We construct a register machine computing $t_{M,k}(w, v)$ that iterates over all words $u \in \mathbb{W}$ with shortlex index strictly less than $\#v$ — equivalently, all $u$ with $\#u < \#v$ — and, for each such $u$, queries the configuration function $h$ of [Computability of the Configuration Function](/theorems/1818) to obtain $\operatorname{code}(C(M, w, \#u))$. For each queried configuration, we extract its state field and compare it to $\operatorname{code}(q_H)$; if any comparison succeeds, $M$ has halted before time $\#v$ on input $w$ and we output $a$; if no comparison succeeds after all $u < v$ (in shortlex order) have been examined, we output $\varepsilon$. The enumeration uses the shortlex successor $s$ from [Shortlex Order and Computable Successor](/theorems/1815). The loop runs for exactly $\#v$ iterations, each iteration doing a bounded amount of work (one call to the computable $h$, one word-equality test, one successor call), so the total computation is finite. Because $M$ and $k$ are fixed parameters of the function $t_{M,k}$ (not arguments), their encodings $\operatorname{code}(M)$ and the arity $k$ are hard-wired as literal constants into the register machine, eliminating the need to parse $M$ at runtime. [/proofplan]

[step:Fix notation, parameters, and the specification of $t_{M,k}$] The function under study is \begin{align*} t_{M, k} : \mathbb{W}^{k+1} &\to \mathbb{W}, \\ (w, v) &\mapsto \begin{cases} a & \text{if there exists } n \in \mathbb{N} \text{ with } n < \#v \text{ and } C(M, w, n) \text{ is in state } q_H, \\ \varepsilon & \text{otherwise}, \end{cases} \end{align*} where $M$ is a fixed register machine of arity $k$, $q_H$ is $M$'s halt state, $C(M, w, n)$ denotes the configuration after $n$ instruction steps (with the convention that once $M$ halts, further steps leave the configuration unchanged — see Step 1 of the proof of [Computability of the Configuration Function](/theorems/1818)), and $a \in \Sigma$ is a fixed distinguished "accept" letter. The shortlex index $\#v$ is the order isomorphism of [Shortlex Order and Computable Successor](/theorems/1815). Because $M$ and $k$ are *parameters* (not arguments of the function), the register machine we construct will depend on $M$ and $k$, but within that machine the encoding $\operatorname{code}(M)$ and the arity $k$ are literal constants baked into the program at construction time. This is the standard distinction: the course's $t_{M,k}$ is one computable function per pair $(M, k)$, not a uniformly computable family indexed by $(M, k)$. Note further that because $M$ is fixed, so is its halt state $q_H$, and in particular $\operatorname{code}(q_H)$ is a fixed finite word known at construction time. [/step]

[step:Describe the algorithm] Since $M$ and $k$ are fixed, we use the configuration function \begin{align*} h_M : \mathbb{W}^k \times \mathbb{W} &\to \mathbb{W}, \\ (w, u) &\mapsto \operatorname{code}(C(M, w, \#u)) \end{align*} which is a *partial* function in the formulation of [Computability of the Configuration Function](/theorems/1818), but here — because $\operatorname{code}(M)$ and $k$ are hard-wired — we can suppress the encoding checks on the first two arguments: the machine computing $h$ from [Computability of the Configuration Function](/theorems/1818) only diverged on ill-formed encodings of the first two arguments; when those arguments are always valid (as they are here, because $\operatorname{code}(M)$ is hard-wired and $w$ is a valid $k$-tuple by assumption), $h$ is effectively a total function of $(w, u)$ and halts in bounded time (bounded by the time $M_h$ needs to simulate $\#u$ steps of $M$). Recall also from Step 1 of the proof of [Computability of the Configuration Function](/theorems/1818) that $\#u$ in this formulation equals $|u|$ under the course's convention; so "$n < \#v$" means "$n < |v|$" under that convention. The existence clause "$\exists n \in \mathbb{N}$ with $n < \#v$ and $C(M, w, n)$ in state $q_H$" is equivalent to "$\exists u \in \mathbb{W}$ with $\#u < \#v$ and the state-field of $h_M(w, u)$ equals $\operatorname{code}(q_H)$". *Algorithm.* On input $(w, v)$, initialise $u := \varepsilon$. Loop: (i) *Termination test for the loop:* compare $u$ to $v$ using the shortlex comparison machine $M_<$ of [Shortlex Order and Computable Successor](/theorems/1815). If $u \not< v$ (i.e. $u \ge v$, meaning $\#u \ge \#v$), exit the loop and output $\varepsilon$. (ii) *Query the configuration at step $\#u$:* compute $c := h_M(w, u)$ using the (fixed-$M$) configuration machine. (iii) *Halt-test:* extract the state field of $c$ (the prefix before the first $|$) and compare it to the literal constant $\operatorname{code}(q_H)$ using a word-equality test. If equal, exit the loop and output $a$. (iv) *Advance:* replace $u$ by $s(u)$ using the successor machine $M_s$ of [Shortlex Order and Computable Successor](/theorems/1815), and return to (i). [/step]

[step:Implement each subroutine and assemble the machine] We detail the register-machine realisation of the algorithm. *Register layout.* Input registers $0, \ldots, k-1$ hold $w_1, \ldots, w_k$; register $k$ holds $v$. Fresh scratch registers: - $R_0, \ldots, R_{k-1}$: master copies of $w$, preserved across loop iterations. - $R_v$: master copy of $v$. - $R_u$: the loop counter $u$. - $R_c$: the current configuration code $c$. - $R_\text{st}$: scratch for the extracted state field. - $R_{\text{out}}$: output staging (written to register $0$ at the end). *Phase 0: initialisation.* - Copy $w_1, \ldots, w_k$ into $R_0, \ldots, R_{k-1}$, and copy $v$ into $R_v$ (these master copies will be restored before each subroutine call that destructively reads its input registers). - Erase $R_u$ (set $u := \varepsilon$). *Phase 1: the main loop body.* (1a) *Compare $u$ to $v$.* Copy $R_u$ into input register $0$ of the shortlex-comparison machine $M_<$ (renamed to avoid register clashes), copy $R_v$ into input register $1$, and run $M_<$. By [Shortlex Order and Computable Successor](/theorems/1815), $M_<$ halts in finite time with output register $0$ holding $a$ iff $u < v$, and $\varepsilon$ otherwise. Read the output: if it is $\varepsilon$, branch to Phase 3 with output $\varepsilon$; if it is $a$, continue. (1b) *Compute $c := h_M(w, u)$.* By [Computability of the Configuration Function](/theorems/1818), there is a register machine $M_h$ that computes $h$ on input $(\operatorname{code}(M), \operatorname{code}(w), u)$. We specialise it to fixed $M$: the first input is always the literal $\operatorname{code}(M)$ (a hard-wired finite word), and the second input is $\operatorname{code}(w) = \sharp w_1 \sharp w_2 \sharp \cdots \sharp w_k \sharp$ built at runtime from $R_0, \ldots, R_{k-1}$ via a fixed sequence of "write $\sharp$" and "copy from $R_i$" instructions (the sequence is finite because $k$ is the fixed arity). The third input is $u$ from $R_u$. Concretely, restore the three input registers of $M_h$: write $\operatorname{code}(M)$ as a literal into input register $0$ of $M_h$ (a finite sequence of "write letter" instructions, one per letter of $\operatorname{code}(M)$); assemble $\operatorname{code}(w)$ into input register $1$ of $M_h$ as above; copy $R_u$ into input register $2$ of $M_h$. Run $M_h$. It halts in finite time (its divergent branches are triggered only by ill-formed inputs, and our inputs are well-formed by construction). Copy its output into $R_c$. (1c) *Extract the state field of $c$.* The encoding is $\operatorname{code}(C) = \operatorname{code}(q) \cdot | \cdot \sharp r_0 \sharp \cdots \sharp r_{N-1} \sharp$. Scan $R_c$ from the left (using the reversal trick to read left-to-right as in the proof of [Regular Languages are Computable](/theorems/1814)), copying letters one at a time into $R_\text{st}$ until the separator $|$ is read; discard the $|$ and do not copy any further letters. The register $R_\text{st}$ now holds $\operatorname{code}(q)$ where $q$ is the current state of $C = C(M, w, \#u)$. (1d) *Compare $\operatorname{code}(q)$ to $\operatorname{code}(q_H)$.* Since $\operatorname{code}(q_H)$ is a fixed finite word known at construction time (because $M$ is fixed), word-equality with $\operatorname{code}(q_H)$ is a finite regular-language test: the test is equivalent to "$\operatorname{code}(q)$ belongs to the singleton language $\{\operatorname{code}(q_H)\}$", which is regular. By [Regular Languages are Computable](/theorems/1814), word-equality with a fixed word is computable; a direct letter-by-letter comparison machine also works (read letters of $R_\text{st}$ and compare with the hard-wired literal sequence from $\operatorname{code}(q_H)$, branching on any mismatch or on a length mismatch). The test yields: if $\operatorname{code}(q) = \operatorname{code}(q_H)$, branch to Phase 2 with output $a$; otherwise, continue. (1e) *Advance $u := s(u)$.* Copy $R_u$ into the input register of the successor machine $M_s$ of [Shortlex Order and Computable Successor](/theorems/1815), run $M_s$, copy its output back into $R_u$. By the cited theorem, $s(u)$ is the shortlex-successor of $u$, and $\#s(u) = \#u + 1$. Return to step (1a). *Phase 2: emit $a$.* Erase register $0$, write $a$ to register $0$, halt. *Phase 3: emit $\varepsilon$.* Erase register $0$, halt. [claim:The loop terminates after exactly $\min(\#v, \#v^\star)$ iterations, where $\#v^\star$ is the least $n$ with $C(M, w, n)$ in state $q_H$ (or $+\infty$ if no such $n$ exists within $\#v$ steps), and the output is $a$ iff such an $n$ exists] Let us track the value of $u$ across iterations. Initially $u = \varepsilon$ and $\#u = 0$. After $t$ successful completions of step (1e) without early exit, $u = s^t(\varepsilon)$ and $\#u = t$, by $t$-fold application of $\#s = \# + 1$. At each iteration the loop either (A) exits through (1a) when $\#u \ge \#v$, or (B) exits through (1d) when the state of $C(M, w, \#u)$ is $q_H$, or (C) continues. - If there is no $n < \#v$ with $C(M, w, n)$ in state $q_H$, then (B) never triggers. The loop runs iterations $t = 0, 1, 2, \ldots$ with $\#u = t$ at the start of each. Iteration $t = \#v$ has $\#u = \#v$, so (1a) fires and the loop exits via (A) with output $\varepsilon$. The output matches the specification. - If there is some $n < \#v$ with $C(M, w, n)$ in state $q_H$, let $n^\star$ be the least such. At iteration $t = n^\star$, $\#u = n^\star < \#v$, so (1a) continues; (1b) computes $c = \operatorname{code}(C(M, w, n^\star))$, whose state field is $\operatorname{code}(q_H)$ (by the choice of $n^\star$); (1d) triggers the $a$ branch, and the output is $a$. The output matches the specification. In either case the loop runs at most $\#v$ iterations, each iteration consists of a bounded number of subroutine calls (each halting in finite time because the called machines $M_<$, $M_h$, $M_s$ always halt on their valid inputs), so the total number of steps is finite. The machine halts on every input. [/claim] [/step]

[step:Conclude] By Step 3, the machine constructed above halts on every input $(w, v) \in \mathbb{W}^{k+1}$ and outputs $t_{M, k}(w, v)$ in register $0$. Hence $t_{M, k}$ is a computable total function. [/step]