Problem:
 g(0(),f(x,x)) -> x
 g(x,s(y)) -> g(f(x,y),0())
 g(s(x),y) -> g(f(x,y),0())
 g(f(x,y),0()) -> f(g(x,0()),g(y,0()))

Proof:
 Complexity Transformation Processor:
  strict:
   g(0(),f(x,x)) -> x
   g(x,s(y)) -> g(f(x,y),0())
   g(s(x),y) -> g(f(x,y),0())
   g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [s](x0) = x0,
     
     [g](x0, x1) = x0 + x1 + 1,
     
     [f](x0, x1) = x0 + x1 + 3,
     
     [0] = 0
    orientation:
     g(0(),f(x,x)) = 2x + 4 >= x = x
     
     g(x,s(y)) = x + y + 1 >= x + y + 4 = g(f(x,y),0())
     
     g(s(x),y) = x + y + 1 >= x + y + 4 = g(f(x,y),0())
     
     g(f(x,y),0()) = x + y + 4 >= x + y + 5 = f(g(x,0()),g(y,0()))
    problem:
     strict:
      g(x,s(y)) -> g(f(x,y),0())
      g(s(x),y) -> g(f(x,y),0())
      g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
     weak:
      g(0(),f(x,x)) -> x
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [s](x0) = x0 + 1,
       
       [g](x0, x1) = x0 + x1,
       
       [f](x0, x1) = x0 + x1,
       
       [0] = 0
      orientation:
       g(x,s(y)) = x + y + 1 >= x + y = g(f(x,y),0())
       
       g(s(x),y) = x + y + 1 >= x + y = g(f(x,y),0())
       
       g(f(x,y),0()) = x + y >= x + y = f(g(x,0()),g(y,0()))
       
       g(0(),f(x,x)) = 2x >= x = x
      problem:
       strict:
        g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
       weak:
        g(x,s(y)) -> g(f(x,y),0())
        g(s(x),y) -> g(f(x,y),0())
        g(0(),f(x,x)) -> x
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 3]
        [0 1]
        interpretation:
                        [3]
         [s](x0) = x0 + [3],
         
                       [1 3]     [1 3]     [3]
         [g](x0, x1) = [0 1]x0 + [0 1]x1 + [0],
         
                                 [0]
         [f](x0, x1) = x0 + x1 + [3],
         
               [1]
         [0] = [0]
        orientation:
                         [1 3]    [1 3]    [13]    [1 3]    [1 3]    [8]                       
         g(f(x,y),0()) = [0 1]x + [0 1]y + [3 ] >= [0 1]x + [0 1]y + [3] = f(g(x,0()),g(y,0()))
         
                     [1 3]    [1 3]    [15]    [1 3]    [1 3]    [13]                
         g(x,s(y)) = [0 1]x + [0 1]y + [3 ] >= [0 1]x + [0 1]y + [3 ] = g(f(x,y),0())
         
                     [1 3]    [1 3]    [15]    [1 3]    [1 3]    [13]                
         g(s(x),y) = [0 1]x + [0 1]y + [3 ] >= [0 1]x + [0 1]y + [3 ] = g(f(x,y),0())
         
                         [2 6]    [13]         
         g(0(),f(x,x)) = [0 2]x + [3 ] >= x = x
        problem:
         strict:
          
         weak:
          g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
          g(x,s(y)) -> g(f(x,y),0())
          g(s(x),y) -> g(f(x,y),0())
          g(0(),f(x,x)) -> x
        Qed