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:
    [I](x0) = 4x0 + 4,
    
    [G](x0) = 4x0,
    
    [F](x0, x1) = 6x0 + 4x1 + 1,
    
    [H](x0) = 2x0 + 4
   orientation:
    F(H(x),y) = 12x + 4y + 25 >= 8x + 16 = G(H(x))
    
    H(I(x)) = 8x + 12 >= 4x + 4 = I(x)
    
    F(I(x),y) = 24x + 4y + 25 >= 16x + 16 = G(I(x))
   problem:
    
   Qed