Permutation proof of HNN normal form uniqueness

With convention $t^{-1}at=\varphi (a)$, choose representatives of the right cosets of $A$ and $B$ in the base group, with identity representing each subgroup. Normal strings have the form $g_0{t}^{{ϵ}_1}{r}_1\cdots t^{{ϵ}_n}{r}_n$, where $r_i$ represents a coset of $B$ for ${ϵ}_i=1$ and of $A$ for ${ϵ}_i=-1$, and $r_i\ne 1$ when adjacent exponents are opposite. Left multiplication by base elements or stable letters defines permutations of these strings. They satisfy the HNN relations. Applying the induced action to the empty string distinguishes different normal strings, proving uniqueness without presupposing Britton's lemma.

// Target: geometry-and-topology.bigb