- ... convergent
^{1}
- Convergent
presentations for groups are string rewriting systems which are terminating and confluent.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

- ... rewriting
^{2}
- A rule
can be used to prefix (string) rewrite a word
*u* if
,
i.e.
is a prefix of *u*
as a word. *u* is then replaced by *rw*.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

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

- ... length
^{4}
- 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
^{5}
- 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.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

- ...
^{6}
- We
can omit the formal inverse
*X* of *x* as completion would lead to an identification of the
two.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

- ... block
^{7}
- See the
appendix for a proof.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.