YES ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) -(0(),x) -> 0() -(x,0()) -> x -(s(x),s(y)) -> -(x,y) CP(R): 0() -> 0() 0() -> 0()