YES

Problem:
 F(H(x),y) -> G(H(x))
 H(I(x)) -> I(x)
 F(I(x),y) -> G(I(x))

Proof:
 Church Rosser Transformation Processor (kb):
  F(H(x),y) -> G(H(x))
  H(I(x)) -> I(x)
  F(I(x),y) -> G(I(x))
  critical peaks: joinable
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [F](x0, x1) = 4x0 + 4x1 + 4,
     
     [I](x0) = x0 + 3,
     
     [H](x0) = 7x0 + 4,
     
     [G](x0) = x0 + 4
    orientation:
     F(H(x),y) = 28x + 4y + 20 >= 7x + 8 = G(H(x))
     
     H(I(x)) = 7x + 25 >= x + 3 = I(x)
     
     F(I(x),y) = 4x + 4y + 16 >= x + 7 = G(I(x))
    problem:
     
    Qed