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:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                   [1 4]     [1 1]     [0]
   [rem](x0, x1) = [0 1]x0 + [0 0]x1 + [5],
   
                 [1  14]     [1 2]     [1 ]
   [f](x0, x1) = [0  0 ]x0 + [0 1]x1 + [10],
   
             [1 8]     [1]
   [s](x0) = [0 0]x0 + [1],
   
                      [1  10]     [0]
   [g](x0, x1) = x0 + [0  0 ]x1 + [4],
   
         [7]
   [0] = [1],
   
                [1 4]     [0]
   [norm](x0) = [0 0]x0 + [1],
   
           [0]
   [nil] = [7]
  orientation:
                 [28]    [7]      
   norm(nil()) = [1 ] >= [1] = 0()
   
                  [1 4]    [1  10]    [16]    [1 4]    [9]             
   norm(g(x,y)) = [0 0]x + [0  0 ]y + [1 ] >= [0 0]x + [1] = s(norm(x))
   
                [1  14]    [15]    [1  10]    [0 ]             
   f(x,nil()) = [0  0 ]x + [17] >= [0  0 ]x + [11] = g(nil(),x)
   
                 [1  14]    [1 2]    [1  10]    [9 ]    [1  14]    [1 2]    [1  10]    [1 ]              
   f(x,g(y,z)) = [0  0 ]x + [0 1]y + [0  0 ]z + [14] >= [0  0 ]x + [0 1]y + [0  0 ]z + [14] = g(f(x,y),z)
   
                  [1 1]    [28]    [0]        
   rem(nil(),y) = [0 0]y + [12] >= [7] = nil()
   
                     [1 4]    [1  10]    [24]        [1  10]    [0]         
   rem(g(x,y),0()) = [0 1]x + [0  0 ]y + [9 ] >= x + [0  0 ]y + [4] = g(x,y)
   
                      [1 4]    [1  10]    [1 8]    [18]    [1 4]    [1 1]    [0]           
   rem(g(x,y),s(z)) = [0 1]x + [0  0 ]y + [0 0]z + [9 ] >= [0 1]x + [0 0]z + [5] = rem(x,z)
  problem:
   
  Qed