YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (114ms).
 | – Problem 2 was processed with processor SubtermCriterion (0ms).
 | – Problem 3 was processed with processor SubtermCriterion (3ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

natsFrom(N)cons(N, n__natsFrom(n__s(N)))fst(pair(XS, YS))XS
snd(pair(XS, YS))YSsplitAt(0, XS)pair(nil, XS)
splitAt(s(N), cons(X, XS))u(splitAt(N, activate(XS)), N, X, activate(XS))u(pair(YS, ZS), N, X, XS)pair(cons(activate(X), YS), ZS)
head(cons(N, XS))Ntail(cons(N, XS))activate(XS)
sel(N, XS)head(afterNth(N, XS))take(N, XS)fst(splitAt(N, XS))
afterNth(N, XS)snd(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, n__s, fst, activate, u, 0, s, take, afterNth, head, sel, nil, snd, cons

Strategy


The following SCCs where found

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

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

natsFrom(N)cons(N, n__natsFrom(n__s(N)))fst(pair(XS, YS))XS
snd(pair(XS, YS))YSsplitAt(0, XS)pair(nil, XS)
splitAt(s(N), cons(X, XS))u(splitAt(N, activate(XS)), N, X, activate(XS))u(pair(YS, ZS), N, X, XS)pair(cons(activate(X), YS), ZS)
head(cons(N, XS))Ntail(cons(N, XS))activate(XS)
sel(N, XS)head(afterNth(N, XS))take(N, XS)fst(splitAt(N, XS))
afterNth(N, XS)snd(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, n__s, fst, activate, u, 0, s, take, afterNth, head, sel, nil, snd, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

natsFrom(N)cons(N, n__natsFrom(n__s(N)))fst(pair(XS, YS))XS
snd(pair(XS, YS))YSsplitAt(0, XS)pair(nil, XS)
splitAt(s(N), cons(X, XS))u(splitAt(N, activate(XS)), N, X, activate(XS))u(pair(YS, ZS), N, X, XS)pair(cons(activate(X), YS), ZS)
head(cons(N, XS))Ntail(cons(N, XS))activate(XS)
sel(N, XS)head(afterNth(N, XS))take(N, XS)fst(splitAt(N, XS))
afterNth(N, XS)snd(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, n__s, fst, activate, u, 0, s, take, afterNth, head, sel, nil, snd, cons

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)