 would allow the further reduction of 1 + der(0) to 1 + 0 and then, by R5, to 1. Although the presence of this new rule actually increases the number of alternative paths—der(x + 0) can now be reduced in four possible ways—they all end up with the same normal form, namely 1. This is no coincidence as it can be shown that (R6) actually restores confluency. This motivates another fundamental question: Under what conditions can a non-confluent system be made into an equivalent confluent one? The Knuth-Bendix completion algorithm (Knuth &amp; Bendix 1970) gives a partial answer to this question.