TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60017 ms.

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (timeout)].

The following open problems remain:



Open Dependency Pair Problem 1

Dependency Pairs

U11#(tt, N, XS)splitAt#(activate(N), activate(XS))U41#(tt, V1, V2)U42#(isNatural(activate(V1)), activate(V2))
activate#(n__tail(X))activate#(X)afterNth#(N, XS)isNatural#(N)
isLNatKind#(n__natsFrom(V1))isNaturalKind#(activate(V1))isNatural#(n__sel(V1, V2))isNaturalKind#(activate(V1))
U121#(tt, V1)U122#(isNatural(activate(V1)))U151#(tt, V1, V2)activate#(V1)
U91#(tt, V1)isLNat#(activate(V1))head#(cons(N, XS))and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))
U191#(tt, XS)pair#(nil, activate(XS))isLNat#(n__natsFrom(V1))U71#(isNaturalKind(activate(V1)), activate(V1))
activate#(n__cons(X1, X2))cons#(activate(X1), X2)splitAt#(s(N), cons(X, XS))and#(isNatural(N), n__isNaturalKind(N))
isNaturalKind#(n__sel(V1, V2))activate#(V2)isLNat#(n__cons(V1, V2))activate#(V2)
isLNatKind#(n__tail(V1))isLNatKind#(activate(V1))U141#(tt, V1, V2)activate#(V1)
U91#(tt, V1)activate#(V1)U201#(tt, N, X, XS)activate#(XS)
U71#(tt, V1)isNatural#(activate(V1))U181#(tt, Y)activate#(Y)
isLNatKind#(n__afterNth(V1, V2))and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))isPLNat#(n__pair(V1, V2))activate#(V1)
U132#(tt, V2)isLNat#(activate(V2))U202#(pair(YS, ZS), X)cons#(activate(X), YS)
U102#(tt, V2)activate#(V2)isPLNatKind#(n__pair(V1, V2))isLNatKind#(activate(V1))
splitAt#(s(N), cons(X, XS))and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))))isNaturalKind#(n__sel(V1, V2))and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
U111#(tt, V1)U112#(isLNat(activate(V1)))isPLNat#(n__splitAt(V1, V2))and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isLNatKind#(n__afterNth(V1, V2))isNaturalKind#(activate(V1))U51#(tt, V1, V2)U52#(isNatural(activate(V1)), activate(V2))
U221#(tt, N, XS)fst#(splitAt(activate(N), activate(XS)))U131#(tt, V1, V2)activate#(V2)
isNaturalKind#(n__head(V1))isLNatKind#(activate(V1))tail#(cons(N, XS))and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))
activate#(n__sel(X1, X2))activate#(X2)U52#(tt, V2)isLNat#(activate(V2))
activate#(n__s(X))activate#(X)isPLNatKind#(n__pair(V1, V2))activate#(V2)
isNaturalKind#(n__sel(V1, V2))activate#(V1)isPLNat#(n__pair(V1, V2))and#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
isPLNatKind#(n__splitAt(V1, V2))activate#(V1)isLNatKind#(n__afterNth(V1, V2))activate#(V2)
isNatural#(n__head(V1))activate#(V1)U152#(tt, V2)activate#(V2)
isLNat#(n__take(V1, V2))and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))U131#(tt, V1, V2)isNatural#(activate(V1))
isLNat#(n__natsFrom(V1))isNaturalKind#(activate(V1))activate#(n__isLNatKind(X))isLNatKind#(X)
isNaturalKind#(n__s(V1))isNaturalKind#(activate(V1))take#(N, XS)isNatural#(N)
U81#(tt, V1)U82#(isPLNat(activate(V1)))isLNat#(n__fst(V1))U61#(isPLNatKind(activate(V1)), activate(V1))
head#(cons(N, XS))isNatural#(N)U151#(tt, V1, V2)activate#(V2)
isLNat#(n__take(V1, V2))U101#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))U201#(tt, N, X, XS)activate#(N)
isNatural#(n__sel(V1, V2))U131#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))activate#(n__pair(X1, X2))pair#(activate(X1), activate(X2))
head#(cons(N, XS))and#(isNatural(N), n__isNaturalKind(N))take#(N, XS)U221#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
splitAt#(s(N), cons(X, XS))activate#(XS)U71#(tt, V1)U72#(isNatural(activate(V1)))
U52#(tt, V2)U53#(isLNat(activate(V2)))U141#(tt, V1, V2)U142#(isLNat(activate(V1)), activate(V2))
isLNatKind#(n__take(V1, V2))activate#(V2)isLNat#(n__tail(V1))isLNatKind#(activate(V1))
activate#(n__snd(X))activate#(X)U101#(tt, V1, V2)isNatural#(activate(V1))
activate#(n__cons(X1, X2))activate#(X1)U142#(tt, V2)activate#(V2)
U41#(tt, V1, V2)isNatural#(activate(V1))tail#(cons(N, XS))isNatural#(N)
isLNat#(n__take(V1, V2))activate#(V2)U171#(tt, N, XS)activate#(XS)
U102#(tt, V2)U103#(isLNat(activate(V2)))U191#(tt, XS)activate#(XS)
activate#(n__tail(X))tail#(activate(X))isLNatKind#(n__snd(V1))activate#(V1)
isNatural#(n__sel(V1, V2))activate#(V2)isPLNat#(n__splitAt(V1, V2))U151#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
U121#(tt, V1)isNatural#(activate(V1))activate#(n__natsFrom(X))activate#(X)
U161#(tt, N)activate#(N)U111#(tt, V1)isLNat#(activate(V1))
fst#(pair(X, Y))and#(isLNat(X), n__isLNatKind(X))afterNth#(N, XS)U11#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
U131#(tt, V1, V2)activate#(V1)U151#(tt, V1, V2)isNatural#(activate(V1))
isNatural#(n__sel(V1, V2))and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))U171#(tt, N, XS)head#(afterNth(activate(N), activate(XS)))
tail#(cons(N, XS))U211#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))activate#(n__and(X1, X2))activate#(X1)
activate#(n__natsFrom(X))natsFrom#(activate(X))isLNatKind#(n__take(V1, V2))isNaturalKind#(activate(V1))
snd#(pair(X, Y))U181#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)take#(N, XS)and#(isNatural(N), n__isNaturalKind(N))
isNatural#(n__sel(V1, V2))activate#(V1)activate#(n__afterNth(X1, X2))activate#(X2)
splitAt#(0, XS)and#(isLNat(XS), n__isLNatKind(XS))isLNat#(n__fst(V1))activate#(V1)
splitAt#(0, XS)isLNat#(XS)activate#(n__splitAt(X1, X2))splitAt#(activate(X1), activate(X2))
activate#(n__afterNth(X1, X2))activate#(X1)isLNat#(n__afterNth(V1, V2))activate#(V1)
activate#(n__take(X1, X2))activate#(X2)U11#(tt, N, XS)activate#(N)
activate#(n__afterNth(X1, X2))afterNth#(activate(X1), activate(X2))U171#(tt, N, XS)activate#(N)
isLNatKind#(n__cons(V1, V2))activate#(V1)activate#(n__sel(X1, X2))sel#(activate(X1), activate(X2))
isPLNat#(n__pair(V1, V2))activate#(V2)isLNat#(n__cons(V1, V2))and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isNatural#(n__s(V1))isNaturalKind#(activate(V1))isLNatKind#(n__snd(V1))isPLNatKind#(activate(V1))
isPLNatKind#(n__pair(V1, V2))activate#(V1)isLNat#(n__cons(V1, V2))activate#(V1)
U111#(tt, V1)activate#(V1)U142#(tt, V2)U143#(isLNat(activate(V2)))
snd#(pair(X, Y))and#(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y)))isLNatKind#(n__cons(V1, V2))and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
and#(tt, X)activate#(X)sel#(N, XS)isNatural#(N)
activate#(n__and(X1, X2))and#(activate(X1), X2)activate#(n__head(X))activate#(X)
isLNat#(n__afterNth(V1, V2))and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))U11#(tt, N, XS)snd#(splitAt(activate(N), activate(XS)))
afterNth#(N, XS)and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS)))U61#(tt, V1)isPLNat#(activate(V1))
U42#(tt, V2)isLNat#(activate(V2))U161#(tt, N)cons#(activate(N), n__natsFrom(n__s(activate(N))))
isLNat#(n__take(V1, V2))activate#(V1)U52#(tt, V2)activate#(V2)
head#(cons(N, XS))activate#(XS)isNatural#(n__s(V1))U121#(isNaturalKind(activate(V1)), activate(V1))
snd#(pair(X, Y))isLNat#(X)isLNat#(n__tail(V1))U91#(isLNatKind(activate(V1)), activate(V1))
isLNat#(n__tail(V1))activate#(V1)isLNatKind#(n__cons(V1, V2))activate#(V2)
activate#(n__isNatural(X))isNatural#(X)activate#(n__isLNat(X))isLNat#(X)
take#(N, XS)and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS)))U102#(tt, V2)isLNat#(activate(V2))
isLNat#(n__snd(V1))isPLNatKind#(activate(V1))splitAt#(0, XS)U191#(and(isLNat(XS), n__isLNatKind(XS)), XS)
U131#(tt, V1, V2)U132#(isNatural(activate(V1)), activate(V2))sel#(N, XS)U171#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
activate#(n__fst(X))activate#(X)isLNat#(n__snd(V1))U81#(isPLNatKind(activate(V1)), activate(V1))
isPLNat#(n__pair(V1, V2))isLNatKind#(activate(V1))U42#(tt, V2)U43#(isLNat(activate(V2)))
isLNatKind#(n__natsFrom(V1))activate#(V1)U201#(tt, N, X, XS)splitAt#(activate(N), activate(XS))
isLNat#(n__cons(V1, V2))U51#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))isLNatKind#(n__cons(V1, V2))isNaturalKind#(activate(V1))
activate#(n__fst(X))fst#(activate(X))natsFrom#(N)U161#(and(isNatural(N), n__isNaturalKind(N)), N)
afterNth#(N, XS)and#(isNatural(N), n__isNaturalKind(N))tail#(cons(N, XS))and#(isNatural(N), n__isNaturalKind(N))
isNaturalKind#(n__sel(V1, V2))isNaturalKind#(activate(V1))isLNatKind#(n__fst(V1))isPLNatKind#(activate(V1))
isLNat#(n__natsFrom(V1))activate#(V1)isPLNat#(n__splitAt(V1, V2))isNaturalKind#(activate(V1))
U221#(tt, N, XS)activate#(XS)U202#(pair(YS, ZS), X)activate#(X)
U101#(tt, V1, V2)U102#(isNatural(activate(V1)), activate(V2))natsFrom#(N)isNatural#(N)
fst#(pair(X, Y))isLNat#(X)U201#(tt, N, X, XS)U202#(splitAt(activate(N), activate(XS)), activate(X))
isNatural#(n__s(V1))activate#(V1)isLNat#(n__afterNth(V1, V2))isNaturalKind#(activate(V1))
isLNat#(n__afterNth(V1, V2))activate#(V2)U202#(pair(YS, ZS), X)pair#(cons(activate(X), YS), ZS)
U41#(tt, V1, V2)activate#(V2)U171#(tt, N, XS)afterNth#(activate(N), activate(XS))
U152#(tt, V2)U153#(isLNat(activate(V2)))U132#(tt, V2)activate#(V2)
U211#(tt, XS)activate#(XS)isPLNat#(n__splitAt(V1, V2))activate#(V2)
U142#(tt, V2)isLNat#(activate(V2))activate#(n__take(X1, X2))activate#(X1)
snd#(pair(X, Y))and#(isLNat(X), n__isLNatKind(X))U11#(tt, N, XS)activate#(XS)
U141#(tt, V1, V2)activate#(V2)activate#(n__s(X))s#(activate(X))
isLNat#(n__snd(V1))activate#(V1)splitAt#(s(N), cons(X, XS))isNatural#(N)
U51#(tt, V1, V2)activate#(V1)activate#(n__isNaturalKind(X))isNaturalKind#(X)
U151#(tt, V1, V2)U152#(isNatural(activate(V1)), activate(V2))natsFrom#(N)and#(isNatural(N), n__isNaturalKind(N))
isPLNatKind#(n__splitAt(V1, V2))isNaturalKind#(activate(V1))activate#(n__sel(X1, X2))activate#(X1)
activate#(n__take(X1, X2))take#(activate(X1), activate(X2))activate#(n__snd(X))snd#(activate(X))
fst#(pair(X, Y))U21#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)isPLNatKind#(n__splitAt(V1, V2))and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
U191#(tt, XS)nil#isLNatKind#(n__afterNth(V1, V2))activate#(V1)
isPLNatKind#(n__splitAt(V1, V2))activate#(V2)U101#(tt, V1, V2)activate#(V1)
U152#(tt, V2)isLNat#(activate(V2))head#(cons(N, XS))U31#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)
sel#(N, XS)and#(isNatural(N), n__isNaturalKind(N))isLNat#(n__fst(V1))isPLNatKind#(activate(V1))
isLNatKind#(n__tail(V1))activate#(V1)isLNat#(n__take(V1, V2))isNaturalKind#(activate(V1))
isLNatKind#(n__take(V1, V2))and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))U221#(tt, N, XS)activate#(N)
U41#(tt, V1, V2)activate#(V1)splitAt#(s(N), cons(X, XS))U201#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))
isNatural#(n__head(V1))U111#(isLNatKind(activate(V1)), activate(V1))isPLNat#(n__pair(V1, V2))U141#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
U121#(tt, V1)activate#(V1)isLNatKind#(n__fst(V1))activate#(V1)
activate#(n__pair(X1, X2))activate#(X2)activate#(n__0)0#
U81#(tt, V1)isPLNat#(activate(V1))activate#(n__pair(X1, X2))activate#(X1)
U91#(tt, V1)U92#(isLNat(activate(V1)))isNaturalKind#(n__head(V1))activate#(V1)
U51#(tt, V1, V2)activate#(V2)tail#(cons(N, XS))activate#(XS)
U21#(tt, X)activate#(X)U101#(tt, V1, V2)activate#(V2)
isPLNat#(n__splitAt(V1, V2))activate#(V1)isPLNatKind#(n__pair(V1, V2))and#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
U201#(tt, N, X, XS)activate#(X)U42#(tt, V2)activate#(V2)
sel#(N, XS)and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS)))U61#(tt, V1)activate#(V1)
U81#(tt, V1)activate#(V1)U71#(tt, V1)activate#(V1)
isLNatKind#(n__take(V1, V2))activate#(V1)U132#(tt, V2)U133#(isLNat(activate(V2)))
U51#(tt, V1, V2)isNatural#(activate(V1))isNaturalKind#(n__s(V1))activate#(V1)
fst#(pair(X, Y))and#(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y)))U31#(tt, N)activate#(N)
isNatural#(n__head(V1))isLNatKind#(activate(V1))isLNat#(n__cons(V1, V2))isNaturalKind#(activate(V1))
activate#(n__head(X))head#(activate(X))activate#(n__nil)nil#
U61#(tt, V1)U62#(isPLNat(activate(V1)))activate#(n__splitAt(X1, X2))activate#(X1)
U141#(tt, V1, V2)isLNat#(activate(V1))isLNat#(n__afterNth(V1, V2))U41#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
activate#(n__splitAt(X1, X2))activate#(X2)U221#(tt, N, XS)splitAt#(activate(N), activate(XS))

Rewrite Rules

U101(tt, V1, V2)U102(isNatural(activate(V1)), activate(V2))U102(tt, V2)U103(isLNat(activate(V2)))
U103(tt)ttU11(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)ttU141(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)ttU161(tt, N)cons(activate(N), n__natsFrom(n__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)ttU61(tt, V1)U62(isPLNat(activate(V1)))
U62(tt)ttU71(tt, V1)U72(isNatural(activate(V1)))
U72(tt)ttU81(tt, V1)U82(isPLNat(activate(V1)))
U82(tt)ttU91(tt, V1)U92(isLNat(activate(V1)))
U92(tt)ttafterNth(N, XS)U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__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(n__isLNat(Y), n__isLNatKind(Y))), X)
head(cons(N, XS))U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__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(n__isLNat(XS), n__isLNatKind(XS))), N, XS)snd(pair(X, Y))U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__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(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__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(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))take(N, XS)U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
natsFrom(X)n__natsFrom(X)s(X)n__s(X)
isNaturalKind(X)n__isNaturalKind(X)and(X1, X2)n__and(X1, X2)
isLNat(X)n__isLNat(X)isLNatKind(X)n__isLNatKind(X)
niln__nilafterNth(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)0n__0
head(X)n__head(X)sel(X1, X2)n__sel(X1, X2)
pair(X1, X2)n__pair(X1, X2)splitAt(X1, X2)n__splitAt(X1, X2)
isNatural(X)n__isNatural(X)activate(n__natsFrom(X))natsFrom(activate(X))
activate(n__s(X))s(activate(X))activate(n__isNaturalKind(X))isNaturalKind(X)
activate(n__and(X1, X2))and(activate(X1), X2)activate(n__isLNat(X))isLNat(X)
activate(n__isLNatKind(X))isLNatKind(X)activate(n__nil)nil
activate(n__afterNth(X1, X2))afterNth(activate(X1), activate(X2))activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__fst(X))fst(activate(X))activate(n__snd(X))snd(activate(X))
activate(n__tail(X))tail(activate(X))activate(n__take(X1, X2))take(activate(X1), activate(X2))
activate(n__0)0activate(n__head(X))head(activate(X))
activate(n__sel(X1, X2))sel(activate(X1), activate(X2))activate(n__pair(X1, X2))pair(activate(X1), activate(X2))
activate(n__splitAt(X1, X2))splitAt(activate(X1), activate(X2))activate(n__isNatural(X))isNatural(X)
activate(X)X

Original Signature

Termination of terms over the following signature is verified: natsFrom, U161, n__snd, n__sel, n__fst, n__s, activate, U112, fst, U111, U62, U61, U211, n__isLNatKind, n__nil, head, U21, n__tail, U153, U151, isLNatKind, isPLNat, U152, tail, n__natsFrom, and, U71, U191, n__cons, U72, 0, isPLNatKind, U122, U121, U221, isLNat, U31, U181, pair, isNatural, n__head, n__splitAt, U132, n__0, U131, U43, n__afterNth, n__isLNat, U42, U92, U133, U41, U91, n__isNatural, snd, cons, isNaturalKind, U171, n__isNaturalKind, n__take, splitAt, U143, U201, n__and, U142, U202, U141, s, U51, tt, take, U82, U53, U81, U52, U11, n__pair, afterNth, U102, sel, U103, U101, nil