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)) | → | X | | head(cons(N, XS)) | → | N |
| natsFrom(N) | → | cons(N, n__natsFrom(n__s(N))) | | sel(N, XS) | → | head(afterNth(N, XS)) |
| snd(pair(X, Y)) | → | Y | | splitAt(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)) | → | X | | head(cons(N, XS)) | → | N |
| natsFrom(N) | → | cons(N, n__natsFrom(n__s(N))) | | sel(N, XS) | → | head(afterNth(N, XS)) |
| snd(pair(X, Y)) | → | Y | | splitAt(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
- 0: 0
- U11(x1,x2,x3,x4): 0
- U11#(x1,x2,x3,x4): 2x2 + 1
- U12(x,y): 0
- activate(x): 2x
- afterNth(x,y): 0
- and(x,y): 0
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- n__natsFrom(x): 1
- n__s(x): 3x + 1
- natsFrom(x): 1
- nil: 0
- pair(x,y): 0
- s(x): 3x + 1
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- splitAt#(x,y): x + 1
- tail(x): 0
- take(x,y): 0
- tt: 0
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)) | → | X | | head(cons(N, XS)) | → | N |
| natsFrom(N) | → | cons(N, n__natsFrom(n__s(N))) | | sel(N, XS) | → | head(afterNth(N, XS)) |
| snd(pair(X, Y)) | → | Y | | splitAt(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)) | → | X | | head(cons(N, XS)) | → | N |
| natsFrom(N) | → | cons(N, n__natsFrom(n__s(N))) | | sel(N, XS) | → | head(afterNth(N, XS)) |
| snd(pair(X, Y)) | → | Y | | splitAt(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) |