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