---- CR(R) ---- [van Oostrom, RTA 2008]. R: F(H(x),y) -> F(H(x),I(I(y))) F(x,G(y)) -> F(I(x),G(y)) I(x) -> x Label: [F(H(x),y) -> F(H(x),I(I(y)))] = 3 [F(x,G(y)) -> F(I(x),G(y))] = 0 [I(x) -> x] = 0