YES ---- CR(R) ---- Hot decreasingness. R: F(H(x),y) -> F(H(x),I(I(y))) F(x,G(y)) -> F(I(x),G(y)) I(x) -> x C: I(x) -> x Label: [F(H(x),y) -> F(H(x),I(I(y)))] = 0 [F(x,G(y)) -> F(I(x),G(y))] = 0