YES

The TRS could be proven terminating. The proof took 740 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (187ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (352ms).
 |    | – Problem 4 was processed with processor DependencyGraph (2ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

and#(tt, X)activate#(X)splitAt#(s(N), cons(X, XS))activate#(XS)
activate#(n__natsFrom(X))activate#(X)activate#(n__natsFrom(X))natsFrom#(activate(X))
afterNth#(N, XS)snd#(splitAt(N, XS))activate#(n__s(X))activate#(X)
tail#(cons(N, XS))activate#(XS)U11#(tt, N, X, XS)U12#(splitAt(activate(N), activate(XS)), activate(X))
sel#(N, XS)afterNth#(N, XS)U11#(tt, N, X, XS)activate#(N)
take#(N, XS)splitAt#(N, XS)sel#(N, XS)head#(afterNth(N, XS))
take#(N, XS)fst#(splitAt(N, XS))afterNth#(N, XS)splitAt#(N, XS)
U12#(pair(YS, ZS), X)activate#(X)U11#(tt, N, X, XS)activate#(X)
splitAt#(s(N), cons(X, XS))U11#(tt, N, X, activate(XS))U11#(tt, N, X, XS)splitAt#(activate(N), activate(XS))
U11#(tt, N, X, XS)activate#(XS)activate#(n__s(X))s#(activate(X))

Rewrite Rules

U11(tt, N, X, XS)U12(splitAt(activate(N), activate(XS)), activate(X))U12(pair(YS, ZS), X)pair(cons(activate(X), YS), ZS)
afterNth(N, XS)snd(splitAt(N, XS))and(tt, X)activate(X)
fst(pair(X, Y))Xhead(cons(N, XS))N
natsFrom(N)cons(N, n__natsFrom(n__s(N)))sel(N, XS)head(afterNth(N, XS))
snd(pair(X, Y))YsplitAt(0, XS)pair(nil, XS)
splitAt(s(N), cons(X, XS))U11(tt, N, X, activate(XS))tail(cons(N, XS))activate(XS)
take(N, XS)fst(splitAt(N, XS))natsFrom(X)n__natsFrom(X)
s(X)n__s(X)activate(n__natsFrom(X))natsFrom(activate(X))
activate(n__s(X))s(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, tail, n__natsFrom, splitAt, and, activate, fst, n__s, 0, s, tt, take, U11, U12, afterNth, head, sel, snd, cons, nil

Strategy


The following SCCs where found

splitAt#(s(N), cons(X, XS)) → U11#(tt, N, X, activate(XS))U11#(tt, N, X, XS) → splitAt#(activate(N), activate(XS))

activate#(n__natsFrom(X)) → activate#(X)activate#(n__s(X)) → activate#(X)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

splitAt#(s(N), cons(X, XS))U11#(tt, N, X, activate(XS))U11#(tt, N, X, XS)splitAt#(activate(N), activate(XS))

Rewrite Rules

U11(tt, N, X, XS)U12(splitAt(activate(N), activate(XS)), activate(X))U12(pair(YS, ZS), X)pair(cons(activate(X), YS), ZS)
afterNth(N, XS)snd(splitAt(N, XS))and(tt, X)activate(X)
fst(pair(X, Y))Xhead(cons(N, XS))N
natsFrom(N)cons(N, n__natsFrom(n__s(N)))sel(N, XS)head(afterNth(N, XS))
snd(pair(X, Y))YsplitAt(0, XS)pair(nil, XS)
splitAt(s(N), cons(X, XS))U11(tt, N, X, activate(XS))tail(cons(N, XS))activate(XS)
take(N, XS)fst(splitAt(N, XS))natsFrom(X)n__natsFrom(X)
s(X)n__s(X)activate(n__natsFrom(X))natsFrom(activate(X))
activate(n__s(X))s(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, tail, n__natsFrom, splitAt, and, activate, fst, n__s, 0, s, tt, take, U11, U12, afterNth, head, sel, snd, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

s(X)n__s(X)activate(X)X
activate(n__natsFrom(X))natsFrom(activate(X))natsFrom(X)n__natsFrom(X)
activate(n__s(X))s(activate(X))natsFrom(N)cons(N, n__natsFrom(n__s(N)))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

splitAt#(s(N), cons(X, XS))U11#(tt, N, X, activate(XS))

Problem 4: DependencyGraph



Dependency Pair Problem

Dependency Pairs

U11#(tt, N, X, XS)splitAt#(activate(N), activate(XS))

Rewrite Rules

U11(tt, N, X, XS)U12(splitAt(activate(N), activate(XS)), activate(X))U12(pair(YS, ZS), X)pair(cons(activate(X), YS), ZS)
afterNth(N, XS)snd(splitAt(N, XS))and(tt, X)activate(X)
fst(pair(X, Y))Xhead(cons(N, XS))N
natsFrom(N)cons(N, n__natsFrom(n__s(N)))sel(N, XS)head(afterNth(N, XS))
snd(pair(X, Y))YsplitAt(0, XS)pair(nil, XS)
splitAt(s(N), cons(X, XS))U11(tt, N, X, activate(XS))tail(cons(N, XS))activate(XS)
take(N, XS)fst(splitAt(N, XS))natsFrom(X)n__natsFrom(X)
s(X)n__s(X)activate(n__natsFrom(X))natsFrom(activate(X))
activate(n__s(X))s(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, tail, n__natsFrom, splitAt, and, activate, fst, n__s, 0, s, tt, take, U11, U12, afterNth, head, sel, nil, cons, snd

Strategy


There are no SCCs!

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

activate#(n__natsFrom(X))activate#(X)activate#(n__s(X))activate#(X)

Rewrite Rules

U11(tt, N, X, XS)U12(splitAt(activate(N), activate(XS)), activate(X))U12(pair(YS, ZS), X)pair(cons(activate(X), YS), ZS)
afterNth(N, XS)snd(splitAt(N, XS))and(tt, X)activate(X)
fst(pair(X, Y))Xhead(cons(N, XS))N
natsFrom(N)cons(N, n__natsFrom(n__s(N)))sel(N, XS)head(afterNth(N, XS))
snd(pair(X, Y))YsplitAt(0, XS)pair(nil, XS)
splitAt(s(N), cons(X, XS))U11(tt, N, X, activate(XS))tail(cons(N, XS))activate(XS)
take(N, XS)fst(splitAt(N, XS))natsFrom(X)n__natsFrom(X)
s(X)n__s(X)activate(n__natsFrom(X))natsFrom(activate(X))
activate(n__s(X))s(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, tail, n__natsFrom, splitAt, and, activate, fst, n__s, 0, s, tt, take, U11, U12, afterNth, head, sel, snd, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

activate#(n__natsFrom(X))activate#(X)activate#(n__s(X))activate#(X)