[proofplan] We build the desired machine $M^\star$ by *routing*: run $M$ first to diagnose which case $A_i$ the input belongs to, then branch into a relabelled copy of the appropriate operation machine $M_i$. The routing is implemented at the level of syntax on states: for each $i$, we replace every occurrence of the start state $q_{S,i}$ of $M_i$ by the answer state $q_i$ of $M$. Concretely, when $M$ reaches $q_i$ it becomes simultaneously the "continuation point" for the case-$i$ computation, so control flows directly into the body of $M_i$ without any intermediate dispatch. We assemble the component state sets disjointly except for a single shared halt state $q_H$, which guarantees all branches terminate uniformly. Two invariants are then verified: (a) the first phase of the computation of $M^\star$ coincides with the computation of $M$ (because the instructions of $M$ are preserved on $Q$, and $Q$ is disjoint from the modified components); (b) once $M^\star$ reaches the answer state $q_i$, its subsequent computation coincides with the computation of $M_i$ under the renaming $q_{S,i} \mapsto q_i$, because $P_i^\star$ is obtained from $P_i$ precisely by that renaming. Combining (a) and (b) shows $M^\star$ computes $G$. [/proofplan]

[step:Fix the data and the disjointness conventions] Let $\mathsf{Q}$ be a question with answer partition $A_0, \ldots, A_k$ of the input space $\mathbb{W}^{n+1}$, i.e. pairwise disjoint subsets with $\bigsqcup_{i \le k} A_i = \mathbb{W}^{n+1}$. Let $F_i : \mathbb{W}^{n+1} \rightharpoonup \mathbb{W}^{n+1}$ for $i \le k$ be partial operations. Let $M = (\Sigma, Q, P)$ be a [register machine](/pages/???) with start state $q_S \in Q$, answer states $q_0, \ldots, q_k \in Q$, and halt state $q_H \in Q$, which *answers $\mathsf{Q}$*: for every input $w \in \mathbb{W}^{n+1}$, the computation of $M$ on $w$ reaches state $q_i$ at the first time that $w \in A_i$ (well-defined because the $A_i$ partition the input space), after which $M$ halts by transitioning to $q_H$. For each $i \le k$, let $M_i = (\Sigma, Q_i, P_i)$ be a register machine performing $F_i$, with start state $q_{S,i} \in Q_i$ and halt state $q_{H,i} \in Q_i$. [claim:Without loss of generality the state sets satisfy $Q \cap Q_i = \varnothing$ for each $i \le k$, $Q_i \cap Q_j = \{q_H\}$ for all $i \ne j$ with $q_H = q_{H,i} = q_{H,j}$, and $q_H \notin Q$] Strong equivalence of a register machine is preserved under bijective renaming of its states (the program is transported along the renaming). Choose a countably infinite reservoir of fresh symbols disjoint from $Q$ and from $\bigcup_{i} Q_i$; replace the states of each $Q_i$ by distinct fresh symbols, keeping only the halt state, which we identify across all $Q_i$ with a single common symbol $q_H$, chosen to be distinct from every element of $Q$. The resulting renamed machines are [strongly equivalent](/pages/???) to the originals, hence still perform $F_i$, and satisfy the stated disjointness conditions. [/claim] We henceforth assume these conditions hold. [/step]

[step:Construct the relabelled programs $P_i^\star$] For each $i \le k$, define the *substitution* $\sigma_i : Q_i \to (Q_i \setminus \{q_{S,i}\}) \cup \{q_i\}$ by \begin{align*} \sigma_i(q) &= \begin{cases} q_i & q = q_{S,i}, \\ q & q \in Q_i \setminus \{q_{S,i}\}. \end{cases} \end{align*} This is a bijection onto its image because $q_i \ne q$ for any $q \in Q_i \setminus \{q_{S,i}\}$ (we have $q_i \in Q$ and $Q \cap Q_i = \varnothing$, while $q \in Q_i \setminus \{q_{S,i}\} \subseteq Q_i$, so $q \notin Q$). Extend $\sigma_i$ to instructions by applying it to every state appearing in the instruction. If $\iota$ is an instruction over $(\Sigma, Q_i)$ with successor states $q'_1, \ldots, q'_m$ (which may be: a single $q' \in Q_i$ for write/erase/halt, or a family $(q'_a)_{a \in \Sigma}$ for read), write $\sigma_i(\iota)$ for the instruction with the same shape and same register and letter parameters but with each successor $q'_j$ replaced by $\sigma_i(q'_j)$. This defines a function \begin{align*} \sigma_i : \operatorname{Instr}(\Sigma, Q_i) &\to \operatorname{Instr}(\Sigma, (Q_i \setminus \{q_{S,i}\}) \cup \{q_i\}). \end{align*} Now define \begin{align*} P_i^\star : Q_i \setminus \{q_{S,i}\} \cup \{q_i\} &\to \operatorname{Instr}(\Sigma, (Q_i \setminus \{q_{S,i}\}) \cup \{q_i\}), \\ P_i^\star(q) &:= \sigma_i(P_i(\sigma_i^{-1}(q))). \end{align*} That is, the value of $P_i^\star$ at $q_i$ is the image under $\sigma_i$ of $P_i(q_{S,i})$ — the instruction $M_i$ would execute at its start — and the value at any other $q \in Q_i \setminus \{q_{S,i}\}$ is $\sigma_i(P_i(q))$, the instruction of $M_i$ at $q$ with its successor states renamed by $\sigma_i$. [/step]

[step:Assemble the composite machine $M^\star$] Define the composite state set and program: \begin{align*} Q^\star &:= Q \cup \bigcup_{i \le k} (Q_i \setminus \{q_{S,i}\}), \\ P^\star : Q^\star &\to \operatorname{Instr}(\Sigma, Q^\star), \\ P^\star(q) &:= \begin{cases} P(q) & q \in Q \setminus \{q_0, \ldots, q_k\}, \\ P_i^\star(q_i) & q = q_i \text{ for some } i \le k, \\ P_i^\star(q) & q \in Q_i \setminus \{q_{S,i}\} \text{ for some } i \le k. \end{cases} \end{align*} The three cases are mutually exclusive and exhaustive: the union $Q^\star$ is disjoint by the disjointness conventions (each $Q_i \setminus \{q_{S,i}\}$ is disjoint from $Q$ and from $Q_j \setminus \{q_{S,j}\}$ for $j \ne i$, because distinct $Q_i, Q_j$ share only $q_H$, and $q_H$ is removed from at most one of them — by convention we include $q_H$ in exactly one copy, say via the first index $i$ where it appears, with no consequence for the construction because every $P_i^\star$ agrees on $q_H$). The answer states $q_0, \ldots, q_k$ all lie in $Q$, so the middle case is well-defined. On $q_i$, the prescription $P^\star(q_i) = P_i^\star(q_i) = \sigma_i(P_i(q_{S,i}))$ *replaces* the original $P(q_i)$ — which signalled "answer is $A_i$, halt" — by the first instruction of the case-$i$ operation $M_i$ with its start state renamed to $q_i$. The successor states of $P_i^\star(q_i)$ land in $(Q_i \setminus \{q_{S,i}\}) \cup \{q_i\} \subseteq Q^\star$, so $P^\star(q_i)$ is a valid instruction over $Q^\star$. Define $M^\star := (\Sigma, Q^\star, P^\star)$ with start state $q_S \in Q \subseteq Q^\star$ and halt state $q_H \in Q^\star$ (inherited as the common halt state). [/step]

[step:Verify the diagnosis phase of $M^\star$ coincides with $M$] [claim:For every input $w \in \mathbb{W}^{n+1}$ and every step $t \ge 0$ at which the computation of $M$ on $w$ has not yet reached an answer state $q_i$, the $t$-th configuration of the computation of $M^\star$ on $w$ equals the $t$-th configuration of the computation of $M$ on $w$] By induction on $t$. At $t = 0$, both machines begin in start state $q_S$ with the same input register contents $w$; the configurations coincide. For the inductive step, assume the $t$-th configuration is $(q_t, \rho_t)$ with $q_t \in Q \setminus \{q_0, \ldots, q_k\}$ (no answer state reached yet). By construction $P^\star(q_t) = P(q_t)$, and the instruction's successor states all lie in $Q$ (because they are the successor states prescribed by $P$ in the original machine $M$). The successor states of $P(q_t)$ are states of $M$; because the instruction has not yet signalled an answer, these successors may be any states of $Q$, including possibly some $q_i$. Executing $P^\star(q_t) = P(q_t)$ from configuration $(q_t, \rho_t)$ produces exactly the same next configuration as executing $P(q_t)$ would, because the instruction's effect on the register valuation depends only on the instruction and the current valuation, both of which coincide. Thus the $(t+1)$-th configurations coincide, which completes the induction. [/claim] In particular, there is a first step $T = T(w)$ at which the state component of the configuration is an answer state. Since $M$ answers $\mathsf{Q}$, we have $q_T = q_i$ where $i$ is the unique index with $w \in A_i$ (uniqueness by disjointness of the $A_i$). At this step, the register valuation $\rho_T$ of $M^\star$ equals the register valuation $\rho_T^M$ of $M$ on input $w$ at step $T$; but we have made no hypothesis that $\rho_T = w$. However, the statement of the theorem specifies $M$ as a machine *answering* $\mathsf{Q}$; the standard convention is that such a machine leaves the input registers undisturbed up to reaching the answer state. If this is the convention in effect, then $\rho_T = w$. Otherwise, we amend $M$ beforehand by prepending a copy-and-restore subroutine; this amendment produces a strongly equivalent machine that does not change the answer behaviour, so we may assume $\rho_T = w$ without loss of generality. [/step]

[step:Verify the execution phase of $M^\star$ simulates $M_i$] Fix $w \in A_i$. From step $T = T(w)$ onwards, $M^\star$ is in state $q_i$ with register valuation $w$, and the instructions it executes are prescribed by $P_i^\star$ on the domain $(Q_i \setminus \{q_{S,i}\}) \cup \{q_i\}$. [claim:For every $s \ge 0$ at which $M_i$ has not halted on input $w$, the $(T + s)$-th configuration of $M^\star$ equals the image under $\sigma_i$ of the $s$-th configuration of $M_i$ on input $w$] By induction on $s$. At $s = 0$, the configuration of $M_i$ is $(q_{S,i}, w)$; its image under $\sigma_i$ (applied to the state component only) is $(\sigma_i(q_{S,i}), w) = (q_i, w)$, which matches the configuration of $M^\star$ at step $T$. For the inductive step, suppose the $s$-th configuration of $M_i$ is $(q, \rho)$ and the $(T + s)$-th configuration of $M^\star$ is $(\sigma_i(q), \rho)$. By the definition of $P_i^\star$, $P^\star(\sigma_i(q)) = \sigma_i(P_i(q))$; this instruction has the same shape, register parameters, and letter parameters as $P_i(q)$, and its successor states are the $\sigma_i$-images of those of $P_i(q)$. Executing either instruction from valuation $\rho$ produces the same updated valuation $\rho'$ (because register operations and branching tests depend only on the register contents and the letter parameters, both of which coincide), and moves to a successor state which is the $\sigma_i$-image of the successor state $M_i$ would choose. Thus the $(s+1)$-th configuration of $M_i$ is $(q', \rho')$ and the $(T + s + 1)$-th configuration of $M^\star$ is $(\sigma_i(q'), \rho')$, matching under $\sigma_i$ as required. [/claim] Because $\sigma_i$ fixes every state of $Q_i$ except $q_{S,i}$ (and the start state is never revisited during the computation of $M_i$ after step $0$ — if $M_i$ ever returned to $q_{S,i}$ we could eliminate this by inserting a pass-through state, yielding a strongly equivalent machine; we assume this normalisation), the image under $\sigma_i$ of the computation of $M_i$ is faithful. When $M_i$ halts at some step $s^\star$ with final valuation $F_i(w) \in \mathbb{W}^{n+1}$ (assuming the partial function is defined at $w$), the $(T + s^\star)$-th configuration of $M^\star$ is $(\sigma_i(q_{H,i}), F_i(w)) = (q_H, F_i(w))$, because $\sigma_i(q_{H,i}) = q_{H,i} = q_H$ (the halt state is fixed by $\sigma_i$ since $q_{H,i} \ne q_{S,i}$ and $\sigma_i$ fixes everything else). Hence $M^\star$ halts with final register contents $F_i(w)$, which is $G(w)$. [/step]

[step:Conclude that $M^\star$ performs $G$] Combining the previous two steps: for every $w \in \mathbb{W}^{n+1}$ such that $G(w)$ is defined, let $i$ be the unique index with $w \in A_i$; then $G(w) = F_i(w)$ is defined. The computation of $M^\star$ on $w$ proceeds first as $M$ does (up to step $T$ where it arrives at $q_i$ with register contents $w$), and then as $M_i$ does under the renaming $\sigma_i$ (from step $T$ through step $T + s^\star$ where it halts at $q_H$ with register contents $F_i(w) = G(w)$). If $G(w)$ is undefined (i.e., $F_i(w)$ is undefined), then $M_i$ does not halt on $w$, and the computation of $M^\star$ from step $T$ onwards is the $\sigma_i$-image of the non-halting computation of $M_i$, hence also non-halting. In both cases, $M^\star$ realises $G$. [/step]