YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN R: f(g(x),g(y)) -> f(g(x),h(y)) f(h(x),g(y)) -> f(g(x),g(y)) f(g(x),h(y)) -> f(x,y) f(h(x),h(y)) -> f(y,x) f(x,y) -> f(y,x) g(x) -> h(x) h(x) -> g(x) CP(R): f(g(___y17),h(___y18)) -> f(g(___y18),g(___y17)) f(g(___y43),g(___y44)) -> f(g(___y44),h(___y43)) f(___y69,___y70) -> f(h(___y70),g(___y69)) f(___y96,___y95) -> f(h(___y96),h(___y95)) f(g(___y108),g(___y107)) -> f(g(___y107),h(___y108)) f(g(___y112),h(___y111)) -> f(g(___y111),g(___y112)) f(h(___y116),g(___y115)) -> f(___y115,___y116) f(h(___y120),h(___y119)) -> f(___y120,___y119) f(h(___y131),g(___y133)) -> f(g(___y131),h(___y133)) f(g(___y132),h(___y131)) -> f(g(___y132),h(___y131)) f(h(___y135),h(___y134)) -> f(g(___y135),g(___y134)) f(h(___y137),h(___y139)) -> f(___y137,___y139) f(g(___y153),g(___y155)) -> f(g(___y153),g(___y155)) f(g(___y157),g(___y156)) -> f(___y157,___y156) f(g(___y159),h(___y161)) -> f(___y161,___y159) f(h(___y160),g(___y159)) -> f(___y159,___y160) critical-pair-closing system C: f(g(x),g(y)) -> f(g(x),h(y)) f(h(x),h(y)) -> f(y,x) f(x,y) -> f(y,x) g(x) -> h(x) CR(C): see below. ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: f(g(x),g(y)) -> f(g(x),h(y)) f(h(x),h(y)) -> f(y,x) f(x,y) -> f(y,x) g(x) -> h(x) CP(R): f(g(___y2549),h(___y2550)) -> f(g(___y2550),g(___y2549)) f(___y2565,___y2564) -> f(h(___y2565),h(___y2564)) f(g(___y2574),g(___y2573)) -> f(g(___y2573),h(___y2574)) f(h(___y2578),h(___y2577)) -> f(___y2578,___y2577) f(h(___y2586),g(___y2588)) -> f(g(___y2586),h(___y2588)) f(g(___y2587),h(___y2586)) -> f(g(___y2587),h(___y2586))