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