YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN R: foo(0(x)) -> 0(s(p(p(p(s(s(s(p(s(x)))))))))) foo(s(x)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x)))))))))))))))))))))))))) bar(0(x)) -> 0(p(s(s(s(x))))) bar(s(x)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x)))))))))))) p(p(s(x))) -> p(x) p(s(x)) -> x p(0(x)) -> 0(s(s(s(s(x))))) CP(R): p(___y79) -> p(___y79) critical-pair-closing system C: foo(0(x)) -> 0(s(p(p(p(s(s(s(p(s(x)))))))))) bar(0(x)) -> 0(p(s(s(s(x))))) p(p(s(x))) -> p(x) p(0(x)) -> 0(s(s(s(s(x))))) CR(C): see below. ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: foo(0(x)) -> 0(s(p(p(p(s(s(s(p(s(x)))))))))) bar(0(x)) -> 0(p(s(s(s(x))))) p(p(s(x))) -> p(x) p(0(x)) -> 0(s(s(s(s(x))))) CP(R):