YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN R: a() -> a'() h(x,a'(),y) -> h(x,y,y) h(x,y,a'()) -> h(x,y,y) g() -> f() h(f(),a(),a()) -> h(g(),a(),a()) h(g(),a(),a()) -> h(f(),a(),a()) CP(R): h(f(),a'(),a()) -> h(g(),a(),a()) h(f(),a(),a'()) -> h(g(),a(),a()) h(g(),a'(),a()) -> h(f(),a(),a()) h(g(),a(),a'()) -> h(f(),a(),a()) h(___y11,a'(),a'()) -> h(___y11,a'(),a'()) h(___y23,a'(),a'()) -> h(___y23,a'(),a'()) h(f(),a(),a()) -> h(f(),a(),a()) critical-pair-closing system C: a() -> a'() g() -> f() CR(C): see below. ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: a() -> a'() g() -> f() CP(R):