[proofplan] We show that any register machine $M$ admits infinitely many strongly equivalent machines by explicit construction: pad the state set with a fresh unreachable state and add a single program line for it. Because computations of a register machine are driven by a *start state* and the program's transition function, and because the transition function's behaviour on visited states is entirely determined by the program lines at those states, adding a line at a never-visited state cannot alter any trajectory. Consequently, for every choice of fresh state $\hat q$ and every choice of program line $\hat p$ for $\hat q$ (there are infinitely many choices of $\hat p$ because the command set allows unbounded target-state or register indices), the padded machine realises the same input-output function and the same step-by-step computation sequence as $M$. The set of machines produced by varying $\hat p$ (and optionally iterating the padding) is infinite, and all are strongly equivalent to $M$. [/proofplan]

[step:Fix the register-machine model and define strong equivalence] A [register machine](/pages/???) is a triple $M = (\Sigma, Q, P)$ where $\Sigma$ is a finite set of registers, $Q$ is a finite set of states, and the *program* $P$ is a function \begin{align*} P : Q &\to \mathsf{Commands}(\Sigma, Q) \end{align*} assigning to each state $q \in Q$ a *command* $P(q)$ drawn from the command set parameterised by $\Sigma$ and $Q$. A typical command has one of the shapes \begin{align*} \mathsf{inc}(r, q') \quad &\text{(increment register $r \in \Sigma$, go to state $q' \in Q$)}, \\ \mathsf{dec}(r, q', q'') \quad &\text{(decrement $r$ if $r > 0$ and go to $q'$; else go to $q''$)}, \\ \mathsf{halt} \quad &\text{(halt)}. \end{align*} The exact command syntax is not important; what matters is that $P(q)$ determines, together with the current register valuation, the *successor state* and the *successor register valuation* — i.e., there is a transition function \begin{align*} \delta_M : Q \times \mathbb{N}^\Sigma &\to (Q \cup \{\mathsf{halted}\}) \times \mathbb{N}^\Sigma \end{align*} defined by $\delta_M(q, \rho) := \text{outcome of executing } P(q) \text{ from valuation } \rho$. A designated *start state* $q_S \in Q$ is fixed. Given an input register valuation $\rho_0 \in \mathbb{N}^\Sigma$, the *computation sequence* of $M$ from $\rho_0$ is the (finite or infinite) sequence of configurations \begin{align*} (q_0, \rho_0), (q_1, \rho_1), (q_2, \rho_2), \dots \quad \text{with } q_0 = q_S \text{ and } (q_{i+1}, \rho_{i+1}) = \delta_M(q_i, \rho_i), \end{align*} terminating the first time the outcome is $\mathsf{halted}$, in which case the final configuration is $(\mathsf{halted}, \rho_{\text{final}})$. A *reached state* of $M$ on input $\rho_0$ is any $q \in Q$ appearing as some $q_i$ in this sequence. Two register machines $M$ and $M'$ over the same register set $\Sigma$ are *strongly equivalent* iff for every input valuation $\rho_0 \in \mathbb{N}^\Sigma$, the computation sequences of $M$ and $M'$ on input $\rho_0$ are identical on their shared state names and, in particular, halt at the same step with the same register valuations. Equivalently, strong equivalence requires the machines to execute the *same number of steps*, pass through a matching sequence of register valuations, and reach an agreement on the halting state's register contents. We adopt this as the working definition. [/step]

[step:Pad $M$ with a fresh state and a chosen program line] Let $\hat{q}$ be a symbol not belonging to $Q$; such symbols exist in unlimited supply (we may take, e.g., $\hat{q} := q_0$ for any symbol $q_0 \notin Q$ from a countably infinite reservoir of names). Define the *padded state set* and the *padded program*: \begin{align*} Q' &:= Q \cup \{\hat{q}\}, \\ P' : Q' &\to \mathsf{Commands}(\Sigma, Q'), & P'(q) &:= \begin{cases} P(q) & q \in Q, \\ \hat{p} & q = \hat{q}, \end{cases} \end{align*} where $\hat{p} \in \mathsf{Commands}(\Sigma, Q')$ is an arbitrarily chosen command. For example, one may take $\hat{p} := \mathsf{halt}$ or $\hat{p} := \mathsf{inc}(r, \hat{q})$ for any register $r$ and the self-loop target $\hat{q}$, etc. Let $M_{\hat{p}} := (\Sigma, Q', P')$, with start state $q_S$ (unchanged). We must verify $M_{\hat{p}}$ is a well-defined register machine: $P'$ is a total function $Q' \to \mathsf{Commands}(\Sigma, Q')$, its finite domain $Q'$ has size $|Q| + 1$, its image lies in the command set over $(\Sigma, Q')$, and $q_S \in Q \subseteq Q'$. These are all explicit by construction. [/step]

[step:Show $\hat{q}$ is never the current state during any computation of $M_{\hat{p}}$] [claim:For every input valuation $\rho_0 \in \mathbb{N}^\Sigma$, the computation sequence of $M_{\hat{p}}$ from $\rho_0$ never enters state $\hat{q}$] We induct on $i \ge 0$ with the invariant: the $i$-th configuration $(q_i, \rho_i)$ of $M_{\hat{p}}$ satisfies $q_i \in Q$ and equals the $i$-th configuration of the computation sequence of $M$ from $\rho_0$. *Base case $i = 0$.* By definition $q_0 = q_S \in Q$, and $\rho_0$ is the input valuation, identical for both machines. Invariant holds. *Inductive step.* Assume the $i$-th configuration $(q_i, \rho_i)$ of $M_{\hat{p}}$ equals the $i$-th configuration of $M$ and $q_i \in Q$. If $M$ halts at step $i$ (i.e., $P(q_i) = \mathsf{halt}$ or the transition issues the $\mathsf{halted}$ outcome), then so does $M_{\hat{p}}$ because $P'(q_i) = P(q_i)$ by construction; the sequences agree on termination at step $i$ and there is no $(i+1)$-th configuration to analyse. Otherwise, both machines proceed; the $(i+1)$-th configurations are \begin{align*} (q_{i+1}^M, \rho_{i+1}^M) &= \delta_M(q_i, \rho_i), & (q_{i+1}^{M_{\hat{p}}}, \rho_{i+1}^{M_{\hat{p}}}) &= \delta_{M_{\hat{p}}}(q_i, \rho_i). \end{align*} Since $q_i \in Q$, we have $P'(q_i) = P(q_i)$, and the command set interpretation of a command depends only on the command and the register valuation, not on the ambient state set $Q$ vs.\ $Q'$. (Concretely: $\mathsf{inc}(r, q')$ yields next state $q'$, which must lie in $Q$ because it was an already-valid target in $M$; $\mathsf{dec}(r, q', q'')$ yields next state $q'$ or $q''$, both in $Q$; $\mathsf{halt}$ issues $\mathsf{halted}$.) Hence both transitions produce the same outcome, so \begin{align*} q_{i+1}^{M_{\hat{p}}} = q_{i+1}^M \in Q, \qquad \rho_{i+1}^{M_{\hat{p}}} = \rho_{i+1}^M. \end{align*} The invariant is preserved. By induction, every $q_i$ in the computation sequence of $M_{\hat{p}}$ from $\rho_0$ lies in $Q$, which is the complement of $\{\hat{q}\}$ in $Q'$. In particular $\hat{q}$ is never the current state. [/claim] A consequence is that the command $\hat{p} = P'(\hat{q})$ is never executed during any computation of $M_{\hat{p}}$, regardless of input. [/step]

[step:Conclude strong equivalence of $M_{\hat{p}}$ and $M$] The same induction established that the computation sequences of $M$ and $M_{\hat{p}}$ agree configuration-by-configuration on every input $\rho_0$ and terminate (or fail to terminate) in lock-step with identical register valuations. This is exactly the definition of strong equivalence. Therefore \begin{align*} M_{\hat{p}} &\text{ is strongly equivalent to } M \quad \text{for every choice of } \hat{p}. \end{align*} [/step]

[step:Produce infinitely many pairwise distinct padded machines] [claim:The set $\{M_{\hat{p}} : \hat{p} \in \mathsf{Commands}(\Sigma, Q')\}$ is infinite] It suffices to exhibit an infinite family of pairwise distinct program lines $\hat{p}$ — i.e., distinct commands over register set $\Sigma$ and state set $Q'$ — because two padded machines $M_{\hat{p}}$ and $M_{\hat{p}'}$ with $\hat{p} \ne \hat{p}'$ differ in the value of their program function at state $\hat{q}$ and hence are distinct as triples $(\Sigma, Q', P')$. The command $\mathsf{inc}(r, q)$ with $r \in \Sigma$ and $q \in Q'$ is parameterised by the target state $q$. Since $Q' \supseteq Q$ is finite, this gives only finitely many choices, which is insufficient. To obtain infinitely many choices, we iterate the padding: pad $M$ first with $\hat{q}_1$ to get $M^{(1)}$, then pad $M^{(1)}$ with $\hat{q}_2$ to get $M^{(2)}$, and so on. The construction of the previous steps applies equally to $M^{(k)}$ as input grammar; by induction on $k$, the $k$-fold padded machine $M^{(k)} = (\Sigma, Q \cup \{\hat{q}_1, \dots, \hat{q}_k\}, P^{(k)})$ is strongly equivalent to $M$ (by transitivity: strong equivalence is reflexive and transitive on register machines over the same register set, since the definition is a pointwise agreement condition on computation sequences). The machines $M^{(k)}$ for $k = 0, 1, 2, \dots$ differ as tuples because their state sets have cardinalities $|Q|, |Q| + 1, |Q| + 2, \dots$, which are pairwise distinct. Hence $\{M^{(k)} : k \ge 0\}$ is an infinite set of pairwise distinct machines, each strongly equivalent to $M$. [/claim] This completes the construction of an infinite strong-equivalence class around $M$, and hence proves the Padding Lemma. [/step]