[proofplan] We prove three linked assertions about the shortlex order on $\mathbb{W}$: (i) it is order-isomorphic to $(\mathbb{N}, <)$, (ii) the relation $v < w$ is computable, and (iii) the successor function $s : \mathbb{W} \to \mathbb{W}$ is computable. Part (i) follows from the fact that the *index function* $\#(w) := |\{v \in \mathbb{W} : v < w\}|$ is well-defined and order-preserving, and a careful verification that every natural number is hit (surjectivity), because $\mathbb{W}$ itself is infinite and the initial segment below any $w$ is finite. Part (ii) is proved by explicit register-machine construction: a length-comparison phase reduces the problem to either a positive answer (shorter $<$ longer) or a letter-by-letter dictionary comparison on words of equal length; each comparison uses destructive reads with a queue-shaped accumulator to restore registers as needed. Part (iii) is a combinatorial algorithm on words: find the rightmost non-maximal letter, increment it to the next letter in the alphabet's order, and replace every letter to its right by the minimum letter; if no non-maximal letter exists, the successor jumps to a word of length $|w| + 1$ consisting entirely of the minimum letter. Each of the three machines is assembled from primitive register operations and the [case distinction lemma](/theorems/1812). [/proofplan]

[step:Fix the shortlex order and the index function] Let $\Sigma$ be a finite alphabet with a fixed total order $<_\Sigma$ on its letters; write $a_0 <_\Sigma a_1 <_\Sigma \cdots <_\Sigma a_{m-1}$ for the letters, where $m = |\Sigma| \ge 1$. The *shortlex order* on $\mathbb{W} := \Sigma^*$ is the total order $<$ defined for $v, w \in \mathbb{W}$ by \begin{align*} v < w &\iff |v| < |w|, \text{ or } (|v| = |w| \text{ and } v <_{\text{lex}} w), \end{align*} where $<_{\text{lex}}$ is the lexicographic order: for equal-length words $v = v_1 \cdots v_n$ and $w = w_1 \cdots w_n$, $v <_{\text{lex}} w$ iff there is $i$ with $v_1 = w_1, \ldots, v_{i-1} = w_{i-1}$ and $v_i <_\Sigma w_i$. The shortlex order is a total order on $\mathbb{W}$ (totality: exactly one of the three cases $|v| < |w|$, $|v| > |w|$, or $|v| = |w|$ holds; on equal-length words the lexicographic order is total because $<_\Sigma$ is; transitivity and irreflexivity follow from the same properties for $|\cdot|$ and $<_{\text{lex}}$). Define the *index function* \begin{align*} \# : \mathbb{W} &\to \mathbb{N}, \\ w &\mapsto |\{v \in \mathbb{W} : v < w\}|. \end{align*} [claim:For every $w \in \mathbb{W}$, the set $\{v \in \mathbb{W} : v < w\}$ is finite] Every $v < w$ satisfies either $|v| < |w|$ or ($|v| = |w|$ and $v <_{\text{lex}} w$). In either case $|v| \le |w|$. The set of words of length at most $|w|$ over an alphabet of size $m$ is \begin{align*} \sum_{k = 0}^{|w|} m^k &= \frac{m^{|w| + 1} - 1}{m - 1} \quad (\text{or } |w| + 1 \text{ if } m = 1), \end{align*} which is finite. The initial segment below $w$ is a subset of this finite set and hence finite. [/claim] In particular $\#(w) \in \mathbb{N}$ is well-defined for every $w$. [/step]

[step:Prove $\#$ is a bijection and an order isomorphism from $(\mathbb{W}, <)$ to $(\mathbb{N}, <)$] [claim:$\#$ is strictly order-preserving: if $v < w$ then $\#(v) < \#(w)$] Assume $v < w$. Every $u < v$ satisfies $u < w$ by transitivity of $<$, so $\{u : u < v\} \subseteq \{u : u < w\}$; moreover $v \in \{u : u < w\}$ but $v \notin \{u : u < v\}$ (since $<$ is irreflexive). So the inclusion is strict: \begin{align*} \{u : u < v\} &\subsetneq \{u : u < w\}. \end{align*} Taking cardinalities of finite sets preserves strict inclusion: $\#(v) < \#(w)$. [/claim] [claim:$\#$ is injective] If $v \ne w$ then by totality either $v < w$ or $w < v$; in either case the previous claim gives $\#(v) \ne \#(w)$. [/claim] [claim:$\#$ is surjective, and its image is all of $\mathbb{N}$] We show $\#$ realises all values $0, 1, 2, \ldots$. Observe that for any $w \in \mathbb{W}$, the set $\{v : v < w\}$ is an *initial segment* of $(\mathbb{W}, <)$, i.e. downward-closed: $u < v < w$ implies $u < w$. Conversely every initial segment is of this form, because given a non-empty initial segment $I$ that is not all of $\mathbb{W}$, we may take $w = \min(\mathbb{W} \setminus I)$ (well-defined because $(\mathbb{W}, <)$ is well-ordered — every non-empty subset has a minimum, seen by taking first the minimum length, then the lexicographic minimum at that length), and then $I = \{v : v < w\}$. For any $n \in \mathbb{N}$, consider the set $S_n := \{v \in \mathbb{W} : \#(v) < n\}$, which is an initial segment (because $\#$ is order-preserving, this equals $\{v : v < w\}$ for some specific $w$, which we now identify). More directly: by the strict order preservation of $\#$ proved above, list the elements of $\mathbb{W}$ in increasing shortlex order as $w^{(0)} < w^{(1)} < w^{(2)} < \cdots$, which is possible because $(\mathbb{W}, <)$ is well-ordered with every initial segment finite, so we may iteratively define $w^{(n)} := \min(\mathbb{W} \setminus \{w^{(0)}, \ldots, w^{(n-1)}\})$. This enumeration exhausts $\mathbb{W}$ because $\mathbb{W}$ is countably infinite (it is a countable union of finite sets $\Sigma^k$) and the enumeration is strictly increasing, hence injective, with image an unbounded initial segment; if the image were a proper initial segment of $\mathbb{W}$, then $\mathbb{W}$ would have a minimum element above all $w^{(n)}$, contradicting that initial segments are finite. By induction on $n$, $\#(w^{(n)}) = n$: the base case $\#(w^{(0)}) = 0$ holds because $w^{(0)}$ is the minimum and has no predecessors; for the induction step, if $\#(w^{(n-1)}) = n - 1$, the set $\{v : v < w^{(n)}\}$ equals $\{w^{(0)}, \ldots, w^{(n-1)}\}$, which has exactly $n$ elements. Hence $\#$ is surjective, attaining every value in $\mathbb{N}$. [/claim] Combining injectivity and surjectivity, $\# : \mathbb{W} \to \mathbb{N}$ is a bijection. Combined with strict order preservation, it is an order isomorphism: \begin{align*} \# : (\mathbb{W}, <) &\xrightarrow{\cong} (\mathbb{N}, <). \end{align*} [/step]

[step:Computability of the shortlex order — construct the comparison machine] We construct a register machine $M_<$ with input registers $0$ (for $v$) and $1$ (for $w$), which halts with register $0$ containing $a$ (the fixed "true" marker, e.g. $a = a_0$) if $v < w$ and $\varepsilon$ otherwise. *Register layout.* - Registers $0, 1$ hold $v, w$ respectively. - Registers $2, 3$ are length-counters (initialised to $\varepsilon$). - Registers $4, 5$ are scratch copies of $v, w$ for the lexicographic phase. - Register $6$ is the output accumulator. *Phase 1: compute lengths into unary.* For each input register, we run a sub-machine that destructively reads the register one letter at a time and writes a fixed tally letter (say $a_0$) to the corresponding counter register per letter read, simultaneously writing the read letter onto a scratch register (for restoration). Explicitly: \begin{align*} & (\text{register } 0 = v, \text{ register } 2 = \varepsilon, \text{ register } 4 = \varepsilon) \\ & \longrightarrow (\text{register } 0 = \varepsilon, \text{ register } 2 = a_0^{|v|}, \text{ register } 4 = \text{rev}(v)), \end{align*} using the reversal-with-tally technique established in [Regular Languages are Computable](/theorems/1814): a loop that reads the last letter of register $0$, appends it to register $4$, and appends $a_0$ to register $2$. When register $0$ is empty, exit the loop. Repeat analogously for $w$: $(\text{register } 1, \text{register } 3, \text{register } 5) : (w, \varepsilon, \varepsilon) \to (\varepsilon, a_0^{|w|}, \text{rev}(w))$. *Phase 2: compare lengths by simultaneous depletion.* Now registers $2$ and $3$ hold unary encodings $a_0^{|v|}$ and $a_0^{|w|}$. In a loop, read the last letter of each of registers $2$ and $3$: - If both reads return $a_0$, both registers are simultaneously shortened by one; continue the loop. - If register $2$ read returns $\varepsilon$ (i.e., register $2$ was already empty) and register $3$ read returns $a_0$, then $|v| < |w|$: jump to the output-$a$ branch. - If register $2$ read returns $a_0$ and register $3$ read returns $\varepsilon$, then $|v| > |w|$: jump to the output-$\varepsilon$ branch. - If both reads return $\varepsilon$, then $|v| = |w|$: jump to Phase 3. This case distinction is a finite decision, implementable by a single read of register $2$, each branch of which triggers a read of register $3$ with four possible combinations, each combination routed to one of four successor states. No dynamic information beyond the current reads is needed. *Phase 3: lexicographic comparison on equal-length words.* Registers $4$ and $5$ hold $\text{rev}(v)$ and $\text{rev}(w)$; we want to compare them from the *front*, i.e. compare $v_1$ to $w_1$, then $v_2$ to $w_2$, etc. The reversed storage means the first letter is now at the end (right) of each register. We loop: - Read the last letter of register $4$ (call it $v_j$) and the last letter of register $5$ (call it $w_j$). - If both reads return $\varepsilon$, the words are equal (we have consumed all letters without finding a difference); jump to output-$\varepsilon$ (since $v = w$ means $v \not< w$). - Otherwise, both reads return a letter in $\Sigma$ (because $|v| = |w|$ guarantees the two registers are emptied in lock-step). Compare the letters using a hard-wired case distinction on the finitely many pairs $(v_j, w_j) \in \Sigma \times \Sigma$: if $v_j <_\Sigma w_j$ branch to output-$a$; if $v_j >_\Sigma w_j$ branch to output-$\varepsilon$; if $v_j = w_j$ continue the loop. *Phase 4: emit output.* The output-$a$ branch writes $a$ to register $0$ (after ensuring register $0$ is empty, which it already is after Phase 1) and halts. The output-$\varepsilon$ branch simply halts (register $0$ is already $\varepsilon$). [claim:The machine $M_<$ halts on every input pair $(v, w) \in \mathbb{W}^2$ and outputs $\mathbb{1}_{\{(v, w) : v < w\}}(v, w)$ in register $0$] Phase 1 halts in $|v|$ plus $|w|$ loop iterations. Phase 2 halts in $\min(|v|, |w|) + 1$ iterations (each iteration strictly decreases the total length of registers $2$ and $3$ until at least one reaches $\varepsilon$). Phase 3, if entered, halts in at most $|v| = |w|$ iterations. Each phase transitions exactly once to the next phase or directly to output emission; no phase can be re-entered. Therefore the computation is finite, and by the case analysis the output register $0$ holds $a$ iff $v < w$ (from either Phase 2 detecting shorter $v$ or Phase 3 detecting $v <_{\text{lex}} w$) and $\varepsilon$ otherwise. [/claim] Hence the set $\{(v, w) \in \mathbb{W}^2 : v < w\}$ is computable. [/step]

[step:Computability of the successor function — construct $M_s$] We construct a register machine $M_s$ with input register $0$ holding $w \in \mathbb{W}$, which halts with register $0$ containing $s(w) \in \mathbb{W}$, where $s$ is the successor in the shortlex order. Throughout, write $a_0 <_\Sigma a_1 <_\Sigma \cdots <_\Sigma a_{m-1}$ for the ordered letters; $a_0$ is the *minimum* letter and $a_{m-1}$ is the *maximum*. [claim:If $w$ has at least one letter strictly less than $a_{m-1}$, then $s(w)$ is obtained from $w$ by: finding the rightmost such letter, incrementing it to the next letter in $<_\Sigma$, and replacing every letter to the right of it by $a_0$] Write $w = w_1 \cdots w_n$. Let $j^\star$ be the largest index with $w_{j^\star} <_\Sigma a_{m-1}$ (which exists by hypothesis). Define \begin{align*} w' &= w_1 \cdots w_{j^\star - 1} \cdot \text{next}(w_{j^\star}) \cdot a_0^{n - j^\star}, \end{align*} where $\text{next}(a_i) = a_{i+1}$ for $i < m - 1$. We must check $w' = s(w)$, i.e. $w' > w$ and no $u$ satisfies $w < u < w'$. - *$w' > w$*: $|w'| = |w| = n$, so we compare lexicographically. The prefixes agree up to index $j^\star - 1$. At index $j^\star$: $w_{j^\star} <_\Sigma \text{next}(w_{j^\star})$ by definition of $\text{next}$. Hence $w <_{\text{lex}} w'$. - *No $u$ with $w <_{\text{lex}} u <_{\text{lex}} w'$ at length $n$*: such $u = u_1 \cdots u_n$ would satisfy $u_1 \cdots u_{j^\star - 1} = w_1 \cdots w_{j^\star - 1}$ (agreeing with $w'$ on this prefix) and $u_{j^\star} \in \{w_{j^\star}, w_{j^\star} + 1, \ldots\}$ (for $u \ge w$) intersected with $\{a_0, \ldots, w_{j^\star}\}$ in the shortlex order sense, up to $u < w'$. Formally: - If $u_{j^\star} = w_{j^\star}$: then $u > w$ forces the suffix $u_{j^\star + 1} \cdots u_n$ to be shortlex-greater than $w_{j^\star + 1} \cdots w_n = a_{m-1}^{n - j^\star}$ (by maximality of $j^\star$, all letters after index $j^\star$ in $w$ equal $a_{m-1}$). But $a_{m-1}^{n - j^\star}$ is the lexicographic *maximum* among all length-$(n - j^\star)$ strings, so no strictly greater string of equal length exists. Contradiction. - If $u_{j^\star} = \text{next}(w_{j^\star})$: then $u = w' $ is forced for $u < w'$ to hold, which requires $u_{j^\star + 1} \cdots u_n <_{\text{lex}} a_0^{n - j^\star}$; but $a_0^{n - j^\star}$ is the lexicographic *minimum* of length $n - j^\star$, so no strictly smaller string of equal length exists. Contradiction. - If $u_{j^\star} >_\Sigma \text{next}(w_{j^\star})$: then $u >_{\text{lex}} w'$ at position $j^\star$, contradicting $u < w'$. - *No $u$ with $w < u < w'$ at any length*: if $|u| < n$, then $u < w$ by the length rule, contradicting $u > w$. If $|u| > n = |w'|$, then $u > w'$ by the length rule, contradicting $u < w'$. Hence $|u| = n$, handled above. Therefore $w' = s(w)$. [/claim] [claim:If every letter of $w$ equals $a_{m-1}$ (i.e. $w = a_{m-1}^n$ for some $n \ge 0$), then $s(w) = a_0^{n + 1}$] Every length-$n$ word $u$ with $u > w$ satisfies either $|u| > n$ or $|u| = n$ and $u >_{\text{lex}} w$. The latter is impossible because $w = a_{m-1}^n$ is the lexicographic maximum of length $n$. So $s(w)$ has length $> n$, hence length $\ge n + 1$. Among words of length exactly $n + 1$, the minimum is $a_0^{n + 1}$ (lexicographic minimum of length $n+1$). Among words of length $> n + 1$, all exceed $a_0^{n+1}$ by the length rule. And $a_0^{n + 1} > w$ because $|a_0^{n+1}| = n + 1 > n = |w|$. Hence $s(w) = a_0^{n + 1}$. [/claim] *Machine construction.* $M_s$ implements the algorithm encoded by the two claims: - *Phase A: scan $w$ from the right to find $j^\star$.* Repeatedly read the last letter of register $0$; each letter is either $a_{m-1}$ (push onto a scratch register $2$, continue) or some $a_i$ with $i < m - 1$ (this is the rightmost non-maximal letter; retain $a_i$ and its position implicitly via the contents of registers $0$ and $2$, and proceed to Phase B). If register $0$ becomes empty before a non-maximal letter is found, this signals $w = a_{m-1}^n$; proceed to Phase C. - *Phase B: construct $w'$.* At this moment register $0$ holds $w_1 \cdots w_{j^\star - 1}$ and register $2$ holds $a_{m-1}^{n - j^\star}$ (the maximal-letter suffix, in reverse). We append to register $0$ the letter $\text{next}(a_i)$ where $a_i$ was the non-maximal letter just found. Then, using a dedicated loop, we drain register $2$ (reading its letters), but instead of writing back what we read, we write $a_0$ for each read. When register $2$ is empty, register $0$ holds $w_1 \cdots w_{j^\star - 1} \cdot \text{next}(a_i) \cdot a_0^{n - j^\star} = w' = s(w)$. Halt. - *Phase C: emit $a_0^{n + 1}$.* When Phase A exhausts register $0$, register $2$ holds $a_{m-1}^n$ (the entire input, since every letter was maximal). Drain register $2$ into register $0$ as $a_0$'s: a loop reading one letter from register $2$ per iteration and writing $a_0$ to register $0$. After register $2$ becomes empty, register $0$ holds $a_0^n$. Append one more $a_0$ to register $0$ (a single write instruction) to produce $a_0^{n + 1}$. Halt. The selection between "non-maximal letter found" and "empty register $0$" in Phase A is a case distinction on the read instruction's branch (letter vs $\varepsilon$), implementable directly in the register-machine instruction set. The selection among the letters $a_0, a_1, \ldots, a_{m-1}$ when a non-maximal letter is found is a finite hard-wired case distinction (each letter gets its own branch target), using the case distinction technique established in [the case distinction lemma](/theorems/1812). [claim:$M_s$ halts on every input $w \in \mathbb{W}$ and outputs $s(w)$ in register $0$] Phase A runs for at most $|w|$ iterations, each strictly decreasing $|\text{register } 0|$. Phase B or Phase C runs for at most $|w|$ iterations, each strictly decreasing $|\text{register } 2|$. So the total computation is bounded by $2|w| + O(1)$ steps. By the two claims above, the final register $0$ contents equal $s(w)$. [/claim] Hence $s$ is a computable total function. [/step]

[step:Combine the three results] We have established: - $\# : (\mathbb{W}, <) \to (\mathbb{N}, <)$ is a bijection and an order isomorphism (Step 2). - The binary relation $\{(v, w) \in \mathbb{W}^2 : v < w\}$ is computable (Step 3). - The successor function $s : \mathbb{W} \to \mathbb{W}$ is a computable total function (Step 4). These are precisely the three assertions of the theorem. [/step]