Boone Machine Simulation and Fixed-Presentation Undecidability

Give each symbol $a$ an undotted copy $a$ and a dotted copy $\dot{a}$. Let $f$ send accepting state to $q_0$, rejecting state to a new state $\mathrm{\ell }$, and each other state to its tagged simulator copy. Add a new start state $z$. On any undotted $a$, its instruction writes $\dot{a}$ and enters $f(p_{\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{r}\mathrm{t}})$. This also defines initialization for empty input, by writing ${\dot{s}}_0$.

For each table entry $(p,a)\mapsto (p^{\mathrm{\prime }},b,D)$ and bit $d\in \{0,1\}$, add a fresh intermediate state $j_{p,a,d}$. In state $f(p)$ scanning $a^{(d)}$, write $b^{(d)}$ and enter $j_{p,a,d}$. On $b^{(d)}$, this intermediate state moves in direction $D$ and enters $f(p^{\mathrm{\prime }})$, except that for $d=1,D=L$ it writes the same $b^{(1)}$ without moving and enters $f(p^{\mathrm{\prime }})$. Every other symbol in that intermediate state goes by a no-op write to $\mathrm{\ell }$. State $\mathrm{\ell }$ no-op writes every symbol and stays in $\mathrm{\ell }$. The unused dotted inputs at $z$ also go to $\mathrm{\ell }$. There are no entries at $q_0$. The cases are disjoint and exhaust every nonstopping state/symbol pair. Their indexing sets are finite, so this is a literal finite deterministic table.

After initialization, the unique dot is at cell zero; undotting the nonnegative tape gives precisely $R$'s initial tape, and all negative cells are blank. Suppose this invariant holds at a simulated nonhalting state. The first instruction writes precisely $R$'s new symbol, retaining the dot bit. The second instruction scans that very symbol, so it follows the designated intermediate branch. Away from zero it makes $R$'s move. At zero a left move is the no-op specified in step 2.1, while a right move reaches cell one. Thus no negative cell is visited and the unique dot is neither lost nor copied. The next macro boundary has exactly $R$'s new head, tape and mapped state. Repeating this calculation proves the invariant after every simulated step.

The macro boundaries occur at times $1+2n$ until a halting outcome. Every intervening time is the intermediate state for the preceding table entry, so a run cannot reach $q_0$ in an unaccounted intermediate step. If $R$ accepts at step $n$, $T$ reaches $q_0$ at time $1+2n$. Conversely the only reached entry into $q_0$ finishes a macro whose target is acceptance. Rejection reaches $\mathrm{\ell }$ and loops forever; an infinite nonhalting run gives infinitely many two-instruction macros. This proves both stopping directions and divergence.

Represent the two-sided tape after any finite time by the finite interval containing the input and all visited cells, including the scanned cell. A move out of that interval adjoins one blank at the appropriate end; a write changes only its scanned cell. These are exactly the five finite-description cases (write, internal/end right, internal/end left), with nonempty scanned right segment. Extra unvisited blanks do not change the infinite-tape run. Thus the constructed machine has the finite-description interface used by the semigroup construction.

Computing $v$ merely tests whether the input is empty and, in that case, writes one blank symbol in its finite-word encoding. A decider for $T$'s stopping language composed with this procedure would decide membership of every binary $w$ in $HAL{T}_{TM}$ by step 4.1, contradicting [F1]. The same fixed table works for all $w$, including words of lengths zero and one.

Every table entry contributes at most $\mathrm{\mid }S\mathrm{\mid }+1$ transition equations, and cleanup contributes $2\mathrm{\mid }S\mathrm{\mid }+1$. Every side is nonempty and contains exactly one state letter, including $q$ on the final right side. Thus replacements stay in $A^{+}$ and the list is finite.

The length-zero path proves $a\sim a$. Reversing a path proves symmetry because each replacement permits both directions. Joining two finite paths with common endpoint proves transitivity. Hence $\sim$ is an equivalence relation and its classes form a set.

Prefixing and suffixing every word of a path by fixed words prefixes and suffixes every replacement context. Therefore $a\sim a^{\mathrm{\prime }}$ implies $uav\sim u{a}^{\mathrm{\prime }}v$. If also $b\sim b^{\mathrm{\prime }}$, first use the path from $a$ to $a^{\mathrm{\prime }}$ with suffix $b$, then the path from $b$ to $b^{\mathrm{\prime }}$ with prefix $a^{\mathrm{\prime }}$, obtaining $ab\sim a^{\mathrm{\prime }}{b}^{\mathrm{\prime }}$. Thus $[a][b]=[ab]$ is independent of both representatives.

Word concatenation is associative: both $(ab)c$ and $a(bc)$ list the letters of $a$, then $b$, then $c$ at the same indices. Consequently $([a][b])[c]=[(ab)c]=[a(bc)]=[a]([b][c])$. Products stay nonempty, so this is the claimed semigroup. Empty contexts and one-letter words cause no exception; an empty word is not adjoined as an identity element.

A write replacement in either direction changes the state and its following scanned symbol, retaining the two outer markers and a nonempty right segment. Internal right swaps $q_a{s}_j{s}_{\beta }$ with $s_j{q}_b{s}_{\beta }$; both sides retain a scanned symbol. End right swaps $q_a{s}_{j}h$ with $s_j{q}_b{s}_{0}h$; the displayed $h$ must be the right outer marker, so the inverse deletes exactly the added blank and restores the earlier scanned cell. Internal left swaps $s_{\beta }{q}_a{s}_j$ with $q_b{s}_{\beta }{s}_j$; both sides have a scanned cell. End left swaps $h{q}_a{s}_j$ with $h{q}_b{s}_0{s}_j$; the displayed $h$ must be the left outer marker, and the inverse again restores a nonempty scanned segment. Since there is exactly one state letter, any applicable contextual transition occurs at that state. All five families therefore preserve augmented shape in both directions.

At $q_0$, erasing or inserting the first right tape letter via $q_{0}s=q_0$ preserves augmented shape, including the empty segment. The equation $s{q}_{0}h=q_{0}h$ applies exactly when the right segment is empty, removing or inserting the last left tape symbol. Finally $h{q}_{0}h=q$ changes exactly the whole word: the markers must be the two outer markers and there are no remaining tape symbols. Conversely $q$ occurs alone in the augmented domain and expands to $h{q}_{0}h$. Thus every symmetric derivation starting at $C(w)$ stays in the augmented domain.

At a nonstopping configuration the unique table entry fixes the instruction. The symbol adjacent to the moved side is either a tape symbol or the outer marker, so exactly one internal/end family applies. At $q_0$ with nonempty right tape the unique forward rule erases its first symbol. With empty right tape and nonempty left tape it erases the last left symbol. With both empty it sends $h{q}_{0}h$ to $q$, which has no successor. Thus the oriented graph on augmented configurations has at most one successor per vertex. Self-loops, if present, do not affect this assertion.

If $T$ stops, its finite description history gives the same transition replacements until $hU{q}_{0}Vh$. Erase the $\mathrm{\mid }V\mathrm{\mid }$ right symbols, then the $\mathrm{\mid }U\mathrm{\mid }$ left symbols, then use $h{q}_{0}h=q$. This constructs a finite derivation from $C(w)$ to $q$.

Conversely, suppose $C(w)=q$. Among finite derivations choose one of least length, $z_0=C(w),\dots ,z_n=q$. It has no repeated vertex or self-loop, since deleting the intervening segment would shorten it. The last edge is forward because $q$ has no successor. If any earlier edge were backward, there would be consecutive edges $z_{j-1}\leftarrow z_j\to z_{j+1}$. Uniqueness of the successor would give $z_{j-1}=z_{j+1}$, contrary to minimality. Every edge is therefore forward. The initial state is not $q_0$; reaching $q$ requires first reaching $q_0$, and before that first occurrence all edges are actual machine steps. Thus $T$ stops. Least length is a least natural number of a nonempty set; it uses no arbitrary choice.

Steps 4.1 and 4.2 prove the two implications. For empty input $v(w)=s_0$ supplies the scanned cell; for one-symbol input the end rules apply as specified. Empty cleanup segments were included explicitly, so these cases do not require a stronger invariant.

Fix the table of $T$ and hence the finite relation list of $\mathrm{\Gamma }$ once. On input $w$, test emptiness, write the encoding of $s_0$ in the empty case and otherwise copy $w$, and prefix $h{q}_{\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{r}\mathrm{t}}$ and suffix $h$. This computes $C(w)$ by finite-symbol scans; no part of the presentation depends on $w$.

A decider answering whether this $C(w)$ equals $q$ would answer yes exactly when $T$ stops on $v(w)$, hence exactly when $w\in HAL{T}_{TM}$. Running it after the terminating encoding in step 1.1 would be a total decider of that language, contradicting [F1].

An unrestricted terminal-equality decider could be run on these initial words; an unrestricted two-word equality decider could be run on $(C(w),q)$. Each would give the impossible decider in step 2.1. The reductions include $C(\epsilon )=h{q}_{\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{r}\mathrm{t}}{s}_{0}h$.

For finitely many edge maps between subgroups of a base $E$, adjoin their letters successively. The edge subgroups remain embedded after each addition by [F5], so the next map is still an isomorphism of actual subgroups. AC chooses representatives of their nonempty cosets for the single-letter normal forms underlying [F4]. This is the choice use throughout the construction.

Prove the multiple-letter pinch assertion by induction on the number of letters. With no letters there is nothing to assert; with one letter apply [F4] to the word times the inverse of its asserted base value. For the next letter, regard all older-letter blocks as coefficients. If the new letter occurs, single-letter Britton supplies a new-letter pinch whose intervening older-letter block represents an element of an original edge subgroup in $E$. If that block contains older letters, the induction hypothesis supplies an older-letter pinch in the original spelling. Otherwise the new-letter pinch is already a pinch over $E$. If the new letter never occurs, use the induction hypothesis directly. This proves the assertion for every finite family, without changing any edge subgroup.

For completeness, compare two multiple-letter reduced words $U,V$ with $U=V$. In $U{V}^{-1}$ a pinch can occur only across the seam, since neither side has an internal pinch. It must pair the last signed letter of $U$ with the inverse of the last signed letter of $V$, with the same label. Reducing this pinch replaces the seam coefficient by a base element, leaving shortened prefixes of the original reduced words. Repeat. If one prefix had stable letters after the other ran out, it would be a reduced word equal to a base element, contradicting step 2.1. Hence all paired letters agree in reverse order and both prefixes run out together. This proves the sequence assertion, including length zero.

Start with the free group on $x$. By [F2], $x^n\mathrm{\ne }1$ for every nonzero integer $n$. The map $x^n\mapsto x^{2n}$ is an isomorphism $⟨x⟩\to ⟨x^2⟩$: it preserves addition of exponents, is injective and has precisely that image. Successively adjoin each $s$ with $s^{-1}xs=x^2$. Steps 1.1–2.1 apply (the local stable letter is $s^{-1}$), giving $H$ and preserving the infinite order of $x$. Form $G_0=H\ast F(\bar{Q})$ using [F3]; states have no relations with $H$.

Sending $x\mapsto 1$ and $s\mapsto s$ respects every relator of $H$, giving $\rho :H\to F(\bar{S})$. For either $\eta =1$ or $\eta =-1$, a nonempty reduced word in the abstract letters $z_s$ maps under $z_s\mapsto s{x}^{\eta }$ and then $\rho$ to the same nonempty reduced tape word. By [F2] it is nonidentity. Thus $T_{\eta }=⟨s{x}^{\eta }:s\in \bar{S}⟩$ is free on that displayed basis, and $\rho$ restricts injectively to $T_{\eta }$.

In $G_0$, the subgroup $⟨q_{a(i)}⟩\ast T_1$ is a free product: any alternating product of its nonidentity state powers and tape elements is a nonempty reduced syllable word by [F3]. The assignment fixing $H$ and all other states and sending $q_{a(i)}$ to $F_i^{\mathrm{\#}}{q}_{a(i)}{G}_i$ defines an automorphism of $G_0$. Its inverse sends that state to $(F_i^{\mathrm{\#}}{)}^{-1}{q}_{a(i)}{G}_i^{-1}$ and fixes the same other generators; substitution verifies both composites on every generator. This automorphism carries the preceding free product to $A_i$, proving its asserted free basis. Empty $F_i$ or $G_i$ give the same substitution with an identity factor.

Replace the state by $q_{b(i)}$, the contexts by $H_i^{\mathrm{\#}},K_i$, and $T_1$ by $T_{-1}$ in the explicit automorphism construction of step 5.1. Its inverse is $q_{b(i)}\mapsto (H_i^{\mathrm{\#}}{)}^{-1}{q}_{b(i)}{K}_i^{-1}$. Thus $B_i$ is free on the stated basis. The unique homomorphisms given by the forward and reverse basis correspondences compose to the identity on every basis element, hence on both groups. They are inverse isomorphisms, proving the assertion about ${\varphi }_i$.

Inverting the equation $s^{-1}xs=x^2$ gives $s^{-1}{x}^{-1}s=x^{-2}$, exactly its image under $\theta$. Thus $\theta$ defines an endomorphism of $H$. Its square fixes $x$ and every $s$, so it is an involutive automorphism. It interchanges $T_1$ and $T_{-1}$. All claims now follow.

Since every ${\varphi }_i$ is an isomorphism of actual subgroups of $G_0$, the successive construction in [F1] forms $G_2$ with embedded bases. Its relations need only be imposed on the free bases, because conjugation and ${\varphi }_i$ preserve products and inverses. The tape relation $r_i^{-1}(sx)r_i=s{x}^{-1}$ is equivalent to $sx{r}_i=r_{i}s{x}^{-1}$ and then $r_{i}s=sx{r}_{i}x$. Thus the finite presentation of $G_2$ is exactly the tape/state/rule portion of $\mathcal{B}$.

The automorphism used in [F1] fixes $H$ and carries $⟨q_{a(i)}⟩\ast T_1$ onto $A_i$. A reduced free-product word with a state syllable cannot belong to $H$, so $A_i\cap H=T_1$. Similarly $B_i\cap H=T_{-1}$. If an element of $T_{\eta }$ equals $x^m$, applying $\rho$ gives identity, and the injectivity on $T_{\eta }$ gives that element equal to $1$. The infinite order of $x$ then gives $m=0$. Hence $A_i\cap ⟨x⟩=B_i\cap ⟨x⟩=\{1\}$.

Let a nonempty freely reduced word on $x,r_i$ be given, consolidating consecutive $x$ letters into powers. A possible rule pinch has the form $r_i^{ϵ}{x}^m{r}_i^{-ϵ}$. If $m\mathrm{\ne }0$, step 1.2 excludes subgroup membership. If $m=0$, the displayed pair would cancel freely, contrary to the chosen spelling. Thus a word with rule letters is nonidentity by multiple-letter Britton in [F1]; without rule letters it is a nonzero power of the embedded $x$. This proves freeness of $C$ on $x,r_i$, including the case of zero rule letters.

The identity map of the actual subgroup $C\le G_2$ is an isomorphism, so adjoining $t$ with that edge map is an HNN extension. Choose representatives by [A1]; [F2]–[F3] embed $G_2$ in $G_3$. Commutation with each $x,r_i$ is equivalent to commutation with every product and inverse, hence with all of $C$.

By [F4], $q$ is a specified generator in the embedded state group, so $q^{-1}tq\in G_3$ is defined. Let $D$ be the subgroup generated by the finite list $x,r_i,q^{-1}tq$. Its identity map is an isomorphism regardless of relations among that list. Adjoining $k$ with this edge map therefore embeds $G_3$ by [F2]–[F3], again using [A1]. Requiring commutation with the displayed generators is equivalent to commutation with $D$. By [F5], these are exactly the remaining defining relations of $\mathcal{B}$; both presentations are the same free-group quotient. This proves the tower and every asserted embedding.

For every integer $a$, $x^{a}s=s{x}^{2a}$ follows by taking powers in $s^{-1}xs=x^2$. The rule relation also gives $r_i^{-1}s=s{x}^{-1}{r}_i^{-1}{x}^{-1}$: from $r_{i}s=sx{r}_{i}x$, obtain $r_i^{-1}sx=s{x}^{-1}{r}_i^{-1}$ and multiply on the right by $x^{-1}$. Thus for either $ϵ=1$ or $-1$, $r_i^{ϵ}s=s{x}^{ϵ}{r}_i^{ϵ}{x}^{ϵ}$.

For a positive word $V$ of length $m$, set $d_m=2^m-1$. At $m=0$, $r_i^{ϵ}V=V{x}^{ϵd_m}{r}_i^{ϵ}{x}^{ϵd_m}$. If this holds for $V$ and $a=ϵd_m$, then $r_i^{ϵ}Vs=V{x}^a{r}_i^{ϵ}{x}^{a}s=V{x}^a{r}_i^{ϵ}s{x}^{2a}=Vs{x}^{2a+ϵ}{r}_i^{ϵ}{x}^{2a+ϵ}\mathrm{.}$ Since $2a+ϵ=ϵd_{m+1}$, this proves the formula for all $m$, for both signs.

Let $U$ be positive of length $n$, let $Z$ be its reversal and put $e=2^n-1$. Then $U^{\mathrm{\#}}=Z^{-1}$. Applying step 2.1 to $r_i^{ϵ}Z=Z{x}^{ϵe}{r}_i^{ϵ}{x}^{ϵe}$ and multiplying by $Z^{-1}$ gives $U^{\mathrm{\#}}{r}_i^{ϵ}=x^{ϵe}{r}_i^{ϵ}{x}^{ϵe}{U}^{\mathrm{\#}}\mathrm{.}$ Together with step 2.1 these are all four signed pushing identities, including $n=0$ and $m=0$.

Every word in a history beginning at ${\mathrm{\Sigma }}^{\ast }$ has exactly one positive state letter, since every relation preserves that count. Hence a contextual forward replacement has old word $U{F}_i{q}_{a(i)}{G}_{i}V$ and new word $U{H}_i{q}_{b(i)}{K}_{i}V$ with positive tape contexts $U,V$. With $e=2^{\mathrm{\mid }U\mathrm{\mid }}-1$, $d=2^{\mathrm{\mid }V\mathrm{\mid }}-1$, the corresponding special spellings $Z_{\mathrm{o}\mathrm{l}\mathrm{d}},Z_{\mathrm{n}\mathrm{e}\mathrm{w}}$ satisfy $Z_{\mathrm{n}\mathrm{e}\mathrm{w}}=U^{\mathrm{\#}}{r}_i^{-1}{a}_i{r}_{i}V=(x^{-e}{r}_i^{-1}{x}^{-e})Z_{\mathrm{o}\mathrm{l}\mathrm{d}}(x^d{r}_i{x}^d)\mathrm{.}$ The reverse replacement uses $a_i=r_i{b}_i{r}_i^{-1}$ and gives $Z_{\mathrm{o}\mathrm{l}\mathrm{d}}=(x^e{r}_i{x}^e)Z_{\mathrm{n}\mathrm{e}\mathrm{w}}(x^{-d}{r}_i^{-1}{x}^{-d})\mathrm{.}$ These equalities use only relations of $G_2$.

Along the finite symmetric path choose, at each edge, the applicable equality expressing the earlier spelling as an auxiliary left factor times the later spelling times an auxiliary right factor. Substitution multiplies the left factors in path order and the right factors in reverse path order. Since the last spelling is $q$, it yields $\mathrm{\Sigma }=LqR$. For a path of length zero both factors are empty. This is a finite product of explicitly given factors, with no choice of infinite histories.

Put $g=q^{-1}tq$. Since $t$ commutes with $L$, ${\mathrm{\Sigma }}^{-1}t\mathrm{\Sigma }=R^{-1}gR$. Since $k$ commutes with $R$ and $g$, $W(\mathrm{\Sigma })=k{R}^{-1}gR{k}^{-1}{R}^{-1}{g}^{-1}R=R^{-1}(kg{k}^{-1}{g}^{-1})R=1.$ These equalities hold in $\mathcal{B}$ by the embedded tower, under its stated AC assumption.

Set $g={\mathrm{\Sigma }}^{-1}t\mathrm{\Sigma }\in G_3$. It has one $t$, hence is nonidentity by [F2]. In the identity word $kg{k}^{-1}{g}^{-1}$ the only two $k$ letters must form a pinch. For the identity edge map of $D$ this says precisely $g\in D$, with membership in the embedded base $G_3$.

Write $g^{-1}=R_0(q^{-1}{t}^{e_1}q)R_1\cdots (q^{-1}{t}^{e_n}q)R_n,$ where $R_j\in C$ are auxiliary words and $e_j\in \{1,-1\}$, and choose the least possible $n$. Such finite expressions exist by $g\in D$ and the definition of generated subgroup. If $n=0$, the equality ${\mathrm{\Sigma }}^{-1}t\mathrm{\Sigma }{R}_0=1$ has exactly one $t$ and violates [F2]. Thus $n\ge 1$.

Apply [F2] to the displayed word for $g{g}^{-1}$ in $G_3$. If a pinch uses its first $t$, it pairs that $t$ with $t^{e_1}$, so $e_1=-1$ and $\mathrm{\Sigma }{R}_0{q}^{-1}=P\in C$ in $G_2$. Multiplying gives $P^{-1}\mathrm{\Sigma }{R}_0=q$. This is the desired auxiliary equation.

Any other pinch pairs consecutive $t^{e_j},t^{e_{j+1}}$ with $e_{j+1}=-e_j$ and $q{R}_j{q}^{-1}\in C$. Since $t$ commutes with $C$, for either sign $e_j$ the corresponding subexpression satisfies $(q^{-1}{t}^{e_j}q)R_j(q^{-1}{t}^{-e_j}q)=q^{-1}(q{R}_j{q}^{-1})q=R_j\mathrm{.}$ Replacing it combines the neighboring auxiliary factors and gives an expression for $g^{-1}$ with $n-2$ such occurrences, contrary to minimality. Thus this kind of pinch cannot occur.

A pinch exists, so step 3.1 must apply. Freely reducing $P^{-1}$ and $R_0$ changes neither represented element nor alphabet, and yields the claimed $L,R$. All coefficient equalities were obtained in $G_2$, by the embedded-base clause in [F1]. Least finite length and finite free reduction need no additional choice.

Here is also the intersection check directly. Undoing the state-twisting automorphism in [F1] fixes $H$. A reduced word with a state syllable then cannot lie in $H$, so an element of $A_i\cap ⟨x⟩$ must lie in $T_1=⟨sx⟩$. The tape retraction sends a nonempty reduced basis word there to a nonempty reduced tape word, whereas it sends $x^m$ to identity. Therefore the basis word is empty and $x^m=1$, whence $m=0$. For $B_i$ the same computation uses $T_{-1}=⟨s{x}^{-1}⟩$, with the identical retraction image. This verifies the intersections used in [F2].

An internal pinch in a reduced auxiliary word must pair $r_i^{ϵ},r_i^{-ϵ}$ across a pure power $x^m$. By step 1.1 membership in the requisite edge subgroup forces $m=0$. But then the two letters freely cancel, contrary to reducedness. There is thus no internal pinch.

Rewrite the given equality as $L{X}^{\mathrm{\#}}{q}_j=q{R}^{-1}{Y}^{-1}$. Both sides are rule-reduced by step 2.1, since all their rule letters occur in their single auxiliary block. The multiple-letter comparison of [F1], derived by successively pairing letters across the seam, shows their signed rule sequences agree. In particular their lengths agree. This is consistent with the single-letter normal-form invariant [F3], with choices licensed by [A1]; the finite comparison here uses the proved multiple-letter version.

If the common length is positive, multiple-letter Britton applied to $L{X}^{\mathrm{\#}}{q}_{j}YR{q}^{-1}=1$ supplies a pinch. It cannot be wholly within either auxiliary block by step 2.1. The only other consecutive pair of rule letters is the last one of $L$ and the first one of $R$, with intervening coefficient $x^m{X}^{\mathrm{\#}}{q}_{j}Y{x}^n$ for their adjacent terminal/initial powers. Thus it has exactly the central form in the statement. If the common length is zero, the whole equality is in $G_0$ by base embedding.

We prove a stronger assertion: for freely reduced, possibly signed tape words $X,Y$, the equation $L{X}^{\mathrm{\#}}{q}_{j}YR=q$ forces $X,Y$ to be positive and $X{q}_{j}Y=q$ in $\mathrm{\Gamma }$. Freely reduce $L,R$, which does not change their elements. By [F1] their rule-letter counts have a common value $p$. We use strong induction on $p$, under the AC normal-form assumptions.

If $p=0$, the equation is $x^m{X}^{\mathrm{\#}}{q}_{j}Y{x}^n=q$ in $G_0=H\ast F(\bar{Q})$, since the base embeds. Unique reduced syllables give $q_j=q$, $x^m{X}^{\mathrm{\#}}=1$ and $Y{x}^n=1$. Applying $\rho$ shows the freely reduced tape words $X^{\mathrm{\#}},Y$ are empty. Infinite order of $x$ then gives $m=n=0$. Thus $X,Y$ are empty positive words and $X{q}_{j}Y=q$ literally, proving the initial case.

We first establish the tape sign test used at a pinch. Suppose $Z$ is a freely reduced signed tape word and $Z{x}^a\in T_1=⟨sx⟩$. Choose its reduced basis spelling $u$ in $sx$. Then $x^a{u}^{-1}Z=1$ in $H$. Expand $u^{-1}$ in tape stable letters and $x$. This expansion has no tape pinch: opposite successive tape signs of the same label would come from consecutive inverse basis letters, forbidden by basis reduction; opposite signs of different labels are not a pinch. Any cancellations of neighboring $x,x^{-1}$ do not change this observation. The same is true of $Z$, since it is freely reduced. If $Z$ began with $s^{-1}$, the only possible first pinch in $x^a{u}^{-1}Z$ would be across that seam. The last basis letter of $u^{-1}$ would have to be $sx$, giving exactly $sx{s}^{-1}$. For the tape relation $s^{-1}xs=x^2$, such a pinch requires $x\in ⟨x^2⟩$, impossible because $x$ has infinite order and $1$ is not an even integer. If $u$ is empty there is no seam pinch at all. Multiple-letter Britton therefore rules out a negative first letter of $Z$. Thus $Z$ is empty or begins positively.