YES ---- CR(R) ---- Development Closedness Theorem [van Oostrom, TCS 1994]. R: s(p(x)) -> x p(s(x)) -> x CP(R): p(___y3) -> p(___y3) s(___y5) -> s(___y5)