Sufficiency Conditions for Bokut' Normal Forms

We provide sufficient conditions for the existence and uniqueness of normal forms of sequences of HNN extensions defined by Bokut'. Furthermore, we show that under an assumption, which holds for various applications, such normal forms always exist (but might not be unique). The conditions are amenable to be used in automatic theorem provers. We discuss also how to obtain a Gröbner-Shirshov basis from the rewrite rules of Bokut' normal forms under certain assumptions. Finally, we provide an application drawn from a paper of Aanderaa and Cohen to illustrate the sufficiency conditions.