TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (16268ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| | – Problem 16 was processed with processor PolynomialLinearRange4iUR (42ms).
| | | – Problem 24 was processed with processor PolynomialLinearRange4iUR (16ms).
| – Problem 3 was processed with processor SubtermCriterion (4ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| | – Problem 17 was processed with processor PolynomialLinearRange4iUR (126ms).
| | | – Problem 23 was processed with processor PolynomialLinearRange4iUR (76ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (2ms).
| – Problem 8 was processed with processor SubtermCriterion (3ms).
| | – Problem 18 was processed with processor PolynomialLinearRange4iUR (69ms).
| | | – Problem 26 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (5ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (5ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (8ms), DependencyGraph (3ms)].
| – Problem 9 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (2746ms), PolynomialLinearRange4iUR (1283ms), DependencyGraph (2749ms), PolynomialLinearRange4iUR (1428ms), DependencyGraph (2762ms), PolynomialLinearRange4iUR (2000ms), DependencyGraph (2857ms), PolynomialLinearRange4iUR (2512ms), DependencyGraph (2841ms), PolynomialLinearRange8NegiUR (7500ms), DependencyGraph (2915ms), ReductionPairSAT (timeout)].
| – Problem 10 was processed with processor SubtermCriterion (1ms).
| | – Problem 19 was processed with processor PolynomialLinearRange4iUR (51ms).
| | | – Problem 25 was processed with processor PolynomialLinearRange4iUR (29ms).
| – Problem 11 was processed with processor SubtermCriterion (2ms).
| – Problem 12 was processed with processor SubtermCriterion (3ms).
| | – Problem 20 was processed with processor PolynomialLinearRange4iUR (77ms).
| – Problem 13 was processed with processor SubtermCriterion (2ms).
| | – Problem 21 was processed with processor PolynomialLinearRange4iUR (28ms).
| | | – Problem 27 remains open; application of the following processors failed [DependencyGraph (2ms), PolynomialLinearRange4iUR (4ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (21ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (9ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (16ms), DependencyGraph (3ms)].
| – Problem 14 was processed with processor SubtermCriterion (1ms).
| – Problem 15 was processed with processor SubtermCriterion (2ms).
| | – Problem 22 was processed with processor PolynomialLinearRange4iUR (57ms).
| | | – Problem 28 remains open; application of the following processors failed [DependencyGraph (24ms), PolynomialLinearRange4iUR (3ms), DependencyGraph (26ms), PolynomialLinearRange4iUR (6ms), DependencyGraph (23ms), PolynomialLinearRange4iUR (10ms), DependencyGraph (26ms), PolynomialLinearRange8NegiUR (6ms), DependencyGraph (24ms)].
The following open problems remain:
Open Dependency Pair Problem 9
Dependency Pairs
| active#(take(N, XS)) | → | mark#(fst(splitAt(N, XS))) | | mark#(fst(X)) | → | active#(fst(mark(X))) |
| mark#(head(X)) | → | active#(head(mark(X))) | | mark#(cons(X1, X2)) | → | active#(cons(mark(X1), X2)) |
| mark#(take(X1, X2)) | → | mark#(X1) | | active#(u(pair(YS, ZS), N, X, XS)) | → | mark#(pair(cons(X, YS), ZS)) |
| active#(splitAt(0, XS)) | → | mark#(pair(nil, XS)) | | mark#(pair(X1, X2)) | → | mark#(X2) |
| mark#(u(X1, X2, X3, X4)) | → | active#(u(mark(X1), X2, X3, X4)) | | mark#(take(X1, X2)) | → | active#(take(mark(X1), mark(X2))) |
| active#(head(cons(N, XS))) | → | mark#(N) | | mark#(tail(X)) | → | active#(tail(mark(X))) |
| mark#(head(X)) | → | mark#(X) | | mark#(nil) | → | active#(nil) |
| mark#(splitAt(X1, X2)) | → | mark#(X1) | | active#(natsFrom(N)) | → | mark#(cons(N, natsFrom(s(N)))) |
| active#(tail(cons(N, XS))) | → | mark#(XS) | | mark#(snd(X)) | → | active#(snd(mark(X))) |
| mark#(sel(X1, X2)) | → | mark#(X2) | | mark#(s(X)) | → | mark#(X) |
| mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | | mark#(sel(X1, X2)) | → | mark#(X1) |
| mark#(fst(X)) | → | mark#(X) | | active#(afterNth(N, XS)) | → | mark#(snd(splitAt(N, XS))) |
| mark#(0) | → | active#(0) | | mark#(s(X)) | → | active#(s(mark(X))) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(splitAt(X1, X2)) | → | mark#(X2) |
| mark#(snd(X)) | → | mark#(X) | | mark#(afterNth(X1, X2)) | → | mark#(X1) |
| mark#(natsFrom(X)) | → | mark#(X) | | mark#(splitAt(X1, X2)) | → | active#(splitAt(mark(X1), mark(X2))) |
| mark#(sel(X1, X2)) | → | active#(sel(mark(X1), mark(X2))) | | mark#(afterNth(X1, X2)) | → | active#(afterNth(mark(X1), mark(X2))) |
| mark#(pair(X1, X2)) | → | mark#(X1) | | active#(splitAt(s(N), cons(X, XS))) | → | mark#(u(splitAt(N, XS), N, X, XS)) |
| mark#(tail(X)) | → | mark#(X) | | mark#(u(X1, X2, X3, X4)) | → | mark#(X1) |
| active#(sel(N, XS)) | → | mark#(head(afterNth(N, XS))) | | mark#(take(X1, X2)) | → | mark#(X2) |
| active#(snd(pair(XS, YS))) | → | mark#(YS) | | active#(fst(pair(XS, YS))) | → | mark#(XS) |
| mark#(afterNth(X1, X2)) | → | mark#(X2) | | mark#(pair(X1, X2)) | → | active#(pair(mark(X1), mark(X2))) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Open Dependency Pair Problem 27
Dependency Pairs
| sel#(X1, mark(X2)) | → | sel#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Open Dependency Pair Problem 26
Dependency Pairs
| pair#(X1, mark(X2)) | → | pair#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Open Dependency Pair Problem 28
Dependency Pairs
| u#(X1, mark(X2), X3, X4) | → | u#(X1, X2, X3, X4) | | u#(X1, X2, active(X3), X4) | → | u#(X1, X2, X3, X4) |
| u#(X1, X2, X3, active(X4)) | → | u#(X1, X2, X3, X4) | | u#(X1, active(X2), X3, X4) | → | u#(X1, X2, X3, X4) |
| u#(X1, X2, mark(X3), X4) | → | u#(X1, X2, X3, X4) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(fst(X)) | → | active#(fst(mark(X))) | | active#(u(pair(YS, ZS), N, X, XS)) | → | mark#(pair(cons(X, YS), ZS)) |
| active#(take(N, XS)) | → | splitAt#(N, XS) | | mark#(pair(X1, X2)) | → | mark#(X2) |
| mark#(take(X1, X2)) | → | active#(take(mark(X1), mark(X2))) | | u#(X1, X2, X3, active(X4)) | → | u#(X1, X2, X3, X4) |
| splitAt#(mark(X1), X2) | → | splitAt#(X1, X2) | | active#(afterNth(N, XS)) | → | snd#(splitAt(N, XS)) |
| mark#(snd(X)) | → | active#(snd(mark(X))) | | active#(splitAt(0, XS)) | → | pair#(nil, XS) |
| mark#(s(X)) | → | mark#(X) | | mark#(sel(X1, X2)) | → | mark#(X1) |
| afterNth#(active(X1), X2) | → | afterNth#(X1, X2) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| pair#(X1, mark(X2)) | → | pair#(X1, X2) | | splitAt#(X1, mark(X2)) | → | splitAt#(X1, X2) |
| mark#(afterNth(X1, X2)) | → | mark#(X1) | | fst#(active(X)) | → | fst#(X) |
| sel#(X1, mark(X2)) | → | sel#(X1, X2) | | active#(sel(N, XS)) | → | head#(afterNth(N, XS)) |
| u#(active(X1), X2, X3, X4) | → | u#(X1, X2, X3, X4) | | mark#(pair(X1, X2)) | → | mark#(X1) |
| sel#(X1, active(X2)) | → | sel#(X1, X2) | | mark#(tail(X)) | → | mark#(X) |
| active#(u(pair(YS, ZS), N, X, XS)) | → | cons#(X, YS) | | head#(active(X)) | → | head#(X) |
| mark#(afterNth(X1, X2)) | → | mark#(X2) | | active#(take(N, XS)) | → | mark#(fst(splitAt(N, XS))) |
| pair#(mark(X1), X2) | → | pair#(X1, X2) | | active#(afterNth(N, XS)) | → | splitAt#(N, XS) |
| natsFrom#(mark(X)) | → | natsFrom#(X) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| active#(splitAt(0, XS)) | → | mark#(pair(nil, XS)) | | mark#(tail(X)) | → | tail#(mark(X)) |
| mark#(splitAt(X1, X2)) | → | splitAt#(mark(X1), mark(X2)) | | mark#(u(X1, X2, X3, X4)) | → | u#(mark(X1), X2, X3, X4) |
| mark#(head(X)) | → | mark#(X) | | mark#(splitAt(X1, X2)) | → | mark#(X1) |
| u#(X1, X2, active(X3), X4) | → | u#(X1, X2, X3, X4) | | splitAt#(X1, active(X2)) | → | splitAt#(X1, X2) |
| cons#(X1, mark(X2)) | → | cons#(X1, X2) | | mark#(fst(X)) | → | mark#(X) |
| active#(afterNth(N, XS)) | → | mark#(snd(splitAt(N, XS))) | | mark#(0) | → | active#(0) |
| mark#(s(X)) | → | active#(s(mark(X))) | | snd#(mark(X)) | → | snd#(X) |
| head#(mark(X)) | → | head#(X) | | pair#(X1, active(X2)) | → | pair#(X1, X2) |
| mark#(snd(X)) | → | mark#(X) | | mark#(natsFrom(X)) | → | mark#(X) |
| cons#(active(X1), X2) | → | cons#(X1, X2) | | mark#(afterNth(X1, X2)) | → | active#(afterNth(mark(X1), mark(X2))) |
| snd#(active(X)) | → | snd#(X) | | u#(mark(X1), X2, X3, X4) | → | u#(X1, X2, X3, X4) |
| active#(natsFrom(N)) | → | natsFrom#(s(N)) | | mark#(cons(X1, X2)) | → | active#(cons(mark(X1), X2)) |
| mark#(fst(X)) | → | fst#(mark(X)) | | mark#(take(X1, X2)) | → | mark#(X1) |
| active#(splitAt(s(N), cons(X, XS))) | → | u#(splitAt(N, XS), N, X, XS) | | mark#(snd(X)) | → | snd#(mark(X)) |
| afterNth#(X1, mark(X2)) | → | afterNth#(X1, X2) | | mark#(u(X1, X2, X3, X4)) | → | active#(u(mark(X1), X2, X3, X4)) |
| mark#(s(X)) | → | s#(mark(X)) | | mark#(tail(X)) | → | active#(tail(mark(X))) |
| active#(sel(N, XS)) | → | afterNth#(N, XS) | | active#(natsFrom(N)) | → | mark#(cons(N, natsFrom(s(N)))) |
| active#(tail(cons(N, XS))) | → | mark#(XS) | | afterNth#(mark(X1), X2) | → | afterNth#(X1, X2) |
| mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | | pair#(active(X1), X2) | → | pair#(X1, X2) |
| mark#(sel(X1, X2)) | → | sel#(mark(X1), mark(X2)) | | tail#(mark(X)) | → | tail#(X) |
| take#(X1, mark(X2)) | → | take#(X1, X2) | | mark#(splitAt(X1, X2)) | → | active#(splitAt(mark(X1), mark(X2))) |
| mark#(sel(X1, X2)) | → | active#(sel(mark(X1), mark(X2))) | | sel#(active(X1), X2) | → | sel#(X1, X2) |
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | mark#(u(X1, X2, X3, X4)) | → | mark#(X1) |
| active#(snd(pair(XS, YS))) | → | mark#(YS) | | mark#(afterNth(X1, X2)) | → | afterNth#(mark(X1), mark(X2)) |
| active#(splitAt(s(N), cons(X, XS))) | → | splitAt#(N, XS) | | sel#(mark(X1), X2) | → | sel#(X1, X2) |
| active#(u(pair(YS, ZS), N, X, XS)) | → | pair#(cons(X, YS), ZS) | | mark#(head(X)) | → | active#(head(mark(X))) |
| take#(mark(X1), X2) | → | take#(X1, X2) | | active#(natsFrom(N)) | → | s#(N) |
| mark#(pair(X1, X2)) | → | pair#(mark(X1), mark(X2)) | | u#(X1, X2, X3, mark(X4)) | → | u#(X1, X2, X3, X4) |
| u#(X1, active(X2), X3, X4) | → | u#(X1, X2, X3, X4) | | splitAt#(active(X1), X2) | → | splitAt#(X1, X2) |
| u#(X1, X2, mark(X3), X4) | → | u#(X1, X2, X3, X4) | | active#(head(cons(N, XS))) | → | mark#(N) |
| mark#(nil) | → | active#(nil) | | take#(X1, active(X2)) | → | take#(X1, X2) |
| tail#(active(X)) | → | tail#(X) | | mark#(sel(X1, X2)) | → | mark#(X2) |
| fst#(mark(X)) | → | fst#(X) | | active#(take(N, XS)) | → | fst#(splitAt(N, XS)) |
| afterNth#(X1, active(X2)) | → | afterNth#(X1, X2) | | mark#(cons(X1, X2)) | → | cons#(mark(X1), X2) |
| natsFrom#(active(X)) | → | natsFrom#(X) | | u#(X1, mark(X2), X3, X4) | → | u#(X1, X2, X3, X4) |
| mark#(splitAt(X1, X2)) | → | mark#(X2) | | mark#(head(X)) | → | head#(mark(X)) |
| mark#(take(X1, X2)) | → | take#(mark(X1), mark(X2)) | | s#(mark(X)) | → | s#(X) |
| active#(splitAt(s(N), cons(X, XS))) | → | mark#(u(splitAt(N, XS), N, X, XS)) | | mark#(take(X1, X2)) | → | mark#(X2) |
| active#(sel(N, XS)) | → | mark#(head(afterNth(N, XS))) | | s#(active(X)) | → | s#(X) |
| active#(natsFrom(N)) | → | cons#(N, natsFrom(s(N))) | | active#(fst(pair(XS, YS))) | → | mark#(XS) |
| mark#(natsFrom(X)) | → | natsFrom#(mark(X)) | | mark#(pair(X1, X2)) | → | active#(pair(mark(X1), mark(X2))) |
| take#(active(X1), X2) | → | take#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
The following SCCs where found
| active#(take(N, XS)) → mark#(fst(splitAt(N, XS))) | mark#(cons(X1, X2)) → active#(cons(mark(X1), X2)) |
| mark#(head(X)) → active#(head(mark(X))) | mark#(fst(X)) → active#(fst(mark(X))) |
| mark#(take(X1, X2)) → mark#(X1) | active#(u(pair(YS, ZS), N, X, XS)) → mark#(pair(cons(X, YS), ZS)) |
| active#(splitAt(0, XS)) → mark#(pair(nil, XS)) | mark#(pair(X1, X2)) → mark#(X2) |
| mark#(u(X1, X2, X3, X4)) → active#(u(mark(X1), X2, X3, X4)) | mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2))) |
| active#(head(cons(N, XS))) → mark#(N) | mark#(tail(X)) → active#(tail(mark(X))) |
| mark#(nil) → active#(nil) | mark#(head(X)) → mark#(X) |
| active#(natsFrom(N)) → mark#(cons(N, natsFrom(s(N)))) | mark#(splitAt(X1, X2)) → mark#(X1) |
| active#(tail(cons(N, XS))) → mark#(XS) | mark#(snd(X)) → active#(snd(mark(X))) |
| mark#(sel(X1, X2)) → mark#(X2) | mark#(s(X)) → mark#(X) |
| mark#(sel(X1, X2)) → mark#(X1) | mark#(natsFrom(X)) → active#(natsFrom(mark(X))) |
| mark#(fst(X)) → mark#(X) | active#(afterNth(N, XS)) → mark#(snd(splitAt(N, XS))) |
| mark#(0) → active#(0) | mark#(s(X)) → active#(s(mark(X))) |
| mark#(cons(X1, X2)) → mark#(X1) | mark#(snd(X)) → mark#(X) |
| mark#(splitAt(X1, X2)) → mark#(X2) | mark#(natsFrom(X)) → mark#(X) |
| mark#(afterNth(X1, X2)) → mark#(X1) | mark#(sel(X1, X2)) → active#(sel(mark(X1), mark(X2))) |
| mark#(splitAt(X1, X2)) → active#(splitAt(mark(X1), mark(X2))) | mark#(afterNth(X1, X2)) → active#(afterNth(mark(X1), mark(X2))) |
| mark#(pair(X1, X2)) → mark#(X1) | active#(splitAt(s(N), cons(X, XS))) → mark#(u(splitAt(N, XS), N, X, XS)) |
| mark#(tail(X)) → mark#(X) | mark#(u(X1, X2, X3, X4)) → mark#(X1) |
| mark#(take(X1, X2)) → mark#(X2) | active#(sel(N, XS)) → mark#(head(afterNth(N, XS))) |
| active#(snd(pair(XS, YS))) → mark#(YS) | mark#(afterNth(X1, X2)) → mark#(X2) |
| active#(fst(pair(XS, YS))) → mark#(XS) | mark#(pair(X1, X2)) → active#(pair(mark(X1), mark(X2))) |
| u#(mark(X1), X2, X3, X4) → u#(X1, X2, X3, X4) | u#(active(X1), X2, X3, X4) → u#(X1, X2, X3, X4) |
| u#(X1, mark(X2), X3, X4) → u#(X1, X2, X3, X4) | u#(X1, X2, active(X3), X4) → u#(X1, X2, X3, X4) |
| u#(X1, X2, X3, mark(X4)) → u#(X1, X2, X3, X4) | u#(X1, active(X2), X3, X4) → u#(X1, X2, X3, X4) |
| u#(X1, X2, X3, active(X4)) → u#(X1, X2, X3, X4) | u#(X1, X2, mark(X3), X4) → u#(X1, X2, X3, X4) |
| cons#(X1, active(X2)) → cons#(X1, X2) | cons#(mark(X1), X2) → cons#(X1, X2) |
| cons#(active(X1), X2) → cons#(X1, X2) | cons#(X1, mark(X2)) → cons#(X1, X2) |
| sel#(active(X1), X2) → sel#(X1, X2) | sel#(mark(X1), X2) → sel#(X1, X2) |
| sel#(X1, active(X2)) → sel#(X1, X2) | sel#(X1, mark(X2)) → sel#(X1, X2) |
| pair#(mark(X1), X2) → pair#(X1, X2) | pair#(X1, active(X2)) → pair#(X1, X2) |
| pair#(X1, mark(X2)) → pair#(X1, X2) | pair#(active(X1), X2) → pair#(X1, X2) |
| afterNth#(active(X1), X2) → afterNth#(X1, X2) | afterNth#(X1, mark(X2)) → afterNth#(X1, X2) |
| afterNth#(X1, active(X2)) → afterNth#(X1, X2) | afterNth#(mark(X1), X2) → afterNth#(X1, X2) |
| fst#(mark(X)) → fst#(X) | fst#(active(X)) → fst#(X) |
| natsFrom#(mark(X)) → natsFrom#(X) | natsFrom#(active(X)) → natsFrom#(X) |
| tail#(active(X)) → tail#(X) | tail#(mark(X)) → tail#(X) |
| snd#(active(X)) → snd#(X) | snd#(mark(X)) → snd#(X) |
| s#(mark(X)) → s#(X) | s#(active(X)) → s#(X) |
| take#(mark(X1), X2) → take#(X1, X2) | take#(X1, active(X2)) → take#(X1, X2) |
| take#(X1, mark(X2)) → take#(X1, X2) | take#(active(X1), X2) → take#(X1, X2) |
| splitAt#(X1, mark(X2)) → splitAt#(X1, X2) | splitAt#(X1, active(X2)) → splitAt#(X1, X2) |
| splitAt#(active(X1), X2) → splitAt#(X1, X2) | splitAt#(mark(X1), X2) → splitAt#(X1, X2) |
| head#(mark(X)) → head#(X) | head#(active(X)) → head#(X) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| afterNth#(active(X1), X2) | → | afterNth#(X1, X2) | | afterNth#(X1, mark(X2)) | → | afterNth#(X1, X2) |
| afterNth#(X1, active(X2)) | → | afterNth#(X1, X2) | | afterNth#(mark(X1), X2) | → | afterNth#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| afterNth#(active(X1), X2) | → | afterNth#(X1, X2) | | afterNth#(mark(X1), X2) | → | afterNth#(X1, X2) |
Problem 16: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| afterNth#(X1, mark(X2)) | → | afterNth#(X1, X2) | | afterNth#(X1, active(X2)) | → | afterNth#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x + 1
- afterNth(x,y): 0
- afterNth#(x,y): 2y
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- mark(x): 2x
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): 0
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- u(x1,x2,x3,x4): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| afterNth#(X1, active(X2)) | → | afterNth#(X1, X2) |
Problem 24: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| afterNth#(X1, mark(X2)) | → | afterNth#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 0
- afterNth(x,y): 0
- afterNth#(x,y): y + x + 1
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- mark(x): x + 2
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): 0
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- u(x1,x2,x3,x4): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| afterNth#(X1, mark(X2)) | → | afterNth#(X1, X2) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| tail#(active(X)) | → | tail#(X) | | tail#(mark(X)) | → | tail#(X) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| tail#(active(X)) | → | tail#(X) | | tail#(mark(X)) | → | tail#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| take#(mark(X1), X2) | → | take#(X1, X2) | | take#(X1, active(X2)) | → | take#(X1, X2) |
| take#(X1, mark(X2)) | → | take#(X1, X2) | | take#(active(X1), X2) | → | take#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| take#(mark(X1), X2) | → | take#(X1, X2) | | take#(active(X1), X2) | → | take#(X1, X2) |
Problem 17: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| take#(X1, active(X2)) | → | take#(X1, X2) | | take#(X1, mark(X2)) | → | take#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 2x + 2
- afterNth(x,y): 0
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- mark(x): 2x
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): 0
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- take#(x,y): y
- u(x1,x2,x3,x4): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| take#(X1, active(X2)) | → | take#(X1, X2) |
Problem 23: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| take#(X1, mark(X2)) | → | take#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 0
- afterNth(x,y): 0
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- mark(x): x + 2
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): 0
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- take#(x,y): y + 3x + 1
- u(x1,x2,x3,x4): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| take#(X1, mark(X2)) | → | take#(X1, X2) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| natsFrom#(mark(X)) | → | natsFrom#(X) | | natsFrom#(active(X)) | → | natsFrom#(X) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| natsFrom#(mark(X)) | → | natsFrom#(X) | | natsFrom#(active(X)) | → | natsFrom#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| head#(mark(X)) | → | head#(X) | | head#(active(X)) | → | head#(X) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| head#(mark(X)) | → | head#(X) | | head#(active(X)) | → | head#(X) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| pair#(mark(X1), X2) | → | pair#(X1, X2) | | pair#(X1, active(X2)) | → | pair#(X1, X2) |
| pair#(X1, mark(X2)) | → | pair#(X1, X2) | | pair#(active(X1), X2) | → | pair#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| pair#(mark(X1), X2) | → | pair#(X1, X2) | | pair#(active(X1), X2) | → | pair#(X1, X2) |
Problem 18: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| pair#(X1, mark(X2)) | → | pair#(X1, X2) | | pair#(X1, active(X2)) | → | pair#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 2x + 2
- afterNth(x,y): 0
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- mark(x): 2x
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- pair#(x,y): y
- s(x): 0
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- u(x1,x2,x3,x4): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| pair#(X1, active(X2)) | → | pair#(X1, X2) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| splitAt#(X1, mark(X2)) | → | splitAt#(X1, X2) | | splitAt#(X1, active(X2)) | → | splitAt#(X1, X2) |
| splitAt#(active(X1), X2) | → | splitAt#(X1, X2) | | splitAt#(mark(X1), X2) | → | splitAt#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| splitAt#(active(X1), X2) | → | splitAt#(X1, X2) | | splitAt#(mark(X1), X2) | → | splitAt#(X1, X2) |
Problem 19: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| splitAt#(X1, mark(X2)) | → | splitAt#(X1, X2) | | splitAt#(X1, active(X2)) | → | splitAt#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 2x
- afterNth(x,y): 0
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- mark(x): 2x + 2
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): 0
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- splitAt#(x,y): y
- tail(x): 0
- take(x,y): 0
- u(x1,x2,x3,x4): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| splitAt#(X1, mark(X2)) | → | splitAt#(X1, X2) |
Problem 25: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| splitAt#(X1, active(X2)) | → | splitAt#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 2x + 1
- afterNth(x,y): 0
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- mark(x): 0
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): 0
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- splitAt#(x,y): 2y + x
- tail(x): 0
- take(x,y): 0
- u(x1,x2,x3,x4): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| splitAt#(X1, active(X2)) | → | splitAt#(X1, X2) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| fst#(mark(X)) | → | fst#(X) | | fst#(active(X)) | → | fst#(X) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| fst#(mark(X)) | → | fst#(X) | | fst#(active(X)) | → | fst#(X) |
Problem 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| cons#(active(X1), X2) | → | cons#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(active(X1), X2) | → | cons#(X1, X2) |
Problem 20: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x + 1
- afterNth(x,y): 0
- cons(x,y): 0
- cons#(x,y): y + 1
- fst(x): 0
- head(x): 0
- mark(x): 2x + 2
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): 0
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- u(x1,x2,x3,x4): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Problem 13: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sel#(active(X1), X2) | → | sel#(X1, X2) | | sel#(mark(X1), X2) | → | sel#(X1, X2) |
| sel#(X1, active(X2)) | → | sel#(X1, X2) | | sel#(X1, mark(X2)) | → | sel#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sel#(mark(X1), X2) | → | sel#(X1, X2) | | sel#(active(X1), X2) | → | sel#(X1, X2) |
Problem 21: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sel#(X1, active(X2)) | → | sel#(X1, X2) | | sel#(X1, mark(X2)) | → | sel#(X1, X2) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 2x + 1
- afterNth(x,y): 0
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- mark(x): x
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): 0
- sel(x,y): 0
- sel#(x,y): 2y + x
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- u(x1,x2,x3,x4): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| sel#(X1, active(X2)) | → | sel#(X1, X2) |
Problem 14: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| snd#(active(X)) | → | snd#(X) | | snd#(mark(X)) | → | snd#(X) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| snd#(active(X)) | → | snd#(X) | | snd#(mark(X)) | → | snd#(X) |
Problem 15: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| u#(mark(X1), X2, X3, X4) | → | u#(X1, X2, X3, X4) | | u#(active(X1), X2, X3, X4) | → | u#(X1, X2, X3, X4) |
| u#(X1, mark(X2), X3, X4) | → | u#(X1, X2, X3, X4) | | u#(X1, X2, active(X3), X4) | → | u#(X1, X2, X3, X4) |
| u#(X1, X2, X3, mark(X4)) | → | u#(X1, X2, X3, X4) | | u#(X1, active(X2), X3, X4) | → | u#(X1, X2, X3, X4) |
| u#(X1, X2, X3, active(X4)) | → | u#(X1, X2, X3, X4) | | u#(X1, X2, mark(X3), X4) | → | u#(X1, X2, X3, X4) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| u#(mark(X1), X2, X3, X4) | → | u#(X1, X2, X3, X4) | | u#(active(X1), X2, X3, X4) | → | u#(X1, X2, X3, X4) |
Problem 22: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| u#(X1, mark(X2), X3, X4) | → | u#(X1, X2, X3, X4) | | u#(X1, X2, active(X3), X4) | → | u#(X1, X2, X3, X4) |
| u#(X1, X2, X3, mark(X4)) | → | u#(X1, X2, X3, X4) | | u#(X1, X2, X3, active(X4)) | → | u#(X1, X2, X3, X4) |
| u#(X1, active(X2), X3, X4) | → | u#(X1, X2, X3, X4) | | u#(X1, X2, mark(X3), X4) | → | u#(X1, X2, X3, X4) |
Rewrite Rules
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(fst(pair(XS, YS))) | → | mark(XS) |
| active(snd(pair(XS, YS))) | → | mark(YS) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(u(splitAt(N, XS), N, X, XS)) | | active(u(pair(YS, ZS), N, X, XS)) | → | mark(pair(cons(X, YS), ZS)) |
| active(head(cons(N, XS))) | → | mark(N) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) | | active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | mark(natsFrom(X)) | → | active(natsFrom(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(fst(X)) | → | active(fst(mark(X))) | | mark(pair(X1, X2)) | → | active(pair(mark(X1), mark(X2))) |
| mark(snd(X)) | → | active(snd(mark(X))) | | mark(splitAt(X1, X2)) | → | active(splitAt(mark(X1), mark(X2))) |
| mark(0) | → | active(0) | | mark(nil) | → | active(nil) |
| mark(u(X1, X2, X3, X4)) | → | active(u(mark(X1), X2, X3, X4)) | | mark(head(X)) | → | active(head(mark(X))) |
| mark(tail(X)) | → | active(tail(mark(X))) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(afterNth(X1, X2)) | → | active(afterNth(mark(X1), mark(X2))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| natsFrom(mark(X)) | → | natsFrom(X) | | natsFrom(active(X)) | → | natsFrom(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| fst(mark(X)) | → | fst(X) | | fst(active(X)) | → | fst(X) |
| pair(mark(X1), X2) | → | pair(X1, X2) | | pair(X1, mark(X2)) | → | pair(X1, X2) |
| pair(active(X1), X2) | → | pair(X1, X2) | | pair(X1, active(X2)) | → | pair(X1, X2) |
| snd(mark(X)) | → | snd(X) | | snd(active(X)) | → | snd(X) |
| splitAt(mark(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, mark(X2)) | → | splitAt(X1, X2) |
| splitAt(active(X1), X2) | → | splitAt(X1, X2) | | splitAt(X1, active(X2)) | → | splitAt(X1, X2) |
| u(mark(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, mark(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, mark(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, mark(X4)) | → | u(X1, X2, X3, X4) |
| u(active(X1), X2, X3, X4) | → | u(X1, X2, X3, X4) | | u(X1, active(X2), X3, X4) | → | u(X1, X2, X3, X4) |
| u(X1, X2, active(X3), X4) | → | u(X1, X2, X3, X4) | | u(X1, X2, X3, active(X4)) | → | u(X1, X2, X3, X4) |
| head(mark(X)) | → | head(X) | | head(active(X)) | → | head(X) |
| tail(mark(X)) | → | tail(X) | | tail(active(X)) | → | tail(X) |
| sel(mark(X1), X2) | → | sel(X1, X2) | | sel(X1, mark(X2)) | → | sel(X1, X2) |
| sel(active(X1), X2) | → | sel(X1, X2) | | sel(X1, active(X2)) | → | sel(X1, X2) |
| afterNth(mark(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, mark(X2)) | → | afterNth(X1, X2) |
| afterNth(active(X1), X2) | → | afterNth(X1, X2) | | afterNth(X1, active(X2)) | → | afterNth(X1, X2) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- afterNth(x,y): 0
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- mark(x): 2x + 1
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): 0
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- u(x1,x2,x3,x4): 0
- u#(x1,x2,x3,x4): 2x4
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| u#(X1, X2, X3, mark(X4)) | → | u#(X1, X2, X3, X4) |