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)}
 LMPO:
  Quasi-Precedence:
  empty
  
Normal:
   pi(rem) = [1,2], pi(f) = [1,2], pi(norm) = [1]
  
Safe:
   
  
Predicative System:
   {       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