8. Appendix

Let
be a polycyclic group with
a convergent
PCP-system as described
in section 2.
For the set of rules *T* we define
and
,
,
,
.
It is easily seen that this rewriting system is terminating with respect
to the syllable ordering with status right induced by the precedence
.
In order to show (local) confluence we will need the following fact:

This is due to the fact that in case then there exists a rule in such that .Ifis the normal form ofxwith respect toT, thenis a normal form ofwith respect to.

Now to see that our system
is confluent we
take a closer look at possible critical pairs.
Such pairs are due to the following two possible overlaps of rules
and
:
In case we have *x*,*y* in
such that
this corresponds to an overlap
respectively if we have
this corresponds
to an overlap
of the rules (*l*_{1},*r*_{1})
and (*l*_{2},*r*_{2}) in *T*.
Now since the critical pairs for *T* are confluent and the overlaps
for
are just reversed instances of these systems, we
know that they reduce to the same common descendant which is a
reverse instance of
the common descendant in the *T*-case.
Hence the rewriting system is confluent and obviously it has similar
properties as the original system and gives us normal forms of the desired
form.