Discrete Algebraic Methods

The system S terminates because the rules are length preserving, and every rewriting step reduces words lexicographically. A direct consideration of the critical pairs provides local confluence. For instance, we have and for a, b, c ∈ Σ, a < b < c, (c, bu) ∈ I, (a, bcuυ) ∈ I.

In particular, we can decide the word problem for M (Σ, I) by determining irreducible normal forms. The set IRR(S) describes the set of the lexicographic normal forms. Since ...