YES 1: F(H(x1),x2) -> G(H(x1)) 2: H(I(x1)) -> I(x1) 3: F(I(x1),x2) -> G(I(x1)) @Jouannaud and Kirchner's criterion --- R 1: F(H(x1),x2) -> G(H(x1)) 2: H(I(x1)) -> I(x1) 3: F(I(x1),x2) -> G(I(x1)) --- S 1: F(H(x1),x2) -> G(H(x1)) 2: H(I(x1)) -> I(x1) 3: F(I(x1),x2) -> G(I(x1))