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