The right-left macro simulates one stay-put step

The state product exists by F4. By F5, $(p,0)=(q,1)$ would imply $0=1$, which is false by F7. Also $(p,e)=(q,e)$ implies $p=q$. Thus marked and unmarked copies are disjoint even when the original state objects themselves are pairs; the three unmarked designated states remain pairwise distinct.

Take a bijection $e:n\to Q$ by F3. The tagged states over its first $j$ values form a finite set, by induction on $j\le n$. For $j=0$ this set is empty with its empty bijection. To pass to $j+1$, append $(e(j),0)$ and then $(e(j),1)$; neither equals an earlier state, and they differ from each other by step 1.1 and injectivity of $e$. If $f:r\to A$ is a bijection and $x\mathrm{\notin }A$, the map agreeing with $f$ on $r$ and taking $r$ to $x$ is a bijection $r+1\to A\cup \{x\}$: old images stay distinct, the new image is fresh, and every target is old or $x$. Applying this twice proves the induction step. At $j=n$ the finite set is exactly $Q\times \{0,1\}$.

Every nonhalting simulator state is either $(q,0)$ with $q$ originally nonhalting, or $(p,1)$ for some $p\in Q$. The former has a unique original entry and exactly one of the two displayed replacement clauses applies. The latter has the displayed return entry for each scanned symbol. The cases are disjoint and exhaust all required entries; outputs have state in the product, symbol in $\mathrm{\Gamma }$ and direction in $\{L,R\}$. The only states with no entries are the two unmarked halting states. Along with finite control and the unchanged finite alphabets, these checks establish that $N$ is a legal ordinary machine.

Suppose $C=(q,h,t)$ is nonhalting and $\delta (q,t(h))=(p,b,D)$ with $D=L$ or $R$. The first clause writes $b$ at $h$, changes the state to $(p,0)$, and applies the same $H_D$ as $M$. Thus its successor is $((p,0),H_D(h),t[h:=b])=E(C^{\mathrm{\prime }})$. It is already unmarked, so no earlier positive time in this segment is unmarked. This includes $D=L,h=0$, where both heads remain zero.

For $D=S$, put $u=t[h:=b]$. The first simulator step is exactly $E(C){⊢}_N((p,1),h+1,u)$. Its state is marked and hence nonhalting, even if $p=q_{\mathrm{a}\mathrm{c}\mathrm{c}}$ or $q_{\mathrm{r}\mathrm{e}\mathrm{j}}$. Write $c=u(h+1)$. The forced return entry rewrites $c$ as $c$, so its updated tape $v$ has $v(h+1)=u(h+1)$ and $v(j)=u(j)$ for every other $j$; consequently $v=u$. The head is at a positive successor by F7, whose unique predecessor is $h$, so the return ends at $((p,0),h,u)=E(C^{\mathrm{\prime }})$. At $h=0$ the head trace is $0,1,0$. The symbol $c$ may be blank or any nonblank symbol; the whole tape equality used no assumption about it.

Conversely, an unmarked starting configuration has the unique form $E(q,h,t)$ by F5. If $q$ is halting it has no successor. Otherwise its unique original entry has direction $L$, $R$ or $S$. The first two give the one-step segment of step 4.1. The third gives the marked first state and forced unmarked second state of step 4.2, with no unmarked interior. There is no fourth case and no freedom to take a different return transition. Thus all and only the next-unmarked segments are precisely the claimed simulations, in both directions.