YES(?,O(n^2))

Problem:
 norm(nil()) -> 0()
 norm(g(x,y)) -> s(norm(x))
 f(x,nil()) -> g(nil(),x)
 f(x,g(y,z)) -> g(f(x,y),z)
 rem(nil(),y) -> nil()
 rem(g(x,y),0()) -> g(x,y)
 rem(g(x,y),s(z)) -> rem(x,z)

Proof:
 RT Transformation Processor:
  strict:
   norm(nil()) -> 0()
   norm(g(x,y)) -> s(norm(x))
   f(x,nil()) -> g(nil(),x)
   f(x,g(y,z)) -> g(f(x,y),z)
   rem(nil(),y) -> nil()
   rem(g(x,y),0()) -> g(x,y)
   rem(g(x,y),s(z)) -> rem(x,z)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [rem](x0, x1) = x0 + x1 + 14,
    
    [f](x0, x1) = x0 + x1 + 14,
    
    [s](x0) = x0 + 14,
    
    [g](x0, x1) = x0 + x1 + 19,
    
    [0] = 0,
    
    [norm](x0) = x0 + 10,
    
    [nil] = 16
   orientation:
    norm(nil()) = 26 >= 0 = 0()
    
    norm(g(x,y)) = x + y + 29 >= x + 24 = s(norm(x))
    
    f(x,nil()) = x + 30 >= x + 35 = g(nil(),x)
    
    f(x,g(y,z)) = x + y + z + 33 >= x + y + z + 33 = g(f(x,y),z)
    
    rem(nil(),y) = y + 30 >= 16 = nil()
    
    rem(g(x,y),0()) = x + y + 33 >= x + y + 19 = g(x,y)
    
    rem(g(x,y),s(z)) = x + y + z + 47 >= x + z + 14 = rem(x,z)
   problem:
    strict:
     f(x,nil()) -> g(nil(),x)
     f(x,g(y,z)) -> g(f(x,y),z)
    weak:
     norm(nil()) -> 0()
     norm(g(x,y)) -> s(norm(x))
     rem(nil(),y) -> nil()
     rem(g(x,y),0()) -> g(x,y)
     rem(g(x,y),s(z)) -> rem(x,z)
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [rem](x0, x1) = x0 + x1,
     
     [f](x0, x1) = x0 + x1 + 8,
     
     [s](x0) = x0 + 4,
     
     [g](x0, x1) = x0 + x1 + 4,
     
     [0] = 8,
     
     [norm](x0) = x0 + 4,
     
     [nil] = 4
    orientation:
     f(x,nil()) = x + 12 >= x + 8 = g(nil(),x)
     
     f(x,g(y,z)) = x + y + z + 12 >= x + y + z + 12 = g(f(x,y),z)
     
     norm(nil()) = 8 >= 8 = 0()
     
     norm(g(x,y)) = x + y + 8 >= x + 8 = s(norm(x))
     
     rem(nil(),y) = y + 4 >= 4 = nil()
     
     rem(g(x,y),0()) = x + y + 12 >= x + y + 4 = g(x,y)
     
     rem(g(x,y),s(z)) = x + y + z + 8 >= x + z = rem(x,z)
    problem:
     strict:
      f(x,g(y,z)) -> g(f(x,y),z)
     weak:
      f(x,nil()) -> g(nil(),x)
      norm(nil()) -> 0()
      norm(g(x,y)) -> s(norm(x))
      rem(nil(),y) -> nil()
      rem(g(x,y),0()) -> g(x,y)
      rem(g(x,y),s(z)) -> rem(x,z)
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                      [1 1]     [1 5]     [5 ]
      [rem](x0, x1) = [0 1]x0 + [0 0]x1 + [14],
      
                    [1 6]     [1 1]     [0]
      [f](x0, x1) = [0 1]x0 + [0 1]x1 + [4],
      
                [1  11]     [14]
      [s](x0) = [0  1 ]x0 + [0 ],
      
                         [1 1]     [0]
      [g](x0, x1) = x0 + [0 1]x1 + [2],
      
            [0]
      [0] = [0],
      
                   [1 8]     [1]
      [norm](x0) = [0 0]x0 + [0],
      
              [15]
      [nil] = [0 ]
     orientation:
                    [1 6]    [1 1]    [1 2]    [2]    [1 6]    [1 1]    [1 1]    [0]              
      f(x,g(y,z)) = [0 1]x + [0 1]y + [0 1]z + [6] >= [0 1]x + [0 1]y + [0 1]z + [6] = g(f(x,y),z)
      
                   [1 6]    [15]    [1 1]    [15]             
      f(x,nil()) = [0 1]x + [4 ] >= [0 1]x + [2 ] = g(nil(),x)
      
                    [16]    [0]      
      norm(nil()) = [0 ] >= [0] = 0()
      
                     [1 8]    [1 9]    [17]    [1 8]    [15]             
      norm(g(x,y)) = [0 0]x + [0 0]y + [0 ] >= [0 0]x + [0 ] = s(norm(x))
      
                     [1 5]    [20]    [15]        
      rem(nil(),y) = [0 0]y + [14] >= [0 ] = nil()
      
                        [1 1]    [1 2]    [7 ]        [1 1]    [0]         
      rem(g(x,y),0()) = [0 1]x + [0 1]y + [16] >= x + [0 1]y + [2] = g(x,y)
      
                         [1 1]    [1 2]    [1  16]    [21]    [1 1]    [1 5]    [5 ]           
      rem(g(x,y),s(z)) = [0 1]x + [0 1]y + [0  0 ]z + [16] >= [0 1]x + [0 0]z + [14] = rem(x,z)
     problem:
      strict:
       
      weak:
       f(x,g(y,z)) -> g(f(x,y),z)
       f(x,nil()) -> g(nil(),x)
       norm(nil()) -> 0()
       norm(g(x,y)) -> s(norm(x))
       rem(nil(),y) -> nil()
       rem(g(x,y),0()) -> g(x,y)
       rem(g(x,y),s(z)) -> rem(x,z)
     Qed