YES
Time: 0.016866
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)}
 DP:
  DP:
   {     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)}
  UR:
   {}
   EDG:
    {(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)}
    STATUS:
     arrows: 0.666667
     SCCS (3):
      Scc:
       {f#(x, g(y, z)) -> f#(x, y)}
      Scc:
       {rem#(g(x, y), s z) -> rem#(x, z)}
      Scc:
       {norm# g(x, y) -> norm# x}
      
      SCC (1):
       Strict:
        {f#(x, g(y, z)) -> f#(x, y)}
       Weak:
       {       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)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [g](x0, x1) = x0 + 1,
         
         [f](x0, x1) = x0 + 1,
         
         [rem](x0, x1) = x0 + 1,
         
         [norm](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [0] = 0,
         
         [nil] = 1,
         
         [f#](x0, x1) = x0
        Strict:
         f#(x, g(y, z)) -> f#(x, y)
         1 + 0x + 1y + 0z >= 0 + 0x + 1y
        Weak:
         rem(g(x, y), s z) -> rem(x, z)
         2 + 1x + 0y + 0z >= 1 + 1x + 0z
         rem(g(x, y), 0()) -> g(x, y)
         2 + 1x + 0y >= 1 + 1x + 0y
         rem(nil(), y) -> nil()
         2 + 0y >= 1
         f(x, g(y, z)) -> g(f(x, y), z)
         2 + 0x + 1y + 0z >= 2 + 0x + 1y + 0z
         f(x, nil()) -> g(nil(), x)
         2 + 0x >= 2 + 0x
         norm g(x, y) -> s norm x
         2 + 1x + 0y >= 2 + 1x
         norm nil() -> 0()
         2 >= 0
       Qed
     SCC (1):
      Strict:
       {rem#(g(x, y), s z) -> rem#(x, z)}
      Weak:
      {       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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [g](x0, x1) = 1,
        
        [f](x0, x1) = x0 + 1,
        
        [rem](x0, x1) = 0,
        
        [norm](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [0] = 0,
        
        [nil] = 1,
        
        [rem#](x0, x1) = x0
       Strict:
        rem#(g(x, y), s z) -> rem#(x, z)
        1 + 0x + 0y + 1z >= 0 + 0x + 1z
       Weak:
        rem(g(x, y), s z) -> rem(x, z)
        0 + 0x + 0y + 0z >= 0 + 0x + 0z
        rem(g(x, y), 0()) -> g(x, y)
        0 + 0x + 0y >= 1 + 0x + 0y
        rem(nil(), y) -> nil()
        0 + 0y >= 1
        f(x, g(y, z)) -> g(f(x, y), z)
        2 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z
        f(x, nil()) -> g(nil(), x)
        2 + 0x >= 1 + 0x
        norm g(x, y) -> s norm x
        2 + 0x + 0y >= 2 + 1x
        norm nil() -> 0()
        2 >= 0
      Qed
     SCC (1):
      Strict:
       {norm# g(x, y) -> norm# x}
      Weak:
      {       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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [g](x0, x1) = x0 + 1,
        
        [f](x0, x1) = x0 + 1,
        
        [rem](x0, x1) = x0 + 1,
        
        [norm](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [0] = 0,
        
        [nil] = 1,
        
        [norm#](x0) = x0
       Strict:
        norm# g(x, y) -> norm# x
        1 + 1x + 0y >= 0 + 1x
       Weak:
        rem(g(x, y), s z) -> rem(x, z)
        2 + 1x + 0y + 0z >= 1 + 1x + 0z
        rem(g(x, y), 0()) -> g(x, y)
        2 + 1x + 0y >= 1 + 1x + 0y
        rem(nil(), y) -> nil()
        2 + 0y >= 1
        f(x, g(y, z)) -> g(f(x, y), z)
        2 + 0x + 1y + 0z >= 2 + 0x + 1y + 0z
        f(x, nil()) -> g(nil(), x)
        2 + 0x >= 2 + 0x
        norm g(x, y) -> s norm x
        2 + 1x + 0y >= 2 + 1x
        norm nil() -> 0()
        2 >= 0
      Qed