MAYBE
MAYBE
TRS:
 {
                   eq(X, Y) -> false(),
         eq(n__0(), n__0()) -> true(),
       eq(n__s(X), n__s(Y)) -> eq(activate(X), activate(Y)),
                activate(X) -> X,
           activate(n__0()) -> 0(),
          activate(n__s(X)) -> s(X),
        activate(n__inf(X)) -> inf(activate(X)),
  activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
     activate(n__length(X)) -> length(activate(X)),
                     inf(X) -> cons(X, n__inf(n__s(X))),
                     inf(X) -> n__inf(X),
               take(X1, X2) -> n__take(X1, X2),
               take(0(), X) -> nil(),
     take(s(X), cons(Y, L)) ->
  cons(activate(Y), n__take(activate(X), activate(L))),
                        0() -> n__0(),
                       s(X) -> n__s(X),
                  length(X) -> n__length(X),
         length(cons(X, L)) -> s(n__length(activate(L))),
              length(nil()) -> 0()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                     eq(X, Y) -> false(),
           eq(n__0(), n__0()) -> true(),
         eq(n__s(X), n__s(Y)) -> eq(activate(X), activate(Y)),
                  activate(X) -> X,
             activate(n__0()) -> 0(),
            activate(n__s(X)) -> s(X),
          activate(n__inf(X)) -> inf(activate(X)),
    activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
       activate(n__length(X)) -> length(activate(X)),
                       inf(X) -> cons(X, n__inf(n__s(X))),
                       inf(X) -> n__inf(X),
                 take(X1, X2) -> n__take(X1, X2),
                 take(0(), X) -> nil(),
       take(s(X), cons(Y, L)) ->
    cons(activate(Y), n__take(activate(X), activate(L))),
                          0() -> n__0(),
                         s(X) -> n__s(X),
                    length(X) -> n__length(X),
           length(cons(X, L)) -> s(n__length(activate(L))),
                length(nil()) -> 0()
   }
  Fail