MAYBE Problem: U101(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS))) U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS))) U21(tt(),X) -> activate(X) U31(tt(),N) -> activate(N) U41(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N)))) U51(tt(),N,XS) -> head(afterNth(activate(N),activate(XS))) U61(tt(),Y) -> activate(Y) U71(tt(),XS) -> pair(nil(),activate(XS)) U81(tt(),N,X,XS) -> U82(splitAt(activate(N),activate(XS)),activate(X)) U82(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) U91(tt(),XS) -> activate(XS) afterNth(N,XS) -> U11(and(isNatural(N),n__isLNat(XS)),N,XS) and(tt(),X) -> activate(X) fst(pair(X,Y)) -> U21(and(isLNat(X),n__isLNat(Y)),X) head(cons(N,XS)) -> U31(and(isNatural(N),n__isLNat(activate(XS))),N) isLNat(n__nil()) -> tt() isLNat(n__afterNth(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat(n__cons(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat(n__fst(V1)) -> isPLNat(activate(V1)) isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)) isLNat(n__snd(V1)) -> isPLNat(activate(V1)) isLNat(n__tail(V1)) -> isLNat(activate(V1)) isLNat(n__take(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural(n__0()) -> tt() isNatural(n__head(V1)) -> isLNat(activate(V1)) isNatural(n__s(V1)) -> isNatural(activate(V1)) isNatural(n__sel(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isPLNat(n__pair(V1,V2)) -> and(isLNat(activate(V1)),n__isLNat(activate(V2))) isPLNat(n__splitAt(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) natsFrom(N) -> U41(isNatural(N),N) sel(N,XS) -> U51(and(isNatural(N),n__isLNat(XS)),N,XS) snd(pair(X,Y)) -> U61(and(isLNat(X),n__isLNat(Y)),Y) splitAt(0(),XS) -> U71(isLNat(XS),XS) splitAt(s(N),cons(X,XS)) -> U81(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) tail(cons(N,XS)) -> U91(and(isNatural(N),n__isLNat(activate(XS))),activate(XS)) take(N,XS) -> U101(and(isNatural(N),n__isLNat(XS)),N,XS) natsFrom(X) -> n__natsFrom(X) isLNat(X) -> n__isLNat(X) nil() -> n__nil() afterNth(X1,X2) -> n__afterNth(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fst(X) -> n__fst(X) snd(X) -> n__snd(X) tail(X) -> n__tail(X) take(X1,X2) -> n__take(X1,X2) 0() -> n__0() head(X) -> n__head(X) s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) pair(X1,X2) -> n__pair(X1,X2) splitAt(X1,X2) -> n__splitAt(X1,X2) and(X1,X2) -> n__and(X1,X2) activate(n__natsFrom(X)) -> natsFrom(X) activate(n__isLNat(X)) -> isLNat(X) activate(n__nil()) -> nil() activate(n__afterNth(X1,X2)) -> afterNth(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__fst(X)) -> fst(X) activate(n__snd(X)) -> snd(X) activate(n__tail(X)) -> tail(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__0()) -> 0() activate(n__head(X)) -> head(X) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__pair(X1,X2)) -> pair(X1,X2) activate(n__splitAt(X1,X2)) -> splitAt(X1,X2) activate(n__and(X1,X2)) -> and(X1,X2) activate(X) -> X Proof: DP Processor: DPs: U101#(tt(),N,XS) -> activate#(XS) U101#(tt(),N,XS) -> activate#(N) U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) U101#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS))) U11#(tt(),N,XS) -> activate#(XS) U11#(tt(),N,XS) -> activate#(N) U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS))) U21#(tt(),X) -> activate#(X) U31#(tt(),N) -> activate#(N) U41#(tt(),N) -> s#(activate(N)) U41#(tt(),N) -> activate#(N) U41#(tt(),N) -> cons#(activate(N),n__natsFrom(s(activate(N)))) U51#(tt(),N,XS) -> activate#(XS) U51#(tt(),N,XS) -> activate#(N) U51#(tt(),N,XS) -> afterNth#(activate(N),activate(XS)) U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) U61#(tt(),Y) -> activate#(Y) U71#(tt(),XS) -> activate#(XS) U71#(tt(),XS) -> nil#() U71#(tt(),XS) -> pair#(nil(),activate(XS)) U81#(tt(),N,X,XS) -> activate#(X) U81#(tt(),N,X,XS) -> activate#(XS) U81#(tt(),N,X,XS) -> activate#(N) U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) U81#(tt(),N,X,XS) -> U82#(splitAt(activate(N),activate(XS)),activate(X)) U82#(pair(YS,ZS),X) -> activate#(X) U82#(pair(YS,ZS),X) -> cons#(activate(X),YS) U82#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS) U91#(tt(),XS) -> activate#(XS) afterNth#(N,XS) -> isNatural#(N) afterNth#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS) and#(tt(),X) -> activate#(X) fst#(pair(X,Y)) -> isLNat#(X) fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) fst#(pair(X,Y)) -> U21#(and(isLNat(X),n__isLNat(Y)),X) head#(cons(N,XS)) -> activate#(XS) head#(cons(N,XS)) -> isNatural#(N) head#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) head#(cons(N,XS)) -> U31#(and(isNatural(N),n__isLNat(activate(XS))),N) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__cons(V1,V2)) -> activate#(V2) isLNat#(n__cons(V1,V2)) -> activate#(V1) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__fst(V1)) -> activate#(V1) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) isLNat#(n__natsFrom(V1)) -> activate#(V1) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) isLNat#(n__snd(V1)) -> activate#(V1) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) isLNat#(n__tail(V1)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) isLNat#(n__take(V1,V2)) -> activate#(V2) isLNat#(n__take(V1,V2)) -> activate#(V1) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural#(n__head(V1)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) isNatural#(n__s(V1)) -> activate#(V1) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) isNatural#(n__sel(V1,V2)) -> activate#(V2) isNatural#(n__sel(V1,V2)) -> activate#(V1) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isPLNat#(n__pair(V1,V2)) -> activate#(V2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> and#(isLNat(activate(V1)),n__isLNat(activate(V2))) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) isPLNat#(n__splitAt(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) natsFrom#(N) -> isNatural#(N) natsFrom#(N) -> U41#(isNatural(N),N) sel#(N,XS) -> isNatural#(N) sel#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS) snd#(pair(X,Y)) -> isLNat#(X) snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) snd#(pair(X,Y)) -> U61#(and(isLNat(X),n__isLNat(Y)),Y) splitAt#(0(),XS) -> isLNat#(XS) splitAt#(0(),XS) -> U71#(isLNat(XS),XS) splitAt#(s(N),cons(X,XS)) -> activate#(XS) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))) splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) tail#(cons(N,XS)) -> activate#(XS) tail#(cons(N,XS)) -> isNatural#(N) tail#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) tail#(cons(N,XS)) -> U91#(and(isNatural(N),n__isLNat(activate(XS))),activate(XS)) take#(N,XS) -> isNatural#(N) take#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS) activate#(n__natsFrom(X)) -> natsFrom#(X) activate#(n__isLNat(X)) -> isLNat#(X) activate#(n__nil()) -> nil#() activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) activate#(n__cons(X1,X2)) -> cons#(X1,X2) activate#(n__fst(X)) -> fst#(X) activate#(n__snd(X)) -> snd#(X) activate#(n__tail(X)) -> tail#(X) activate#(n__take(X1,X2)) -> take#(X1,X2) activate#(n__0()) -> 0#() activate#(n__head(X)) -> head#(X) activate#(n__s(X)) -> s#(X) activate#(n__sel(X1,X2)) -> sel#(X1,X2) activate#(n__pair(X1,X2)) -> pair#(X1,X2) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) activate#(n__and(X1,X2)) -> and#(X1,X2) TRS: U101(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS))) U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS))) U21(tt(),X) -> activate(X) U31(tt(),N) -> activate(N) U41(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N)))) U51(tt(),N,XS) -> head(afterNth(activate(N),activate(XS))) U61(tt(),Y) -> activate(Y) U71(tt(),XS) -> pair(nil(),activate(XS)) U81(tt(),N,X,XS) -> U82(splitAt(activate(N),activate(XS)),activate(X)) U82(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) U91(tt(),XS) -> activate(XS) afterNth(N,XS) -> U11(and(isNatural(N),n__isLNat(XS)),N,XS) and(tt(),X) -> activate(X) fst(pair(X,Y)) -> U21(and(isLNat(X),n__isLNat(Y)),X) head(cons(N,XS)) -> U31(and(isNatural(N),n__isLNat(activate(XS))),N) isLNat(n__nil()) -> tt() isLNat(n__afterNth(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat(n__cons(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat(n__fst(V1)) -> isPLNat(activate(V1)) isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)) isLNat(n__snd(V1)) -> isPLNat(activate(V1)) isLNat(n__tail(V1)) -> isLNat(activate(V1)) isLNat(n__take(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural(n__0()) -> tt() isNatural(n__head(V1)) -> isLNat(activate(V1)) isNatural(n__s(V1)) -> isNatural(activate(V1)) isNatural(n__sel(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isPLNat(n__pair(V1,V2)) -> and(isLNat(activate(V1)),n__isLNat(activate(V2))) isPLNat(n__splitAt(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) natsFrom(N) -> U41(isNatural(N),N) sel(N,XS) -> U51(and(isNatural(N),n__isLNat(XS)),N,XS) snd(pair(X,Y)) -> U61(and(isLNat(X),n__isLNat(Y)),Y) splitAt(0(),XS) -> U71(isLNat(XS),XS) splitAt(s(N),cons(X,XS)) -> U81(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) tail(cons(N,XS)) -> U91(and(isNatural(N),n__isLNat(activate(XS))),activate(XS)) take(N,XS) -> U101(and(isNatural(N),n__isLNat(XS)),N,XS) natsFrom(X) -> n__natsFrom(X) isLNat(X) -> n__isLNat(X) nil() -> n__nil() afterNth(X1,X2) -> n__afterNth(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fst(X) -> n__fst(X) snd(X) -> n__snd(X) tail(X) -> n__tail(X) take(X1,X2) -> n__take(X1,X2) 0() -> n__0() head(X) -> n__head(X) s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) pair(X1,X2) -> n__pair(X1,X2) splitAt(X1,X2) -> n__splitAt(X1,X2) and(X1,X2) -> n__and(X1,X2) activate(n__natsFrom(X)) -> natsFrom(X) activate(n__isLNat(X)) -> isLNat(X) activate(n__nil()) -> nil() activate(n__afterNth(X1,X2)) -> afterNth(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__fst(X)) -> fst(X) activate(n__snd(X)) -> snd(X) activate(n__tail(X)) -> tail(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__0()) -> 0() activate(n__head(X)) -> head(X) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__pair(X1,X2)) -> pair(X1,X2) activate(n__splitAt(X1,X2)) -> splitAt(X1,X2) activate(n__and(X1,X2)) -> and(X1,X2) activate(X) -> X TDG Processor: DPs: U101#(tt(),N,XS) -> activate#(XS) U101#(tt(),N,XS) -> activate#(N) U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) U101#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS))) U11#(tt(),N,XS) -> activate#(XS) U11#(tt(),N,XS) -> activate#(N) U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS))) U21#(tt(),X) -> activate#(X) U31#(tt(),N) -> activate#(N) U41#(tt(),N) -> s#(activate(N)) U41#(tt(),N) -> activate#(N) U41#(tt(),N) -> cons#(activate(N),n__natsFrom(s(activate(N)))) U51#(tt(),N,XS) -> activate#(XS) U51#(tt(),N,XS) -> activate#(N) U51#(tt(),N,XS) -> afterNth#(activate(N),activate(XS)) U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) U61#(tt(),Y) -> activate#(Y) U71#(tt(),XS) -> activate#(XS) U71#(tt(),XS) -> nil#() U71#(tt(),XS) -> pair#(nil(),activate(XS)) U81#(tt(),N,X,XS) -> activate#(X) U81#(tt(),N,X,XS) -> activate#(XS) U81#(tt(),N,X,XS) -> activate#(N) U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) U81#(tt(),N,X,XS) -> U82#(splitAt(activate(N),activate(XS)),activate(X)) U82#(pair(YS,ZS),X) -> activate#(X) U82#(pair(YS,ZS),X) -> cons#(activate(X),YS) U82#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS) U91#(tt(),XS) -> activate#(XS) afterNth#(N,XS) -> isNatural#(N) afterNth#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS) and#(tt(),X) -> activate#(X) fst#(pair(X,Y)) -> isLNat#(X) fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) fst#(pair(X,Y)) -> U21#(and(isLNat(X),n__isLNat(Y)),X) head#(cons(N,XS)) -> activate#(XS) head#(cons(N,XS)) -> isNatural#(N) head#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) head#(cons(N,XS)) -> U31#(and(isNatural(N),n__isLNat(activate(XS))),N) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__cons(V1,V2)) -> activate#(V2) isLNat#(n__cons(V1,V2)) -> activate#(V1) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__fst(V1)) -> activate#(V1) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) isLNat#(n__natsFrom(V1)) -> activate#(V1) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) isLNat#(n__snd(V1)) -> activate#(V1) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) isLNat#(n__tail(V1)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) isLNat#(n__take(V1,V2)) -> activate#(V2) isLNat#(n__take(V1,V2)) -> activate#(V1) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural#(n__head(V1)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) isNatural#(n__s(V1)) -> activate#(V1) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) isNatural#(n__sel(V1,V2)) -> activate#(V2) isNatural#(n__sel(V1,V2)) -> activate#(V1) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isPLNat#(n__pair(V1,V2)) -> activate#(V2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> and#(isLNat(activate(V1)),n__isLNat(activate(V2))) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) isPLNat#(n__splitAt(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) natsFrom#(N) -> isNatural#(N) natsFrom#(N) -> U41#(isNatural(N),N) sel#(N,XS) -> isNatural#(N) sel#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS) snd#(pair(X,Y)) -> isLNat#(X) snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) snd#(pair(X,Y)) -> U61#(and(isLNat(X),n__isLNat(Y)),Y) splitAt#(0(),XS) -> isLNat#(XS) splitAt#(0(),XS) -> U71#(isLNat(XS),XS) splitAt#(s(N),cons(X,XS)) -> activate#(XS) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))) splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) tail#(cons(N,XS)) -> activate#(XS) tail#(cons(N,XS)) -> isNatural#(N) tail#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) tail#(cons(N,XS)) -> U91#(and(isNatural(N),n__isLNat(activate(XS))),activate(XS)) take#(N,XS) -> isNatural#(N) take#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS) activate#(n__natsFrom(X)) -> natsFrom#(X) activate#(n__isLNat(X)) -> isLNat#(X) activate#(n__nil()) -> nil#() activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) activate#(n__cons(X1,X2)) -> cons#(X1,X2) activate#(n__fst(X)) -> fst#(X) activate#(n__snd(X)) -> snd#(X) activate#(n__tail(X)) -> tail#(X) activate#(n__take(X1,X2)) -> take#(X1,X2) activate#(n__0()) -> 0#() activate#(n__head(X)) -> head#(X) activate#(n__s(X)) -> s#(X) activate#(n__sel(X1,X2)) -> sel#(X1,X2) activate#(n__pair(X1,X2)) -> pair#(X1,X2) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) activate#(n__and(X1,X2)) -> and#(X1,X2) TRS: U101(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS))) U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS))) U21(tt(),X) -> activate(X) U31(tt(),N) -> activate(N) U41(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N)))) U51(tt(),N,XS) -> head(afterNth(activate(N),activate(XS))) U61(tt(),Y) -> activate(Y) U71(tt(),XS) -> pair(nil(),activate(XS)) U81(tt(),N,X,XS) -> U82(splitAt(activate(N),activate(XS)),activate(X)) U82(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) U91(tt(),XS) -> activate(XS) afterNth(N,XS) -> U11(and(isNatural(N),n__isLNat(XS)),N,XS) and(tt(),X) -> activate(X) fst(pair(X,Y)) -> U21(and(isLNat(X),n__isLNat(Y)),X) head(cons(N,XS)) -> U31(and(isNatural(N),n__isLNat(activate(XS))),N) isLNat(n__nil()) -> tt() isLNat(n__afterNth(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat(n__cons(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat(n__fst(V1)) -> isPLNat(activate(V1)) isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)) isLNat(n__snd(V1)) -> isPLNat(activate(V1)) isLNat(n__tail(V1)) -> isLNat(activate(V1)) isLNat(n__take(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural(n__0()) -> tt() isNatural(n__head(V1)) -> isLNat(activate(V1)) isNatural(n__s(V1)) -> isNatural(activate(V1)) isNatural(n__sel(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isPLNat(n__pair(V1,V2)) -> and(isLNat(activate(V1)),n__isLNat(activate(V2))) isPLNat(n__splitAt(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) natsFrom(N) -> U41(isNatural(N),N) sel(N,XS) -> U51(and(isNatural(N),n__isLNat(XS)),N,XS) snd(pair(X,Y)) -> U61(and(isLNat(X),n__isLNat(Y)),Y) splitAt(0(),XS) -> U71(isLNat(XS),XS) splitAt(s(N),cons(X,XS)) -> U81(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) tail(cons(N,XS)) -> U91(and(isNatural(N),n__isLNat(activate(XS))),activate(XS)) take(N,XS) -> U101(and(isNatural(N),n__isLNat(XS)),N,XS) natsFrom(X) -> n__natsFrom(X) isLNat(X) -> n__isLNat(X) nil() -> n__nil() afterNth(X1,X2) -> n__afterNth(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fst(X) -> n__fst(X) snd(X) -> n__snd(X) tail(X) -> n__tail(X) take(X1,X2) -> n__take(X1,X2) 0() -> n__0() head(X) -> n__head(X) s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) pair(X1,X2) -> n__pair(X1,X2) splitAt(X1,X2) -> n__splitAt(X1,X2) and(X1,X2) -> n__and(X1,X2) activate(n__natsFrom(X)) -> natsFrom(X) activate(n__isLNat(X)) -> isLNat(X) activate(n__nil()) -> nil() activate(n__afterNth(X1,X2)) -> afterNth(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__fst(X)) -> fst(X) activate(n__snd(X)) -> snd(X) activate(n__tail(X)) -> tail(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__0()) -> 0() activate(n__head(X)) -> head(X) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__pair(X1,X2)) -> pair(X1,X2) activate(n__splitAt(X1,X2)) -> splitAt(X1,X2) activate(n__and(X1,X2)) -> and(X1,X2) activate(X) -> X graph: take#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) -> and#(tt(),X) -> activate#(X) take#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) take#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) take#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) take#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) take#(N,XS) -> isNatural#(N) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) take#(N,XS) -> isNatural#(N) -> isNatural#(n__s(V1)) -> activate#(V1) take#(N,XS) -> isNatural#(N) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) take#(N,XS) -> isNatural#(N) -> isNatural#(n__head(V1)) -> activate#(V1) take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U101#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS))) take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U101#(tt(),N,XS) -> activate#(N) take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U101#(tt(),N,XS) -> activate#(XS) tail#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) -> and#(tt(),X) -> activate#(X) tail#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) tail#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) tail#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) tail#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) tail#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) tail#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__s(V1)) -> activate#(V1) tail#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) tail#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__head(V1)) -> activate#(V1) tail#(cons(N,XS)) -> U91#(and(isNatural(N),n__isLNat(activate(XS))),activate(XS)) -> U91#(tt(),XS) -> activate#(XS) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__and(X1,X2)) -> and#(X1,X2) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__s(X)) -> s#(X) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__head(X)) -> head#(X) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__0()) -> 0#() tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__take(X1,X2)) -> take#(X1,X2) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__tail(X)) -> tail#(X) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__snd(X)) -> snd#(X) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__fst(X)) -> fst#(X) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__nil()) -> nil#() tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__isLNat(X)) -> isLNat#(X) tail#(cons(N,XS)) -> activate#(XS) -> activate#(n__natsFrom(X)) -> natsFrom#(X) sel#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) -> and#(tt(),X) -> activate#(X) sel#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) sel#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) sel#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) sel#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) sel#(N,XS) -> isNatural#(N) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) sel#(N,XS) -> isNatural#(N) -> isNatural#(n__s(V1)) -> activate#(V1) sel#(N,XS) -> isNatural#(N) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) sel#(N,XS) -> isNatural#(N) -> isNatural#(n__head(V1)) -> activate#(V1) sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U51#(tt(),N,XS) -> afterNth#(activate(N),activate(XS)) sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U51#(tt(),N,XS) -> activate#(N) sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U51#(tt(),N,XS) -> activate#(XS) natsFrom#(N) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) natsFrom#(N) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) natsFrom#(N) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) natsFrom#(N) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) natsFrom#(N) -> isNatural#(N) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) natsFrom#(N) -> isNatural#(N) -> isNatural#(n__s(V1)) -> activate#(V1) natsFrom#(N) -> isNatural#(N) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) natsFrom#(N) -> isNatural#(N) -> isNatural#(n__head(V1)) -> activate#(V1) natsFrom#(N) -> U41#(isNatural(N),N) -> U41#(tt(),N) -> cons#(activate(N),n__natsFrom(s(activate(N)))) natsFrom#(N) -> U41#(isNatural(N),N) -> U41#(tt(),N) -> activate#(N) natsFrom#(N) -> U41#(isNatural(N),N) -> U41#(tt(),N) -> s#(activate(N)) isPLNat#(n__splitAt(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) -> and#(tt(),X) -> activate#(X) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> activate#(V1) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> activate#(V1) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__head(X)) -> head#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__tail(X)) -> tail#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__snd(X)) -> snd#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__fst(X)) -> fst#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__isLNat(X)) -> isLNat#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> activate#(V2) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__tail(V1)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__snd(V1)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__natsFrom(V1)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__fst(V1)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> activate#(V2) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V2) isPLNat#(n__pair(V1,V2)) -> and#(isLNat(activate(V1)),n__isLNat(activate(V2))) -> and#(tt(),X) -> activate#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__head(X)) -> head#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__tail(X)) -> tail#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__snd(X)) -> snd#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__fst(X)) -> fst#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__isLNat(X)) -> isLNat#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V2) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isPLNat#(n__pair(V1,V2)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) -> and#(tt(),X) -> activate#(X) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> activate#(V1) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> activate#(V1) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__head(X)) -> head#(X) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__tail(X)) -> tail#(X) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__snd(X)) -> snd#(X) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__fst(X)) -> fst#(X) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__take(V1,V2)) -> activate#(V2) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__take(V1,V2)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> activate#(V2) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__tail(V1)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__snd(V1)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__natsFrom(V1)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__fst(V1)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> activate#(V2) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V2) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__tail(V1)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__splitAt(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__pair(V1,V2)) -> and#(isLNat(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__pair(V1,V2)) -> activate#(V1) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__pair(V1,V2)) -> activate#(V2) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__snd(V1)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__splitAt(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__pair(V1,V2)) -> and#(isLNat(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__pair(V1,V2)) -> activate#(V1) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) -> isPLNat#(n__pair(V1,V2)) -> activate#(V2) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__fst(V1)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) -> and#(tt(),X) -> activate#(X) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> activate#(V1) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> activate#(V1) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__head(X)) -> head#(X) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__tail(X)) -> tail#(X) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__snd(X)) -> snd#(X) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__fst(X)) -> fst#(X) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) -> and#(tt(),X) -> activate#(X) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> activate#(V1) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> activate#(V1) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__head(X)) -> head#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__tail(X)) -> tail#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__snd(X)) -> snd#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__fst(X)) -> fst#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> activate#(V1) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> activate#(V1) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__natsFrom(V1)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) and#(tt(),X) -> activate#(X) -> activate#(n__and(X1,X2)) -> and#(X1,X2) and#(tt(),X) -> activate#(X) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) and#(tt(),X) -> activate#(X) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) and#(tt(),X) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) and#(tt(),X) -> activate#(X) -> activate#(n__s(X)) -> s#(X) and#(tt(),X) -> activate#(X) -> activate#(n__head(X)) -> head#(X) and#(tt(),X) -> activate#(X) -> activate#(n__0()) -> 0#() and#(tt(),X) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(X1,X2) and#(tt(),X) -> activate#(X) -> activate#(n__tail(X)) -> tail#(X) and#(tt(),X) -> activate#(X) -> activate#(n__snd(X)) -> snd#(X) and#(tt(),X) -> activate#(X) -> activate#(n__fst(X)) -> fst#(X) and#(tt(),X) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) and#(tt(),X) -> activate#(X) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) and#(tt(),X) -> activate#(X) -> activate#(n__nil()) -> nil#() and#(tt(),X) -> activate#(X) -> activate#(n__isLNat(X)) -> isLNat#(X) and#(tt(),X) -> activate#(X) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) -> and#(tt(),X) -> activate#(X) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> activate#(V1) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> activate#(V1) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__head(X)) -> head#(X) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__tail(X)) -> tail#(X) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__snd(X)) -> snd#(X) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__fst(X)) -> fst#(X) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__isLNat(X)) -> isLNat#(X) isNatural#(n__sel(V1,V2)) -> activate#(V2) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isNatural#(n__sel(V1,V2)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__s(V1)) -> activate#(V1) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) -> isNatural#(n__head(V1)) -> activate#(V1) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isNatural#(n__s(V1)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__take(V1,V2)) -> activate#(V2) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__tail(V1)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__snd(V1)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__natsFrom(V1)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__fst(V1)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__cons(V1,V2)) -> activate#(V2) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V2) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__and(X1,X2)) -> and#(X1,X2) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__head(X)) -> head#(X) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__take(X1,X2)) -> take#(X1,X2) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__tail(X)) -> tail#(X) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__snd(X)) -> snd#(X) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__fst(X)) -> fst#(X) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__isLNat(X)) -> isLNat#(X) isNatural#(n__head(V1)) -> activate#(V1) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U91#(tt(),XS) -> activate#(XS) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U91#(tt(),XS) -> activate#(XS) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U91#(tt(),XS) -> activate#(XS) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U91#(tt(),XS) -> activate#(XS) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U91#(tt(),XS) -> activate#(XS) -> activate#(n__s(X)) -> s#(X) U91#(tt(),XS) -> activate#(XS) -> activate#(n__head(X)) -> head#(X) U91#(tt(),XS) -> activate#(XS) -> activate#(n__0()) -> 0#() U91#(tt(),XS) -> activate#(XS) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U91#(tt(),XS) -> activate#(XS) -> activate#(n__tail(X)) -> tail#(X) U91#(tt(),XS) -> activate#(XS) -> activate#(n__snd(X)) -> snd#(X) U91#(tt(),XS) -> activate#(XS) -> activate#(n__fst(X)) -> fst#(X) U91#(tt(),XS) -> activate#(XS) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U91#(tt(),XS) -> activate#(XS) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U91#(tt(),XS) -> activate#(XS) -> activate#(n__nil()) -> nil#() U91#(tt(),XS) -> activate#(XS) -> activate#(n__isLNat(X)) -> isLNat#(X) U91#(tt(),XS) -> activate#(XS) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__s(X)) -> s#(X) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__head(X)) -> head#(X) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__0()) -> 0#() U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__tail(X)) -> tail#(X) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__snd(X)) -> snd#(X) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__fst(X)) -> fst#(X) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__nil()) -> nil#() U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__isLNat(X)) -> isLNat#(X) U82#(pair(YS,ZS),X) -> activate#(X) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U81#(tt(),N,X,XS) -> U82#(splitAt(activate(N),activate(XS)),activate(X)) -> U82#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS) U81#(tt(),N,X,XS) -> U82#(splitAt(activate(N),activate(XS)),activate(X)) -> U82#(pair(YS,ZS),X) -> cons#(activate(X),YS) U81#(tt(),N,X,XS) -> U82#(splitAt(activate(N),activate(XS)),activate(X)) -> U82#(pair(YS,ZS),X) -> activate#(X) U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))) U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> isNatural#(N) U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> isNatural#(X) U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> activate#(XS) U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(0(),XS) -> U71#(isLNat(XS),XS) U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(0(),XS) -> isLNat#(XS) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__s(X)) -> s#(X) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__head(X)) -> head#(X) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__0()) -> 0#() U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__tail(X)) -> tail#(X) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__snd(X)) -> snd#(X) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__fst(X)) -> fst#(X) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__nil()) -> nil#() U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__isLNat(X)) -> isLNat#(X) U81#(tt(),N,X,XS) -> activate#(XS) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__s(X)) -> s#(X) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__head(X)) -> head#(X) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__0()) -> 0#() U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__tail(X)) -> tail#(X) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__snd(X)) -> snd#(X) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__fst(X)) -> fst#(X) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__nil()) -> nil#() U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__isLNat(X)) -> isLNat#(X) U81#(tt(),N,X,XS) -> activate#(X) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__head(X)) -> head#(X) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__0()) -> 0#() U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__tail(X)) -> tail#(X) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__snd(X)) -> snd#(X) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__fst(X)) -> fst#(X) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__nil()) -> nil#() U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__isLNat(X)) -> isLNat#(X) U81#(tt(),N,X,XS) -> activate#(N) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U71#(tt(),XS) -> activate#(XS) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U71#(tt(),XS) -> activate#(XS) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U71#(tt(),XS) -> activate#(XS) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U71#(tt(),XS) -> activate#(XS) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U71#(tt(),XS) -> activate#(XS) -> activate#(n__s(X)) -> s#(X) U71#(tt(),XS) -> activate#(XS) -> activate#(n__head(X)) -> head#(X) U71#(tt(),XS) -> activate#(XS) -> activate#(n__0()) -> 0#() U71#(tt(),XS) -> activate#(XS) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U71#(tt(),XS) -> activate#(XS) -> activate#(n__tail(X)) -> tail#(X) U71#(tt(),XS) -> activate#(XS) -> activate#(n__snd(X)) -> snd#(X) U71#(tt(),XS) -> activate#(XS) -> activate#(n__fst(X)) -> fst#(X) U71#(tt(),XS) -> activate#(XS) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U71#(tt(),XS) -> activate#(XS) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U71#(tt(),XS) -> activate#(XS) -> activate#(n__nil()) -> nil#() U71#(tt(),XS) -> activate#(XS) -> activate#(n__isLNat(X)) -> isLNat#(X) U71#(tt(),XS) -> activate#(XS) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U61#(tt(),Y) -> activate#(Y) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U61#(tt(),Y) -> activate#(Y) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U61#(tt(),Y) -> activate#(Y) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U61#(tt(),Y) -> activate#(Y) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U61#(tt(),Y) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) U61#(tt(),Y) -> activate#(Y) -> activate#(n__head(X)) -> head#(X) U61#(tt(),Y) -> activate#(Y) -> activate#(n__0()) -> 0#() U61#(tt(),Y) -> activate#(Y) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U61#(tt(),Y) -> activate#(Y) -> activate#(n__tail(X)) -> tail#(X) U61#(tt(),Y) -> activate#(Y) -> activate#(n__snd(X)) -> snd#(X) U61#(tt(),Y) -> activate#(Y) -> activate#(n__fst(X)) -> fst#(X) U61#(tt(),Y) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U61#(tt(),Y) -> activate#(Y) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U61#(tt(),Y) -> activate#(Y) -> activate#(n__nil()) -> nil#() U61#(tt(),Y) -> activate#(Y) -> activate#(n__isLNat(X)) -> isLNat#(X) U61#(tt(),Y) -> activate#(Y) -> activate#(n__natsFrom(X)) -> natsFrom#(X) head#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) -> and#(tt(),X) -> activate#(X) head#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) head#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) head#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) head#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) head#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) head#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__s(V1)) -> activate#(V1) head#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) head#(cons(N,XS)) -> isNatural#(N) -> isNatural#(n__head(V1)) -> activate#(V1) head#(cons(N,XS)) -> U31#(and(isNatural(N),n__isLNat(activate(XS))),N) -> U31#(tt(),N) -> activate#(N) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__and(X1,X2)) -> and#(X1,X2) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__s(X)) -> s#(X) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__head(X)) -> head#(X) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__0()) -> 0#() head#(cons(N,XS)) -> activate#(XS) -> activate#(n__take(X1,X2)) -> take#(X1,X2) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__tail(X)) -> tail#(X) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__snd(X)) -> snd#(X) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__fst(X)) -> fst#(X) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__nil()) -> nil#() head#(cons(N,XS)) -> activate#(XS) -> activate#(n__isLNat(X)) -> isLNat#(X) head#(cons(N,XS)) -> activate#(XS) -> activate#(n__natsFrom(X)) -> natsFrom#(X) afterNth#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) -> and#(tt(),X) -> activate#(X) afterNth#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) afterNth#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) afterNth#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) afterNth#(N,XS) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) afterNth#(N,XS) -> isNatural#(N) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) afterNth#(N,XS) -> isNatural#(N) -> isNatural#(n__s(V1)) -> activate#(V1) afterNth#(N,XS) -> isNatural#(N) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) afterNth#(N,XS) -> isNatural#(N) -> isNatural#(n__head(V1)) -> activate#(V1) afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS))) afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U11#(tt(),N,XS) -> activate#(N) afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS) -> U11#(tt(),N,XS) -> activate#(XS) U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) -> head#(cons(N,XS)) -> U31#(and(isNatural(N),n__isLNat(activate(XS))),N) U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) -> head#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) -> head#(cons(N,XS)) -> isNatural#(N) U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) -> head#(cons(N,XS)) -> activate#(XS) U51#(tt(),N,XS) -> afterNth#(activate(N),activate(XS)) -> afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS) U51#(tt(),N,XS) -> afterNth#(activate(N),activate(XS)) -> afterNth#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) U51#(tt(),N,XS) -> afterNth#(activate(N),activate(XS)) -> afterNth#(N,XS) -> isNatural#(N) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__s(X)) -> s#(X) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__head(X)) -> head#(X) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__0()) -> 0#() U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__tail(X)) -> tail#(X) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__snd(X)) -> snd#(X) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__fst(X)) -> fst#(X) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__nil()) -> nil#() U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__isLNat(X)) -> isLNat#(X) U51#(tt(),N,XS) -> activate#(XS) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__head(X)) -> head#(X) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__0()) -> 0#() U51#(tt(),N,XS) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__tail(X)) -> tail#(X) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__snd(X)) -> snd#(X) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__fst(X)) -> fst#(X) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__nil()) -> nil#() U51#(tt(),N,XS) -> activate#(N) -> activate#(n__isLNat(X)) -> isLNat#(X) U51#(tt(),N,XS) -> activate#(N) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U41#(tt(),N) -> activate#(N) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U41#(tt(),N) -> activate#(N) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U41#(tt(),N) -> activate#(N) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U41#(tt(),N) -> activate#(N) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U41#(tt(),N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U41#(tt(),N) -> activate#(N) -> activate#(n__head(X)) -> head#(X) U41#(tt(),N) -> activate#(N) -> activate#(n__0()) -> 0#() U41#(tt(),N) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U41#(tt(),N) -> activate#(N) -> activate#(n__tail(X)) -> tail#(X) U41#(tt(),N) -> activate#(N) -> activate#(n__snd(X)) -> snd#(X) U41#(tt(),N) -> activate#(N) -> activate#(n__fst(X)) -> fst#(X) U41#(tt(),N) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U41#(tt(),N) -> activate#(N) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U41#(tt(),N) -> activate#(N) -> activate#(n__nil()) -> nil#() U41#(tt(),N) -> activate#(N) -> activate#(n__isLNat(X)) -> isLNat#(X) U41#(tt(),N) -> activate#(N) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U31#(tt(),N) -> activate#(N) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U31#(tt(),N) -> activate#(N) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U31#(tt(),N) -> activate#(N) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U31#(tt(),N) -> activate#(N) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U31#(tt(),N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U31#(tt(),N) -> activate#(N) -> activate#(n__head(X)) -> head#(X) U31#(tt(),N) -> activate#(N) -> activate#(n__0()) -> 0#() U31#(tt(),N) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U31#(tt(),N) -> activate#(N) -> activate#(n__tail(X)) -> tail#(X) U31#(tt(),N) -> activate#(N) -> activate#(n__snd(X)) -> snd#(X) U31#(tt(),N) -> activate#(N) -> activate#(n__fst(X)) -> fst#(X) U31#(tt(),N) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U31#(tt(),N) -> activate#(N) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U31#(tt(),N) -> activate#(N) -> activate#(n__nil()) -> nil#() U31#(tt(),N) -> activate#(N) -> activate#(n__isLNat(X)) -> isLNat#(X) U31#(tt(),N) -> activate#(N) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U21#(tt(),X) -> activate#(X) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U21#(tt(),X) -> activate#(X) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U21#(tt(),X) -> activate#(X) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U21#(tt(),X) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U21#(tt(),X) -> activate#(X) -> activate#(n__s(X)) -> s#(X) U21#(tt(),X) -> activate#(X) -> activate#(n__head(X)) -> head#(X) U21#(tt(),X) -> activate#(X) -> activate#(n__0()) -> 0#() U21#(tt(),X) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U21#(tt(),X) -> activate#(X) -> activate#(n__tail(X)) -> tail#(X) U21#(tt(),X) -> activate#(X) -> activate#(n__snd(X)) -> snd#(X) U21#(tt(),X) -> activate#(X) -> activate#(n__fst(X)) -> fst#(X) U21#(tt(),X) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U21#(tt(),X) -> activate#(X) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U21#(tt(),X) -> activate#(X) -> activate#(n__nil()) -> nil#() U21#(tt(),X) -> activate#(X) -> activate#(n__isLNat(X)) -> isLNat#(X) U21#(tt(),X) -> activate#(X) -> activate#(n__natsFrom(X)) -> natsFrom#(X) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> activate#(V1) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> activate#(V2) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__tail(V1)) -> activate#(V1) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__snd(V1)) -> activate#(V1) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__natsFrom(V1)) -> activate#(V1) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__fst(V1)) -> activate#(V1) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> activate#(V1) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> activate#(V2) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V1) snd#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V2) snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) -> and#(tt(),X) -> activate#(X) snd#(pair(X,Y)) -> U61#(and(isLNat(X),n__isLNat(Y)),Y) -> U61#(tt(),Y) -> activate#(Y) U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS))) -> snd#(pair(X,Y)) -> U61#(and(isLNat(X),n__isLNat(Y)),Y) U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS))) -> snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS))) -> snd#(pair(X,Y)) -> isLNat#(X) U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))) U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> isNatural#(N) U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> isNatural#(X) U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> activate#(XS) U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(0(),XS) -> U71#(isLNat(XS),XS) U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(0(),XS) -> isLNat#(XS) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__s(X)) -> s#(X) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__head(X)) -> head#(X) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__0()) -> 0#() U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__tail(X)) -> tail#(X) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__snd(X)) -> snd#(X) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__fst(X)) -> fst#(X) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__nil()) -> nil#() U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__isLNat(X)) -> isLNat#(X) U11#(tt(),N,XS) -> activate#(XS) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__head(X)) -> head#(X) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__0()) -> 0#() U11#(tt(),N,XS) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__tail(X)) -> tail#(X) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__snd(X)) -> snd#(X) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__fst(X)) -> fst#(X) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__nil()) -> nil#() U11#(tt(),N,XS) -> activate#(N) -> activate#(n__isLNat(X)) -> isLNat#(X) U11#(tt(),N,XS) -> activate#(N) -> activate#(n__natsFrom(X)) -> natsFrom#(X) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> activate#(V1) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> activate#(V2) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__tail(V1)) -> activate#(V1) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__snd(V1)) -> activate#(V1) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__natsFrom(V1)) -> activate#(V1) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__fst(V1)) -> activate#(V1) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> activate#(V1) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> activate#(V2) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V1) fst#(pair(X,Y)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V2) fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) -> and#(tt(),X) -> activate#(X) fst#(pair(X,Y)) -> U21#(and(isLNat(X),n__isLNat(Y)),X) -> U21#(tt(),X) -> activate#(X) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__take(V1,V2)) -> activate#(V1) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__take(V1,V2)) -> activate#(V2) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__tail(V1)) -> activate#(V1) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__snd(V1)) -> activate#(V1) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__natsFrom(V1)) -> activate#(V1) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__fst(V1)) -> activate#(V1) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__cons(V1,V2)) -> activate#(V1) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__cons(V1,V2)) -> activate#(V2) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V1) splitAt#(0(),XS) -> isLNat#(XS) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V2) splitAt#(0(),XS) -> U71#(isLNat(XS),XS) -> U71#(tt(),XS) -> pair#(nil(),activate(XS)) splitAt#(0(),XS) -> U71#(isLNat(XS),XS) -> U71#(tt(),XS) -> nil#() splitAt#(0(),XS) -> U71#(isLNat(XS),XS) -> U71#(tt(),XS) -> activate#(XS) splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))) -> and#(tt(),X) -> activate#(X) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) -> isNatural#(n__s(V1)) -> activate#(V1) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) -> isNatural#(n__head(V1)) -> activate#(V1) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V1) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) -> isNatural#(n__sel(V1,V2)) -> activate#(V2) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) -> isNatural#(n__s(V1)) -> isNatural#(activate(V1)) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) -> isNatural#(n__s(V1)) -> activate#(V1) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) -> isNatural#(n__head(V1)) -> isLNat#(activate(V1)) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) -> isNatural#(n__head(V1)) -> activate#(V1) splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) -> U81#(tt(),N,X,XS) -> U82#(splitAt(activate(N),activate(XS)),activate(X)) splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) -> U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) -> U81#(tt(),N,X,XS) -> activate#(N) splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) -> U81#(tt(),N,X,XS) -> activate#(XS) splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) -> U81#(tt(),N,X,XS) -> activate#(X) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__and(X1,X2)) -> and#(X1,X2) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__s(X)) -> s#(X) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__head(X)) -> head#(X) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__0()) -> 0#() splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__take(X1,X2)) -> take#(X1,X2) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__tail(X)) -> tail#(X) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__snd(X)) -> snd#(X) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__fst(X)) -> fst#(X) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__nil()) -> nil#() splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__isLNat(X)) -> isLNat#(X) splitAt#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__natsFrom(X)) -> natsFrom#(X) activate#(n__and(X1,X2)) -> and#(X1,X2) -> and#(tt(),X) -> activate#(X) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) -> splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) -> splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) -> splitAt#(s(N),cons(X,XS)) -> isNatural#(N) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) -> splitAt#(s(N),cons(X,XS)) -> isNatural#(X) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) -> splitAt#(s(N),cons(X,XS)) -> activate#(XS) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) -> splitAt#(0(),XS) -> U71#(isLNat(XS),XS) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) -> splitAt#(0(),XS) -> isLNat#(XS) activate#(n__sel(X1,X2)) -> sel#(X1,X2) -> sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS) activate#(n__sel(X1,X2)) -> sel#(X1,X2) -> sel#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) activate#(n__sel(X1,X2)) -> sel#(X1,X2) -> sel#(N,XS) -> isNatural#(N) activate#(n__head(X)) -> head#(X) -> head#(cons(N,XS)) -> U31#(and(isNatural(N),n__isLNat(activate(XS))),N) activate#(n__head(X)) -> head#(X) -> head#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) activate#(n__head(X)) -> head#(X) -> head#(cons(N,XS)) -> isNatural#(N) activate#(n__head(X)) -> head#(X) -> head#(cons(N,XS)) -> activate#(XS) activate#(n__take(X1,X2)) -> take#(X1,X2) -> take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS) activate#(n__take(X1,X2)) -> take#(X1,X2) -> take#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) activate#(n__take(X1,X2)) -> take#(X1,X2) -> take#(N,XS) -> isNatural#(N) activate#(n__tail(X)) -> tail#(X) -> tail#(cons(N,XS)) -> U91#(and(isNatural(N),n__isLNat(activate(XS))),activate(XS)) activate#(n__tail(X)) -> tail#(X) -> tail#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) activate#(n__tail(X)) -> tail#(X) -> tail#(cons(N,XS)) -> isNatural#(N) activate#(n__tail(X)) -> tail#(X) -> tail#(cons(N,XS)) -> activate#(XS) activate#(n__snd(X)) -> snd#(X) -> snd#(pair(X,Y)) -> U61#(and(isLNat(X),n__isLNat(Y)),Y) activate#(n__snd(X)) -> snd#(X) -> snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) activate#(n__snd(X)) -> snd#(X) -> snd#(pair(X,Y)) -> isLNat#(X) activate#(n__fst(X)) -> fst#(X) -> fst#(pair(X,Y)) -> U21#(and(isLNat(X),n__isLNat(Y)),X) activate#(n__fst(X)) -> fst#(X) -> fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) activate#(n__fst(X)) -> fst#(X) -> fst#(pair(X,Y)) -> isLNat#(X) activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) -> afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS) activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) -> afterNth#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) -> afterNth#(N,XS) -> isNatural#(N) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> activate#(V1) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__take(V1,V2)) -> activate#(V2) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__tail(V1)) -> activate#(V1) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__snd(V1)) -> activate#(V1) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__natsFrom(V1)) -> activate#(V1) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__fst(V1)) -> activate#(V1) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> activate#(V1) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__cons(V1,V2)) -> activate#(V2) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V1) activate#(n__isLNat(X)) -> isLNat#(X) -> isLNat#(n__afterNth(V1,V2)) -> activate#(V2) activate#(n__natsFrom(X)) -> natsFrom#(X) -> natsFrom#(N) -> U41#(isNatural(N),N) activate#(n__natsFrom(X)) -> natsFrom#(X) -> natsFrom#(N) -> isNatural#(N) U101#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS))) -> fst#(pair(X,Y)) -> U21#(and(isLNat(X),n__isLNat(Y)),X) U101#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS))) -> fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) U101#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS))) -> fst#(pair(X,Y)) -> isLNat#(X) U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))) U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> isNatural#(N) U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> isNatural#(X) U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(s(N),cons(X,XS)) -> activate#(XS) U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(0(),XS) -> U71#(isLNat(XS),XS) U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) -> splitAt#(0(),XS) -> isLNat#(XS) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__s(X)) -> s#(X) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__head(X)) -> head#(X) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__0()) -> 0#() U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__tail(X)) -> tail#(X) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__snd(X)) -> snd#(X) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__fst(X)) -> fst#(X) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__nil()) -> nil#() U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__isLNat(X)) -> isLNat#(X) U101#(tt(),N,XS) -> activate#(XS) -> activate#(n__natsFrom(X)) -> natsFrom#(X) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__and(X1,X2)) -> and#(X1,X2) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__pair(X1,X2)) -> pair#(X1,X2) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__head(X)) -> head#(X) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__0()) -> 0#() U101#(tt(),N,XS) -> activate#(N) -> activate#(n__take(X1,X2)) -> take#(X1,X2) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__tail(X)) -> tail#(X) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__snd(X)) -> snd#(X) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__fst(X)) -> fst#(X) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__nil()) -> nil#() U101#(tt(),N,XS) -> activate#(N) -> activate#(n__isLNat(X)) -> isLNat#(X) U101#(tt(),N,XS) -> activate#(N) -> activate#(n__natsFrom(X)) -> natsFrom#(X) SCC Processor: #sccs: 1 #rules: 104 #arcs: 995/13225 DPs: take#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) and#(tt(),X) -> activate#(X) activate#(n__natsFrom(X)) -> natsFrom#(X) natsFrom#(N) -> isNatural#(N) isNatural#(n__head(V1)) -> activate#(V1) activate#(n__isLNat(X)) -> isLNat#(X) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) afterNth#(N,XS) -> isNatural#(N) isNatural#(n__head(V1)) -> isLNat#(activate(V1)) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) activate#(n__fst(X)) -> fst#(X) fst#(pair(X,Y)) -> isLNat#(X) isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1)) isNatural#(n__s(V1)) -> activate#(V1) activate#(n__snd(X)) -> snd#(X) snd#(pair(X,Y)) -> isLNat#(X) isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__cons(V1,V2)) -> activate#(V2) activate#(n__tail(X)) -> tail#(X) tail#(cons(N,XS)) -> activate#(XS) activate#(n__take(X1,X2)) -> take#(X1,X2) take#(N,XS) -> isNatural#(N) isNatural#(n__s(V1)) -> isNatural#(activate(V1)) isNatural#(n__sel(V1,V2)) -> activate#(V2) activate#(n__head(X)) -> head#(X) head#(cons(N,XS)) -> activate#(XS) activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(N,XS) -> isNatural#(N) isNatural#(n__sel(V1,V2)) -> activate#(V1) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) splitAt#(0(),XS) -> isLNat#(XS) isLNat#(n__cons(V1,V2)) -> activate#(V1) activate#(n__and(X1,X2)) -> and#(X1,X2) isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1)) isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1)) isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__fst(V1)) -> activate#(V1) isLNat#(n__fst(V1)) -> isPLNat#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> activate#(V2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1)) isLNat#(n__natsFrom(V1)) -> activate#(V1) isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1)) isLNat#(n__snd(V1)) -> activate#(V1) isLNat#(n__snd(V1)) -> isPLNat#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> and#(isLNat(activate(V1)),n__isLNat(activate(V2))) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1)) isPLNat#(n__splitAt(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat#(n__tail(V1)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNat#(activate(V1)) isLNat#(n__take(V1,V2)) -> activate#(V2) isLNat#(n__take(V1,V2)) -> activate#(V1) isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1)) isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2))) splitAt#(0(),XS) -> U71#(isLNat(XS),XS) U71#(tt(),XS) -> activate#(XS) splitAt#(s(N),cons(X,XS)) -> activate#(XS) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))) splitAt#(s(N),cons(X,XS)) -> U81#(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) U81#(tt(),N,X,XS) -> activate#(X) U81#(tt(),N,X,XS) -> activate#(XS) U81#(tt(),N,X,XS) -> activate#(N) U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) U81#(tt(),N,X,XS) -> U82#(splitAt(activate(N),activate(XS)),activate(X)) U82#(pair(YS,ZS),X) -> activate#(X) sel#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS) U51#(tt(),N,XS) -> activate#(XS) U51#(tt(),N,XS) -> activate#(N) U51#(tt(),N,XS) -> afterNth#(activate(N),activate(XS)) afterNth#(N,XS) -> and#(isNatural(N),n__isLNat(XS)) afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS) U11#(tt(),N,XS) -> activate#(XS) U11#(tt(),N,XS) -> activate#(N) U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS))) snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) snd#(pair(X,Y)) -> U61#(and(isLNat(X),n__isLNat(Y)),Y) U61#(tt(),Y) -> activate#(Y) U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) head#(cons(N,XS)) -> isNatural#(N) head#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) head#(cons(N,XS)) -> U31#(and(isNatural(N),n__isLNat(activate(XS))),N) U31#(tt(),N) -> activate#(N) take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS) U101#(tt(),N,XS) -> activate#(XS) U101#(tt(),N,XS) -> activate#(N) U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) U101#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS))) fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y)) fst#(pair(X,Y)) -> U21#(and(isLNat(X),n__isLNat(Y)),X) U21#(tt(),X) -> activate#(X) tail#(cons(N,XS)) -> isNatural#(N) tail#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS))) tail#(cons(N,XS)) -> U91#(and(isNatural(N),n__isLNat(activate(XS))),activate(XS)) U91#(tt(),XS) -> activate#(XS) natsFrom#(N) -> U41#(isNatural(N),N) U41#(tt(),N) -> activate#(N) TRS: U101(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS))) U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS))) U21(tt(),X) -> activate(X) U31(tt(),N) -> activate(N) U41(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N)))) U51(tt(),N,XS) -> head(afterNth(activate(N),activate(XS))) U61(tt(),Y) -> activate(Y) U71(tt(),XS) -> pair(nil(),activate(XS)) U81(tt(),N,X,XS) -> U82(splitAt(activate(N),activate(XS)),activate(X)) U82(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) U91(tt(),XS) -> activate(XS) afterNth(N,XS) -> U11(and(isNatural(N),n__isLNat(XS)),N,XS) and(tt(),X) -> activate(X) fst(pair(X,Y)) -> U21(and(isLNat(X),n__isLNat(Y)),X) head(cons(N,XS)) -> U31(and(isNatural(N),n__isLNat(activate(XS))),N) isLNat(n__nil()) -> tt() isLNat(n__afterNth(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat(n__cons(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isLNat(n__fst(V1)) -> isPLNat(activate(V1)) isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)) isLNat(n__snd(V1)) -> isPLNat(activate(V1)) isLNat(n__tail(V1)) -> isLNat(activate(V1)) isLNat(n__take(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isNatural(n__0()) -> tt() isNatural(n__head(V1)) -> isLNat(activate(V1)) isNatural(n__s(V1)) -> isNatural(activate(V1)) isNatural(n__sel(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) isPLNat(n__pair(V1,V2)) -> and(isLNat(activate(V1)),n__isLNat(activate(V2))) isPLNat(n__splitAt(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) natsFrom(N) -> U41(isNatural(N),N) sel(N,XS) -> U51(and(isNatural(N),n__isLNat(XS)),N,XS) snd(pair(X,Y)) -> U61(and(isLNat(X),n__isLNat(Y)),Y) splitAt(0(),XS) -> U71(isLNat(XS),XS) splitAt(s(N),cons(X,XS)) -> U81(and(isNatural(N),n__and(isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS)) tail(cons(N,XS)) -> U91(and(isNatural(N),n__isLNat(activate(XS))),activate(XS)) take(N,XS) -> U101(and(isNatural(N),n__isLNat(XS)),N,XS) natsFrom(X) -> n__natsFrom(X) isLNat(X) -> n__isLNat(X) nil() -> n__nil() afterNth(X1,X2) -> n__afterNth(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fst(X) -> n__fst(X) snd(X) -> n__snd(X) tail(X) -> n__tail(X) take(X1,X2) -> n__take(X1,X2) 0() -> n__0() head(X) -> n__head(X) s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) pair(X1,X2) -> n__pair(X1,X2) splitAt(X1,X2) -> n__splitAt(X1,X2) and(X1,X2) -> n__and(X1,X2) activate(n__natsFrom(X)) -> natsFrom(X) activate(n__isLNat(X)) -> isLNat(X) activate(n__nil()) -> nil() activate(n__afterNth(X1,X2)) -> afterNth(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__fst(X)) -> fst(X) activate(n__snd(X)) -> snd(X) activate(n__tail(X)) -> tail(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__0()) -> 0() activate(n__head(X)) -> head(X) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__pair(X1,X2)) -> pair(X1,X2) activate(n__splitAt(X1,X2)) -> splitAt(X1,X2) activate(n__and(X1,X2)) -> and(X1,X2) activate(X) -> X Open