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 (critical pair closing system, Thm 2.11):
  F(I(x34),x33) -> G(I(x34))
  H(I(x35)) -> I(x35)
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [I](x0) = x0 + 4,
    
    [G](x0) = x0 + 4,
    
    [F](x0, x1) = 4x0 + 4x1,
    
    [H](x0) = x0
   orientation:
    F(I(x34),x33) = 4x33 + 4x34 + 16 >= x34 + 8 = G(I(x34))
    
    H(I(x35)) = x35 + 4 >= x35 + 4 = I(x35)
   problem:
    H(I(x35)) -> I(x35)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [I](x0) = x0 + 4,
     
     [H](x0) = x0 + 1
    orientation:
     H(I(x35)) = x35 + 5 >= x35 + 4 = I(x35)
    problem:
     
    Qed