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