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