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:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [rem](x0, x1) = x0 + x1 + 1,
     
     [f](x0, x1) = x0 + x1 + 1,
     
     [s](x0) = x0,
     
     [g](x0, x1) = x0 + x1 + 1,
     
     [0] = 0,
     
     [norm](x0) = x0,
     
     [nil] = 1
    orientation:
     norm(nil()) = 1 >= 0 = 0()
     
     norm(g(x,y)) = x + y + 1 >= x = s(norm(x))
     
     f(x,nil()) = x + 2 >= x + 2 = g(nil(),x)
     
     f(x,g(y,z)) = x + y + z + 2 >= x + y + z + 2 = g(f(x,y),z)
     
     rem(nil(),y) = y + 2 >= 1 = nil()
     
     rem(g(x,y),0()) = x + y + 2 >= x + y + 1 = g(x,y)
     
     rem(g(x,y),s(z)) = x + y + z + 2 >= x + z + 1 = 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
     max_matrix:
      1
      interpretation:
       [rem](x0, x1) = x0 + x1,
       
       [f](x0, x1) = x0 + x1 + 1,
       
       [s](x0) = x0,
       
       [g](x0, x1) = x0 + x1,
       
       [0] = 0,
       
       [norm](x0) = x0,
       
       [nil] = 0
      orientation:
       f(x,nil()) = x + 1 >= x = g(nil(),x)
       
       f(x,g(y,z)) = x + y + z + 1 >= x + y + z + 1 = g(f(x,y),z)
       
       norm(nil()) = 0 >= 0 = 0()
       
       norm(g(x,y)) = x + y >= x = s(norm(x))
       
       rem(nil(),y) = y >= 0 = nil()
       
       rem(g(x,y),0()) = x + y >= x + y = g(x,y)
       
       rem(g(x,y),s(z)) = x + y + z >= 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
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
                         [1 1]     [1 0]     [1]
         [rem](x0, x1) = [0 1]x0 + [0 0]x1 + [1],
         
                       [1 0]     [1 1]     [1]
         [f](x0, x1) = [0 0]x0 + [0 1]x1 + [1],
         
                   [1 0]     [0]
         [s](x0) = [0 0]x0 + [1],
         
                            [1 0]     [0]
         [g](x0, x1) = x0 + [0 0]x1 + [1],
         
               [0]
         [0] = [0],
         
                      [1 0]     [0]
         [norm](x0) = [0 0]x0 + [1],
         
                 [1]
         [nil] = [0]
        orientation:
                       [1 0]    [1 1]    [1 0]    [2]    [1 0]    [1 1]    [1 0]    [1]              
         f(x,g(y,z)) = [0 0]x + [0 1]y + [0 0]z + [2] >= [0 0]x + [0 1]y + [0 0]z + [2] = g(f(x,y),z)
         
                      [1 0]    [2]    [1 0]    [1]             
         f(x,nil()) = [0 0]x + [1] >= [0 0]x + [1] = g(nil(),x)
         
                       [1]    [0]      
         norm(nil()) = [1] >= [0] = 0()
         
                        [1 0]    [1 0]    [0]    [1 0]    [0]             
         norm(g(x,y)) = [0 0]x + [0 0]y + [1] >= [0 0]x + [1] = s(norm(x))
         
                        [1 0]    [2]    [1]        
         rem(nil(),y) = [0 0]y + [1] >= [0] = nil()
         
                           [1 1]    [1 0]    [2]        [1 0]    [0]         
         rem(g(x,y),0()) = [0 1]x + [0 0]y + [2] >= x + [0 0]y + [1] = g(x,y)
         
                            [1 1]    [1 0]    [1 0]    [2]    [1 1]    [1 0]    [1]           
         rem(g(x,y),s(z)) = [0 1]x + [0 0]y + [0 0]z + [2] >= [0 1]x + [0 0]z + [1] = 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