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

... rewriting2
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.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

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

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

... rule5
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.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... block7
See the appendix for a proof.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

| ZCA Home | Reports |