Reduced sequence in an HNN extension (source code)

= Reduced sequence in an HNN extension

= Reduced sequences in an HNN extension
{synonym}

A reduced sequence is a word $g_0t^{\epsilon_1}g_1\cdots t^{\epsilon_k}g_k$ with no <pinch in an HNN extension>. If $k>0$, <Britton's lemma> makes it nontrivial and prevents it from representing a base-group element. Reduced sequences need not be unique; uniqueness requires the fixed coset representatives in the <normal form theorem for an HNN extension>.