[proofplan] The strong-equivalence class of a $\Sigma$-register machine is determined by its program viewed up to relabelling of states; so to bound the number of classes we bound the number of programs. We stratify the collection of all $\Sigma$-register machines by two integer parameters: the number of states $n = |Q|$, and a *register-index ceiling* $k$ that bounds every numerical register index appearing in any instruction of the program. For each fixed pair $(n, k)$ the instruction set $\operatorname{Instr}(\Sigma, Q)$ is finite (we count the four instruction shapes explicitly), hence the set of programs $P : Q \to \operatorname{Instr}(\Sigma, Q)$ is finite as well. Every $\Sigma$-register machine arises in some stratum $(n, k)$, so the full collection is a countable union $\bigcup_{n, k \in \mathbb{N}} M_{n,k}$ of finite sets, which is [countable](/pages/???) by the standard union argument. Passing to the quotient by strong equivalence can only decrease cardinality. [/proofplan]

[step:Fix the register-machine model, the instruction set, and strong equivalence] Fix a finite input alphabet $\Sigma$, and let $|\Sigma| \ge 1$. A [$\Sigma$-register machine](/pages/???) is a triple $M = (\Sigma, Q, P)$ where $Q$ is a finite set of states (containing a distinguished *start state* $q_S$ and a distinguished *halt state* $q_H$) and \begin{align*} P : Q &\to \operatorname{Instr}(\Sigma, Q) \end{align*} is the *program*, assigning to each state $q \in Q$ an instruction. An *instruction* takes one of four shapes. Using the convention that a register is addressed by a non-negative integer index and a letter of $\Sigma$ is written into or compared from a register, the four shapes are \begin{align*} &\textbf{write}(a, r) \to q': \text{ write letter } a \in \Sigma \text{ to register } r, \text{ go to state } q' \in Q, \\ &\textbf{read}(r) \to (q'_a)_{a \in \Sigma}: \text{ read register } r, \text{ branch to } q'_a \in Q \text{ on letter } a \in \Sigma, \\ &\textbf{erase}(r) \to q': \text{ erase register } r, \text{ go to state } q' \in Q, \\ &\textbf{halt}(r) \to q': \text{ mark register } r \text{ as halting output, go to state } q' \in Q. \end{align*} (The exact operational semantics is not needed for the counting argument; what matters is the *syntactic* parameterisation of each instruction.) For the write shape, the parameters are a letter $a \in \Sigma$, a register index $r$, and a successor state $q' \in Q$. For the read shape, the parameters are a register index $r$ and a family $(q'_a)_{a \in \Sigma}$ of $|\Sigma|$ successor states indexed by letters. For the erase shape, the parameters are a register index $r$ and a successor $q' \in Q$. For the halt shape, the parameters are a register index $r$ and a successor $q' \in Q$. Two register machines $M = (\Sigma, Q, P)$ and $M' = (\Sigma, Q', P')$ over the same alphabet are [strongly equivalent](/pages/???) if there is a bijection $\varphi : Q \to Q'$ preserving start state and halt state such that, relabelling instructions along $\varphi$, we have $P' = \varphi \circ P \circ \varphi^{-1}$ at every state. Strong equivalence is an equivalence relation, and two machines are strongly equivalent iff they agree as programs up to renaming of states. [/step]

[step:Stratify machines by state count and register-index ceiling] Every register machine $M = (\Sigma, Q, P)$ uses only finitely many register indices, because $Q$ is finite and each instruction $P(q)$ names a single register index $r$. Define the *register-index ceiling* of $M$ to be \begin{align*} k(M) &:= \max_{q \in Q} r(P(q)), \end{align*} where $r(P(q))$ is the register index appearing in $P(q)$; this maximum is taken over a finite set, hence finite. The *state count* is $n(M) := |Q|$. For integers $n \ge 1$ and $k \ge 0$, let \begin{align*} M_{n,k} &:= \{\Sigma\text{-register machines } M : n(M) = n \text{ and } k(M) \le k\} / {\sim_{\text{strong}}}, \end{align*} where $\sim_{\text{strong}}$ is strong equivalence. Every machine has some $(n, k)$ with $M \in M_{n,k}$ (take $n = n(M)$ and $k = k(M)$), so the set of all strong-equivalence classes equals $\bigcup_{n \ge 1, \, k \ge 0} M_{n,k}$. [/step]

[step:Count the instructions with parameters bounded by $(n, k)$]Fix $n \ge 1$ and $k \ge 0$, and fix a representative state set $Q$ with $|Q| = n$. We count \begin{align*} \operatorname{Instr}_{n,k}(\Sigma, Q) &:= \{\text{instructions over } (\Sigma, Q) \text{ with register index in } \{0, 1, \ldots, k\}\}. \end{align*} Each of the four shapes contributes a finite tally: [claim:$|\operatorname{Instr}_{n,k}(\Sigma, Q)| = (k+1) n |\Sigma| + (k+1) n^{|\Sigma|} + (k+1) n + (k+1) n$] - *Write instructions.* A write instruction is specified by a letter $a \in \Sigma$ ($|\Sigma|$ choices), a register index $r \in \{0, 1, \ldots, k\}$ ($k+1$ choices), and a successor state $q' \in Q$ ($n$ choices). These choices are independent, so there are \begin{align*} |\Sigma| \cdot (k+1) \cdot n &= (k+1) n |\Sigma| \end{align*} write instructions. - *Read instructions.* A read instruction is specified by a register index $r \in \{0, 1, \ldots, k\}$ ($k+1$ choices) together with a function $a \mapsto q'_a$ from $\Sigma$ to $Q$. The number of such functions is $|Q|^{|\Sigma|} = n^{|\Sigma|}$, so there are \begin{align*} (k+1) \cdot n^{|\Sigma|} \end{align*} read instructions. - *Erase instructions.* An erase instruction is specified by $r \in \{0, 1, \ldots, k\}$ and $q' \in Q$: $(k+1) \cdot n = (k+1) n$ choices. - *Halt instructions.* Analogously, $(k+1) \cdot n = (k+1) n$ choices. Summing across the four disjoint shapes: \begin{align*} |\operatorname{Instr}_{n,k}(\Sigma, Q)| &= (k+1) n |\Sigma| + (k+1) n^{|\Sigma|} + (k+1) n + (k+1) n. \end{align*} [/claim] Denote this sum by $N_{n,k}$. Because $n$, $k$, and $|\Sigma|$ are all finite, $N_{n,k}$ is a finite natural number.[/step]

[guided]We want to count programs, and a program is a function from the $n$ states into the instruction set. Before counting functions, we must count *instructions*. Each instruction has a fixed *shape* (write, read, erase, halt) plus *parameters*. Why is the count finite once we fix $n$ and $k$? Because every parameter ranges over a finite set: letters range over the finite alphabet $\Sigma$; register indices are restricted to $\{0, 1, \ldots, k\}$ by the ceiling; successor states range over the finite set $Q$ of size $n$; and the read instruction's branching function lives in $Q^\Sigma$, which has cardinality $n^{|\Sigma|}$, finite. Let us verify each contribution explicitly. - **Write:** $(a, r, q')$ with $a \in \Sigma$ ($|\Sigma|$ options), $r \in \{0, \ldots, k\}$ ($k + 1$ options), $q' \in Q$ ($n$ options). By the multiplication principle, the count is $|\Sigma|(k+1)n = (k+1)n|\Sigma|$. - **Read:** $(r, (q'_a)_{a \in \Sigma})$. The first factor has $k + 1$ options; the second is a function $\Sigma \to Q$, and the number of such functions is $|Q|^{|\Sigma|} = n^{|\Sigma|}$. The count is $(k+1) n^{|\Sigma|}$. - **Erase:** $(r, q')$. Count $(k+1) n$. - **Halt:** $(r, q')$. Count $(k+1) n$. Since the four shapes are syntactically distinct (an instruction's shape can be read off its header), they partition $\operatorname{Instr}_{n,k}(\Sigma, Q)$, and the total count is the sum: \begin{align*} N_{n,k} &= (k+1) n |\Sigma| + (k+1) n^{|\Sigma|} + (k+1) n + (k+1) n. \end{align*} This is a sum of four finite natural numbers, hence finite. (Note: the value $n^{|\Sigma|}$ in the read contribution is consistent with the sketch's term $(k+1) n^2$ in the binary-alphabet case $|\Sigma| = 2$; we have written the formula for general $|\Sigma|$.)[/guided]

[step:Count the programs with state count $n$ and register-index ceiling $\le k$] A program is a function $P : Q \to \operatorname{Instr}_{n,k}(\Sigma, Q)$. The number of functions from a set of size $n$ to a set of size $N_{n,k}$ is $N_{n,k}^n$, which is finite because both $N_{n,k}$ and $n$ are finite natural numbers. Up to renaming states (strong equivalence), the representative state set $Q$ with $|Q| = n$ may be fixed once and for all (any two sets of size $n$ are bijective). Therefore \begin{align*} |M_{n,k}| &\le N_{n,k}^n < \infty, \end{align*} i.e. $M_{n,k}$ is finite. [/step]

[step:Conclude by a countable union of finite sets] The collection of all $\Sigma$-register machines up to strong equivalence is \begin{align*} \mathcal{M} &= \bigcup_{n \ge 1} \bigcup_{k \ge 0} M_{n,k}, \end{align*} a union indexed by the countable set $\mathbb{N}_{\ge 1} \times \mathbb{N}_{\ge 0}$. Each summand $M_{n,k}$ is finite by the previous step. A [countable union of finite sets is countable](/theorems/???), so $\mathcal{M}$ is countable. This proves the theorem. [/step]