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

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  I(H(x31)) -> H(x31)
  F(H(x33),G(x32)) -> F(H(x33),I(I(G(x32))))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=2
   
   interpretation:
                  [1 1]     [2 0]     [0]
    [F](x0, x1) = [1 0]x0 + [0 0]x1 + [2],
    
              [1 0]     [1]
    [G](x0) = [0 0]x0 + [0],
    
              [1 0]     [3]
    [H](x0) = [2 0]x0 + [1],
    
              [1 2]  
    [I](x0) = [0 2]x0
   orientation:
                [5 0]      [5]    [1 0]      [3]         
    I(H(x31)) = [4 0]x31 + [2] >= [2 0]x31 + [1] = H(x31)
    
                       [2 0]      [3 0]      [6]    [2 0]      [3 0]      [6]                         
    F(H(x33),G(x32)) = [0 0]x32 + [1 0]x33 + [5] >= [0 0]x32 + [1 0]x33 + [5] = F(H(x33),I(I(G(x32))))
   problem:
    F(H(x33),G(x32)) -> F(H(x33),I(I(G(x32))))
   Matrix Interpretation Processor: dim=2
    
    interpretation:
                   [2 0]     [2 3]  
     [F](x0, x1) = [0 0]x0 + [2 2]x1,
     
               [1 0]     [1]
     [G](x0) = [1 2]x0 + [1],
     
               [2 0]  
     [H](x0) = [0 0]x0,
     
               [1 1]  
     [I](x0) = [0 0]x0
    orientation:
                        [5 6]      [4 0]      [5]    [4 4]      [4 0]      [4]                         
     F(H(x33),G(x32)) = [4 4]x32 + [0 0]x33 + [4] >= [4 4]x32 + [0 0]x33 + [4] = F(H(x33),I(I(G(x32))))
    problem:
     
    Qed