YES ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] 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())