YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN R: a() -> c() b() -> c() f(a(),b()) -> d() f(x,c()) -> f(c(),c()) f(c(),x) -> f(c(),c()) d() -> f(a(),c()) d() -> f(c(),b()) CP(R): f(c(),b()) -> d() f(a(),c()) -> d() f(c(),c()) -> f(c(),c()) f(c(),c()) -> f(c(),c()) f(a(),c()) -> f(c(),b()) f(c(),b()) -> f(a(),c()) critical-pair-closing system C: a() -> c() f(a(),b()) -> d() f(c(),x) -> f(c(),c()) d() -> f(c(),b()) CR(C): see below. ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: a() -> c() f(a(),b()) -> d() f(c(),x) -> f(c(),c()) d() -> f(c(),b()) CP(R): f(c(),b()) -> d()