Normal forms in an HNN extension are unique relative to chosen transversals

Starting at the right end of an HNN word, use [L1] to rewrite every coefficient following a $t$ as $cs$ with $c\in C_{-}$ and every coefficient following a $t^{-1}$ as $dr$ with $d\in C_{+}$. Move the subgroup factor to the left by $tc=\varphi (c)t$ or $t^{-1}d={\varphi }^{-1}(d)t^{-1}$. If this creates adjacent inverse stable letters, apply [L2], combine the adjacent base coefficients, and repeat. Each cancellation removes two stable letters; between cancellations the next coset decomposition is unique. The process therefore terminates and yields a transversal normal form.

Let $\mathcal{N}$ be the set of transversal normal forms. For $a\in A$, let ${\lambda }_a$ multiply the initial coefficient by $a$. Define ${\lambda }_t$ by prepending $t$, making the forced decomposition $a_0=cs$ from [L1], and using $tcs=\varphi (c)ts$; define ${\lambda }_{t^{-1}}$ dually from $a_0=dr$ and $t^{-1}dr={\varphi }^{-1}(d)t^{-1}r$. If the new stable letter is inverse to the first old one and $s=e$ or $r=e$, cancel that pair and apply the same front rule again. This recursion terminates because each repetition removes two stable letters.

Uniqueness of the decompositions in [L1] gives ${\lambda }_a{\lambda }_b={\lambda }_{ab}$ and shows directly, in the cancellation and noncancellation cases, that ${\lambda }_t$ and ${\lambda }_{t^{-1}}$ are inverse permutations of $\mathcal{N}$. For $c\in C_{-}$, the front rules reduce the literal pin in $tc{t}^{-1}w$ before touching $w$, so ${\lambda }_t{\lambda }_c{\lambda }_{t^{-1}}={\lambda }_{\varphi (c)}\mathrm{.}$ Thus the factor actions of $A$ and $F(\{t\})$ satisfy every relator in [L3] and descend to an action of the HNN extension on $\mathcal{N}$.

Apply the action from step 1.3 to the length-zero normal word $e_A$. Reading a written normal form from right to left reconstructs it exactly: each terminal coefficient is already in the required transversal, and the nonidentity condition at a sign change prevents cancellation. Hence a normal form sends $e_A$ to that same written normal form. If two normal forms represented one group element, their actions on $e_A$ would agree, so the two written forms would be identical. The identity acts trivially, and therefore its unique normal form is $e_A$.