---- CR(R) ---- [van Oostrom, RTA 2008]. R: f(x) -> g(x) f(x) -> h(f(x)) h(f(x)) -> h(g(x)) g(x) -> h(g(x)) Label: [f(x) -> g(x)] = 1 [f(x) -> h(f(x))] = 0 [h(f(x)) -> h(g(x))] = 1 [g(x) -> h(g(x))] = 0