YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN R: +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) CP(R): +(+(___y1,+(___y2,___y3)),___y6) -> +(+(___y1,___y2),+(___y3,___y6)) +(___y7,+(___y8,+(___y11,___y12))) -> +(+(+(___y7,___y8),___y11),___y12) +(___y10,+(___y7,+(___y8,___y9))) -> +(+(___y10,+(___y7,___y8)),___y9) +(+(+(___y16,___y17),___y14),___y15) -> +(___y16,+(___y17,+(___y14,___y15))) +(+(+(___y13,___y14),___y15),___y18) -> +(___y13,+(+(___y14,___y15),___y18)) +(___y22,+(+(___y19,___y20),___y21)) -> +(+(___y22,___y19),+(___y20,___y21)) critical-pair-closing system C: +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) CR(C): see below. ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) CP(R): +(+(___y31,+(___y32,___y33)),___y36) -> +(+(___y31,___y32),+(___y33,___y36)) +(___y37,+(___y38,+(___y41,___y42))) -> +(+(+(___y37,___y38),___y41),___y42) +(___y40,+(___y37,+(___y38,___y39))) -> +(+(___y40,+(___y37,___y38)),___y39) +(+(+(___y46,___y47),___y44),___y45) -> +(___y46,+(___y47,+(___y44,___y45))) +(+(+(___y43,___y44),___y45),___y48) -> +(___y43,+(+(___y44,___y45),___y48)) +(___y52,+(+(___y49,___y50),___y51)) -> +(+(___y52,___y49),+(___y50,___y51))