YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN 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)) critical-pair-closing system C: max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(y,x)) max(x,y) -> max(y,x) CR(C): see below. ---- 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() ___y86 -> max(0(),___y86) 0() -> 0() ___y96 -> max(___y96,0()) s(max(___y110,___y109)) -> max(s(___y110),s(___y109)) max(0(),___y113) -> ___y113 max(___y117,0()) -> ___y117 max(s(___y122),s(___y121)) -> s(max(___y122,___y121))