YES(?,O(n^2))

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:
 RT 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
   interpretation:
    [s](x0) = x0 + 2,
    
    [g](x0, x1) = x0 + x1 + 12,
    
    [f](x0, x1) = x0 + x1,
    
    [0] = 4
   orientation:
    g(0(),f(x,x)) = 2x + 16 >= x = x
    
    g(x,s(y)) = x + y + 14 >= x + y + 16 = g(f(x,y),0())
    
    g(s(x),y) = x + y + 14 >= x + y + 16 = g(f(x,y),0())
    
    g(f(x,y),0()) = x + y + 16 >= x + y + 32 = 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
    interpretation:
     [s](x0) = x0 + 13,
     
     [g](x0, x1) = x0 + x1,
     
     [f](x0, x1) = x0 + x1 + 9,
     
     [0] = 0
    orientation:
     g(x,s(y)) = x + y + 13 >= x + y + 9 = g(f(x,y),0())
     
     g(s(x),y) = x + y + 13 >= x + y + 9 = g(f(x,y),0())
     
     g(f(x,y),0()) = x + y + 9 >= x + y + 9 = f(g(x,0()),g(y,0()))
     
     g(0(),f(x,x)) = 2x + 9 >= 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
     interpretation:
                [1  15]     [8]
      [s](x0) = [0  1 ]x0 + [8],
      
                    [1 1]     [1 2]     [1]
      [g](x0, x1) = [0 1]x0 + [0 1]x1 + [0],
      
                              [13]
      [f](x0, x1) = x0 + x1 + [2 ],
      
            [0]
      [0] = [0]
     orientation:
                      [1 1]    [1 1]    [16]    [1 1]    [1 1]    [15]                       
      g(f(x,y),0()) = [0 1]x + [0 1]y + [2 ] >= [0 1]x + [0 1]y + [2 ] = f(g(x,0()),g(y,0()))
      
                  [1 1]    [1  17]    [25]    [1 1]    [1 1]    [16]                
      g(x,s(y)) = [0 1]x + [0  1 ]y + [8 ] >= [0 1]x + [0 1]y + [2 ] = g(f(x,y),0())
      
                  [1  16]    [1 2]    [17]    [1 1]    [1 1]    [16]                
      g(s(x),y) = [0  1 ]x + [0 1]y + [8 ] >= [0 1]x + [0 1]y + [2 ] = g(f(x,y),0())
      
                      [2 4]    [18]         
      g(0(),f(x,x)) = [0 2]x + [2 ] >= 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