MAYBE
MAYBE
TRS:
 {
                and(tt(), T) -> T,
    isNatList(n__cons(N, L)) ->
  and(isNat(activate(N)), isNatList(activate(L))),
         isNatList(n__nil()) -> tt(),
   isNatList(n__take(N, IL)) ->
  and(isNat(activate(N)), isNatIList(activate(IL))),
                 activate(X) -> X,
            activate(n__0()) -> 0(),
           activate(n__s(X)) -> s(X),
      activate(n__length(X)) -> length(X),
        activate(n__zeros()) -> zeros(),
   activate(n__cons(X1, X2)) -> cons(X1, X2),
          activate(n__nil()) -> nil(),
   activate(n__take(X1, X2)) -> take(X1, X2),
              isNatIList(IL) -> isNatList(activate(IL)),
      isNatIList(n__zeros()) -> tt(),
  isNatIList(n__cons(N, IL)) ->
  and(isNat(activate(N)), isNatIList(activate(IL))),
               isNat(n__0()) -> tt(),
              isNat(n__s(N)) -> isNat(activate(N)),
         isNat(n__length(L)) -> isNatList(activate(L)),
                cons(X1, X2) -> n__cons(X1, X2),
                         0() -> n__0(),
                     zeros() -> n__zeros(),
                     zeros() -> cons(0(), n__zeros()),
                uTake1(tt()) -> nil(),
                take(X1, X2) -> n__take(X1, X2),
               take(0(), IL) -> uTake1(isNatIList(IL)),
     take(s(M), cons(N, IL)) ->
  uTake2(
        and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N,
        activate(IL)
  ),
                       nil() -> n__nil(),
      uTake2(tt(), M, N, IL) ->
  cons(activate(N), n__take(activate(M), activate(IL))),
                        s(X) -> n__s(X),
            uLength(tt(), L) -> s(length(activate(L))),
                   length(X) -> n__length(X),
          length(cons(N, L)) ->
  uLength(and(isNat(N), isNatList(activate(L))), activate(L))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                  and(tt(), T) -> T,
      isNatList(n__cons(N, L)) ->
    and(isNat(activate(N)), isNatList(activate(L))),
           isNatList(n__nil()) -> tt(),
     isNatList(n__take(N, IL)) ->
    and(isNat(activate(N)), isNatIList(activate(IL))),
                   activate(X) -> X,
              activate(n__0()) -> 0(),
             activate(n__s(X)) -> s(X),
        activate(n__length(X)) -> length(X),
          activate(n__zeros()) -> zeros(),
     activate(n__cons(X1, X2)) -> cons(X1, X2),
            activate(n__nil()) -> nil(),
     activate(n__take(X1, X2)) -> take(X1, X2),
                isNatIList(IL) -> isNatList(activate(IL)),
        isNatIList(n__zeros()) -> tt(),
    isNatIList(n__cons(N, IL)) ->
    and(isNat(activate(N)), isNatIList(activate(IL))),
                 isNat(n__0()) -> tt(),
                isNat(n__s(N)) -> isNat(activate(N)),
           isNat(n__length(L)) -> isNatList(activate(L)),
                  cons(X1, X2) -> n__cons(X1, X2),
                           0() -> n__0(),
                       zeros() -> n__zeros(),
                       zeros() -> cons(0(), n__zeros()),
                  uTake1(tt()) -> nil(),
                  take(X1, X2) -> n__take(X1, X2),
                 take(0(), IL) -> uTake1(isNatIList(IL)),
       take(s(M), cons(N, IL)) ->
    uTake2(
          and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, 
          N, activate(IL)
    ),
                         nil() -> n__nil(),
        uTake2(tt(), M, N, IL) ->
    cons(activate(N), n__take(activate(M), activate(IL))),
                          s(X) -> n__s(X),
              uLength(tt(), L) -> s(length(activate(L))),
                     length(X) -> n__length(X),
            length(cons(N, L)) ->
    uLength(and(isNat(N), isNatList(activate(L))), activate(L))
   }
  Fail