... convergent¹

Convergent presentations for groups are string rewriting systems which are terminating and confluent.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... rewriting²

A rule $\ell \longrightarrow r$ can be used to prefix (string) rewrite a word u if $u \equiv\ell w$, i.e. $\ell$ is a prefix of u as a word. u is then replaced by rw.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... fair³

A fair strategy will ensure that all elements of the critical pair test sets are considered at some time by the procedure.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... length⁴

There are strategies for TC to produce exactly these cosets by using words as coset representatives and bonus and collapse equations as oriented ``rules''.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... rule⁵

Notice that there are trivial rules among these where the left and right hand sides coincide as words. They correspond to the defining equations in TC and of course have to be omitted in order to make the system terminating.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...$\Gamma = \{ x, y, Y \}$⁶

We can omit the formal inverse X of x as completion would lead to an identification of the two.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... block⁷

See the appendix for a proof.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.