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:
If is the normal form of x with respect to T, then is a normal form of with respect to .This is due to the fact that in case then there exists a rule in such that .
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 (l1,r1) and (l2,r2) 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.