MAYBE Problem: U101(tt(),V1,V2) -> U102(isNatural(activate(V1)),activate(V2)) U102(tt(),V2) -> U103(isLNat(activate(V2))) U103(tt()) -> tt() U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS))) U111(tt(),V1) -> U112(isLNat(activate(V1))) U112(tt()) -> tt() U121(tt(),V1) -> U122(isNatural(activate(V1))) U122(tt()) -> tt() U131(tt(),V1,V2) -> U132(isNatural(activate(V1)),activate(V2)) U132(tt(),V2) -> U133(isLNat(activate(V2))) U133(tt()) -> tt() U141(tt(),V1,V2) -> U142(isLNat(activate(V1)),activate(V2)) U142(tt(),V2) -> U143(isLNat(activate(V2))) U143(tt()) -> tt() U151(tt(),V1,V2) -> U152(isNatural(activate(V1)),activate(V2)) U152(tt(),V2) -> U153(isLNat(activate(V2))) U153(tt()) -> tt() U161(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N)))) U171(tt(),N,XS) -> head(afterNth(activate(N),activate(XS))) U181(tt(),Y) -> activate(Y) U191(tt(),XS) -> pair(nil(),activate(XS)) U201(tt(),N,X,XS) -> U202(splitAt(activate(N),activate(XS)),activate(X)) U202(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) U21(tt(),X) -> activate(X) U211(tt(),XS) -> activate(XS) U221(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS))) U31(tt(),N) -> activate(N) U41(tt(),V1,V2) -> U42(isNatural(activate(V1)),activate(V2)) U42(tt(),V2) -> U43(isLNat(activate(V2))) U43(tt()) -> tt() U51(tt(),V1,V2) -> U52(isNatural(activate(V1)),activate(V2)) U52(tt(),V2) -> U53(isLNat(activate(V2))) U53(tt()) -> tt() U61(tt(),V1) -> U62(isPLNat(activate(V1))) U62(tt()) -> tt() U71(tt(),V1) -> U72(isNatural(activate(V1))) U72(tt()) -> tt() U81(tt(),V1) -> U82(isPLNat(activate(V1))) U82(tt()) -> tt() U91(tt(),V1) -> U92(isLNat(activate(V1))) U92(tt()) -> tt() afterNth(N,XS) -> U11(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) and(tt(),X) -> activate(X) fst(pair(X,Y)) -> U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X) head(cons(N,XS)) -> U31(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) isLNat(n__nil()) -> tt() isLNat(n__afterNth(V1,V2)) -> U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat(n__cons(V1,V2)) -> U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1)) isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1)) isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1)) isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1)) isLNat(n__take(V1,V2)) -> U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNatKind(n__nil()) -> tt() isLNatKind(n__afterNth(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind(n__cons(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) isLNatKind(n__take(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isNatural(n__0()) -> tt() isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)),activate(V1)) isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)),activate(V1)) isNatural(n__sel(V1,V2)) -> U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isNaturalKind(n__0()) -> tt() isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) isNaturalKind(n__sel(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat(n__pair(V1,V2)) -> U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNat(n__splitAt(V1,V2)) -> U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNatKind(n__pair(V1,V2)) -> and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNatKind(n__splitAt(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) natsFrom(N) -> U161(and(isNatural(N),n__isNaturalKind(N)),N) sel(N,XS) -> U171(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) snd(pair(X,Y)) -> U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y) splitAt(0(),XS) -> U191(and(isLNat(XS),n__isLNatKind(XS)),XS) splitAt(s(N),cons(X,XS)) -> U201(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS))))), N,X,activate(XS)) tail(cons(N,XS)) -> U211(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) take(N,XS) -> U221(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) natsFrom(X) -> n__natsFrom(X) isNaturalKind(X) -> n__isNaturalKind(X) and(X1,X2) -> n__and(X1,X2) isLNatKind(X) -> n__isLNatKind(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) activate(n__natsFrom(X)) -> natsFrom(X) activate(n__isNaturalKind(X)) -> isNaturalKind(X) activate(n__and(X1,X2)) -> and(X1,X2) activate(n__isLNatKind(X)) -> isLNatKind(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(X) -> X Proof: DP Processor: DPs: U101#(tt(),V1,V2) -> activate#(V2) U101#(tt(),V1,V2) -> activate#(V1) U101#(tt(),V1,V2) -> isNatural#(activate(V1)) U101#(tt(),V1,V2) -> U102#(isNatural(activate(V1)),activate(V2)) U102#(tt(),V2) -> activate#(V2) U102#(tt(),V2) -> isLNat#(activate(V2)) U102#(tt(),V2) -> U103#(isLNat(activate(V2))) 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))) U111#(tt(),V1) -> activate#(V1) U111#(tt(),V1) -> isLNat#(activate(V1)) U111#(tt(),V1) -> U112#(isLNat(activate(V1))) U121#(tt(),V1) -> activate#(V1) U121#(tt(),V1) -> isNatural#(activate(V1)) U121#(tt(),V1) -> U122#(isNatural(activate(V1))) U131#(tt(),V1,V2) -> activate#(V2) U131#(tt(),V1,V2) -> activate#(V1) U131#(tt(),V1,V2) -> isNatural#(activate(V1)) U131#(tt(),V1,V2) -> U132#(isNatural(activate(V1)),activate(V2)) U132#(tt(),V2) -> activate#(V2) U132#(tt(),V2) -> isLNat#(activate(V2)) U132#(tt(),V2) -> U133#(isLNat(activate(V2))) U141#(tt(),V1,V2) -> activate#(V2) U141#(tt(),V1,V2) -> activate#(V1) U141#(tt(),V1,V2) -> isLNat#(activate(V1)) U141#(tt(),V1,V2) -> U142#(isLNat(activate(V1)),activate(V2)) U142#(tt(),V2) -> activate#(V2) U142#(tt(),V2) -> isLNat#(activate(V2)) U142#(tt(),V2) -> U143#(isLNat(activate(V2))) U151#(tt(),V1,V2) -> activate#(V2) U151#(tt(),V1,V2) -> activate#(V1) U151#(tt(),V1,V2) -> isNatural#(activate(V1)) U151#(tt(),V1,V2) -> U152#(isNatural(activate(V1)),activate(V2)) U152#(tt(),V2) -> activate#(V2) U152#(tt(),V2) -> isLNat#(activate(V2)) U152#(tt(),V2) -> U153#(isLNat(activate(V2))) U161#(tt(),N) -> s#(activate(N)) U161#(tt(),N) -> activate#(N) U161#(tt(),N) -> cons#(activate(N),n__natsFrom(s(activate(N)))) U171#(tt(),N,XS) -> activate#(XS) U171#(tt(),N,XS) -> activate#(N) U171#(tt(),N,XS) -> afterNth#(activate(N),activate(XS)) U171#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) U181#(tt(),Y) -> activate#(Y) U191#(tt(),XS) -> activate#(XS) U191#(tt(),XS) -> nil#() U191#(tt(),XS) -> pair#(nil(),activate(XS)) U201#(tt(),N,X,XS) -> activate#(X) U201#(tt(),N,X,XS) -> activate#(XS) U201#(tt(),N,X,XS) -> activate#(N) U201#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) U201#(tt(),N,X,XS) -> U202#(splitAt(activate(N),activate(XS)),activate(X)) U202#(pair(YS,ZS),X) -> activate#(X) U202#(pair(YS,ZS),X) -> cons#(activate(X),YS) U202#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS) U21#(tt(),X) -> activate#(X) U211#(tt(),XS) -> activate#(XS) U221#(tt(),N,XS) -> activate#(XS) U221#(tt(),N,XS) -> activate#(N) U221#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) U221#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS))) U31#(tt(),N) -> activate#(N) U41#(tt(),V1,V2) -> activate#(V2) U41#(tt(),V1,V2) -> activate#(V1) U41#(tt(),V1,V2) -> isNatural#(activate(V1)) U41#(tt(),V1,V2) -> U42#(isNatural(activate(V1)),activate(V2)) U42#(tt(),V2) -> activate#(V2) U42#(tt(),V2) -> isLNat#(activate(V2)) U42#(tt(),V2) -> U43#(isLNat(activate(V2))) U51#(tt(),V1,V2) -> activate#(V2) U51#(tt(),V1,V2) -> activate#(V1) U51#(tt(),V1,V2) -> isNatural#(activate(V1)) U51#(tt(),V1,V2) -> U52#(isNatural(activate(V1)),activate(V2)) U52#(tt(),V2) -> activate#(V2) U52#(tt(),V2) -> isLNat#(activate(V2)) U52#(tt(),V2) -> U53#(isLNat(activate(V2))) U61#(tt(),V1) -> activate#(V1) U61#(tt(),V1) -> isPLNat#(activate(V1)) U61#(tt(),V1) -> U62#(isPLNat(activate(V1))) U71#(tt(),V1) -> activate#(V1) U71#(tt(),V1) -> isNatural#(activate(V1)) U71#(tt(),V1) -> U72#(isNatural(activate(V1))) U81#(tt(),V1) -> activate#(V1) U81#(tt(),V1) -> isPLNat#(activate(V1)) U81#(tt(),V1) -> U82#(isPLNat(activate(V1))) U91#(tt(),V1) -> activate#(V1) U91#(tt(),V1) -> isLNat#(activate(V1)) U91#(tt(),V1) -> U92#(isLNat(activate(V1))) afterNth#(N,XS) -> isLNat#(XS) afterNth#(N,XS) -> isNatural#(N) afterNth#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N)) afterNth#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))) afterNth#(N,XS) -> U11#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) and#(tt(),X) -> activate#(X) fst#(pair(X,Y)) -> isLNat#(Y) fst#(pair(X,Y)) -> isLNat#(X) fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X)) fst#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))) fst#(pair(X,Y)) -> U21#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X) head#(cons(N,XS)) -> activate#(XS) head#(cons(N,XS)) -> isLNat#(activate(XS)) head#(cons(N,XS)) -> isNatural#(N) head#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N)) head#(cons(N,XS)) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) head#(cons(N,XS)) -> U31#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), N) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) isLNat#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1)) isLNat#(n__afterNth(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNat#(n__afterNth(V1,V2)) -> U41#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat#(n__cons(V1,V2)) -> activate#(V2) isLNat#(n__cons(V1,V2)) -> activate#(V1) isLNat#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1)) isLNat#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNat#(n__cons(V1,V2)) -> U51#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat#(n__fst(V1)) -> activate#(V1) isLNat#(n__fst(V1)) -> isPLNatKind#(activate(V1)) isLNat#(n__fst(V1)) -> U61#(isPLNatKind(activate(V1)),activate(V1)) isLNat#(n__natsFrom(V1)) -> activate#(V1) isLNat#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1)) isLNat#(n__natsFrom(V1)) -> U71#(isNaturalKind(activate(V1)),activate(V1)) isLNat#(n__snd(V1)) -> activate#(V1) isLNat#(n__snd(V1)) -> isPLNatKind#(activate(V1)) isLNat#(n__snd(V1)) -> U81#(isPLNatKind(activate(V1)),activate(V1)) isLNat#(n__tail(V1)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNatKind#(activate(V1)) isLNat#(n__tail(V1)) -> U91#(isLNatKind(activate(V1)),activate(V1)) isLNat#(n__take(V1,V2)) -> activate#(V2) isLNat#(n__take(V1,V2)) -> activate#(V1) isLNat#(n__take(V1,V2)) -> isNaturalKind#(activate(V1)) isLNat#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNat#(n__take(V1,V2)) -> U101#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNatKind#(n__afterNth(V1,V2)) -> activate#(V2) isLNatKind#(n__afterNth(V1,V2)) -> activate#(V1) isLNatKind#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__afterNth(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind#(n__cons(V1,V2)) -> activate#(V2) isLNatKind#(n__cons(V1,V2)) -> activate#(V1) isLNatKind#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind#(n__fst(V1)) -> activate#(V1) isLNatKind#(n__fst(V1)) -> isPLNatKind#(activate(V1)) isLNatKind#(n__natsFrom(V1)) -> activate#(V1) isLNatKind#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__snd(V1)) -> activate#(V1) isLNatKind#(n__snd(V1)) -> isPLNatKind#(activate(V1)) isLNatKind#(n__tail(V1)) -> activate#(V1) isLNatKind#(n__tail(V1)) -> isLNatKind#(activate(V1)) isLNatKind#(n__take(V1,V2)) -> activate#(V2) isLNatKind#(n__take(V1,V2)) -> activate#(V1) isLNatKind#(n__take(V1,V2)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isNatural#(n__head(V1)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNatKind#(activate(V1)) isNatural#(n__head(V1)) -> U111#(isLNatKind(activate(V1)),activate(V1)) isNatural#(n__s(V1)) -> activate#(V1) isNatural#(n__s(V1)) -> isNaturalKind#(activate(V1)) isNatural#(n__s(V1)) -> U121#(isNaturalKind(activate(V1)),activate(V1)) isNatural#(n__sel(V1,V2)) -> activate#(V2) isNatural#(n__sel(V1,V2)) -> activate#(V1) isNatural#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1)) isNatural#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isNatural#(n__sel(V1,V2)) -> U131#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isNaturalKind#(n__head(V1)) -> activate#(V1) isNaturalKind#(n__head(V1)) -> isLNatKind#(activate(V1)) isNaturalKind#(n__s(V1)) -> activate#(V1) isNaturalKind#(n__s(V1)) -> isNaturalKind#(activate(V1)) isNaturalKind#(n__sel(V1,V2)) -> activate#(V2) isNaturalKind#(n__sel(V1,V2)) -> activate#(V1) isNaturalKind#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1)) isNaturalKind#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat#(n__pair(V1,V2)) -> activate#(V2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNatKind#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat#(n__pair(V1,V2)) -> U141#(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) isPLNat#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1)) isPLNat#(n__splitAt(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat#(n__splitAt(V1,V2)) -> U151#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNatKind#(n__pair(V1,V2)) -> activate#(V2) isPLNatKind#(n__pair(V1,V2)) -> activate#(V1) isPLNatKind#(n__pair(V1,V2)) -> isLNatKind#(activate(V1)) isPLNatKind#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V2) isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V1) isPLNatKind#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1)) isPLNatKind#(n__splitAt(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) natsFrom#(N) -> isNatural#(N) natsFrom#(N) -> and#(isNatural(N),n__isNaturalKind(N)) natsFrom#(N) -> U161#(and(isNatural(N),n__isNaturalKind(N)),N) sel#(N,XS) -> isLNat#(XS) sel#(N,XS) -> isNatural#(N) sel#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N)) sel#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))) sel#(N,XS) -> U171#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) snd#(pair(X,Y)) -> isLNat#(Y) snd#(pair(X,Y)) -> isLNat#(X) snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X)) snd#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))) snd#(pair(X,Y)) -> U181#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y) splitAt#(0(),XS) -> isLNat#(XS) splitAt#(0(),XS) -> and#(isLNat(XS),n__isLNatKind(XS)) splitAt#(0(),XS) -> U191#(and(isLNat(XS),n__isLNatKind(XS)),XS) splitAt#(s(N),cons(X,XS)) -> activate#(XS) splitAt#(s(N),cons(X,XS)) -> isLNat#(activate(XS)) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) splitAt#(s(N),cons(X,XS)) -> and#(isNatural(X),n__isNaturalKind(X)) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__isNaturalKind(N)) splitAt#(s(N),cons(X,XS)) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS))))) splitAt#(s(N),cons(X,XS)) -> U201#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS))))), N,X,activate(XS)) tail#(cons(N,XS)) -> activate#(XS) tail#(cons(N,XS)) -> isLNat#(activate(XS)) tail#(cons(N,XS)) -> isNatural#(N) tail#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N)) tail#(cons(N,XS)) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) tail#(cons(N,XS)) -> U211#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), activate(XS)) take#(N,XS) -> isLNat#(XS) take#(N,XS) -> isNatural#(N) take#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N)) take#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))) take#(N,XS) -> U221#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) activate#(n__natsFrom(X)) -> natsFrom#(X) activate#(n__isNaturalKind(X)) -> isNaturalKind#(X) activate#(n__and(X1,X2)) -> and#(X1,X2) activate#(n__isLNatKind(X)) -> isLNatKind#(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) TRS: U101(tt(),V1,V2) -> U102(isNatural(activate(V1)),activate(V2)) U102(tt(),V2) -> U103(isLNat(activate(V2))) U103(tt()) -> tt() U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS))) U111(tt(),V1) -> U112(isLNat(activate(V1))) U112(tt()) -> tt() U121(tt(),V1) -> U122(isNatural(activate(V1))) U122(tt()) -> tt() U131(tt(),V1,V2) -> U132(isNatural(activate(V1)),activate(V2)) U132(tt(),V2) -> U133(isLNat(activate(V2))) U133(tt()) -> tt() U141(tt(),V1,V2) -> U142(isLNat(activate(V1)),activate(V2)) U142(tt(),V2) -> U143(isLNat(activate(V2))) U143(tt()) -> tt() U151(tt(),V1,V2) -> U152(isNatural(activate(V1)),activate(V2)) U152(tt(),V2) -> U153(isLNat(activate(V2))) U153(tt()) -> tt() U161(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N)))) U171(tt(),N,XS) -> head(afterNth(activate(N),activate(XS))) U181(tt(),Y) -> activate(Y) U191(tt(),XS) -> pair(nil(),activate(XS)) U201(tt(),N,X,XS) -> U202(splitAt(activate(N),activate(XS)),activate(X)) U202(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) U21(tt(),X) -> activate(X) U211(tt(),XS) -> activate(XS) U221(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS))) U31(tt(),N) -> activate(N) U41(tt(),V1,V2) -> U42(isNatural(activate(V1)),activate(V2)) U42(tt(),V2) -> U43(isLNat(activate(V2))) U43(tt()) -> tt() U51(tt(),V1,V2) -> U52(isNatural(activate(V1)),activate(V2)) U52(tt(),V2) -> U53(isLNat(activate(V2))) U53(tt()) -> tt() U61(tt(),V1) -> U62(isPLNat(activate(V1))) U62(tt()) -> tt() U71(tt(),V1) -> U72(isNatural(activate(V1))) U72(tt()) -> tt() U81(tt(),V1) -> U82(isPLNat(activate(V1))) U82(tt()) -> tt() U91(tt(),V1) -> U92(isLNat(activate(V1))) U92(tt()) -> tt() afterNth(N,XS) -> U11(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) and(tt(),X) -> activate(X) fst(pair(X,Y)) -> U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X) head(cons(N,XS)) -> U31(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), N) isLNat(n__nil()) -> tt() isLNat(n__afterNth(V1,V2)) -> U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat(n__cons(V1,V2)) -> U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1)) isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1)) isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1)) isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1)) isLNat(n__take(V1,V2)) -> U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNatKind(n__nil()) -> tt() isLNatKind(n__afterNth(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind(n__cons(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) isLNatKind(n__take(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isNatural(n__0()) -> tt() isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)),activate(V1)) isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)),activate(V1)) isNatural(n__sel(V1,V2)) -> U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isNaturalKind(n__0()) -> tt() isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) isNaturalKind(n__sel(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat(n__pair(V1,V2)) -> U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNat(n__splitAt(V1,V2)) -> U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNatKind(n__pair(V1,V2)) -> and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNatKind(n__splitAt(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) natsFrom(N) -> U161(and(isNatural(N),n__isNaturalKind(N)),N) sel(N,XS) -> U171(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) snd(pair(X,Y)) -> U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y) splitAt(0(),XS) -> U191(and(isLNat(XS),n__isLNatKind(XS)),XS) splitAt(s(N),cons(X,XS)) -> U201(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS))))), N,X,activate(XS)) tail(cons(N,XS)) -> U211(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), activate(XS)) take(N,XS) -> U221(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) natsFrom(X) -> n__natsFrom(X) isNaturalKind(X) -> n__isNaturalKind(X) and(X1,X2) -> n__and(X1,X2) isLNatKind(X) -> n__isLNatKind(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) activate(n__natsFrom(X)) -> natsFrom(X) activate(n__isNaturalKind(X)) -> isNaturalKind(X) activate(n__and(X1,X2)) -> and(X1,X2) activate(n__isLNatKind(X)) -> isLNatKind(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(X) -> X TDG Processor: DPs: U101#(tt(),V1,V2) -> activate#(V2) U101#(tt(),V1,V2) -> activate#(V1) U101#(tt(),V1,V2) -> isNatural#(activate(V1)) U101#(tt(),V1,V2) -> U102#(isNatural(activate(V1)),activate(V2)) U102#(tt(),V2) -> activate#(V2) U102#(tt(),V2) -> isLNat#(activate(V2)) U102#(tt(),V2) -> U103#(isLNat(activate(V2))) 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))) U111#(tt(),V1) -> activate#(V1) U111#(tt(),V1) -> isLNat#(activate(V1)) U111#(tt(),V1) -> U112#(isLNat(activate(V1))) U121#(tt(),V1) -> activate#(V1) U121#(tt(),V1) -> isNatural#(activate(V1)) U121#(tt(),V1) -> U122#(isNatural(activate(V1))) U131#(tt(),V1,V2) -> activate#(V2) U131#(tt(),V1,V2) -> activate#(V1) U131#(tt(),V1,V2) -> isNatural#(activate(V1)) U131#(tt(),V1,V2) -> U132#(isNatural(activate(V1)),activate(V2)) U132#(tt(),V2) -> activate#(V2) U132#(tt(),V2) -> isLNat#(activate(V2)) U132#(tt(),V2) -> U133#(isLNat(activate(V2))) U141#(tt(),V1,V2) -> activate#(V2) U141#(tt(),V1,V2) -> activate#(V1) U141#(tt(),V1,V2) -> isLNat#(activate(V1)) U141#(tt(),V1,V2) -> U142#(isLNat(activate(V1)),activate(V2)) U142#(tt(),V2) -> activate#(V2) U142#(tt(),V2) -> isLNat#(activate(V2)) U142#(tt(),V2) -> U143#(isLNat(activate(V2))) U151#(tt(),V1,V2) -> activate#(V2) U151#(tt(),V1,V2) -> activate#(V1) U151#(tt(),V1,V2) -> isNatural#(activate(V1)) U151#(tt(),V1,V2) -> U152#(isNatural(activate(V1)),activate(V2)) U152#(tt(),V2) -> activate#(V2) U152#(tt(),V2) -> isLNat#(activate(V2)) U152#(tt(),V2) -> U153#(isLNat(activate(V2))) U161#(tt(),N) -> s#(activate(N)) U161#(tt(),N) -> activate#(N) U161#(tt(),N) -> cons#(activate(N),n__natsFrom(s(activate(N)))) U171#(tt(),N,XS) -> activate#(XS) U171#(tt(),N,XS) -> activate#(N) U171#(tt(),N,XS) -> afterNth#(activate(N),activate(XS)) U171#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) U181#(tt(),Y) -> activate#(Y) U191#(tt(),XS) -> activate#(XS) U191#(tt(),XS) -> nil#() U191#(tt(),XS) -> pair#(nil(),activate(XS)) U201#(tt(),N,X,XS) -> activate#(X) U201#(tt(),N,X,XS) -> activate#(XS) U201#(tt(),N,X,XS) -> activate#(N) U201#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) U201#(tt(),N,X,XS) -> U202#(splitAt(activate(N),activate(XS)),activate(X)) U202#(pair(YS,ZS),X) -> activate#(X) U202#(pair(YS,ZS),X) -> cons#(activate(X),YS) U202#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS) U21#(tt(),X) -> activate#(X) U211#(tt(),XS) -> activate#(XS) U221#(tt(),N,XS) -> activate#(XS) U221#(tt(),N,XS) -> activate#(N) U221#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) U221#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS))) U31#(tt(),N) -> activate#(N) U41#(tt(),V1,V2) -> activate#(V2) U41#(tt(),V1,V2) -> activate#(V1) U41#(tt(),V1,V2) -> isNatural#(activate(V1)) U41#(tt(),V1,V2) -> U42#(isNatural(activate(V1)),activate(V2)) U42#(tt(),V2) -> activate#(V2) U42#(tt(),V2) -> isLNat#(activate(V2)) U42#(tt(),V2) -> U43#(isLNat(activate(V2))) U51#(tt(),V1,V2) -> activate#(V2) U51#(tt(),V1,V2) -> activate#(V1) U51#(tt(),V1,V2) -> isNatural#(activate(V1)) U51#(tt(),V1,V2) -> U52#(isNatural(activate(V1)),activate(V2)) U52#(tt(),V2) -> activate#(V2) U52#(tt(),V2) -> isLNat#(activate(V2)) U52#(tt(),V2) -> U53#(isLNat(activate(V2))) U61#(tt(),V1) -> activate#(V1) U61#(tt(),V1) -> isPLNat#(activate(V1)) U61#(tt(),V1) -> U62#(isPLNat(activate(V1))) U71#(tt(),V1) -> activate#(V1) U71#(tt(),V1) -> isNatural#(activate(V1)) U71#(tt(),V1) -> U72#(isNatural(activate(V1))) U81#(tt(),V1) -> activate#(V1) U81#(tt(),V1) -> isPLNat#(activate(V1)) U81#(tt(),V1) -> U82#(isPLNat(activate(V1))) U91#(tt(),V1) -> activate#(V1) U91#(tt(),V1) -> isLNat#(activate(V1)) U91#(tt(),V1) -> U92#(isLNat(activate(V1))) afterNth#(N,XS) -> isLNat#(XS) afterNth#(N,XS) -> isNatural#(N) afterNth#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N)) afterNth#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))) afterNth#(N,XS) -> U11#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) and#(tt(),X) -> activate#(X) fst#(pair(X,Y)) -> isLNat#(Y) fst#(pair(X,Y)) -> isLNat#(X) fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X)) fst#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))) fst#(pair(X,Y)) -> U21#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X) head#(cons(N,XS)) -> activate#(XS) head#(cons(N,XS)) -> isLNat#(activate(XS)) head#(cons(N,XS)) -> isNatural#(N) head#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N)) head#(cons(N,XS)) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) head#(cons(N,XS)) -> U31#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), N) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) isLNat#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1)) isLNat#(n__afterNth(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNat#(n__afterNth(V1,V2)) -> U41#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat#(n__cons(V1,V2)) -> activate#(V2) isLNat#(n__cons(V1,V2)) -> activate#(V1) isLNat#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1)) isLNat#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNat#(n__cons(V1,V2)) -> U51#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat#(n__fst(V1)) -> activate#(V1) isLNat#(n__fst(V1)) -> isPLNatKind#(activate(V1)) isLNat#(n__fst(V1)) -> U61#(isPLNatKind(activate(V1)),activate(V1)) isLNat#(n__natsFrom(V1)) -> activate#(V1) isLNat#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1)) isLNat#(n__natsFrom(V1)) -> U71#(isNaturalKind(activate(V1)),activate(V1)) isLNat#(n__snd(V1)) -> activate#(V1) isLNat#(n__snd(V1)) -> isPLNatKind#(activate(V1)) isLNat#(n__snd(V1)) -> U81#(isPLNatKind(activate(V1)),activate(V1)) isLNat#(n__tail(V1)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNatKind#(activate(V1)) isLNat#(n__tail(V1)) -> U91#(isLNatKind(activate(V1)),activate(V1)) isLNat#(n__take(V1,V2)) -> activate#(V2) isLNat#(n__take(V1,V2)) -> activate#(V1) isLNat#(n__take(V1,V2)) -> isNaturalKind#(activate(V1)) isLNat#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNat#(n__take(V1,V2)) -> U101#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNatKind#(n__afterNth(V1,V2)) -> activate#(V2) isLNatKind#(n__afterNth(V1,V2)) -> activate#(V1) isLNatKind#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__afterNth(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind#(n__cons(V1,V2)) -> activate#(V2) isLNatKind#(n__cons(V1,V2)) -> activate#(V1) isLNatKind#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind#(n__fst(V1)) -> activate#(V1) isLNatKind#(n__fst(V1)) -> isPLNatKind#(activate(V1)) isLNatKind#(n__natsFrom(V1)) -> activate#(V1) isLNatKind#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__snd(V1)) -> activate#(V1) isLNatKind#(n__snd(V1)) -> isPLNatKind#(activate(V1)) isLNatKind#(n__tail(V1)) -> activate#(V1) isLNatKind#(n__tail(V1)) -> isLNatKind#(activate(V1)) isLNatKind#(n__take(V1,V2)) -> activate#(V2) isLNatKind#(n__take(V1,V2)) -> activate#(V1) isLNatKind#(n__take(V1,V2)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isNatural#(n__head(V1)) -> activate#(V1) isNatural#(n__head(V1)) -> isLNatKind#(activate(V1)) isNatural#(n__head(V1)) -> U111#(isLNatKind(activate(V1)),activate(V1)) isNatural#(n__s(V1)) -> activate#(V1) isNatural#(n__s(V1)) -> isNaturalKind#(activate(V1)) isNatural#(n__s(V1)) -> U121#(isNaturalKind(activate(V1)),activate(V1)) isNatural#(n__sel(V1,V2)) -> activate#(V2) isNatural#(n__sel(V1,V2)) -> activate#(V1) isNatural#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1)) isNatural#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isNatural#(n__sel(V1,V2)) -> U131#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isNaturalKind#(n__head(V1)) -> activate#(V1) isNaturalKind#(n__head(V1)) -> isLNatKind#(activate(V1)) isNaturalKind#(n__s(V1)) -> activate#(V1) isNaturalKind#(n__s(V1)) -> isNaturalKind#(activate(V1)) isNaturalKind#(n__sel(V1,V2)) -> activate#(V2) isNaturalKind#(n__sel(V1,V2)) -> activate#(V1) isNaturalKind#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1)) isNaturalKind#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat#(n__pair(V1,V2)) -> activate#(V2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNatKind#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat#(n__pair(V1,V2)) -> U141#(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) isPLNat#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1)) isPLNat#(n__splitAt(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat#(n__splitAt(V1,V2)) -> U151#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNatKind#(n__pair(V1,V2)) -> activate#(V2) isPLNatKind#(n__pair(V1,V2)) -> activate#(V1) isPLNatKind#(n__pair(V1,V2)) -> isLNatKind#(activate(V1)) isPLNatKind#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V2) isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V1) isPLNatKind#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1)) isPLNatKind#(n__splitAt(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) natsFrom#(N) -> isNatural#(N) natsFrom#(N) -> and#(isNatural(N),n__isNaturalKind(N)) natsFrom#(N) -> U161#(and(isNatural(N),n__isNaturalKind(N)),N) sel#(N,XS) -> isLNat#(XS) sel#(N,XS) -> isNatural#(N) sel#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N)) sel#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))) sel#(N,XS) -> U171#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) snd#(pair(X,Y)) -> isLNat#(Y) snd#(pair(X,Y)) -> isLNat#(X) snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X)) snd#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))) snd#(pair(X,Y)) -> U181#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y) splitAt#(0(),XS) -> isLNat#(XS) splitAt#(0(),XS) -> and#(isLNat(XS),n__isLNatKind(XS)) splitAt#(0(),XS) -> U191#(and(isLNat(XS),n__isLNatKind(XS)),XS) splitAt#(s(N),cons(X,XS)) -> activate#(XS) splitAt#(s(N),cons(X,XS)) -> isLNat#(activate(XS)) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) splitAt#(s(N),cons(X,XS)) -> and#(isNatural(X),n__isNaturalKind(X)) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__isNaturalKind(N)) splitAt#(s(N),cons(X,XS)) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS))))) splitAt#(s(N),cons(X,XS)) -> U201#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS))))), N,X,activate(XS)) tail#(cons(N,XS)) -> activate#(XS) tail#(cons(N,XS)) -> isLNat#(activate(XS)) tail#(cons(N,XS)) -> isNatural#(N) tail#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N)) tail#(cons(N,XS)) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) tail#(cons(N,XS)) -> U211#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), activate(XS)) take#(N,XS) -> isLNat#(XS) take#(N,XS) -> isNatural#(N) take#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N)) take#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))) take#(N,XS) -> U221#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) activate#(n__natsFrom(X)) -> natsFrom#(X) activate#(n__isNaturalKind(X)) -> isNaturalKind#(X) activate#(n__and(X1,X2)) -> and#(X1,X2) activate#(n__isLNatKind(X)) -> isLNatKind#(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) TRS: U101(tt(),V1,V2) -> U102(isNatural(activate(V1)),activate(V2)) U102(tt(),V2) -> U103(isLNat(activate(V2))) U103(tt()) -> tt() U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS))) U111(tt(),V1) -> U112(isLNat(activate(V1))) U112(tt()) -> tt() U121(tt(),V1) -> U122(isNatural(activate(V1))) U122(tt()) -> tt() U131(tt(),V1,V2) -> U132(isNatural(activate(V1)),activate(V2)) U132(tt(),V2) -> U133(isLNat(activate(V2))) U133(tt()) -> tt() U141(tt(),V1,V2) -> U142(isLNat(activate(V1)),activate(V2)) U142(tt(),V2) -> U143(isLNat(activate(V2))) U143(tt()) -> tt() U151(tt(),V1,V2) -> U152(isNatural(activate(V1)),activate(V2)) U152(tt(),V2) -> U153(isLNat(activate(V2))) U153(tt()) -> tt() U161(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N)))) U171(tt(),N,XS) -> head(afterNth(activate(N),activate(XS))) U181(tt(),Y) -> activate(Y) U191(tt(),XS) -> pair(nil(),activate(XS)) U201(tt(),N,X,XS) -> U202(splitAt(activate(N),activate(XS)),activate(X)) U202(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) U21(tt(),X) -> activate(X) U211(tt(),XS) -> activate(XS) U221(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS))) U31(tt(),N) -> activate(N) U41(tt(),V1,V2) -> U42(isNatural(activate(V1)),activate(V2)) U42(tt(),V2) -> U43(isLNat(activate(V2))) U43(tt()) -> tt() U51(tt(),V1,V2) -> U52(isNatural(activate(V1)),activate(V2)) U52(tt(),V2) -> U53(isLNat(activate(V2))) U53(tt()) -> tt() U61(tt(),V1) -> U62(isPLNat(activate(V1))) U62(tt()) -> tt() U71(tt(),V1) -> U72(isNatural(activate(V1))) U72(tt()) -> tt() U81(tt(),V1) -> U82(isPLNat(activate(V1))) U82(tt()) -> tt() U91(tt(),V1) -> U92(isLNat(activate(V1))) U92(tt()) -> tt() afterNth(N,XS) -> U11(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) and(tt(),X) -> activate(X) fst(pair(X,Y)) -> U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X) head(cons(N,XS)) -> U31(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), N) isLNat(n__nil()) -> tt() isLNat(n__afterNth(V1,V2)) -> U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat(n__cons(V1,V2)) -> U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1)) isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1)) isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1)) isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1)) isLNat(n__take(V1,V2)) -> U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNatKind(n__nil()) -> tt() isLNatKind(n__afterNth(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind(n__cons(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) isLNatKind(n__take(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isNatural(n__0()) -> tt() isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)),activate(V1)) isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)),activate(V1)) isNatural(n__sel(V1,V2)) -> U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isNaturalKind(n__0()) -> tt() isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) isNaturalKind(n__sel(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat(n__pair(V1,V2)) -> U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNat(n__splitAt(V1,V2)) -> U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNatKind(n__pair(V1,V2)) -> and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNatKind(n__splitAt(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) natsFrom(N) -> U161(and(isNatural(N),n__isNaturalKind(N)),N) sel(N,XS) -> U171(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) snd(pair(X,Y)) -> U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y) splitAt(0(),XS) -> U191(and(isLNat(XS),n__isLNatKind(XS)),XS) splitAt(s(N),cons(X,XS)) -> U201(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS))))), N,X,activate(XS)) tail(cons(N,XS)) -> U211(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), activate(XS)) take(N,XS) -> U221(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) natsFrom(X) -> n__natsFrom(X) isNaturalKind(X) -> n__isNaturalKind(X) and(X1,X2) -> n__and(X1,X2) isLNatKind(X) -> n__isLNatKind(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) activate(n__natsFrom(X)) -> natsFrom(X) activate(n__isNaturalKind(X)) -> isNaturalKind(X) activate(n__and(X1,X2)) -> and(X1,X2) activate(n__isLNatKind(X)) -> isLNatKind(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(X) -> X graph: ... SCC Processor: #sccs: 1 #rules: 220 #arcs: 2604/59049 DPs: take#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))) and#(tt(),X) -> activate#(X) activate#(n__natsFrom(X)) -> natsFrom#(X) natsFrom#(N) -> isNatural#(N) isNatural#(n__head(V1)) -> activate#(V1) activate#(n__isNaturalKind(X)) -> isNaturalKind#(X) isNaturalKind#(n__head(V1)) -> activate#(V1) activate#(n__and(X1,X2)) -> and#(X1,X2) activate#(n__isLNatKind(X)) -> isLNatKind#(X) isLNatKind#(n__afterNth(V1,V2)) -> activate#(V2) activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2) afterNth#(N,XS) -> isLNat#(XS) isLNat#(n__afterNth(V1,V2)) -> activate#(V2) activate#(n__fst(X)) -> fst#(X) fst#(pair(X,Y)) -> isLNat#(Y) isLNat#(n__afterNth(V1,V2)) -> activate#(V1) activate#(n__snd(X)) -> snd#(X) snd#(pair(X,Y)) -> isLNat#(Y) isLNat#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1)) isNaturalKind#(n__head(V1)) -> isLNatKind#(activate(V1)) isLNatKind#(n__afterNth(V1,V2)) -> activate#(V1) activate#(n__tail(X)) -> tail#(X) tail#(cons(N,XS)) -> activate#(XS) activate#(n__take(X1,X2)) -> take#(X1,X2) take#(N,XS) -> isLNat#(XS) isLNat#(n__afterNth(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNat#(n__afterNth(V1,V2)) -> U41#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) U41#(tt(),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) -> isLNat#(XS) isLNat#(n__cons(V1,V2)) -> activate#(V2) activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2) splitAt#(0(),XS) -> isLNat#(XS) isLNat#(n__cons(V1,V2)) -> activate#(V1) isLNat#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1)) isNaturalKind#(n__s(V1)) -> activate#(V1) isNaturalKind#(n__s(V1)) -> isNaturalKind#(activate(V1)) isNaturalKind#(n__sel(V1,V2)) -> activate#(V2) isNaturalKind#(n__sel(V1,V2)) -> activate#(V1) isNaturalKind#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1)) isNaturalKind#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNat#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNat#(n__cons(V1,V2)) -> U51#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) U51#(tt(),V1,V2) -> activate#(V2) U51#(tt(),V1,V2) -> activate#(V1) U51#(tt(),V1,V2) -> isNatural#(activate(V1)) isNatural#(n__head(V1)) -> isLNatKind#(activate(V1)) isLNatKind#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__afterNth(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind#(n__cons(V1,V2)) -> activate#(V2) isLNatKind#(n__cons(V1,V2)) -> activate#(V1) isLNatKind#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind#(n__fst(V1)) -> activate#(V1) isLNatKind#(n__fst(V1)) -> isPLNatKind#(activate(V1)) isPLNatKind#(n__pair(V1,V2)) -> activate#(V2) isPLNatKind#(n__pair(V1,V2)) -> activate#(V1) isPLNatKind#(n__pair(V1,V2)) -> isLNatKind#(activate(V1)) isLNatKind#(n__natsFrom(V1)) -> activate#(V1) isLNatKind#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__snd(V1)) -> activate#(V1) isLNatKind#(n__snd(V1)) -> isPLNatKind#(activate(V1)) isPLNatKind#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V2) isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V1) isPLNatKind#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1)) isPLNatKind#(n__splitAt(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind#(n__tail(V1)) -> activate#(V1) isLNatKind#(n__tail(V1)) -> isLNatKind#(activate(V1)) isLNatKind#(n__take(V1,V2)) -> activate#(V2) isLNatKind#(n__take(V1,V2)) -> activate#(V1) isLNatKind#(n__take(V1,V2)) -> isNaturalKind#(activate(V1)) isLNatKind#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isNatural#(n__head(V1)) -> U111#(isLNatKind(activate(V1)),activate(V1)) U111#(tt(),V1) -> activate#(V1) U111#(tt(),V1) -> isLNat#(activate(V1)) isLNat#(n__fst(V1)) -> activate#(V1) isLNat#(n__fst(V1)) -> isPLNatKind#(activate(V1)) isLNat#(n__fst(V1)) -> U61#(isPLNatKind(activate(V1)),activate(V1)) U61#(tt(),V1) -> activate#(V1) U61#(tt(),V1) -> isPLNat#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> activate#(V2) isPLNat#(n__pair(V1,V2)) -> activate#(V1) isPLNat#(n__pair(V1,V2)) -> isLNatKind#(activate(V1)) isPLNat#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat#(n__pair(V1,V2)) -> U141#(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) U141#(tt(),V1,V2) -> activate#(V2) U141#(tt(),V1,V2) -> activate#(V1) U141#(tt(),V1,V2) -> isLNat#(activate(V1)) isLNat#(n__natsFrom(V1)) -> activate#(V1) isLNat#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1)) isLNat#(n__natsFrom(V1)) -> U71#(isNaturalKind(activate(V1)),activate(V1)) U71#(tt(),V1) -> activate#(V1) U71#(tt(),V1) -> isNatural#(activate(V1)) isNatural#(n__s(V1)) -> activate#(V1) isNatural#(n__s(V1)) -> isNaturalKind#(activate(V1)) isNatural#(n__s(V1)) -> U121#(isNaturalKind(activate(V1)),activate(V1)) U121#(tt(),V1) -> activate#(V1) U121#(tt(),V1) -> isNatural#(activate(V1)) isNatural#(n__sel(V1,V2)) -> activate#(V2) isNatural#(n__sel(V1,V2)) -> activate#(V1) isNatural#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1)) isNatural#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isNatural#(n__sel(V1,V2)) -> U131#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) U131#(tt(),V1,V2) -> activate#(V2) U131#(tt(),V1,V2) -> activate#(V1) U131#(tt(),V1,V2) -> isNatural#(activate(V1)) U131#(tt(),V1,V2) -> U132#(isNatural(activate(V1)),activate(V2)) U132#(tt(),V2) -> activate#(V2) U132#(tt(),V2) -> isLNat#(activate(V2)) isLNat#(n__snd(V1)) -> activate#(V1) isLNat#(n__snd(V1)) -> isPLNatKind#(activate(V1)) isLNat#(n__snd(V1)) -> U81#(isPLNatKind(activate(V1)),activate(V1)) U81#(tt(),V1) -> activate#(V1) U81#(tt(),V1) -> isPLNat#(activate(V1)) isPLNat#(n__splitAt(V1,V2)) -> activate#(V2) isPLNat#(n__splitAt(V1,V2)) -> activate#(V1) isPLNat#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1)) isPLNat#(n__splitAt(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat#(n__splitAt(V1,V2)) -> U151#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) U151#(tt(),V1,V2) -> activate#(V2) U151#(tt(),V1,V2) -> activate#(V1) U151#(tt(),V1,V2) -> isNatural#(activate(V1)) U151#(tt(),V1,V2) -> U152#(isNatural(activate(V1)),activate(V2)) U152#(tt(),V2) -> activate#(V2) U152#(tt(),V2) -> isLNat#(activate(V2)) isLNat#(n__tail(V1)) -> activate#(V1) isLNat#(n__tail(V1)) -> isLNatKind#(activate(V1)) isLNat#(n__tail(V1)) -> U91#(isLNatKind(activate(V1)),activate(V1)) U91#(tt(),V1) -> activate#(V1) U91#(tt(),V1) -> isLNat#(activate(V1)) isLNat#(n__take(V1,V2)) -> activate#(V2) isLNat#(n__take(V1,V2)) -> activate#(V1) isLNat#(n__take(V1,V2)) -> isNaturalKind#(activate(V1)) isLNat#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNat#(n__take(V1,V2)) -> U101#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) U101#(tt(),V1,V2) -> activate#(V2) U101#(tt(),V1,V2) -> activate#(V1) U101#(tt(),V1,V2) -> isNatural#(activate(V1)) U101#(tt(),V1,V2) -> U102#(isNatural(activate(V1)),activate(V2)) U102#(tt(),V2) -> activate#(V2) U102#(tt(),V2) -> isLNat#(activate(V2)) U141#(tt(),V1,V2) -> U142#(isLNat(activate(V1)),activate(V2)) U142#(tt(),V2) -> activate#(V2) U142#(tt(),V2) -> isLNat#(activate(V2)) U51#(tt(),V1,V2) -> U52#(isNatural(activate(V1)),activate(V2)) U52#(tt(),V2) -> activate#(V2) U52#(tt(),V2) -> isLNat#(activate(V2)) splitAt#(0(),XS) -> and#(isLNat(XS),n__isLNatKind(XS)) splitAt#(0(),XS) -> U191#(and(isLNat(XS),n__isLNatKind(XS)),XS) U191#(tt(),XS) -> activate#(XS) splitAt#(s(N),cons(X,XS)) -> activate#(XS) splitAt#(s(N),cons(X,XS)) -> isLNat#(activate(XS)) splitAt#(s(N),cons(X,XS)) -> isNatural#(X) splitAt#(s(N),cons(X,XS)) -> and#(isNatural(X),n__isNaturalKind(X)) splitAt#(s(N),cons(X,XS)) -> isNatural#(N) splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__isNaturalKind(N)) splitAt#(s(N),cons(X,XS)) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS))))) splitAt#(s(N),cons(X,XS)) -> U201#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS))))), N,X,activate(XS)) U201#(tt(),N,X,XS) -> activate#(X) U201#(tt(),N,X,XS) -> activate#(XS) U201#(tt(),N,X,XS) -> activate#(N) U201#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) U201#(tt(),N,X,XS) -> U202#(splitAt(activate(N),activate(XS)),activate(X)) U202#(pair(YS,ZS),X) -> activate#(X) sel#(N,XS) -> isNatural#(N) sel#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N)) sel#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))) sel#(N,XS) -> U171#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) U171#(tt(),N,XS) -> activate#(XS) U171#(tt(),N,XS) -> activate#(N) U171#(tt(),N,XS) -> afterNth#(activate(N),activate(XS)) afterNth#(N,XS) -> isNatural#(N) afterNth#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N)) afterNth#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))) afterNth#(N,XS) -> U11#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(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)) -> isLNat#(X) snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X)) snd#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))) snd#(pair(X,Y)) -> U181#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y) U181#(tt(),Y) -> activate#(Y) U171#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS))) head#(cons(N,XS)) -> isLNat#(activate(XS)) head#(cons(N,XS)) -> isNatural#(N) head#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N)) head#(cons(N,XS)) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) head#(cons(N,XS)) -> U31#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), N) U31#(tt(),N) -> activate#(N) U41#(tt(),V1,V2) -> activate#(V1) U41#(tt(),V1,V2) -> isNatural#(activate(V1)) U41#(tt(),V1,V2) -> U42#(isNatural(activate(V1)),activate(V2)) U42#(tt(),V2) -> activate#(V2) U42#(tt(),V2) -> isLNat#(activate(V2)) take#(N,XS) -> isNatural#(N) take#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N)) take#(N,XS) -> U221#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) U221#(tt(),N,XS) -> activate#(XS) U221#(tt(),N,XS) -> activate#(N) U221#(tt(),N,XS) -> splitAt#(activate(N),activate(XS)) U221#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS))) fst#(pair(X,Y)) -> isLNat#(X) fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X)) fst#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))) fst#(pair(X,Y)) -> U21#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X) U21#(tt(),X) -> activate#(X) tail#(cons(N,XS)) -> isLNat#(activate(XS)) tail#(cons(N,XS)) -> isNatural#(N) tail#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N)) tail#(cons(N,XS)) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) tail#(cons(N,XS)) -> U211#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), activate(XS)) U211#(tt(),XS) -> activate#(XS) natsFrom#(N) -> and#(isNatural(N),n__isNaturalKind(N)) natsFrom#(N) -> U161#(and(isNatural(N),n__isNaturalKind(N)),N) U161#(tt(),N) -> activate#(N) TRS: U101(tt(),V1,V2) -> U102(isNatural(activate(V1)),activate(V2)) U102(tt(),V2) -> U103(isLNat(activate(V2))) U103(tt()) -> tt() U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS))) U111(tt(),V1) -> U112(isLNat(activate(V1))) U112(tt()) -> tt() U121(tt(),V1) -> U122(isNatural(activate(V1))) U122(tt()) -> tt() U131(tt(),V1,V2) -> U132(isNatural(activate(V1)),activate(V2)) U132(tt(),V2) -> U133(isLNat(activate(V2))) U133(tt()) -> tt() U141(tt(),V1,V2) -> U142(isLNat(activate(V1)),activate(V2)) U142(tt(),V2) -> U143(isLNat(activate(V2))) U143(tt()) -> tt() U151(tt(),V1,V2) -> U152(isNatural(activate(V1)),activate(V2)) U152(tt(),V2) -> U153(isLNat(activate(V2))) U153(tt()) -> tt() U161(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N)))) U171(tt(),N,XS) -> head(afterNth(activate(N),activate(XS))) U181(tt(),Y) -> activate(Y) U191(tt(),XS) -> pair(nil(),activate(XS)) U201(tt(),N,X,XS) -> U202(splitAt(activate(N),activate(XS)),activate(X)) U202(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) U21(tt(),X) -> activate(X) U211(tt(),XS) -> activate(XS) U221(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS))) U31(tt(),N) -> activate(N) U41(tt(),V1,V2) -> U42(isNatural(activate(V1)),activate(V2)) U42(tt(),V2) -> U43(isLNat(activate(V2))) U43(tt()) -> tt() U51(tt(),V1,V2) -> U52(isNatural(activate(V1)),activate(V2)) U52(tt(),V2) -> U53(isLNat(activate(V2))) U53(tt()) -> tt() U61(tt(),V1) -> U62(isPLNat(activate(V1))) U62(tt()) -> tt() U71(tt(),V1) -> U72(isNatural(activate(V1))) U72(tt()) -> tt() U81(tt(),V1) -> U82(isPLNat(activate(V1))) U82(tt()) -> tt() U91(tt(),V1) -> U92(isLNat(activate(V1))) U92(tt()) -> tt() afterNth(N,XS) -> U11(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) and(tt(),X) -> activate(X) fst(pair(X,Y)) -> U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X) head(cons(N,XS)) -> U31(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), N) isLNat(n__nil()) -> tt() isLNat(n__afterNth(V1,V2)) -> U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat(n__cons(V1,V2)) -> U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1)) isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1)) isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1)) isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1)) isLNat(n__take(V1,V2)) -> U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isLNatKind(n__nil()) -> tt() isLNatKind(n__afterNth(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind(n__cons(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) isLNatKind(n__take(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isNatural(n__0()) -> tt() isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)),activate(V1)) isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)),activate(V1)) isNatural(n__sel(V1,V2)) -> U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isNaturalKind(n__0()) -> tt() isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) isNaturalKind(n__sel(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNat(n__pair(V1,V2)) -> U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNat(n__splitAt(V1,V2)) -> U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2)) isPLNatKind(n__pair(V1,V2)) -> and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) isPLNatKind(n__splitAt(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) natsFrom(N) -> U161(and(isNatural(N),n__isNaturalKind(N)),N) sel(N,XS) -> U171(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) snd(pair(X,Y)) -> U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y) splitAt(0(),XS) -> U191(and(isLNat(XS),n__isLNatKind(XS)),XS) splitAt(s(N),cons(X,XS)) -> U201(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS))))), N,X,activate(XS)) tail(cons(N,XS)) -> U211(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)), n__isLNatKind (activate(XS)))), activate(XS)) take(N,XS) -> U221(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) natsFrom(X) -> n__natsFrom(X) isNaturalKind(X) -> n__isNaturalKind(X) and(X1,X2) -> n__and(X1,X2) isLNatKind(X) -> n__isLNatKind(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) activate(n__natsFrom(X)) -> natsFrom(X) activate(n__isNaturalKind(X)) -> isNaturalKind(X) activate(n__and(X1,X2)) -> and(X1,X2) activate(n__isLNatKind(X)) -> isLNatKind(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(X) -> X Open