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:
    
   ADG 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:
     
    graph:
     rem#(g(x,y),s(z)) -> rem#(x,z) -> rem#(g(x,y),s(z)) -> rem#(x,z)
     f#(x,g(y,z)) -> f#(x,y) -> f#(x,g(y,z)) -> f#(x,y)
     norm#(g(x,y)) -> norm#(x) -> norm#(g(x,y)) -> norm#(x)
    Restore Modifier:
     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)
     SCC Processor:
      #sccs: 3
      #rules: 3
      #arcs: 3/9
      DPs:
       norm#(g(x,y)) -> norm#(x)
      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)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [norm#](x0) = x0 + 1,
        
        [rem](x0, x1) = x0,
        
        [f](x0, x1) = x1 + 1,
        
        [s](x0) = 1,
        
        [g](x0, x1) = x0 + 1,
        
        [0] = 0,
        
        [norm](x0) = 1,
        
        [nil] = 0
       orientation:
        norm#(g(x,y)) = x + 2 >= x + 1 = norm#(x)
        
        norm(nil()) = 1 >= 0 = 0()
        
        norm(g(x,y)) = 1 >= 1 = s(norm(x))
        
        f(x,nil()) = 1 >= 1 = g(nil(),x)
        
        f(x,g(y,z)) = y + 2 >= y + 2 = g(f(x,y),z)
        
        rem(nil(),y) = 0 >= 0 = nil()
        
        rem(g(x,y),0()) = x + 1 >= x + 1 = g(x,y)
        
        rem(g(x,y),s(z)) = x + 1 >= x = rem(x,z)
       problem:
        DPs:
         
        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)
       Qed
      
      DPs:
       f#(x,g(y,z)) -> f#(x,y)
      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)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0, x1) = x1,
        
        [rem](x0, x1) = x0 + x1,
        
        [f](x0, x1) = x1 + 1,
        
        [s](x0) = x0,
        
        [g](x0, x1) = x0 + 1,
        
        [0] = 1,
        
        [norm](x0) = 1,
        
        [nil] = 1
       orientation:
        f#(x,g(y,z)) = y + 1 >= y = f#(x,y)
        
        norm(nil()) = 1 >= 1 = 0()
        
        norm(g(x,y)) = 1 >= 1 = s(norm(x))
        
        f(x,nil()) = 2 >= 2 = g(nil(),x)
        
        f(x,g(y,z)) = y + 2 >= y + 2 = g(f(x,y),z)
        
        rem(nil(),y) = y + 1 >= 1 = nil()
        
        rem(g(x,y),0()) = x + 2 >= x + 1 = g(x,y)
        
        rem(g(x,y),s(z)) = x + z + 1 >= x + z = rem(x,z)
       problem:
        DPs:
         
        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)
       Qed
      
      DPs:
       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)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [rem#](x0, x1) = x0 + x1,
        
        [rem](x0, x1) = x0,
        
        [f](x0, x1) = x1 + 1,
        
        [s](x0) = x0 + 1,
        
        [g](x0, x1) = x0 + 1,
        
        [0] = 1,
        
        [norm](x0) = x0 + 1,
        
        [nil] = 0
       orientation:
        rem#(g(x,y),s(z)) = x + z + 2 >= x + z = rem#(x,z)
        
        norm(nil()) = 1 >= 1 = 0()
        
        norm(g(x,y)) = x + 2 >= x + 2 = s(norm(x))
        
        f(x,nil()) = 1 >= 1 = g(nil(),x)
        
        f(x,g(y,z)) = y + 2 >= y + 2 = g(f(x,y),z)
        
        rem(nil(),y) = 0 >= 0 = nil()
        
        rem(g(x,y),0()) = x + 1 >= x + 1 = g(x,y)
        
        rem(g(x,y),s(z)) = x + 1 >= x = rem(x,z)
       problem:
        DPs:
         
        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)
       Qed