Novikov boone undecidability of the word problem

Fix ${\mathcal{P}}_{\mathcal{B}}$ before reading any input. For binary $w$, compute $v(w)$ using [F6]: if the input is empty, write the single symbol $s_0$ in the finite-word encoding; otherwise copy the binary letters unchanged. Both branches terminate and give a nonempty positive tape word. Then write $\mathrm{\Sigma }(w)=h^{-1}{q}_{\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{r}\mathrm{t}}v(w)h$. By [F5], its positive contexts are $X=h$ and $Y=v(w)h$; by [F2], it is special and its associated positive word is exactly $C(w)$. In particular $\mathrm{\Sigma }(\epsilon )=h^{-1}{q}_{\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{r}\mathrm{t}}{s}_{0}h$.

There is a finite-tape procedure computing $W(\mathrm{\Sigma }(w))$. Store a delimited copy of $\mathrm{\Sigma }(w)$. To copy it, mark each next uncopied source symbol, carry that symbol in finite control, scan to the output end, append it and return to the source; reset the marks after the copy. To copy its inverse, scan source symbols in reverse order and invert each signed letter by a fixed finite lookup. Repeat this for the four displayed copies, inserting the fixed letters $k,t,k^{-1},t^{-1}$. Each scan is between finite delimiters and each copy marks one previously unmarked position, so all loops terminate. Erase the source workspace and move the output left one symbol at a time by the same marking procedure. This produces a valid signed input word for the fixed presentation using a deterministic one-tape machine; no model-equivalence thesis is involved.

If a total decider $D$ of the word problem for ${\mathcal{P}}_{\mathcal{B}}$ existed, first run step 2.1 and then $D$ on its output. By [F3], its answer would be yes exactly when $C(w)=q$. The encoder terminates on every $w$, and the assumed decider terminates on every encoded word, so this would be a total decider of the language ruled out by [F1]. Hence no such $D$ exists.

The generators and relation list are finite by [F2] and never depend on $w$. Step 3.1 therefore proves undecidability for one fixed presentation, as asserted, with AC used only through the group equivalence [F3].