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) = 5x0,
    
    [G](x0) = 4x0,
    
    [F](x0, x1) = 5x0 + 4x1,
    
    [H](x0) = x0 + 3
   orientation:
    F(H(x),y) = 5x + 4y + 15 >= 4x + 12 = G(H(x))
    
    H(I(x)) = 5x + 3 >= 5x = I(x)
    
    F(I(x),y) = 25x + 4y >= 20x = G(I(x))
   problem:
    F(I(x),y) -> G(I(x))
   Matrix Interpretation Processor: dim=3
    
    interpretation:
               [1 0 0]  
     [I](x0) = [0 0 0]x0
               [0 0 0]  ,
     
               [1 0 0]  
     [G](x0) = [0 0 0]x0
               [0 0 0]  ,
     
                   [1 0 0]     [1 0 0]     [1]
     [F](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
                   [0 0 0]     [0 0 0]     [0]
    orientation:
                 [1 0 0]    [1 0 0]    [1]    [1 0 0]           
     F(I(x),y) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x = G(I(x))
                 [0 0 0]    [0 0 0]    [0]    [0 0 0]           
    problem:
     
    Qed