ABSTRACT

RT to <--->. A choice function .1) : A/ RT -4 A is a function which selects exactly one element from each equivalence class with respect to <RT>. (By the axiom of choice such a mapping always exists.) The choice function induces a

Then we define a new relation = on A, by

has the Church-Rosser property and is confluent by Theorem 7.1.10. The relation = is also terminating and therefore complete. This shows that any reduction system does have a completion.