YES ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(y,x)) max(x,y) -> max(y,x) CP(R): 0() -> 0() ___y8 -> max(0(),___y8) 0() -> 0() ___y18 -> max(___y18,0()) s(max(___y32,___y31)) -> max(s(___y32),s(___y31)) max(0(),___y35) -> ___y35 max(___y39,0()) -> ___y39 max(s(___y44),s(___y43)) -> s(max(___y44,___y43))