YES
The TRS could be proven terminating. The proof took 153 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (74ms).
| – Problem 2 was processed with processor SubtermCriterion (6ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| afterNth#(N, XS) | → | splitAt#(N, XS) | | splitAt#(s(N), cons(X, XS)) | → | activate#(XS) |
| activate#(n__natsFrom(X)) | → | natsFrom#(X) | | splitAt#(s(N), cons(X, XS)) | → | u#(splitAt(N, activate(XS)), N, X, activate(XS)) |
| afterNth#(N, XS) | → | snd#(splitAt(N, XS)) | | tail#(cons(N, XS)) | → | activate#(XS) |
| splitAt#(s(N), cons(X, XS)) | → | splitAt#(N, activate(XS)) | | sel#(N, XS) | → | afterNth#(N, XS) |
| sel#(N, XS) | → | head#(afterNth(N, XS)) | | take#(N, XS) | → | splitAt#(N, XS) |
| u#(pair(YS, ZS), N, X, XS) | → | activate#(X) | | take#(N, XS) | → | fst#(splitAt(N, XS)) |
Rewrite Rules
| natsFrom(N) | → | cons(N, n__natsFrom(s(N))) | | fst(pair(XS, YS)) | → | XS |
| snd(pair(XS, YS)) | → | YS | | splitAt(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)) | → | N | | tail(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) |
| activate(n__natsFrom(X)) | → | natsFrom(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, tail, n__natsFrom, splitAt, 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)) |
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(s(N))) | | fst(pair(XS, YS)) | → | XS |
| snd(pair(XS, YS)) | → | YS | | splitAt(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)) | → | N | | tail(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) |
| activate(n__natsFrom(X)) | → | natsFrom(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, tail, n__natsFrom, splitAt, 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)) |