Stay-put one-tape machines and their runs

As in the configuration-set construction of F3, separate finite-support functions inside ${\mathrm{\Gamma }}^{\mathbb{N}}$ to obtain $\mathcal{T}$, and take $Q\times \mathbb{N}\times \mathcal{T}$. These formulas use only the displayed sets and blank, so changing the direction codomain has no effect on their sethood. The graph of $t[h:=b]$ is the subset of $\mathbb{N}\times \mathrm{\Gamma }$ given by $(j=h\wedge c=b)\vee (j\mathrm{\ne }h\wedge c=t(j))$. Exactly one clause supplies exactly one value in $\mathrm{\Gamma }$ at each $j$, so this is a total function.

Put $F=\mathrm{supp}(t)$. If $h\in F$, then $F\cup \{h\}=F$ is finite. Otherwise take a bijection $e:n\to F$, available by finiteness; extending it by $e^{\mathrm{\prime }}(n)=h$ gives a bijection $n+1\to F\cup \{h\}$, since the new value is outside the old range. This also works for $F=\mathrm{\varnothing }$ and $n=0$. At every $j\mathrm{\notin }F\cup \{h\}$ the new value equals $t(j)=\bigsqcup$. Hence $\mathrm{supp}(t[h:=b])\subseteq F\cup \{h\}$ is finite by F4.

At a nonhalting state, totality supplies a unique $(p,b,D)$. Exactly one head clause applies, and it returns a natural, including the clamped value zero. Together with the unique updated tape from the preceding steps this gives exactly one successor in ${\mathcal{C}}_M$. For $D=L,R$ this is the ordinary step formula, and for $D=S$ the head is unchanged. At a halting state the explicit nonhalting condition fails, so there is no successor.

Define $T:{\mathcal{C}}_M\to {\mathcal{C}}_M$ by this successor on nonhalting configurations and by $T(X)=X$ on halting ones. Its graph consists of these two disjoint prescriptions and is a set; it is total by the preceding step. F5 with $A={\mathcal{C}}_M$, $a=C$, $f=T$ supplies a unique $u:\mathbb{N}\to {\mathcal{C}}_M$ satisfying $u(0)=C$ and $u(i+1)=T(u(i))$.

Every nonempty set $B$ of natural indices has a least member: take one $b\in B$ and inspect the finite list $0,\dots ,b$. More formally, induction on $n$ proves that $B\cap \{0,\dots ,n\}$ is empty or has a least member. At zero it is empty or $\{0\}$. On adjoining $n+1$, retain the old least member if there was one; otherwise the new intersection is empty or $\{n+1\}$. At $n=b$ it is nonempty, and its least member is also least in $B$, because every index outside this initial list exceeds $b$. Thus, if $u$ ever halts, its first halting index $t$ exists.

If such $t$ exists, all $u(i)$ for $i<t$ are nonhalting, so $u(0),\dots ,u(t)$ is a genuine finite maximal run. Otherwise every transition of $u$ is genuine and $u$ is an infinite maximal run. For any other run with the same start, equality holds at index zero; whenever both prefixes continue, equal nonhalting configurations have equal successors by uniqueness. Induction gives agreement at every common index. A finite maximal run cannot end earlier, since the corresponding $u(i)$ would be nonhalting, and cannot continue past $t$, where there is no successor. An infinite run cannot pass a finite $t$ either. This proves uniqueness and the exhaustive, disjoint accept/reject/diverge alternatives. The constant tail of $u$ after $t$ is never part of a computation.

For any input $w:m\to \mathrm{\Sigma }$, the initial tape prescription assigns a unique value in $\mathrm{\Gamma }$ at each index. Its support is exactly $\{0,\dots ,m-1\}=m$: blank exclusion makes every input cell nonblank and every other cell blank. Thus $I_M(w)$ is a configuration. When $m=0$ the support is empty; when $m=1$ it is $\{0\}$. If $\mathrm{\Sigma }=\mathrm{\varnothing }$ only the empty input exists, and $\mathrm{\Gamma }=\{\bigsqcup \}$ is allowed. The start is nonhalting because the designated states are pairwise distinct. For an arbitrary already-halting start, the unique maximal run has zero transitions. These cover the degenerate inputs without a choice function or a false infinite halting tail.