YES

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:
 DP Processor:
  DPs:
   norm#(g(x,y)) -> norm#(x)
   f#(x,g(y,z)) -> f#(x,y)
   rem#(g(x,y),s(z)) -> rem#(x,z)
  TRS:
   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)
  Usable Rule Processor:
   DPs:
    norm#(g(x,y)) -> norm#(x)
    f#(x,g(y,z)) -> f#(x,y)
    rem#(g(x,y),s(z)) -> rem#(x,z)
   TRS:
    
   Matrix Interpretation Processor: dim=4
    
    usable rules:
     
    interpretation:
     [rem#](x0, x1) = [0 1 1 1]x0 + [1 1 1 1]x1,
     
     [f#](x0, x1) = [1 0 0 0]x1 + [1],
     
     [norm#](x0) = [1 0 0 0]x0 + [1],
     
               [0 0 1 0]  
               [0 0 1 0]  
     [s](x0) = [0 1 1 1]x0
               [1 0 0 0]  ,
     
                   [1 0 0 0]     [1]
                   [1 1 1 0]     [0]
     [g](x0, x1) = [1 0 1 1]x0 + [1]
                   [1 0 0 0]     [0]
    orientation:
     norm#(g(x,y)) = [1 0 0 0]x + [2] >= [1 0 0 0]x + [1] = norm#(x)
     
     f#(x,g(y,z)) = [1 0 0 0]y + [2] >= [1 0 0 0]y + [1] = f#(x,y)
     
     rem#(g(x,y),s(z)) = [3 1 2 1]x + [1 1 3 1]z + [1] >= [0 1 1 1]x + [1 1 1 1]z = rem#(x,z)
    problem:
     DPs:
      
     TRS:
      
    Qed