MAYBE Problem: and(tt(),T) -> T isNatIList(IL) -> isNatList(activate(IL)) isNat(n__0()) -> tt() isNat(n__s(N)) -> isNat(activate(N)) isNat(n__length(L)) -> isNatList(activate(L)) isNatIList(n__zeros()) -> tt() isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__nil()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) zeros() -> cons(0(),n__zeros()) take(0(),IL) -> uTake1(isNatIList(IL)) uTake1(tt()) -> nil() take(s(M),cons(N,IL)) -> uTake2(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) length(cons(N,L)) -> uLength(and(isNat(N),isNatList(activate(L))),activate(L)) uLength(tt(),L) -> s(length(activate(L))) 0() -> n__0() s(X) -> n__s(X) length(X) -> n__length(X) zeros() -> n__zeros() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() take(X1,X2) -> n__take(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__zeros()) -> zeros() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X Proof: DP Processor: DPs: isNatIList#(IL) -> activate#(IL) isNatIList#(IL) -> isNatList#(activate(IL)) isNat#(n__s(N)) -> activate#(N) isNat#(n__s(N)) -> isNat#(activate(N)) isNat#(n__length(L)) -> activate#(L) isNat#(n__length(L)) -> isNatList#(activate(L)) isNatIList#(n__cons(N,IL)) -> activate#(IL) isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) isNatIList#(n__cons(N,IL)) -> activate#(N) isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) isNatIList#(n__cons(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) isNatList#(n__cons(N,L)) -> activate#(L) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) isNatList#(n__cons(N,L)) -> activate#(N) isNatList#(n__cons(N,L)) -> isNat#(activate(N)) isNatList#(n__cons(N,L)) -> and#(isNat(activate(N)),isNatList(activate(L))) isNatList#(n__take(N,IL)) -> activate#(IL) isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) isNatList#(n__take(N,IL)) -> activate#(N) isNatList#(n__take(N,IL)) -> isNat#(activate(N)) isNatList#(n__take(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) zeros#() -> 0#() zeros#() -> cons#(0(),n__zeros()) take#(0(),IL) -> isNatIList#(IL) take#(0(),IL) -> uTake1#(isNatIList(IL)) uTake1#(tt()) -> nil#() take#(s(M),cons(N,IL)) -> activate#(IL) take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) take#(s(M),cons(N,IL)) -> isNat#(N) take#(s(M),cons(N,IL)) -> and#(isNat(N),isNatIList(activate(IL))) take#(s(M),cons(N,IL)) -> isNat#(M) take#(s(M),cons(N,IL)) -> and#(isNat(M),and(isNat(N),isNatIList(activate(IL)))) take#(s(M),cons(N,IL)) -> uTake2#(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) uTake2#(tt(),M,N,IL) -> activate#(IL) uTake2#(tt(),M,N,IL) -> activate#(M) uTake2#(tt(),M,N,IL) -> activate#(N) uTake2#(tt(),M,N,IL) -> cons#(activate(N),n__take(activate(M),activate(IL))) length#(cons(N,L)) -> activate#(L) length#(cons(N,L)) -> isNatList#(activate(L)) length#(cons(N,L)) -> isNat#(N) length#(cons(N,L)) -> and#(isNat(N),isNatList(activate(L))) length#(cons(N,L)) -> uLength#(and(isNat(N),isNatList(activate(L))),activate(L)) uLength#(tt(),L) -> activate#(L) uLength#(tt(),L) -> length#(activate(L)) uLength#(tt(),L) -> s#(length(activate(L))) activate#(n__0()) -> 0#() activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> length#(activate(X)) activate#(n__zeros()) -> zeros#() activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__nil()) -> nil#() activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) TRS: and(tt(),T) -> T isNatIList(IL) -> isNatList(activate(IL)) isNat(n__0()) -> tt() isNat(n__s(N)) -> isNat(activate(N)) isNat(n__length(L)) -> isNatList(activate(L)) isNatIList(n__zeros()) -> tt() isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__nil()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) zeros() -> cons(0(),n__zeros()) take(0(),IL) -> uTake1(isNatIList(IL)) uTake1(tt()) -> nil() take(s(M),cons(N,IL)) -> uTake2(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) length(cons(N,L)) -> uLength(and(isNat(N),isNatList(activate(L))),activate(L)) uLength(tt(),L) -> s(length(activate(L))) 0() -> n__0() s(X) -> n__s(X) length(X) -> n__length(X) zeros() -> n__zeros() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() take(X1,X2) -> n__take(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__zeros()) -> zeros() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X EDG Processor: DPs: isNatIList#(IL) -> activate#(IL) isNatIList#(IL) -> isNatList#(activate(IL)) isNat#(n__s(N)) -> activate#(N) isNat#(n__s(N)) -> isNat#(activate(N)) isNat#(n__length(L)) -> activate#(L) isNat#(n__length(L)) -> isNatList#(activate(L)) isNatIList#(n__cons(N,IL)) -> activate#(IL) isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) isNatIList#(n__cons(N,IL)) -> activate#(N) isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) isNatIList#(n__cons(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) isNatList#(n__cons(N,L)) -> activate#(L) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) isNatList#(n__cons(N,L)) -> activate#(N) isNatList#(n__cons(N,L)) -> isNat#(activate(N)) isNatList#(n__cons(N,L)) -> and#(isNat(activate(N)),isNatList(activate(L))) isNatList#(n__take(N,IL)) -> activate#(IL) isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) isNatList#(n__take(N,IL)) -> activate#(N) isNatList#(n__take(N,IL)) -> isNat#(activate(N)) isNatList#(n__take(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) zeros#() -> 0#() zeros#() -> cons#(0(),n__zeros()) take#(0(),IL) -> isNatIList#(IL) take#(0(),IL) -> uTake1#(isNatIList(IL)) uTake1#(tt()) -> nil#() take#(s(M),cons(N,IL)) -> activate#(IL) take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) take#(s(M),cons(N,IL)) -> isNat#(N) take#(s(M),cons(N,IL)) -> and#(isNat(N),isNatIList(activate(IL))) take#(s(M),cons(N,IL)) -> isNat#(M) take#(s(M),cons(N,IL)) -> and#(isNat(M),and(isNat(N),isNatIList(activate(IL)))) take#(s(M),cons(N,IL)) -> uTake2#(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) uTake2#(tt(),M,N,IL) -> activate#(IL) uTake2#(tt(),M,N,IL) -> activate#(M) uTake2#(tt(),M,N,IL) -> activate#(N) uTake2#(tt(),M,N,IL) -> cons#(activate(N),n__take(activate(M),activate(IL))) length#(cons(N,L)) -> activate#(L) length#(cons(N,L)) -> isNatList#(activate(L)) length#(cons(N,L)) -> isNat#(N) length#(cons(N,L)) -> and#(isNat(N),isNatList(activate(L))) length#(cons(N,L)) -> uLength#(and(isNat(N),isNatList(activate(L))),activate(L)) uLength#(tt(),L) -> activate#(L) uLength#(tt(),L) -> length#(activate(L)) uLength#(tt(),L) -> s#(length(activate(L))) activate#(n__0()) -> 0#() activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> length#(activate(X)) activate#(n__zeros()) -> zeros#() activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__nil()) -> nil#() activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) TRS: and(tt(),T) -> T isNatIList(IL) -> isNatList(activate(IL)) isNat(n__0()) -> tt() isNat(n__s(N)) -> isNat(activate(N)) isNat(n__length(L)) -> isNatList(activate(L)) isNatIList(n__zeros()) -> tt() isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__nil()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) zeros() -> cons(0(),n__zeros()) take(0(),IL) -> uTake1(isNatIList(IL)) uTake1(tt()) -> nil() take(s(M),cons(N,IL)) -> uTake2(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) length(cons(N,L)) -> uLength(and(isNat(N),isNatList(activate(L))),activate(L)) uLength(tt(),L) -> s(length(activate(L))) 0() -> n__0() s(X) -> n__s(X) length(X) -> n__length(X) zeros() -> n__zeros() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() take(X1,X2) -> n__take(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__zeros()) -> zeros() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X graph: uLength#(tt(),L) -> length#(activate(L)) -> length#(cons(N,L)) -> activate#(L) uLength#(tt(),L) -> length#(activate(L)) -> length#(cons(N,L)) -> isNatList#(activate(L)) uLength#(tt(),L) -> length#(activate(L)) -> length#(cons(N,L)) -> isNat#(N) uLength#(tt(),L) -> length#(activate(L)) -> length#(cons(N,L)) -> and#(isNat(N),isNatList(activate(L))) uLength#(tt(),L) -> length#(activate(L)) -> length#(cons(N,L)) -> uLength#(and(isNat(N),isNatList(activate(L))),activate(L)) uLength#(tt(),L) -> activate#(L) -> activate#(n__0()) -> 0#() uLength#(tt(),L) -> activate#(L) -> activate#(n__s(X)) -> activate#(X) uLength#(tt(),L) -> activate#(L) -> activate#(n__s(X)) -> s#(activate(X)) uLength#(tt(),L) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) uLength#(tt(),L) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) uLength#(tt(),L) -> activate#(L) -> activate#(n__zeros()) -> zeros#() uLength#(tt(),L) -> activate#(L) -> activate#(n__cons(X1,X2)) -> activate#(X1) uLength#(tt(),L) -> activate#(L) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) uLength#(tt(),L) -> activate#(L) -> activate#(n__nil()) -> nil#() uLength#(tt(),L) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X2) uLength#(tt(),L) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X1) uLength#(tt(),L) -> activate#(L) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) length#(cons(N,L)) -> uLength#(and(isNat(N),isNatList(activate(L))),activate(L)) -> uLength#(tt(),L) -> activate#(L) length#(cons(N,L)) -> uLength#(and(isNat(N),isNatList(activate(L))),activate(L)) -> uLength#(tt(),L) -> length#(activate(L)) length#(cons(N,L)) -> uLength#(and(isNat(N),isNatList(activate(L))),activate(L)) -> uLength#(tt(),L) -> s#(length(activate(L))) length#(cons(N,L)) -> isNat#(N) -> isNat#(n__s(N)) -> activate#(N) length#(cons(N,L)) -> isNat#(N) -> isNat#(n__s(N)) -> isNat#(activate(N)) length#(cons(N,L)) -> isNat#(N) -> isNat#(n__length(L)) -> activate#(L) length#(cons(N,L)) -> isNat#(N) -> isNat#(n__length(L)) -> isNatList#(activate(L)) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> activate#(L) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> activate#(N) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> isNat#(activate(N)) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> and#(isNat(activate(N)),isNatList(activate(L))) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> activate#(IL) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> activate#(N) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> isNat#(activate(N)) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) length#(cons(N,L)) -> activate#(L) -> activate#(n__0()) -> 0#() length#(cons(N,L)) -> activate#(L) -> activate#(n__s(X)) -> activate#(X) length#(cons(N,L)) -> activate#(L) -> activate#(n__s(X)) -> s#(activate(X)) length#(cons(N,L)) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) length#(cons(N,L)) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) length#(cons(N,L)) -> activate#(L) -> activate#(n__zeros()) -> zeros#() length#(cons(N,L)) -> activate#(L) -> activate#(n__cons(X1,X2)) -> activate#(X1) length#(cons(N,L)) -> activate#(L) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) length#(cons(N,L)) -> activate#(L) -> activate#(n__nil()) -> nil#() length#(cons(N,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X2) length#(cons(N,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X1) length#(cons(N,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__0()) -> 0#() uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__s(X)) -> activate#(X) uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__s(X)) -> s#(activate(X)) uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__length(X)) -> activate#(X) uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__length(X)) -> length#(activate(X)) uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__zeros()) -> zeros#() uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__cons(X1,X2)) -> activate#(X1) uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__nil()) -> nil#() uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__take(X1,X2)) -> activate#(X2) uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__take(X1,X2)) -> activate#(X1) uTake2#(tt(),M,N,IL) -> activate#(M) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__0()) -> 0#() uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__s(X)) -> activate#(X) uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__s(X)) -> s#(activate(X)) uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__length(X)) -> activate#(X) uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__length(X)) -> length#(activate(X)) uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__zeros()) -> zeros#() uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__cons(X1,X2)) -> activate#(X1) uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__nil()) -> nil#() uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__take(X1,X2)) -> activate#(X2) uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__take(X1,X2)) -> activate#(X1) uTake2#(tt(),M,N,IL) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__0()) -> 0#() uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__s(X)) -> activate#(X) uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__s(X)) -> s#(activate(X)) uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__length(X)) -> activate#(X) uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__length(X)) -> length#(activate(X)) uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__zeros()) -> zeros#() uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__cons(X1,X2)) -> activate#(X1) uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__nil()) -> nil#() uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X2) uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X1) uTake2#(tt(),M,N,IL) -> activate#(IL) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(M),cons(N,IL)) -> uTake2#(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) -> uTake2#(tt(),M,N,IL) -> activate#(IL) take#(s(M),cons(N,IL)) -> uTake2#(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) -> uTake2#(tt(),M,N,IL) -> activate#(M) take#(s(M),cons(N,IL)) -> uTake2#(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) -> uTake2#(tt(),M,N,IL) -> activate#(N) take#(s(M),cons(N,IL)) -> uTake2#(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) -> uTake2#(tt(),M,N,IL) -> cons#(activate(N),n__take(activate(M),activate(IL))) take#(s(M),cons(N,IL)) -> isNat#(M) -> isNat#(n__s(N)) -> activate#(N) take#(s(M),cons(N,IL)) -> isNat#(M) -> isNat#(n__s(N)) -> isNat#(activate(N)) take#(s(M),cons(N,IL)) -> isNat#(M) -> isNat#(n__length(L)) -> activate#(L) take#(s(M),cons(N,IL)) -> isNat#(M) -> isNat#(n__length(L)) -> isNatList#(activate(L)) take#(s(M),cons(N,IL)) -> isNat#(N) -> isNat#(n__s(N)) -> activate#(N) take#(s(M),cons(N,IL)) -> isNat#(N) -> isNat#(n__s(N)) -> isNat#(activate(N)) take#(s(M),cons(N,IL)) -> isNat#(N) -> isNat#(n__length(L)) -> activate#(L) take#(s(M),cons(N,IL)) -> isNat#(N) -> isNat#(n__length(L)) -> isNatList#(activate(L)) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__0()) -> 0#() take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__s(X)) -> activate#(X) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__s(X)) -> s#(activate(X)) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__length(X)) -> activate#(X) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__length(X)) -> length#(activate(X)) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__zeros()) -> zeros#() take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__cons(X1,X2)) -> activate#(X1) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__nil()) -> nil#() take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X2) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X1) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(IL) -> activate#(IL) take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(IL) -> isNatList#(activate(IL)) take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> activate#(IL) take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> activate#(N) take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) take#(0(),IL) -> uTake1#(isNatIList(IL)) -> uTake1#(tt()) -> nil#() take#(0(),IL) -> isNatIList#(IL) -> isNatIList#(IL) -> activate#(IL) take#(0(),IL) -> isNatIList#(IL) -> isNatIList#(IL) -> isNatList#(activate(IL)) take#(0(),IL) -> isNatIList#(IL) -> isNatIList#(n__cons(N,IL)) -> activate#(IL) take#(0(),IL) -> isNatIList#(IL) -> isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) take#(0(),IL) -> isNatIList#(IL) -> isNatIList#(n__cons(N,IL)) -> activate#(N) take#(0(),IL) -> isNatIList#(IL) -> isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) take#(0(),IL) -> isNatIList#(IL) -> isNatIList#(n__cons(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) isNat#(n__length(L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> activate#(L) isNat#(n__length(L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) isNat#(n__length(L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> activate#(N) isNat#(n__length(L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> isNat#(activate(N)) isNat#(n__length(L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> and#(isNat(activate(N)),isNatList(activate(L))) isNat#(n__length(L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> activate#(IL) isNat#(n__length(L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) isNat#(n__length(L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> activate#(N) isNat#(n__length(L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> isNat#(activate(N)) isNat#(n__length(L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) isNat#(n__length(L)) -> activate#(L) -> activate#(n__0()) -> 0#() isNat#(n__length(L)) -> activate#(L) -> activate#(n__s(X)) -> activate#(X) isNat#(n__length(L)) -> activate#(L) -> activate#(n__s(X)) -> s#(activate(X)) isNat#(n__length(L)) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) isNat#(n__length(L)) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) isNat#(n__length(L)) -> activate#(L) -> activate#(n__zeros()) -> zeros#() isNat#(n__length(L)) -> activate#(L) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNat#(n__length(L)) -> activate#(L) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNat#(n__length(L)) -> activate#(L) -> activate#(n__nil()) -> nil#() isNat#(n__length(L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X2) isNat#(n__length(L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X1) isNat#(n__length(L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) isNat#(n__s(N)) -> isNat#(activate(N)) -> isNat#(n__s(N)) -> activate#(N) isNat#(n__s(N)) -> isNat#(activate(N)) -> isNat#(n__s(N)) -> isNat#(activate(N)) isNat#(n__s(N)) -> isNat#(activate(N)) -> isNat#(n__length(L)) -> activate#(L) isNat#(n__s(N)) -> isNat#(activate(N)) -> isNat#(n__length(L)) -> isNatList#(activate(L)) isNat#(n__s(N)) -> activate#(N) -> activate#(n__0()) -> 0#() isNat#(n__s(N)) -> activate#(N) -> activate#(n__s(X)) -> activate#(X) isNat#(n__s(N)) -> activate#(N) -> activate#(n__s(X)) -> s#(activate(X)) isNat#(n__s(N)) -> activate#(N) -> activate#(n__length(X)) -> activate#(X) isNat#(n__s(N)) -> activate#(N) -> activate#(n__length(X)) -> length#(activate(X)) isNat#(n__s(N)) -> activate#(N) -> activate#(n__zeros()) -> zeros#() isNat#(n__s(N)) -> activate#(N) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNat#(n__s(N)) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNat#(n__s(N)) -> activate#(N) -> activate#(n__nil()) -> nil#() isNat#(n__s(N)) -> activate#(N) -> activate#(n__take(X1,X2)) -> activate#(X2) isNat#(n__s(N)) -> activate#(N) -> activate#(n__take(X1,X2)) -> activate#(X1) isNat#(n__s(N)) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) isNatList#(n__take(N,IL)) -> isNat#(activate(N)) -> isNat#(n__s(N)) -> activate#(N) isNatList#(n__take(N,IL)) -> isNat#(activate(N)) -> isNat#(n__s(N)) -> isNat#(activate(N)) isNatList#(n__take(N,IL)) -> isNat#(activate(N)) -> isNat#(n__length(L)) -> activate#(L) isNatList#(n__take(N,IL)) -> isNat#(activate(N)) -> isNat#(n__length(L)) -> isNatList#(activate(L)) isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__0()) -> 0#() isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__s(X)) -> activate#(X) isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__s(X)) -> s#(activate(X)) isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__length(X)) -> activate#(X) isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__length(X)) -> length#(activate(X)) isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__zeros()) -> zeros#() isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__nil()) -> nil#() isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__take(X1,X2)) -> activate#(X2) isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__take(X1,X2)) -> activate#(X1) isNatList#(n__take(N,IL)) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__0()) -> 0#() isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__s(X)) -> activate#(X) isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__s(X)) -> s#(activate(X)) isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__length(X)) -> activate#(X) isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__length(X)) -> length#(activate(X)) isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__zeros()) -> zeros#() isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__nil()) -> nil#() isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X2) isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X1) isNatList#(n__take(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(IL) -> activate#(IL) isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(IL) -> isNatList#(activate(IL)) isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> activate#(IL) isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> activate#(N) isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) isNatList#(n__cons(N,L)) -> isNat#(activate(N)) -> isNat#(n__s(N)) -> activate#(N) isNatList#(n__cons(N,L)) -> isNat#(activate(N)) -> isNat#(n__s(N)) -> isNat#(activate(N)) isNatList#(n__cons(N,L)) -> isNat#(activate(N)) -> isNat#(n__length(L)) -> activate#(L) isNatList#(n__cons(N,L)) -> isNat#(activate(N)) -> isNat#(n__length(L)) -> isNatList#(activate(L)) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> activate#(L) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> activate#(N) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> isNat#(activate(N)) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(N,L)) -> and#(isNat(activate(N)),isNatList(activate(L))) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> activate#(IL) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> activate#(N) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> isNat#(activate(N)) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__take(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__0()) -> 0#() isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__s(X)) -> activate#(X) isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__s(X)) -> s#(activate(X)) isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__zeros()) -> zeros#() isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__nil()) -> nil#() isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X2) isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X1) isNatList#(n__cons(N,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__0()) -> 0#() isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__s(X)) -> activate#(X) isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__s(X)) -> s#(activate(X)) isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__length(X)) -> activate#(X) isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__length(X)) -> length#(activate(X)) isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__zeros()) -> zeros#() isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__nil()) -> nil#() isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__take(X1,X2)) -> activate#(X2) isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__take(X1,X2)) -> activate#(X1) isNatList#(n__cons(N,L)) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(0(),IL) -> isNatIList#(IL) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(0(),IL) -> uTake1#(isNatIList(IL)) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(M),cons(N,IL)) -> activate#(IL) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(M),cons(N,IL)) -> isNat#(N) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(M),cons(N,IL)) -> and#(isNat(N),isNatIList(activate(IL))) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(M),cons(N,IL)) -> isNat#(M) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(M),cons(N,IL)) -> and#(isNat(M),and(isNat(N),isNatIList(activate(IL)))) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(M),cons(N,IL)) -> uTake2#(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__0()) -> 0#() activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__length(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__zeros()) -> zeros#() activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__nil()) -> nil#() activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__0()) -> 0#() activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__length(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__zeros()) -> zeros#() activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__nil()) -> nil#() activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__0()) -> 0#() activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__length(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__zeros()) -> zeros#() activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__nil()) -> nil#() activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__zeros()) -> zeros#() -> zeros#() -> 0#() activate#(n__zeros()) -> zeros#() -> zeros#() -> cons#(0(),n__zeros()) activate#(n__length(X)) -> length#(activate(X)) -> length#(cons(N,L)) -> activate#(L) activate#(n__length(X)) -> length#(activate(X)) -> length#(cons(N,L)) -> isNatList#(activate(L)) activate#(n__length(X)) -> length#(activate(X)) -> length#(cons(N,L)) -> isNat#(N) activate#(n__length(X)) -> length#(activate(X)) -> length#(cons(N,L)) -> and#(isNat(N),isNatList(activate(L))) activate#(n__length(X)) -> length#(activate(X)) -> length#(cons(N,L)) -> uLength#(and(isNat(N),isNatList(activate(L))),activate(L)) activate#(n__length(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__length(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__length(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__length(X)) -> activate#(X) -> activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> activate#(X) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__length(X)) -> activate#(X) -> activate#(n__zeros()) -> zeros#() activate#(n__length(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__length(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__length(X)) -> activate#(X) -> activate#(n__nil()) -> nil#() activate#(n__length(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__length(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__length(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__s(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__length(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__zeros()) -> zeros#() activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__nil()) -> nil#() activate#(n__s(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) -> isNat#(n__s(N)) -> activate#(N) isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) -> isNat#(n__s(N)) -> isNat#(activate(N)) isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) -> isNat#(n__length(L)) -> activate#(L) isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) -> isNat#(n__length(L)) -> isNatList#(activate(L)) isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__0()) -> 0#() isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__s(X)) -> activate#(X) isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__s(X)) -> s#(activate(X)) isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__length(X)) -> activate#(X) isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__length(X)) -> length#(activate(X)) isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__zeros()) -> zeros#() isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__nil()) -> nil#() isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__take(X1,X2)) -> activate#(X2) isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__take(X1,X2)) -> activate#(X1) isNatIList#(n__cons(N,IL)) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__0()) -> 0#() isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__s(X)) -> activate#(X) isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__s(X)) -> s#(activate(X)) isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__length(X)) -> activate#(X) isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__length(X)) -> length#(activate(X)) isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__zeros()) -> zeros#() isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__nil()) -> nil#() isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X2) isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X1) isNatIList#(n__cons(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(IL) -> activate#(IL) isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(IL) -> isNatList#(activate(IL)) isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> activate#(IL) isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> activate#(N) isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) -> isNatIList#(n__cons(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) isNatIList#(IL) -> isNatList#(activate(IL)) -> isNatList#(n__cons(N,L)) -> activate#(L) isNatIList#(IL) -> isNatList#(activate(IL)) -> isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) isNatIList#(IL) -> isNatList#(activate(IL)) -> isNatList#(n__cons(N,L)) -> activate#(N) isNatIList#(IL) -> isNatList#(activate(IL)) -> isNatList#(n__cons(N,L)) -> isNat#(activate(N)) isNatIList#(IL) -> isNatList#(activate(IL)) -> isNatList#(n__cons(N,L)) -> and#(isNat(activate(N)),isNatList(activate(L))) isNatIList#(IL) -> isNatList#(activate(IL)) -> isNatList#(n__take(N,IL)) -> activate#(IL) isNatIList#(IL) -> isNatList#(activate(IL)) -> isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) isNatIList#(IL) -> isNatList#(activate(IL)) -> isNatList#(n__take(N,IL)) -> activate#(N) isNatIList#(IL) -> isNatList#(activate(IL)) -> isNatList#(n__take(N,IL)) -> isNat#(activate(N)) isNatIList#(IL) -> isNatList#(activate(IL)) -> isNatList#(n__take(N,IL)) -> and#(isNat(activate(N)),isNatIList(activate(IL))) isNatIList#(IL) -> activate#(IL) -> activate#(n__0()) -> 0#() isNatIList#(IL) -> activate#(IL) -> activate#(n__s(X)) -> activate#(X) isNatIList#(IL) -> activate#(IL) -> activate#(n__s(X)) -> s#(activate(X)) isNatIList#(IL) -> activate#(IL) -> activate#(n__length(X)) -> activate#(X) isNatIList#(IL) -> activate#(IL) -> activate#(n__length(X)) -> length#(activate(X)) isNatIList#(IL) -> activate#(IL) -> activate#(n__zeros()) -> zeros#() isNatIList#(IL) -> activate#(IL) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatIList#(IL) -> activate#(IL) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatIList#(IL) -> activate#(IL) -> activate#(n__nil()) -> nil#() isNatIList#(IL) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X2) isNatIList#(IL) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X1) isNatIList#(IL) -> activate#(IL) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) SCC Processor: #sccs: 1 #rules: 40 #arcs: 365/3249 DPs: uLength#(tt(),L) -> length#(activate(L)) length#(cons(N,L)) -> uLength#(and(isNat(N),isNatList(activate(L))),activate(L)) uLength#(tt(),L) -> activate#(L) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(M),cons(N,IL)) -> uTake2#(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) uTake2#(tt(),M,N,IL) -> activate#(N) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__length(X)) -> length#(activate(X)) length#(cons(N,L)) -> isNat#(N) isNat#(n__length(L)) -> isNatList#(activate(L)) isNatList#(n__take(N,IL)) -> isNat#(activate(N)) isNat#(n__length(L)) -> activate#(L) activate#(n__length(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) isNat#(n__s(N)) -> isNat#(activate(N)) isNat#(n__s(N)) -> activate#(N) isNatList#(n__take(N,IL)) -> activate#(N) isNatList#(n__take(N,IL)) -> isNatIList#(activate(IL)) isNatIList#(n__cons(N,IL)) -> isNat#(activate(N)) isNatIList#(n__cons(N,IL)) -> activate#(N) isNatIList#(n__cons(N,IL)) -> isNatIList#(activate(IL)) isNatIList#(n__cons(N,IL)) -> activate#(IL) isNatIList#(IL) -> isNatList#(activate(IL)) isNatList#(n__take(N,IL)) -> activate#(IL) isNatList#(n__cons(N,L)) -> isNat#(activate(N)) isNatList#(n__cons(N,L)) -> activate#(N) isNatList#(n__cons(N,L)) -> isNatList#(activate(L)) isNatList#(n__cons(N,L)) -> activate#(L) isNatIList#(IL) -> activate#(IL) length#(cons(N,L)) -> isNatList#(activate(L)) length#(cons(N,L)) -> activate#(L) uTake2#(tt(),M,N,IL) -> activate#(M) uTake2#(tt(),M,N,IL) -> activate#(IL) take#(s(M),cons(N,IL)) -> isNat#(M) take#(s(M),cons(N,IL)) -> isNat#(N) take#(s(M),cons(N,IL)) -> isNatIList#(activate(IL)) take#(s(M),cons(N,IL)) -> activate#(IL) take#(0(),IL) -> isNatIList#(IL) TRS: and(tt(),T) -> T isNatIList(IL) -> isNatList(activate(IL)) isNat(n__0()) -> tt() isNat(n__s(N)) -> isNat(activate(N)) isNat(n__length(L)) -> isNatList(activate(L)) isNatIList(n__zeros()) -> tt() isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__nil()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) zeros() -> cons(0(),n__zeros()) take(0(),IL) -> uTake1(isNatIList(IL)) uTake1(tt()) -> nil() take(s(M),cons(N,IL)) -> uTake2(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) length(cons(N,L)) -> uLength(and(isNat(N),isNatList(activate(L))),activate(L)) uLength(tt(),L) -> s(length(activate(L))) 0() -> n__0() s(X) -> n__s(X) length(X) -> n__length(X) zeros() -> n__zeros() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() take(X1,X2) -> n__take(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__zeros()) -> zeros() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X Open