MAYBE Problem: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) Proof: DP Processor: DPs: active#(zeros()) -> cons#(0(),zeros()) active#(zeros()) -> mark#(cons(0(),zeros())) active#(U11(tt(),L)) -> length#(L) active#(U11(tt(),L)) -> s#(length(L)) active#(U11(tt(),L)) -> mark#(s(length(L))) active#(and(tt(),X)) -> mark#(X) active#(isNat(0())) -> mark#(tt()) active#(isNat(length(V1))) -> isNatList#(V1) active#(isNat(length(V1))) -> mark#(isNatList(V1)) active#(isNat(s(V1))) -> isNat#(V1) active#(isNat(s(V1))) -> mark#(isNat(V1)) active#(isNatIList(V)) -> isNatList#(V) active#(isNatIList(V)) -> mark#(isNatList(V)) active#(isNatIList(zeros())) -> mark#(tt()) active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) active#(isNatIList(cons(V1,V2))) -> isNat#(V1) active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) active#(isNatList(nil())) -> mark#(tt()) active#(isNatList(cons(V1,V2))) -> isNatList#(V2) active#(isNatList(cons(V1,V2))) -> isNat#(V1) active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) active#(length(nil())) -> mark#(0()) active#(length(cons(N,L))) -> isNat#(N) active#(length(cons(N,L))) -> isNatList#(L) active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(zeros()) -> active#(zeros()) mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(0()) -> active#(0()) mark#(U11(X1,X2)) -> mark#(X1) mark#(U11(X1,X2)) -> U11#(mark(X1),X2) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) mark#(tt()) -> active#(tt()) mark#(s(X)) -> mark#(X) mark#(s(X)) -> s#(mark(X)) mark#(s(X)) -> active#(s(mark(X))) mark#(length(X)) -> mark#(X) mark#(length(X)) -> length#(mark(X)) mark#(length(X)) -> active#(length(mark(X))) mark#(and(X1,X2)) -> mark#(X1) mark#(and(X1,X2)) -> and#(mark(X1),X2) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) mark#(isNat(X)) -> active#(isNat(X)) mark#(isNatList(X)) -> active#(isNatList(X)) mark#(isNatIList(X)) -> active#(isNatIList(X)) mark#(nil()) -> active#(nil()) cons#(mark(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) U11#(mark(X1),X2) -> U11#(X1,X2) U11#(X1,mark(X2)) -> U11#(X1,X2) U11#(active(X1),X2) -> U11#(X1,X2) U11#(X1,active(X2)) -> U11#(X1,X2) s#(mark(X)) -> s#(X) s#(active(X)) -> s#(X) length#(mark(X)) -> length#(X) length#(active(X)) -> length#(X) and#(mark(X1),X2) -> and#(X1,X2) and#(X1,mark(X2)) -> and#(X1,X2) and#(active(X1),X2) -> and#(X1,X2) and#(X1,active(X2)) -> and#(X1,X2) isNat#(mark(X)) -> isNat#(X) isNat#(active(X)) -> isNat#(X) isNatList#(mark(X)) -> isNatList#(X) isNatList#(active(X)) -> isNatList#(X) isNatIList#(mark(X)) -> isNatIList#(X) isNatIList#(active(X)) -> isNatIList#(X) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) EDG Processor: DPs: active#(zeros()) -> cons#(0(),zeros()) active#(zeros()) -> mark#(cons(0(),zeros())) active#(U11(tt(),L)) -> length#(L) active#(U11(tt(),L)) -> s#(length(L)) active#(U11(tt(),L)) -> mark#(s(length(L))) active#(and(tt(),X)) -> mark#(X) active#(isNat(0())) -> mark#(tt()) active#(isNat(length(V1))) -> isNatList#(V1) active#(isNat(length(V1))) -> mark#(isNatList(V1)) active#(isNat(s(V1))) -> isNat#(V1) active#(isNat(s(V1))) -> mark#(isNat(V1)) active#(isNatIList(V)) -> isNatList#(V) active#(isNatIList(V)) -> mark#(isNatList(V)) active#(isNatIList(zeros())) -> mark#(tt()) active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) active#(isNatIList(cons(V1,V2))) -> isNat#(V1) active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) active#(isNatList(nil())) -> mark#(tt()) active#(isNatList(cons(V1,V2))) -> isNatList#(V2) active#(isNatList(cons(V1,V2))) -> isNat#(V1) active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) active#(length(nil())) -> mark#(0()) active#(length(cons(N,L))) -> isNat#(N) active#(length(cons(N,L))) -> isNatList#(L) active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(zeros()) -> active#(zeros()) mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(0()) -> active#(0()) mark#(U11(X1,X2)) -> mark#(X1) mark#(U11(X1,X2)) -> U11#(mark(X1),X2) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) mark#(tt()) -> active#(tt()) mark#(s(X)) -> mark#(X) mark#(s(X)) -> s#(mark(X)) mark#(s(X)) -> active#(s(mark(X))) mark#(length(X)) -> mark#(X) mark#(length(X)) -> length#(mark(X)) mark#(length(X)) -> active#(length(mark(X))) mark#(and(X1,X2)) -> mark#(X1) mark#(and(X1,X2)) -> and#(mark(X1),X2) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) mark#(isNat(X)) -> active#(isNat(X)) mark#(isNatList(X)) -> active#(isNatList(X)) mark#(isNatIList(X)) -> active#(isNatIList(X)) mark#(nil()) -> active#(nil()) cons#(mark(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) U11#(mark(X1),X2) -> U11#(X1,X2) U11#(X1,mark(X2)) -> U11#(X1,X2) U11#(active(X1),X2) -> U11#(X1,X2) U11#(X1,active(X2)) -> U11#(X1,X2) s#(mark(X)) -> s#(X) s#(active(X)) -> s#(X) length#(mark(X)) -> length#(X) length#(active(X)) -> length#(X) and#(mark(X1),X2) -> and#(X1,X2) and#(X1,mark(X2)) -> and#(X1,X2) and#(active(X1),X2) -> and#(X1,X2) and#(X1,active(X2)) -> and#(X1,X2) isNat#(mark(X)) -> isNat#(X) isNat#(active(X)) -> isNat#(X) isNatList#(mark(X)) -> isNatList#(X) isNatList#(active(X)) -> isNatList#(X) isNatIList#(mark(X)) -> isNatIList#(X) isNatIList#(active(X)) -> isNatIList#(X) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) graph: U11#(mark(X1),X2) -> U11#(X1,X2) -> U11#(mark(X1),X2) -> U11#(X1,X2) U11#(mark(X1),X2) -> U11#(X1,X2) -> U11#(X1,mark(X2)) -> U11#(X1,X2) U11#(mark(X1),X2) -> U11#(X1,X2) -> U11#(active(X1),X2) -> U11#(X1,X2) U11#(mark(X1),X2) -> U11#(X1,X2) -> U11#(X1,active(X2)) -> U11#(X1,X2) U11#(active(X1),X2) -> U11#(X1,X2) -> U11#(mark(X1),X2) -> U11#(X1,X2) U11#(active(X1),X2) -> U11#(X1,X2) -> U11#(X1,mark(X2)) -> U11#(X1,X2) U11#(active(X1),X2) -> U11#(X1,X2) -> U11#(active(X1),X2) -> U11#(X1,X2) U11#(active(X1),X2) -> U11#(X1,X2) -> U11#(X1,active(X2)) -> U11#(X1,X2) U11#(X1,mark(X2)) -> U11#(X1,X2) -> U11#(mark(X1),X2) -> U11#(X1,X2) U11#(X1,mark(X2)) -> U11#(X1,X2) -> U11#(X1,mark(X2)) -> U11#(X1,X2) U11#(X1,mark(X2)) -> U11#(X1,X2) -> U11#(active(X1),X2) -> U11#(X1,X2) U11#(X1,mark(X2)) -> U11#(X1,X2) -> U11#(X1,active(X2)) -> U11#(X1,X2) U11#(X1,active(X2)) -> U11#(X1,X2) -> U11#(mark(X1),X2) -> U11#(X1,X2) U11#(X1,active(X2)) -> U11#(X1,X2) -> U11#(X1,mark(X2)) -> U11#(X1,X2) U11#(X1,active(X2)) -> U11#(X1,X2) -> U11#(active(X1),X2) -> U11#(X1,X2) U11#(X1,active(X2)) -> U11#(X1,X2) -> U11#(X1,active(X2)) -> U11#(X1,X2) and#(mark(X1),X2) -> and#(X1,X2) -> and#(mark(X1),X2) -> and#(X1,X2) and#(mark(X1),X2) -> and#(X1,X2) -> and#(X1,mark(X2)) -> and#(X1,X2) and#(mark(X1),X2) -> and#(X1,X2) -> and#(active(X1),X2) -> and#(X1,X2) and#(mark(X1),X2) -> and#(X1,X2) -> and#(X1,active(X2)) -> and#(X1,X2) and#(active(X1),X2) -> and#(X1,X2) -> and#(mark(X1),X2) -> and#(X1,X2) and#(active(X1),X2) -> and#(X1,X2) -> and#(X1,mark(X2)) -> and#(X1,X2) and#(active(X1),X2) -> and#(X1,X2) -> and#(active(X1),X2) -> and#(X1,X2) and#(active(X1),X2) -> and#(X1,X2) -> and#(X1,active(X2)) -> and#(X1,X2) and#(X1,mark(X2)) -> and#(X1,X2) -> and#(mark(X1),X2) -> and#(X1,X2) and#(X1,mark(X2)) -> and#(X1,X2) -> and#(X1,mark(X2)) -> and#(X1,X2) and#(X1,mark(X2)) -> and#(X1,X2) -> and#(active(X1),X2) -> and#(X1,X2) and#(X1,mark(X2)) -> and#(X1,X2) -> and#(X1,active(X2)) -> and#(X1,X2) and#(X1,active(X2)) -> and#(X1,X2) -> and#(mark(X1),X2) -> and#(X1,X2) and#(X1,active(X2)) -> and#(X1,X2) -> and#(X1,mark(X2)) -> and#(X1,X2) and#(X1,active(X2)) -> and#(X1,X2) -> and#(active(X1),X2) -> and#(X1,X2) and#(X1,active(X2)) -> and#(X1,X2) -> and#(X1,active(X2)) -> and#(X1,X2) isNatIList#(mark(X)) -> isNatIList#(X) -> isNatIList#(mark(X)) -> isNatIList#(X) isNatIList#(mark(X)) -> isNatIList#(X) -> isNatIList#(active(X)) -> isNatIList#(X) isNatIList#(active(X)) -> isNatIList#(X) -> isNatIList#(mark(X)) -> isNatIList#(X) isNatIList#(active(X)) -> isNatIList#(X) -> isNatIList#(active(X)) -> isNatIList#(X) isNat#(mark(X)) -> isNat#(X) -> isNat#(mark(X)) -> isNat#(X) isNat#(mark(X)) -> isNat#(X) -> isNat#(active(X)) -> isNat#(X) isNat#(active(X)) -> isNat#(X) -> isNat#(mark(X)) -> isNat#(X) isNat#(active(X)) -> isNat#(X) -> isNat#(active(X)) -> isNat#(X) isNatList#(mark(X)) -> isNatList#(X) -> isNatList#(mark(X)) -> isNatList#(X) isNatList#(mark(X)) -> isNatList#(X) -> isNatList#(active(X)) -> isNatList#(X) isNatList#(active(X)) -> isNatList#(X) -> isNatList#(mark(X)) -> isNatList#(X) isNatList#(active(X)) -> isNatList#(X) -> isNatList#(active(X)) -> isNatList#(X) s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X) s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X) length#(mark(X)) -> length#(X) -> length#(mark(X)) -> length#(X) length#(mark(X)) -> length#(X) -> length#(active(X)) -> length#(X) length#(active(X)) -> length#(X) -> length#(mark(X)) -> length#(X) length#(active(X)) -> length#(X) -> length#(active(X)) -> length#(X) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(U11(tt(),L)) -> length#(L) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(U11(tt(),L)) -> s#(length(L)) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(U11(tt(),L)) -> mark#(s(length(L))) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(and(tt(),X)) -> mark#(X) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNat(0())) -> mark#(tt()) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNat(length(V1))) -> isNatList#(V1) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNat(length(V1))) -> mark#(isNatList(V1)) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNat(s(V1))) -> isNat#(V1) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNat(s(V1))) -> mark#(isNat(V1)) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatIList(V)) -> isNatList#(V) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatIList(V)) -> mark#(isNatList(V)) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatIList(zeros())) -> mark#(tt()) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatIList(cons(V1,V2))) -> isNat#(V1) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatList(nil())) -> mark#(tt()) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatList(cons(V1,V2))) -> isNatList#(V2) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatList(cons(V1,V2))) -> isNat#(V1) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(length(nil())) -> mark#(0()) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(length(cons(N,L))) -> isNat#(N) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(length(cons(N,L))) -> isNatList#(L) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) mark#(isNatIList(X)) -> active#(isNatIList(X)) -> active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(U11(tt(),L)) -> length#(L) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(U11(tt(),L)) -> s#(length(L)) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(U11(tt(),L)) -> mark#(s(length(L))) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(and(tt(),X)) -> mark#(X) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNat(0())) -> mark#(tt()) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNat(length(V1))) -> isNatList#(V1) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNat(length(V1))) -> mark#(isNatList(V1)) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNat(s(V1))) -> isNat#(V1) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNat(s(V1))) -> mark#(isNat(V1)) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatIList(V)) -> isNatList#(V) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatIList(V)) -> mark#(isNatList(V)) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatIList(zeros())) -> mark#(tt()) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatIList(cons(V1,V2))) -> isNat#(V1) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatList(nil())) -> mark#(tt()) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatList(cons(V1,V2))) -> isNatList#(V2) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatList(cons(V1,V2))) -> isNat#(V1) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(length(nil())) -> mark#(0()) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(length(cons(N,L))) -> isNat#(N) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(length(cons(N,L))) -> isNatList#(L) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) mark#(isNatList(X)) -> active#(isNatList(X)) -> active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(isNat(X)) -> active#(isNat(X)) -> active#(U11(tt(),L)) -> length#(L) mark#(isNat(X)) -> active#(isNat(X)) -> active#(U11(tt(),L)) -> s#(length(L)) mark#(isNat(X)) -> active#(isNat(X)) -> active#(U11(tt(),L)) -> mark#(s(length(L))) mark#(isNat(X)) -> active#(isNat(X)) -> active#(and(tt(),X)) -> mark#(X) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNat(0())) -> mark#(tt()) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNat(length(V1))) -> isNatList#(V1) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNat(length(V1))) -> mark#(isNatList(V1)) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNat(s(V1))) -> isNat#(V1) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNat(s(V1))) -> mark#(isNat(V1)) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatIList(V)) -> isNatList#(V) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatIList(V)) -> mark#(isNatList(V)) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatIList(zeros())) -> mark#(tt()) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatIList(cons(V1,V2))) -> isNat#(V1) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatList(nil())) -> mark#(tt()) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatList(cons(V1,V2))) -> isNatList#(V2) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatList(cons(V1,V2))) -> isNat#(V1) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) mark#(isNat(X)) -> active#(isNat(X)) -> active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) mark#(isNat(X)) -> active#(isNat(X)) -> active#(length(nil())) -> mark#(0()) mark#(isNat(X)) -> active#(isNat(X)) -> active#(length(cons(N,L))) -> isNat#(N) mark#(isNat(X)) -> active#(isNat(X)) -> active#(length(cons(N,L))) -> isNatList#(L) mark#(isNat(X)) -> active#(isNat(X)) -> active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) mark#(isNat(X)) -> active#(isNat(X)) -> active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) mark#(isNat(X)) -> active#(isNat(X)) -> active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(and(X1,X2)) -> and#(mark(X1),X2) -> and#(mark(X1),X2) -> and#(X1,X2) mark#(and(X1,X2)) -> and#(mark(X1),X2) -> and#(X1,mark(X2)) -> and#(X1,X2) mark#(and(X1,X2)) -> and#(mark(X1),X2) -> and#(active(X1),X2) -> and#(X1,X2) mark#(and(X1,X2)) -> and#(mark(X1),X2) -> and#(X1,active(X2)) -> and#(X1,X2) mark#(and(X1,X2)) -> mark#(X1) -> mark#(zeros()) -> active#(zeros()) mark#(and(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(and(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(and(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(and(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0()) mark#(and(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> mark#(X1) mark#(and(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) mark#(and(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) mark#(and(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt()) mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X)) mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(mark(X))) mark#(and(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X) mark#(and(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> length#(mark(X)) mark#(and(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> active#(length(mark(X))) mark#(and(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> mark#(X1) mark#(and(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) mark#(and(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) mark#(and(X1,X2)) -> mark#(X1) -> mark#(isNat(X)) -> active#(isNat(X)) mark#(and(X1,X2)) -> mark#(X1) -> mark#(isNatList(X)) -> active#(isNatList(X)) mark#(and(X1,X2)) -> mark#(X1) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) mark#(and(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil()) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(U11(tt(),L)) -> length#(L) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(U11(tt(),L)) -> s#(length(L)) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(U11(tt(),L)) -> mark#(s(length(L))) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(and(tt(),X)) -> mark#(X) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNat(0())) -> mark#(tt()) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNat(length(V1))) -> isNatList#(V1) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNat(length(V1))) -> mark#(isNatList(V1)) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNat(s(V1))) -> isNat#(V1) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNat(s(V1))) -> mark#(isNat(V1)) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatIList(V)) -> isNatList#(V) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatIList(V)) -> mark#(isNatList(V)) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatIList(zeros())) -> mark#(tt()) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> isNat#(V1) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatList(nil())) -> mark#(tt()) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> isNatList#(V2) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> isNat#(V1) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(length(nil())) -> mark#(0()) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(length(cons(N,L))) -> isNat#(N) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(length(cons(N,L))) -> isNatList#(L) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) -> active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X) mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X) mark#(s(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros()) mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0()) mark#(s(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) mark#(s(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) mark#(s(X)) -> mark#(X) -> mark#(tt()) -> active#(tt()) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> length#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> active#(length(mark(X))) mark#(s(X)) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) mark#(s(X)) -> mark#(X) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) mark#(s(X)) -> mark#(X) -> mark#(isNat(X)) -> active#(isNat(X)) mark#(s(X)) -> mark#(X) -> mark#(isNatList(X)) -> active#(isNatList(X)) mark#(s(X)) -> mark#(X) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) mark#(s(X)) -> mark#(X) -> mark#(nil()) -> active#(nil()) mark#(s(X)) -> active#(s(mark(X))) -> active#(U11(tt(),L)) -> length#(L) mark#(s(X)) -> active#(s(mark(X))) -> active#(U11(tt(),L)) -> s#(length(L)) mark#(s(X)) -> active#(s(mark(X))) -> active#(U11(tt(),L)) -> mark#(s(length(L))) mark#(s(X)) -> active#(s(mark(X))) -> active#(and(tt(),X)) -> mark#(X) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNat(0())) -> mark#(tt()) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNat(length(V1))) -> isNatList#(V1) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNat(length(V1))) -> mark#(isNatList(V1)) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNat(s(V1))) -> isNat#(V1) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNat(s(V1))) -> mark#(isNat(V1)) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatIList(V)) -> isNatList#(V) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatIList(V)) -> mark#(isNatList(V)) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatIList(zeros())) -> mark#(tt()) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatIList(cons(V1,V2))) -> isNat#(V1) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatList(nil())) -> mark#(tt()) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatList(cons(V1,V2))) -> isNatList#(V2) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatList(cons(V1,V2))) -> isNat#(V1) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) mark#(s(X)) -> active#(s(mark(X))) -> active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) mark#(s(X)) -> active#(s(mark(X))) -> active#(length(nil())) -> mark#(0()) mark#(s(X)) -> active#(s(mark(X))) -> active#(length(cons(N,L))) -> isNat#(N) mark#(s(X)) -> active#(s(mark(X))) -> active#(length(cons(N,L))) -> isNatList#(L) mark#(s(X)) -> active#(s(mark(X))) -> active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) mark#(s(X)) -> active#(s(mark(X))) -> active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) mark#(s(X)) -> active#(s(mark(X))) -> active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(length(X)) -> length#(mark(X)) -> length#(mark(X)) -> length#(X) mark#(length(X)) -> length#(mark(X)) -> length#(active(X)) -> length#(X) mark#(length(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros()) mark#(length(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(length(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(length(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(length(X)) -> mark#(X) -> mark#(0()) -> active#(0()) mark#(length(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> mark#(X1) mark#(length(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) mark#(length(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) mark#(length(X)) -> mark#(X) -> mark#(tt()) -> active#(tt()) mark#(length(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(length(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X)) mark#(length(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) mark#(length(X)) -> mark#(X) -> mark#(length(X)) -> mark#(X) mark#(length(X)) -> mark#(X) -> mark#(length(X)) -> length#(mark(X)) mark#(length(X)) -> mark#(X) -> mark#(length(X)) -> active#(length(mark(X))) mark#(length(X)) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1) mark#(length(X)) -> mark#(X) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) mark#(length(X)) -> mark#(X) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) mark#(length(X)) -> mark#(X) -> mark#(isNat(X)) -> active#(isNat(X)) mark#(length(X)) -> mark#(X) -> mark#(isNatList(X)) -> active#(isNatList(X)) mark#(length(X)) -> mark#(X) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) mark#(length(X)) -> mark#(X) -> mark#(nil()) -> active#(nil()) mark#(length(X)) -> active#(length(mark(X))) -> active#(U11(tt(),L)) -> length#(L) mark#(length(X)) -> active#(length(mark(X))) -> active#(U11(tt(),L)) -> s#(length(L)) mark#(length(X)) -> active#(length(mark(X))) -> active#(U11(tt(),L)) -> mark#(s(length(L))) mark#(length(X)) -> active#(length(mark(X))) -> active#(and(tt(),X)) -> mark#(X) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNat(0())) -> mark#(tt()) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNat(length(V1))) -> isNatList#(V1) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNat(length(V1))) -> mark#(isNatList(V1)) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNat(s(V1))) -> isNat#(V1) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNat(s(V1))) -> mark#(isNat(V1)) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatIList(V)) -> isNatList#(V) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatIList(V)) -> mark#(isNatList(V)) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatIList(zeros())) -> mark#(tt()) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatIList(cons(V1,V2))) -> isNat#(V1) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatList(nil())) -> mark#(tt()) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatList(cons(V1,V2))) -> isNatList#(V2) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatList(cons(V1,V2))) -> isNat#(V1) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) mark#(length(X)) -> active#(length(mark(X))) -> active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) mark#(length(X)) -> active#(length(mark(X))) -> active#(length(nil())) -> mark#(0()) mark#(length(X)) -> active#(length(mark(X))) -> active#(length(cons(N,L))) -> isNat#(N) mark#(length(X)) -> active#(length(mark(X))) -> active#(length(cons(N,L))) -> isNatList#(L) mark#(length(X)) -> active#(length(mark(X))) -> active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) mark#(length(X)) -> active#(length(mark(X))) -> active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) mark#(length(X)) -> active#(length(mark(X))) -> active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(U11(X1,X2)) -> U11#(mark(X1),X2) -> U11#(mark(X1),X2) -> U11#(X1,X2) mark#(U11(X1,X2)) -> U11#(mark(X1),X2) -> U11#(X1,mark(X2)) -> U11#(X1,X2) mark#(U11(X1,X2)) -> U11#(mark(X1),X2) -> U11#(active(X1),X2) -> U11#(X1,X2) mark#(U11(X1,X2)) -> U11#(mark(X1),X2) -> U11#(X1,active(X2)) -> U11#(X1,X2) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(zeros()) -> active#(zeros()) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0()) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> mark#(X1) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt()) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X)) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(mark(X))) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> length#(mark(X)) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> active#(length(mark(X))) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> mark#(X1) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(isNat(X)) -> active#(isNat(X)) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(isNatList(X)) -> active#(isNatList(X)) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) mark#(U11(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil()) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(U11(tt(),L)) -> length#(L) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(U11(tt(),L)) -> s#(length(L)) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(U11(tt(),L)) -> mark#(s(length(L))) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(and(tt(),X)) -> mark#(X) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNat(0())) -> mark#(tt()) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNat(length(V1))) -> isNatList#(V1) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNat(length(V1))) -> mark#(isNatList(V1)) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNat(s(V1))) -> isNat#(V1) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNat(s(V1))) -> mark#(isNat(V1)) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatIList(V)) -> isNatList#(V) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatIList(V)) -> mark#(isNatList(V)) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatIList(zeros())) -> mark#(tt()) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> isNat#(V1) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatList(nil())) -> mark#(tt()) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> isNatList#(V2) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> isNat#(V1) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(length(nil())) -> mark#(0()) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(length(cons(N,L))) -> isNat#(N) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(length(cons(N,L))) -> isNatList#(L) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) -> active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(zeros()) -> active#(zeros()) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0()) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt()) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(mark(X))) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> length#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> active#(length(mark(X))) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(isNat(X)) -> active#(isNat(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(isNatList(X)) -> active#(isNatList(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil()) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) -> cons#(X1,mark(X2)) -> cons#(X1,X2) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) -> cons#(active(X1),X2) -> cons#(X1,X2) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(U11(tt(),L)) -> length#(L) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(U11(tt(),L)) -> s#(length(L)) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(U11(tt(),L)) -> mark#(s(length(L))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(and(tt(),X)) -> mark#(X) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNat(0())) -> mark#(tt()) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNat(length(V1))) -> isNatList#(V1) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNat(length(V1))) -> mark#(isNatList(V1)) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNat(s(V1))) -> isNat#(V1) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNat(s(V1))) -> mark#(isNat(V1)) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatIList(V)) -> isNatList#(V) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatIList(V)) -> mark#(isNatList(V)) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatIList(zeros())) -> mark#(tt()) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> isNat#(V1) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatList(nil())) -> mark#(tt()) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> isNatList#(V2) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> isNat#(V1) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(length(nil())) -> mark#(0()) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(length(cons(N,L))) -> isNat#(N) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(length(cons(N,L))) -> isNatList#(L) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(zeros()) -> active#(zeros()) -> active#(zeros()) -> cons#(0(),zeros()) mark#(zeros()) -> active#(zeros()) -> active#(zeros()) -> mark#(cons(0(),zeros())) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(active(X1),X2) -> cons#(X1,X2) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) -> cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) -> cons#(active(X1),X2) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) -> cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) -> cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) -> cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) -> cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) -> and#(mark(X1),X2) -> and#(X1,X2) active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) -> and#(X1,mark(X2)) -> and#(X1,X2) active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) -> and#(active(X1),X2) -> and#(X1,X2) active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) -> and#(X1,active(X2)) -> and#(X1,X2) active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) -> isNatIList#(mark(X)) -> isNatIList#(X) active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) -> isNatIList#(active(X)) -> isNatIList#(X) active#(isNatIList(cons(V1,V2))) -> isNat#(V1) -> isNat#(mark(X)) -> isNat#(X) active#(isNatIList(cons(V1,V2))) -> isNat#(V1) -> isNat#(active(X)) -> isNat#(X) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(cons(X1,X2)) -> mark#(X1) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(U11(X1,X2)) -> mark#(X1) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(s(X)) -> mark#(X) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(s(X)) -> s#(mark(X)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(s(X)) -> active#(s(mark(X))) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(length(X)) -> mark#(X) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(length(X)) -> length#(mark(X)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(length(X)) -> active#(length(mark(X))) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(and(X1,X2)) -> mark#(X1) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(isNat(X)) -> active#(isNat(X)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(isNatList(X)) -> active#(isNatList(X)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) active#(isNatIList(zeros())) -> mark#(tt()) -> mark#(tt()) -> active#(tt()) active#(isNatIList(V)) -> isNatList#(V) -> isNatList#(mark(X)) -> isNatList#(X) active#(isNatIList(V)) -> isNatList#(V) -> isNatList#(active(X)) -> isNatList#(X) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(cons(X1,X2)) -> mark#(X1) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(U11(X1,X2)) -> mark#(X1) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(s(X)) -> mark#(X) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(s(X)) -> s#(mark(X)) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(s(X)) -> active#(s(mark(X))) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(length(X)) -> mark#(X) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(length(X)) -> length#(mark(X)) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(length(X)) -> active#(length(mark(X))) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(and(X1,X2)) -> mark#(X1) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(isNat(X)) -> active#(isNat(X)) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(isNatList(X)) -> active#(isNatList(X)) active#(isNatIList(V)) -> mark#(isNatList(V)) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) active#(isNatList(nil())) -> mark#(tt()) -> mark#(tt()) -> active#(tt()) active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) -> and#(mark(X1),X2) -> and#(X1,X2) active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) -> and#(X1,mark(X2)) -> and#(X1,X2) active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) -> and#(active(X1),X2) -> and#(X1,X2) active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) -> and#(X1,active(X2)) -> and#(X1,X2) active#(isNatList(cons(V1,V2))) -> isNat#(V1) -> isNat#(mark(X)) -> isNat#(X) active#(isNatList(cons(V1,V2))) -> isNat#(V1) -> isNat#(active(X)) -> isNat#(X) active#(isNatList(cons(V1,V2))) -> isNatList#(V2) -> isNatList#(mark(X)) -> isNatList#(X) active#(isNatList(cons(V1,V2))) -> isNatList#(V2) -> isNatList#(active(X)) -> isNatList#(X) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(cons(X1,X2)) -> mark#(X1) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(U11(X1,X2)) -> mark#(X1) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(s(X)) -> mark#(X) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(s(X)) -> s#(mark(X)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(s(X)) -> active#(s(mark(X))) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(length(X)) -> mark#(X) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(length(X)) -> length#(mark(X)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(length(X)) -> active#(length(mark(X))) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(and(X1,X2)) -> mark#(X1) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(isNat(X)) -> active#(isNat(X)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(isNatList(X)) -> active#(isNatList(X)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) active#(isNat(s(V1))) -> isNat#(V1) -> isNat#(mark(X)) -> isNat#(X) active#(isNat(s(V1))) -> isNat#(V1) -> isNat#(active(X)) -> isNat#(X) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(cons(X1,X2)) -> mark#(X1) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(U11(X1,X2)) -> mark#(X1) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(s(X)) -> mark#(X) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(s(X)) -> s#(mark(X)) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(s(X)) -> active#(s(mark(X))) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(length(X)) -> mark#(X) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(length(X)) -> length#(mark(X)) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(length(X)) -> active#(length(mark(X))) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(and(X1,X2)) -> mark#(X1) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(isNat(X)) -> active#(isNat(X)) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(isNatList(X)) -> active#(isNatList(X)) active#(isNat(s(V1))) -> mark#(isNat(V1)) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) active#(isNat(length(V1))) -> isNatList#(V1) -> isNatList#(mark(X)) -> isNatList#(X) active#(isNat(length(V1))) -> isNatList#(V1) -> isNatList#(active(X)) -> isNatList#(X) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(cons(X1,X2)) -> mark#(X1) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(U11(X1,X2)) -> mark#(X1) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(s(X)) -> mark#(X) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(s(X)) -> s#(mark(X)) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(s(X)) -> active#(s(mark(X))) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(length(X)) -> mark#(X) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(length(X)) -> length#(mark(X)) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(length(X)) -> active#(length(mark(X))) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(and(X1,X2)) -> mark#(X1) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(isNat(X)) -> active#(isNat(X)) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(isNatList(X)) -> active#(isNatList(X)) active#(isNat(length(V1))) -> mark#(isNatList(V1)) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) active#(isNat(0())) -> mark#(tt()) -> mark#(tt()) -> active#(tt()) active#(and(tt(),X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros()) active#(and(tt(),X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) active#(and(tt(),X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(and(tt(),X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(and(tt(),X)) -> mark#(X) -> mark#(0()) -> active#(0()) active#(and(tt(),X)) -> mark#(X) -> mark#(U11(X1,X2)) -> mark#(X1) active#(and(tt(),X)) -> mark#(X) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) active#(and(tt(),X)) -> mark#(X) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) active#(and(tt(),X)) -> mark#(X) -> mark#(tt()) -> active#(tt()) active#(and(tt(),X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) active#(and(tt(),X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X)) active#(and(tt(),X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) active#(and(tt(),X)) -> mark#(X) -> mark#(length(X)) -> mark#(X) active#(and(tt(),X)) -> mark#(X) -> mark#(length(X)) -> length#(mark(X)) active#(and(tt(),X)) -> mark#(X) -> mark#(length(X)) -> active#(length(mark(X))) active#(and(tt(),X)) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1) active#(and(tt(),X)) -> mark#(X) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) active#(and(tt(),X)) -> mark#(X) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) active#(and(tt(),X)) -> mark#(X) -> mark#(isNat(X)) -> active#(isNat(X)) active#(and(tt(),X)) -> mark#(X) -> mark#(isNatList(X)) -> active#(isNatList(X)) active#(and(tt(),X)) -> mark#(X) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) active#(and(tt(),X)) -> mark#(X) -> mark#(nil()) -> active#(nil()) active#(length(nil())) -> mark#(0()) -> mark#(0()) -> active#(0()) active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) -> U11#(mark(X1),X2) -> U11#(X1,X2) active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) -> U11#(X1,mark(X2)) -> U11#(X1,X2) active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) -> U11#(active(X1),X2) -> U11#(X1,X2) active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) -> U11#(X1,active(X2)) -> U11#(X1,X2) active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) -> and#(mark(X1),X2) -> and#(X1,X2) active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) -> and#(X1,mark(X2)) -> and#(X1,X2) active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) -> and#(active(X1),X2) -> and#(X1,X2) active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) -> and#(X1,active(X2)) -> and#(X1,X2) active#(length(cons(N,L))) -> isNat#(N) -> isNat#(mark(X)) -> isNat#(X) active#(length(cons(N,L))) -> isNat#(N) -> isNat#(active(X)) -> isNat#(X) active#(length(cons(N,L))) -> isNatList#(L) -> isNatList#(mark(X)) -> isNatList#(X) active#(length(cons(N,L))) -> isNatList#(L) -> isNatList#(active(X)) -> isNatList#(X) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(cons(X1,X2)) -> mark#(X1) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(U11(X1,X2)) -> mark#(X1) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(s(X)) -> mark#(X) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(s(X)) -> s#(mark(X)) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(s(X)) -> active#(s(mark(X))) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(length(X)) -> mark#(X) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(length(X)) -> length#(mark(X)) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(length(X)) -> active#(length(mark(X))) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(and(X1,X2)) -> mark#(X1) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(isNat(X)) -> active#(isNat(X)) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(isNatList(X)) -> active#(isNatList(X)) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) active#(U11(tt(),L)) -> s#(length(L)) -> s#(mark(X)) -> s#(X) active#(U11(tt(),L)) -> s#(length(L)) -> s#(active(X)) -> s#(X) active#(U11(tt(),L)) -> length#(L) -> length#(mark(X)) -> length#(X) active#(U11(tt(),L)) -> length#(L) -> length#(active(X)) -> length#(X) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(cons(X1,X2)) -> mark#(X1) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(U11(X1,X2)) -> mark#(X1) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(s(X)) -> mark#(X) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(s(X)) -> s#(mark(X)) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(s(X)) -> active#(s(mark(X))) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(length(X)) -> mark#(X) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(length(X)) -> length#(mark(X)) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(length(X)) -> active#(length(mark(X))) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(and(X1,X2)) -> mark#(X1) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(and(X1,X2)) -> and#(mark(X1),X2) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(isNat(X)) -> active#(isNat(X)) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(isNatList(X)) -> active#(isNatList(X)) active#(U11(tt(),L)) -> mark#(s(length(L))) -> mark#(isNatIList(X)) -> active#(isNatIList(X)) active#(zeros()) -> mark#(cons(0(),zeros())) -> mark#(cons(X1,X2)) -> mark#(X1) active#(zeros()) -> mark#(cons(0(),zeros())) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(zeros()) -> mark#(cons(0(),zeros())) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) Restore Modifier: DPs: active#(zeros()) -> cons#(0(),zeros()) active#(zeros()) -> mark#(cons(0(),zeros())) active#(U11(tt(),L)) -> length#(L) active#(U11(tt(),L)) -> s#(length(L)) active#(U11(tt(),L)) -> mark#(s(length(L))) active#(and(tt(),X)) -> mark#(X) active#(isNat(0())) -> mark#(tt()) active#(isNat(length(V1))) -> isNatList#(V1) active#(isNat(length(V1))) -> mark#(isNatList(V1)) active#(isNat(s(V1))) -> isNat#(V1) active#(isNat(s(V1))) -> mark#(isNat(V1)) active#(isNatIList(V)) -> isNatList#(V) active#(isNatIList(V)) -> mark#(isNatList(V)) active#(isNatIList(zeros())) -> mark#(tt()) active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) active#(isNatIList(cons(V1,V2))) -> isNat#(V1) active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) active#(isNatList(nil())) -> mark#(tt()) active#(isNatList(cons(V1,V2))) -> isNatList#(V2) active#(isNatList(cons(V1,V2))) -> isNat#(V1) active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) active#(length(nil())) -> mark#(0()) active#(length(cons(N,L))) -> isNat#(N) active#(length(cons(N,L))) -> isNatList#(L) active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(zeros()) -> active#(zeros()) mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(0()) -> active#(0()) mark#(U11(X1,X2)) -> mark#(X1) mark#(U11(X1,X2)) -> U11#(mark(X1),X2) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) mark#(tt()) -> active#(tt()) mark#(s(X)) -> mark#(X) mark#(s(X)) -> s#(mark(X)) mark#(s(X)) -> active#(s(mark(X))) mark#(length(X)) -> mark#(X) mark#(length(X)) -> length#(mark(X)) mark#(length(X)) -> active#(length(mark(X))) mark#(and(X1,X2)) -> mark#(X1) mark#(and(X1,X2)) -> and#(mark(X1),X2) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) mark#(isNat(X)) -> active#(isNat(X)) mark#(isNatList(X)) -> active#(isNatList(X)) mark#(isNatIList(X)) -> active#(isNatIList(X)) mark#(nil()) -> active#(nil()) cons#(mark(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) U11#(mark(X1),X2) -> U11#(X1,X2) U11#(X1,mark(X2)) -> U11#(X1,X2) U11#(active(X1),X2) -> U11#(X1,X2) U11#(X1,active(X2)) -> U11#(X1,X2) s#(mark(X)) -> s#(X) s#(active(X)) -> s#(X) length#(mark(X)) -> length#(X) length#(active(X)) -> length#(X) and#(mark(X1),X2) -> and#(X1,X2) and#(X1,mark(X2)) -> and#(X1,X2) and#(active(X1),X2) -> and#(X1,X2) and#(X1,active(X2)) -> and#(X1,X2) isNat#(mark(X)) -> isNat#(X) isNat#(active(X)) -> isNat#(X) isNatList#(mark(X)) -> isNatList#(X) isNatList#(active(X)) -> isNatList#(X) isNatIList#(mark(X)) -> isNatIList#(X) isNatIList#(active(X)) -> isNatIList#(X) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) SCC Processor: #sccs: 9 #rules: 45 #arcs: 605/5329 DPs: mark#(isNatIList(X)) -> active#(isNatIList(X)) active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) mark#(isNatList(X)) -> active#(isNatList(X)) active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) mark#(isNat(X)) -> active#(isNat(X)) active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) active#(isNatIList(V)) -> mark#(isNatList(V)) mark#(and(X1,X2)) -> mark#(X1) mark#(length(X)) -> active#(length(mark(X))) active#(isNat(s(V1))) -> mark#(isNat(V1)) mark#(length(X)) -> mark#(X) mark#(s(X)) -> active#(s(mark(X))) active#(isNat(length(V1))) -> mark#(isNatList(V1)) mark#(s(X)) -> mark#(X) mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) active#(and(tt(),X)) -> mark#(X) mark#(U11(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(U11(tt(),L)) -> mark#(s(length(L))) mark#(cons(X1,X2)) -> mark#(X1) mark#(zeros()) -> active#(zeros()) active#(zeros()) -> mark#(cons(0(),zeros())) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) Open DPs: cons#(X1,active(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(mark(X1),X2) -> cons#(X1,X2) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) Open DPs: length#(mark(X)) -> length#(X) length#(active(X)) -> length#(X) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) Open DPs: s#(mark(X)) -> s#(X) s#(active(X)) -> s#(X) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) Open DPs: isNatList#(mark(X)) -> isNatList#(X) isNatList#(active(X)) -> isNatList#(X) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) Open DPs: isNat#(mark(X)) -> isNat#(X) isNat#(active(X)) -> isNat#(X) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) Open DPs: isNatIList#(mark(X)) -> isNatIList#(X) isNatIList#(active(X)) -> isNatIList#(X) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) Open DPs: and#(mark(X1),X2) -> and#(X1,X2) and#(X1,active(X2)) -> and#(X1,X2) and#(active(X1),X2) -> and#(X1,X2) and#(X1,mark(X2)) -> and#(X1,X2) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) Open DPs: U11#(mark(X1),X2) -> U11#(X1,X2) U11#(X1,active(X2)) -> U11#(X1,X2) U11#(active(X1),X2) -> U11#(X1,X2) U11#(X1,mark(X2)) -> U11#(X1,X2) TRS: active(zeros()) -> mark(cons(0(),zeros())) active(U11(tt(),L)) -> mark(s(length(L))) active(and(tt(),X)) -> mark(X) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(zeros())) -> mark(tt()) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatList(nil())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(length(nil())) -> mark(0()) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) mark(zeros()) -> active(zeros()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0()) -> active(0()) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(isNatList(X)) -> active(isNatList(X)) mark(isNatIList(X)) -> active(isNatIList(X)) mark(nil()) -> active(nil()) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) Open