---- CR(R) ---- [van Oostrom, RTA 2008]. 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) Label: [f(g(x),g(y)) -> f(g(x),h(y))] = 5 [f(h(x),g(y)) -> f(g(x),g(y))] = 4 [f(g(x),h(y)) -> f(x,y)] = 1 [f(h(x),h(y)) -> f(y,x)] = 0 [f(x,y) -> f(y,x)] = 0 [g(x) -> h(x)] = 1 [h(x) -> g(x)] = 4