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)) | → | 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) |
| 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)) | → | 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) |
| 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)) | → | 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) |
| 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) |