Initial tapes and machine-relative halting configurations

The ambient tape functions form the set ${\mathrm{\Gamma }}^{\mathbb{N}}$. For any such $t$, its support is the subset of $\mathbb{N}$ satisfying $t(i)\mathrm{\ne }\bigsqcup$; Separation forms this set. Separating those functions whose supports are finite forms ${\mathcal{T}}_M\subseteq {\mathrm{\Gamma }}^{\mathbb{N}}$. Taking the product gives the configuration set $Q\times \mathbb{N}\times {\mathcal{T}}_M$. Each separating formula uses the fixed tuple as parameters and does not mention the resulting set as a free variable.

Fix $w:m\to \mathrm{\Sigma }$. For each $i\in \mathbb{N}$, exactly one of $i<m$ and $i\ge m$ holds. In the first case $w(i)$ exists uniquely and belongs to $\mathrm{\Sigma }\subseteq \mathrm{\Gamma }$; in the second the assigned blank belongs to $\mathrm{\Gamma }$. Thus the graph of the displayed prescription, separated inside $\mathbb{N}\times \mathrm{\Gamma }$, defines a unique total $t_w:\mathbb{N}\to \mathrm{\Gamma }$.

If $i<m$, blank exclusion gives $t_w(i)=w(i)\mathrm{\ne }\bigsqcup$, so $i\in \mathrm{supp}(t_w)$. Conversely $i\in \mathrm{supp}(t_w)$ rules out $i\ge m$, since that clause would give $t_w(i)=\bigsqcup$; hence $i<m$. Therefore $\mathrm{supp}(t_w)=m$, which is finite with cardinality $m$. In particular any subset of the occupied cells is finite. Thus $t_w\in {\mathcal{T}}_M$.

If one configuration were both accepting and rejecting, its state would satisfy $q=q_{\mathrm{a}\mathrm{c}\mathrm{c}}=q_{\mathrm{r}\mathrm{e}\mathrm{j}}$, contrary to their distinctness. Conversely every state equal to $q_{\mathrm{a}\mathrm{c}\mathrm{c}}$ satisfies the accepting predicate and cannot satisfy the rejecting one, and every state equal to $q_{\mathrm{r}\mathrm{e}\mathrm{j}}$ satisfies the rejecting predicate and cannot satisfy the accepting one. Membership in the displayed two-element set is equivalent in both directions to one of these equalities, so the halting configurations are precisely the union of these two disjoint classes. Each class is a subset of the configuration set given by its state equality.

For $m=0$, there are no indices $i<m$, so $t_w(i)=\bigsqcup$ everywhere and the support is empty. For $m=1$, its value at zero is $w(0)\mathrm{\ne }\bigsqcup$ and all cells $i\ge 1$ are blank, so its support is $\{0\}$. In general the last occupied cell is $m-1$ when $m>0$, and cell $m$ is blank. Since $q_0\in Q$ and $0\in \mathbb{N}$, $I_M(w)$ is a configuration for every input, including both these cases. If $\mathrm{\Sigma }=\mathrm{\varnothing }$ only the length-zero case occurs.

The state of $I_M(w)$ is $q_0$, distinct from both halting states. It therefore satisfies neither halting equality and is nonhalting, for every $w$. The left endpoint zero remains a natural coordinate under the clamped convention. Neither this endpoint rule nor the boundary predicates assert that any transition has occurred. Empty $Q$ or one-state $Q$ cannot satisfy the tuple hypotheses; the tape alphabet can be just $\{\bigsqcup \}$ when the input alphabet is empty. Thus the construction and all boundary assertions require no extra nonempty selection or computational assumption.