YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN R: W(W(x)) -> W(x) B(I(x)) -> W(x) W(B(x)) -> B(x) F(H(x),y) -> F(H(x),G(y)) F(x,I(y)) -> F(G(x),I(y)) G(x) -> x CP(R): W(W(___y1)) -> W(W(___y1)) W(W(___y19)) -> B(I(___y19)) W(B(___y29)) -> W(B(___y29)) F(H(___y56),G(I(___y59))) -> F(G(H(___y56)),I(___y59)) F(G(H(___y74)),I(___y73)) -> F(H(___y74),G(I(___y73))) critical-pair-closing system C: W(W(x)) -> W(x) B(I(x)) -> W(x) W(B(x)) -> B(x) F(x,I(y)) -> F(G(x),I(y)) G(x) -> x CR(C): see below. ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: W(W(x)) -> W(x) B(I(x)) -> W(x) W(B(x)) -> B(x) F(x,I(y)) -> F(G(x),I(y)) G(x) -> x CP(R): W(W(___y97)) -> W(W(___y97)) W(W(___y112)) -> B(I(___y112)) W(B(___y119)) -> W(B(___y119))