YES ---- CR(R) ---- [Knuth and Bendix, 1970] R: a() -> b() f(a()) -> g(a()) f(b()) -> g(b()) CP(R): f(b()) -> g(a())