Problem:
 h(X,Z) -> f(X,s(X),Z)
 f(X,Y,g(X,Y)) -> h(0(),g(X,Y))
 g(0(),Y) -> 0()
 g(X,s(Y)) -> g(X,Y)

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [0] = 0,
   
   [g](x0, x1) = 4x0 + x1 + 1,
   
   [f](x0, x1, x2) = 4x0 + x1 + x2 + 1,
   
   [s](x0) = x0,
   
   [h](x0, x1) = 5x0 + x1 + 1
  orientation:
   h(X,Z) = 5X + Z + 1 >= 5X + Z + 1 = f(X,s(X),Z)
   
   f(X,Y,g(X,Y)) = 8X + 2Y + 2 >= 4X + Y + 2 = h(0(),g(X,Y))
   
   g(0(),Y) = Y + 1 >= 0 = 0()
   
   g(X,s(Y)) = 4X + Y + 1 >= 4X + Y + 1 = g(X,Y)
  problem:
   h(X,Z) -> f(X,s(X),Z)
   f(X,Y,g(X,Y)) -> h(0(),g(X,Y))
   g(X,s(Y)) -> g(X,Y)
  Matrix Interpretation Processor: dim=2
   
   interpretation:
          [0]
    [0] = [0],
    
                  [2 3]     [2 1]  
    [g](x0, x1) = [0 1]x0 + [2 0]x1,
    
                      [1 2]     [1 0]     [1 0]  
    [f](x0, x1, x2) = [0 0]x0 + [0 0]x1 + [1 2]x2,
    
              [1 0]     [0]
    [s](x0) = [2 1]x0 + [1],
    
                  [3 2]     [1 0]  
    [h](x0, x1) = [0 0]x0 + [1 2]x1
   orientation:
             [3 2]    [1 0]     [2 2]    [1 0]               
    h(X,Z) = [0 0]X + [1 2]Z >= [0 0]X + [1 2]Z = f(X,s(X),Z)
    
                    [3 5]    [3 1]     [2 3]    [2 1]                 
    f(X,Y,g(X,Y)) = [2 5]X + [6 1]Y >= [2 5]X + [6 1]Y = h(0(),g(X,Y))
    
                [2 3]    [4 1]    [1]    [2 3]    [2 1]          
    g(X,s(Y)) = [0 1]X + [2 0]Y + [0] >= [0 1]X + [2 0]Y = g(X,Y)
   problem:
    h(X,Z) -> f(X,s(X),Z)
    f(X,Y,g(X,Y)) -> h(0(),g(X,Y))
   Unfolding Processor:
    loop length: 2
    terms:
     h(0(),g(0(),s(0())))
     f(0(),s(0()),g(0(),s(0())))
    context: []
    substitution:
     
    Qed