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