YES ---- CR(R) ---- Development Closedness Theorem [van Oostrom, TCS 1994]. R: f(a(),a()) -> g(f(a(),a())) a() -> b() f(b(),x) -> g(f(x,x)) f(x,b()) -> g(f(x,x)) CP(R): f(b(),a()) -> g(f(a(),a())) f(a(),b()) -> g(f(a(),a())) g(f(b(),b())) -> g(f(b(),b())) g(f(b(),b())) -> g(f(b(),b()))