MAYBE
MAYBE
TRS:
 {
         and(tt(), T) -> T,
          isNatList() -> and(isNat(), isNatList()),
          isNatList() -> and(isNat(), isNatIList()),
          isNatList() -> tt(),
         isNatIList() -> and(isNat(), isNatIList()),
         isNatIList() -> tt(),
         isNatIList() -> isNatList(),
              isNat() -> tt(),
              isNat() -> isNatList(),
              isNat() -> isNat(),
              zeros() -> cons(0()),
         uTake1(tt()) -> nil(),
        take(0(), IL) -> uTake1(isNatIList()),
  take(s(M), cons(N)) -> uTake2(and(isNat(), and(isNat(), isNatIList()))),
         uTake2(tt()) -> cons(N),
        uLength(tt()) -> s(length(L)),
      length(cons(N)) -> uLength(and(isNat(), isNatList()))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
           and(tt(), T) -> T,
            isNatList() -> and(isNat(), isNatList()),
            isNatList() -> and(isNat(), isNatIList()),
            isNatList() -> tt(),
           isNatIList() -> and(isNat(), isNatIList()),
           isNatIList() -> tt(),
           isNatIList() -> isNatList(),
                isNat() -> tt(),
                isNat() -> isNatList(),
                isNat() -> isNat(),
                zeros() -> cons(0()),
           uTake1(tt()) -> nil(),
          take(0(), IL) -> uTake1(isNatIList()),
    take(s(M), cons(N)) -> uTake2(and(isNat(), and(isNat(), isNatIList()))),
           uTake2(tt()) -> cons(N),
          uLength(tt()) -> s(length(L)),
        length(cons(N)) -> uLength(and(isNat(), isNatList()))
   }
  Fail