TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (11886ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (8783ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (8844ms), PolynomialLinearRange8NegiUR (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

U11#(tt, N, XS) → splitAt#(activate(N), activate(XS))and#(tt, X) → activate#(X)
sel#(N, XS) → isNatural#(N)U81#(tt, N, X, XS) → splitAt#(activate(N), activate(XS))
isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1))activate#(n__snd(X)) → snd#(X)
afterNth#(N, XS) → isNatural#(N)U11#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS)))
take#(N, XS) → and#(isNatural(N), n__isLNat(XS))fst#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y))
isLNat#(n__cons(V1, V2)) → activate#(V2)isLNat#(n__take(V1, V2)) → activate#(V1)
isLNat#(n__take(V1, V2)) → isNatural#(activate(V1))isNatural#(n__s(V1)) → isNatural#(activate(V1))
U51#(tt, N, XS) → activate#(N)take#(N, XS) → U101#(and(isNatural(N), n__isLNat(XS)), N, XS)
head#(cons(N, XS)) → activate#(XS)snd#(pair(X, Y)) → isLNat#(X)
isLNat#(n__take(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))fst#(pair(X, Y)) → U21#(and(isLNat(X), n__isLNat(Y)), X)
isPLNat#(n__pair(V1, V2)) → activate#(V1)isLNat#(n__tail(V1)) → activate#(V1)
activate#(n__head(X)) → head#(X)U91#(tt, XS) → activate#(XS)
U81#(tt, N, X, XS) → activate#(N)activate#(n__isLNat(X)) → isLNat#(X)
activate#(n__splitAt(X1, X2)) → splitAt#(X1, X2)U101#(tt, N, XS) → splitAt#(activate(N), activate(XS))
activate#(n__tail(X)) → tail#(X)isPLNat#(n__splitAt(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))
head#(cons(N, XS)) → U31#(and(isNatural(N), n__isLNat(activate(XS))), N)U51#(tt, N, XS) → activate#(XS)
isLNat#(n__natsFrom(V1)) → activate#(V1)activate#(n__sel(X1, X2)) → sel#(X1, X2)
isNatural#(n__head(V1)) → activate#(V1)afterNth#(N, XS) → and#(isNatural(N), n__isLNat(XS))
natsFrom#(N) → isNatural#(N)fst#(pair(X, Y)) → isLNat#(X)
sel#(N, XS) → U51#(and(isNatural(N), n__isLNat(XS)), N, XS)isNatural#(n__s(V1)) → activate#(V1)
isLNat#(n__afterNth(V1, V2)) → activate#(V2)isLNat#(n__cons(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))
splitAt#(s(N), cons(X, XS)) → and#(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS))))isLNat#(n__tail(V1)) → isLNat#(activate(V1))
splitAt#(s(N), cons(X, XS)) → U81#(and(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1))
take#(N, XS) → isNatural#(N)isLNat#(n__afterNth(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))
isPLNat#(n__splitAt(V1, V2)) → activate#(V2)head#(cons(N, XS)) → isNatural#(N)
isNatural#(n__sel(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1))
activate#(n__afterNth(X1, X2)) → afterNth#(X1, X2)isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1))
U11#(tt, N, XS) → activate#(XS)activate#(n__take(X1, X2)) → take#(X1, X2)
isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1))isLNat#(n__snd(V1)) → activate#(V1)
isLNat#(n__snd(V1)) → isPLNat#(activate(V1))activate#(n__and(X1, X2)) → and#(X1, X2)
snd#(pair(X, Y)) → U61#(and(isLNat(X), n__isLNat(Y)), Y)splitAt#(s(N), cons(X, XS)) → activate#(XS)
splitAt#(s(N), cons(X, XS)) → isNatural#(N)U41#(tt, N) → activate#(N)
U101#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS)))sel#(N, XS) → and#(isNatural(N), n__isLNat(XS))
U51#(tt, N, XS) → afterNth#(activate(N), activate(XS))tail#(cons(N, XS)) → isNatural#(N)
isLNat#(n__take(V1, V2)) → activate#(V2)tail#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS)))
isNatural#(n__sel(V1, V2)) → activate#(V2)snd#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y))
splitAt#(s(N), cons(X, XS)) → isNatural#(X)head#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS)))
U81#(tt, N, X, XS) → activate#(X)tail#(cons(N, XS)) → U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
isPLNat#(n__pair(V1, V2)) → and#(isLNat(activate(V1)), n__isLNat(activate(V2)))U81#(tt, N, X, XS) → U82#(splitAt(activate(N), activate(XS)), activate(X))
U82#(pair(YS, ZS), X) → activate#(X)afterNth#(N, XS) → U11#(and(isNatural(N), n__isLNat(XS)), N, XS)
natsFrom#(N) → U41#(isNatural(N), N)tail#(cons(N, XS)) → activate#(XS)
U21#(tt, X) → activate#(X)U61#(tt, Y) → activate#(Y)
isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1))isNatural#(n__sel(V1, V2)) → activate#(V1)
U101#(tt, N, XS) → activate#(XS)isPLNat#(n__splitAt(V1, V2)) → activate#(V1)
isLNat#(n__fst(V1)) → activate#(V1)splitAt#(0, XS) → isLNat#(XS)
isLNat#(n__afterNth(V1, V2)) → activate#(V1)U11#(tt, N, XS) → activate#(N)
activate#(n__natsFrom(X)) → natsFrom#(X)isLNat#(n__fst(V1)) → isPLNat#(activate(V1))
isPLNat#(n__pair(V1, V2)) → activate#(V2)activate#(n__fst(X)) → fst#(X)
U31#(tt, N) → activate#(N)U51#(tt, N, XS) → head#(afterNth(activate(N), activate(XS)))
splitAt#(0, XS) → U71#(isLNat(XS), XS)isNatural#(n__head(V1)) → isLNat#(activate(V1))
isLNat#(n__cons(V1, V2)) → activate#(V1)U71#(tt, XS) → activate#(XS)
U101#(tt, N, XS) → activate#(N)U81#(tt, N, X, XS) → activate#(XS)

Rewrite Rules

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__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)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) → nilactivate(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

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, isNatural, n__snd, n__head, n__sel, n__splitAt, n__fst, n__s, activate, fst, n__0, U61, n__afterNth, n__isLNat, U41, U91, n__nil, head, U21, cons, snd, n__tail, isPLNat, n__take, tail, n__natsFrom, splitAt, and, U71, n__and, n__cons, 0, s, U51, tt, take, U82, isLNat, U81, U11, n__pair, U31, afterNth, sel, U101, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

U11#(tt, N, XS) → splitAt#(activate(N), activate(XS))and#(tt, X) → activate#(X)
sel#(N, XS) → isNatural#(N)U81#(tt, N, X, XS) → splitAt#(activate(N), activate(XS))
isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1))activate#(n__snd(X)) → snd#(X)
afterNth#(N, XS) → isNatural#(N)U11#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS)))
take#(N, XS) → and#(isNatural(N), n__isLNat(XS))fst#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y))
isLNat#(n__cons(V1, V2)) → activate#(V2)isLNat#(n__take(V1, V2)) → isNatural#(activate(V1))
U82#(pair(YS, ZS), X) → pair#(cons(activate(X), YS), ZS)isLNat#(n__take(V1, V2)) → activate#(V1)
isNatural#(n__s(V1)) → isNatural#(activate(V1))U51#(tt, N, XS) → activate#(N)
take#(N, XS) → U101#(and(isNatural(N), n__isLNat(XS)), N, XS)head#(cons(N, XS)) → activate#(XS)
snd#(pair(X, Y)) → isLNat#(X)isLNat#(n__take(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))
fst#(pair(X, Y)) → U21#(and(isLNat(X), n__isLNat(Y)), X)isPLNat#(n__pair(V1, V2)) → activate#(V1)
isLNat#(n__tail(V1)) → activate#(V1)activate#(n__head(X)) → head#(X)
U91#(tt, XS) → activate#(XS)U81#(tt, N, X, XS) → activate#(N)
activate#(n__isLNat(X)) → isLNat#(X)activate#(n__splitAt(X1, X2)) → splitAt#(X1, X2)
U101#(tt, N, XS) → splitAt#(activate(N), activate(XS))activate#(n__tail(X)) → tail#(X)
U82#(pair(YS, ZS), X) → cons#(activate(X), YS)U41#(tt, N) → s#(activate(N))
isPLNat#(n__splitAt(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))head#(cons(N, XS)) → U31#(and(isNatural(N), n__isLNat(activate(XS))), N)
U51#(tt, N, XS) → activate#(XS)isLNat#(n__natsFrom(V1)) → activate#(V1)
activate#(n__sel(X1, X2)) → sel#(X1, X2)isNatural#(n__head(V1)) → activate#(V1)
afterNth#(N, XS) → and#(isNatural(N), n__isLNat(XS))natsFrom#(N) → isNatural#(N)
fst#(pair(X, Y)) → isLNat#(X)sel#(N, XS) → U51#(and(isNatural(N), n__isLNat(XS)), N, XS)
isNatural#(n__s(V1)) → activate#(V1)isLNat#(n__afterNth(V1, V2)) → activate#(V2)
isLNat#(n__cons(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))splitAt#(s(N), cons(X, XS)) → and#(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS))))
isLNat#(n__tail(V1)) → isLNat#(activate(V1))splitAt#(s(N), cons(X, XS)) → U81#(and(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))
isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1))take#(N, XS) → isNatural#(N)
isLNat#(n__afterNth(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))head#(cons(N, XS)) → isNatural#(N)
isPLNat#(n__splitAt(V1, V2)) → activate#(V2)isNatural#(n__sel(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))
isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1))activate#(n__afterNth(X1, X2)) → afterNth#(X1, X2)
isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1))U11#(tt, N, XS) → activate#(XS)
activate#(n__take(X1, X2)) → take#(X1, X2)isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1))
isLNat#(n__snd(V1)) → isPLNat#(activate(V1))isLNat#(n__snd(V1)) → activate#(V1)
activate#(n__and(X1, X2)) → and#(X1, X2)snd#(pair(X, Y)) → U61#(and(isLNat(X), n__isLNat(Y)), Y)
U41#(tt, N) → cons#(activate(N), n__natsFrom(s(activate(N))))splitAt#(s(N), cons(X, XS)) → isNatural#(N)
splitAt#(s(N), cons(X, XS)) → activate#(XS)U41#(tt, N) → activate#(N)
U101#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS)))sel#(N, XS) → and#(isNatural(N), n__isLNat(XS))
U51#(tt, N, XS) → afterNth#(activate(N), activate(XS))tail#(cons(N, XS)) → isNatural#(N)
isLNat#(n__take(V1, V2)) → activate#(V2)tail#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS)))
isNatural#(n__sel(V1, V2)) → activate#(V2)snd#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y))
splitAt#(s(N), cons(X, XS)) → isNatural#(X)activate#(n__pair(X1, X2)) → pair#(X1, X2)
head#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS)))activate#(n__0) → 0#
U81#(tt, N, X, XS) → activate#(X)isPLNat#(n__pair(V1, V2)) → and#(isLNat(activate(V1)), n__isLNat(activate(V2)))
tail#(cons(N, XS)) → U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))U82#(pair(YS, ZS), X) → activate#(X)
U81#(tt, N, X, XS) → U82#(splitAt(activate(N), activate(XS)), activate(X))afterNth#(N, XS) → U11#(and(isNatural(N), n__isLNat(XS)), N, XS)
natsFrom#(N) → U41#(isNatural(N), N)tail#(cons(N, XS)) → activate#(XS)
U21#(tt, X) → activate#(X)U61#(tt, Y) → activate#(Y)
isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1))isNatural#(n__sel(V1, V2)) → activate#(V1)
U101#(tt, N, XS) → activate#(XS)U71#(tt, XS) → pair#(nil, activate(XS))
isPLNat#(n__splitAt(V1, V2)) → activate#(V1)U71#(tt, XS) → nil#
isLNat#(n__fst(V1)) → activate#(V1)splitAt#(0, XS) → isLNat#(XS)
isLNat#(n__afterNth(V1, V2)) → activate#(V1)U11#(tt, N, XS) → activate#(N)
activate#(n__cons(X1, X2)) → cons#(X1, X2)isLNat#(n__fst(V1)) → isPLNat#(activate(V1))
activate#(n__natsFrom(X)) → natsFrom#(X)isPLNat#(n__pair(V1, V2)) → activate#(V2)
U31#(tt, N) → activate#(N)activate#(n__fst(X)) → fst#(X)
activate#(n__s(X)) → s#(X)U51#(tt, N, XS) → head#(afterNth(activate(N), activate(XS)))
activate#(n__nil) → nil#splitAt#(0, XS) → U71#(isLNat(XS), XS)
isNatural#(n__head(V1)) → isLNat#(activate(V1))isLNat#(n__cons(V1, V2)) → activate#(V1)
U71#(tt, XS) → activate#(XS)U101#(tt, N, XS) → activate#(N)
U81#(tt, N, X, XS) → activate#(XS)

Rewrite Rules

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__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)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) → nilactivate(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

Original Signature

Termination of terms over the following signature is verified: pair, isNatural, natsFrom, n__snd, n__head, n__sel, n__fst, n__splitAt, fst, activate, n__s, U61, n__0, n__afterNth, n__isLNat, U41, U91, n__nil, head, U21, cons, snd, n__tail, isPLNat, n__take, n__natsFrom, tail, splitAt, U71, and, n__cons, n__and, 0, U51, s, tt, U82, take, U81, isLNat, U11, n__pair, afterNth, U31, sel, nil, U101

Strategy

The following SCCs where found

U11#(tt, N, XS) → splitAt#(activate(N), activate(XS))and#(tt, X) → activate#(X)
U81#(tt, N, X, XS) → splitAt#(activate(N), activate(XS))sel#(N, XS) → isNatural#(N)
isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1))activate#(n__snd(X)) → snd#(X)
afterNth#(N, XS) → isNatural#(N)U11#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS)))
take#(N, XS) → and#(isNatural(N), n__isLNat(XS))fst#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y))
isLNat#(n__cons(V1, V2)) → activate#(V2)isLNat#(n__take(V1, V2)) → isNatural#(activate(V1))
isLNat#(n__take(V1, V2)) → activate#(V1)isNatural#(n__s(V1)) → isNatural#(activate(V1))
take#(N, XS) → U101#(and(isNatural(N), n__isLNat(XS)), N, XS)U51#(tt, N, XS) → activate#(N)
head#(cons(N, XS)) → activate#(XS)snd#(pair(X, Y)) → isLNat#(X)
isLNat#(n__take(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))fst#(pair(X, Y)) → U21#(and(isLNat(X), n__isLNat(Y)), X)
isPLNat#(n__pair(V1, V2)) → activate#(V1)isLNat#(n__tail(V1)) → activate#(V1)
activate#(n__head(X)) → head#(X)U91#(tt, XS) → activate#(XS)
U81#(tt, N, X, XS) → activate#(N)activate#(n__isLNat(X)) → isLNat#(X)
activate#(n__splitAt(X1, X2)) → splitAt#(X1, X2)U101#(tt, N, XS) → splitAt#(activate(N), activate(XS))
activate#(n__tail(X)) → tail#(X)isPLNat#(n__splitAt(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))
head#(cons(N, XS)) → U31#(and(isNatural(N), n__isLNat(activate(XS))), N)U51#(tt, N, XS) → activate#(XS)
isLNat#(n__natsFrom(V1)) → activate#(V1)activate#(n__sel(X1, X2)) → sel#(X1, X2)
afterNth#(N, XS) → and#(isNatural(N), n__isLNat(XS))isNatural#(n__head(V1)) → activate#(V1)
natsFrom#(N) → isNatural#(N)fst#(pair(X, Y)) → isLNat#(X)
sel#(N, XS) → U51#(and(isNatural(N), n__isLNat(XS)), N, XS)isNatural#(n__s(V1)) → activate#(V1)
isLNat#(n__afterNth(V1, V2)) → activate#(V2)isLNat#(n__cons(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))
isLNat#(n__tail(V1)) → isLNat#(activate(V1))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))isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1))
take#(N, XS) → isNatural#(N)head#(cons(N, XS)) → isNatural#(N)
isPLNat#(n__splitAt(V1, V2)) → activate#(V2)isLNat#(n__afterNth(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))
isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1))isNatural#(n__sel(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2)))
activate#(n__afterNth(X1, X2)) → afterNth#(X1, X2)isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1))
U11#(tt, N, XS) → activate#(XS)activate#(n__take(X1, X2)) → take#(X1, X2)
isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1))isLNat#(n__snd(V1)) → isPLNat#(activate(V1))
isLNat#(n__snd(V1)) → activate#(V1)activate#(n__and(X1, X2)) → and#(X1, X2)
snd#(pair(X, Y)) → U61#(and(isLNat(X), n__isLNat(Y)), Y)splitAt#(s(N), cons(X, XS)) → isNatural#(N)
splitAt#(s(N), cons(X, XS)) → activate#(XS)U41#(tt, N) → activate#(N)
U101#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS)))sel#(N, XS) → and#(isNatural(N), n__isLNat(XS))
U51#(tt, N, XS) → afterNth#(activate(N), activate(XS))tail#(cons(N, XS)) → isNatural#(N)
isLNat#(n__take(V1, V2)) → activate#(V2)tail#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS)))
isNatural#(n__sel(V1, V2)) → activate#(V2)snd#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y))
splitAt#(s(N), cons(X, XS)) → isNatural#(X)head#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS)))
U81#(tt, N, X, XS) → activate#(X)isPLNat#(n__pair(V1, V2)) → and#(isLNat(activate(V1)), n__isLNat(activate(V2)))
tail#(cons(N, XS)) → U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))U82#(pair(YS, ZS), X) → activate#(X)
U81#(tt, N, X, XS) → U82#(splitAt(activate(N), activate(XS)), activate(X))afterNth#(N, XS) → U11#(and(isNatural(N), n__isLNat(XS)), N, XS)
tail#(cons(N, XS)) → activate#(XS)natsFrom#(N) → U41#(isNatural(N), N)
U21#(tt, X) → activate#(X)isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1))
U61#(tt, Y) → activate#(Y)isNatural#(n__sel(V1, V2)) → activate#(V1)
U101#(tt, N, XS) → activate#(XS)isPLNat#(n__splitAt(V1, V2)) → activate#(V1)
isLNat#(n__fst(V1)) → activate#(V1)splitAt#(0, XS) → isLNat#(XS)
isLNat#(n__afterNth(V1, V2)) → activate#(V1)U11#(tt, N, XS) → activate#(N)
isLNat#(n__fst(V1)) → isPLNat#(activate(V1))activate#(n__natsFrom(X)) → natsFrom#(X)
isPLNat#(n__pair(V1, V2)) → activate#(V2)U31#(tt, N) → activate#(N)
activate#(n__fst(X)) → fst#(X)U51#(tt, N, XS) → head#(afterNth(activate(N), activate(XS)))
splitAt#(0, XS) → U71#(isLNat(XS), XS)isLNat#(n__cons(V1, V2)) → activate#(V1)
isNatural#(n__head(V1)) → isLNat#(activate(V1))U71#(tt, XS) → activate#(XS)
U101#(tt, N, XS) → activate#(N)U81#(tt, N, X, XS) → activate#(XS)