YES ---- CR(R) ---- [Knuth and Bendix, 1970] R: F(x,y) -> c(y) G(x) -> x f(x) -> g(x) g(x) -> c(x) CP(R):