YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN R: F(H(x),y) -> F(H(x),I(I(y))) F(x,G(y)) -> F(I(x),G(y)) I(x) -> x CP(R): F(H(___y5),I(I(G(___y8)))) -> F(I(H(___y5)),G(___y8)) F(I(H(___y14)),G(___y13)) -> F(H(___y14),I(I(G(___y13)))) critical-pair-closing system C: F(H(x),y) -> F(H(x),I(I(y))) I(x) -> x CR(C): see below. ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: F(H(x),y) -> F(H(x),I(I(y))) I(x) -> x CP(R):