TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60081 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (16359ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (10ms), PolynomialLinearRange4iUR (1689ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (2000ms), DependencyGraph (6ms), PolynomialLinearRange8NegiUR (6001ms), DependencyGraph (8ms), ReductionPairSAT (33281ms)].
| – Problem 3 was processed with processor SubtermCriterion (2ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| – Problem 5 was processed with processor SubtermCriterion (3ms).
| – Problem 6 was processed with processor SubtermCriterion (2ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| | – Problem 18 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (11ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (17ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (30ms), DependencyGraph (2ms), ReductionPairSAT (timeout)].
| – Problem 8 was processed with processor SubtermCriterion (4ms).
| – Problem 9 was processed with processor SubtermCriterion (2ms).
| | – Problem 19 was processed with processor PolynomialLinearRange4iUR (115ms).
| – Problem 10 was processed with processor SubtermCriterion (3ms).
| | – Problem 20 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (11ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (4ms)].
| – Problem 11 was processed with processor SubtermCriterion (5ms).
| – Problem 12 was processed with processor SubtermCriterion (1ms).
| – Problem 13 was processed with processor SubtermCriterion (2ms).
| | – Problem 21 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (9ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (1ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (3ms)].
| – Problem 14 was processed with processor SubtermCriterion (2ms).
| – Problem 15 was processed with processor SubtermCriterion (4ms).
| – Problem 16 was processed with processor SubtermCriterion (1ms).
| – Problem 17 was processed with processor SubtermCriterion (2ms).
| | – Problem 22 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (43ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (2ms), DependencyGraph (3ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, proper, afterNth, head, sel, top, cons, snd, nil
Open Dependency Pair Problem 18
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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Open Dependency Pair Problem 21
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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Open Dependency Pair Problem 20
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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Open Dependency Pair Problem 22
Dependency Pairs
| splitAt#(X1, mark(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(tail(X)) | → | proper#(X) |
| active#(take(N, XS)) | → | splitAt#(N, XS) | | proper#(snd(X)) | → | snd#(proper(X)) |
| splitAt#(mark(X1), X2) | → | splitAt#(X1, X2) | | active#(afterNth(N, XS)) | → | snd#(splitAt(N, XS)) |
| active#(take(X1, X2)) | → | take#(active(X1), X2) | | tail#(ok(X)) | → | tail#(X) |
| active#(splitAt(X1, X2)) | → | splitAt#(active(X1), X2) | | active#(splitAt(X1, X2)) | → | splitAt#(X1, active(X2)) |
| active#(splitAt(0, XS)) | → | pair#(nil, XS) | | top#(mark(X)) | → | proper#(X) |
| active#(take(X1, X2)) | → | active#(X2) | | pair#(X1, mark(X2)) | → | pair#(X1, X2) |
| splitAt#(X1, mark(X2)) | → | splitAt#(X1, X2) | | sel#(X1, mark(X2)) | → | sel#(X1, X2) |
| active#(afterNth(X1, X2)) | → | afterNth#(active(X1), X2) | | active#(sel(N, XS)) | → | head#(afterNth(N, XS)) |
| head#(ok(X)) | → | head#(X) | | sel#(ok(X1), ok(X2)) | → | sel#(X1, X2) |
| active#(u(pair(YS, ZS), N, X, XS)) | → | cons#(X, YS) | | proper#(splitAt(X1, X2)) | → | proper#(X2) |
| pair#(mark(X1), X2) | → | pair#(X1, X2) | | proper#(head(X)) | → | proper#(X) |
| active#(afterNth(N, XS)) | → | splitAt#(N, XS) | | natsFrom#(mark(X)) | → | natsFrom#(X) |
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | active#(afterNth(X1, X2)) | → | afterNth#(X1, active(X2)) |
| u#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | u#(X1, X2, X3, X4) | | top#(ok(X)) | → | active#(X) |
| active#(u(X1, X2, X3, X4)) | → | active#(X1) | | active#(snd(X)) | → | snd#(active(X)) |
| active#(sel(X1, X2)) | → | active#(X1) | | active#(pair(X1, X2)) | → | active#(X1) |
| natsFrom#(ok(X)) | → | natsFrom#(X) | | proper#(sel(X1, X2)) | → | proper#(X2) |
| take#(ok(X1), ok(X2)) | → | take#(X1, X2) | | active#(sel(X1, X2)) | → | sel#(active(X1), X2) |
| active#(sel(X1, X2)) | → | sel#(X1, active(X2)) | | snd#(mark(X)) | → | snd#(X) |
| head#(mark(X)) | → | head#(X) | | pair#(ok(X1), ok(X2)) | → | pair#(X1, X2) |
| active#(head(X)) | → | head#(active(X)) | | active#(afterNth(X1, X2)) | → | active#(X2) |
| active#(s(X)) | → | s#(active(X)) | | proper#(u(X1, X2, X3, X4)) | → | proper#(X3) |
| s#(ok(X)) | → | s#(X) | | proper#(pair(X1, X2)) | → | pair#(proper(X1), proper(X2)) |
| u#(mark(X1), X2, X3, X4) | → | u#(X1, X2, X3, X4) | | proper#(sel(X1, X2)) | → | proper#(X1) |
| proper#(tail(X)) | → | tail#(proper(X)) | | active#(take(X1, X2)) | → | take#(X1, active(X2)) |
| proper#(s(X)) | → | s#(proper(X)) | | active#(splitAt(X1, X2)) | → | active#(X1) |
| active#(natsFrom(N)) | → | natsFrom#(s(N)) | | top#(ok(X)) | → | top#(active(X)) |
| active#(splitAt(s(N), cons(X, XS))) | → | u#(splitAt(N, XS), N, X, XS) | | proper#(natsFrom(X)) | → | proper#(X) |
| afterNth#(X1, mark(X2)) | → | afterNth#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
| active#(cons(X1, X2)) | → | cons#(active(X1), X2) | | active#(tail(X)) | → | tail#(active(X)) |
| active#(sel(N, XS)) | → | afterNth#(N, XS) | | active#(sel(X1, X2)) | → | active#(X2) |
| active#(pair(X1, X2)) | → | active#(X2) | | snd#(ok(X)) | → | snd#(X) |
| active#(u(X1, X2, X3, X4)) | → | u#(active(X1), X2, X3, X4) | | active#(head(X)) | → | active#(X) |
| afterNth#(mark(X1), X2) | → | afterNth#(X1, X2) | | proper#(afterNth(X1, X2)) | → | proper#(X1) |
| proper#(u(X1, X2, X3, X4)) | → | proper#(X4) | | top#(mark(X)) | → | top#(proper(X)) |
| proper#(fst(X)) | → | fst#(proper(X)) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(pair(X1, X2)) | → | proper#(X2) | | active#(pair(X1, X2)) | → | pair#(active(X1), X2) |
| tail#(mark(X)) | → | tail#(X) | | take#(X1, mark(X2)) | → | take#(X1, X2) |
| proper#(afterNth(X1, X2)) | → | proper#(X2) | | proper#(pair(X1, X2)) | → | proper#(X1) |
| proper#(u(X1, X2, X3, X4)) | → | proper#(X1) | | proper#(s(X)) | → | proper#(X) |
| proper#(snd(X)) | → | proper#(X) | | proper#(head(X)) | → | head#(proper(X)) |
| proper#(splitAt(X1, X2)) | → | splitAt#(proper(X1), proper(X2)) | | proper#(natsFrom(X)) | → | natsFrom#(proper(X)) |
| proper#(take(X1, X2)) | → | take#(proper(X1), proper(X2)) | | active#(snd(X)) | → | active#(X) |
| active#(splitAt(s(N), cons(X, XS))) | → | splitAt#(N, XS) | | active#(cons(X1, X2)) | → | active#(X1) |
| active#(u(pair(YS, ZS), N, X, XS)) | → | pair#(cons(X, YS), ZS) | | sel#(mark(X1), X2) | → | sel#(X1, X2) |
| take#(mark(X1), X2) | → | take#(X1, X2) | | active#(natsFrom(N)) | → | s#(N) |
| active#(pair(X1, X2)) | → | pair#(X1, active(X2)) | | proper#(u(X1, X2, X3, X4)) | → | u#(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper#(u(X1, X2, X3, X4)) | → | proper#(X2) | | active#(natsFrom(X)) | → | active#(X) |
| proper#(fst(X)) | → | proper#(X) | | proper#(sel(X1, X2)) | → | sel#(proper(X1), proper(X2)) |
| afterNth#(ok(X1), ok(X2)) | → | afterNth#(X1, X2) | | active#(afterNth(X1, X2)) | → | active#(X1) |
| splitAt#(ok(X1), ok(X2)) | → | splitAt#(X1, X2) | | active#(splitAt(X1, X2)) | → | active#(X2) |
| proper#(take(X1, X2)) | → | proper#(X1) | | fst#(mark(X)) | → | fst#(X) |
| active#(take(N, XS)) | → | fst#(splitAt(N, XS)) | | active#(natsFrom(X)) | → | natsFrom#(active(X)) |
| active#(fst(X)) | → | active#(X) | | active#(fst(X)) | → | fst#(active(X)) |
| active#(take(X1, X2)) | → | active#(X1) | | proper#(take(X1, X2)) | → | proper#(X2) |
| fst#(ok(X)) | → | fst#(X) | | s#(mark(X)) | → | s#(X) |
| proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) | | active#(s(X)) | → | active#(X) |
| active#(tail(X)) | → | active#(X) | | active#(natsFrom(N)) | → | cons#(N, natsFrom(s(N))) |
| proper#(afterNth(X1, X2)) | → | afterNth#(proper(X1), proper(X2)) | | proper#(splitAt(X1, X2)) | → | proper#(X1) |
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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
The following SCCs where found
| sel#(mark(X1), X2) → sel#(X1, X2) | sel#(ok(X1), ok(X2)) → sel#(X1, X2) |
| sel#(X1, mark(X2)) → sel#(X1, X2) |
| head#(ok(X)) → head#(X) | head#(mark(X)) → head#(X) |
| u#(mark(X1), X2, X3, X4) → u#(X1, X2, X3, X4) | u#(ok(X1), ok(X2), ok(X3), ok(X4)) → u#(X1, X2, X3, X4) |
| pair#(mark(X1), X2) → pair#(X1, X2) | pair#(ok(X1), ok(X2)) → pair#(X1, X2) |
| pair#(X1, mark(X2)) → pair#(X1, X2) |
| take#(mark(X1), X2) → take#(X1, X2) | take#(X1, mark(X2)) → take#(X1, X2) |
| take#(ok(X1), ok(X2)) → take#(X1, X2) |
| active#(take(X1, X2)) → active#(X2) | active#(fst(X)) → active#(X) |
| active#(take(X1, X2)) → active#(X1) | active#(afterNth(X1, X2)) → active#(X2) |
| active#(natsFrom(X)) → active#(X) | active#(u(X1, X2, X3, X4)) → active#(X1) |
| active#(sel(X1, X2)) → active#(X2) | active#(afterNth(X1, X2)) → active#(X1) |
| active#(splitAt(X1, X2)) → active#(X2) | active#(sel(X1, X2)) → active#(X1) |
| active#(s(X)) → active#(X) | active#(pair(X1, X2)) → active#(X2) |
| active#(pair(X1, X2)) → active#(X1) | active#(tail(X)) → active#(X) |
| active#(head(X)) → active#(X) | active#(splitAt(X1, X2)) → active#(X1) |
| active#(snd(X)) → active#(X) | active#(cons(X1, X2)) → active#(X1) |
| s#(mark(X)) → s#(X) | s#(ok(X)) → s#(X) |
| cons#(mark(X1), X2) → cons#(X1, X2) | cons#(ok(X1), ok(X2)) → cons#(X1, X2) |
| natsFrom#(mark(X)) → natsFrom#(X) | natsFrom#(ok(X)) → natsFrom#(X) |
| tail#(ok(X)) → tail#(X) | tail#(mark(X)) → tail#(X) |
| proper#(u(X1, X2, X3, X4)) → proper#(X4) | proper#(cons(X1, X2)) → proper#(X1) |
| proper#(head(X)) → proper#(X) | proper#(cons(X1, X2)) → proper#(X2) |
| proper#(tail(X)) → proper#(X) | proper#(natsFrom(X)) → proper#(X) |
| proper#(pair(X1, X2)) → proper#(X2) | proper#(take(X1, X2)) → proper#(X2) |
| proper#(u(X1, X2, X3, X4)) → proper#(X2) | proper#(fst(X)) → proper#(X) |
| proper#(u(X1, X2, X3, X4)) → proper#(X3) | proper#(afterNth(X1, X2)) → proper#(X2) |
| proper#(pair(X1, X2)) → proper#(X1) | proper#(u(X1, X2, X3, X4)) → proper#(X1) |
| proper#(sel(X1, X2)) → proper#(X1) | proper#(snd(X)) → proper#(X) |
| proper#(s(X)) → proper#(X) | proper#(take(X1, X2)) → proper#(X1) |
| proper#(splitAt(X1, X2)) → proper#(X2) | proper#(sel(X1, X2)) → proper#(X2) |
| proper#(splitAt(X1, X2)) → proper#(X1) | proper#(afterNth(X1, X2)) → proper#(X1) |
| splitAt#(ok(X1), ok(X2)) → splitAt#(X1, X2) | splitAt#(X1, mark(X2)) → splitAt#(X1, X2) |
| splitAt#(mark(X1), X2) → splitAt#(X1, X2) |
| fst#(mark(X)) → fst#(X) | fst#(ok(X)) → fst#(X) |
| snd#(mark(X)) → snd#(X) | snd#(ok(X)) → snd#(X) |
| afterNth#(X1, mark(X2)) → afterNth#(X1, X2) | afterNth#(mark(X1), X2) → afterNth#(X1, X2) |
| afterNth#(ok(X1), ok(X2)) → afterNth#(X1, X2) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| fst#(mark(X)) | → | fst#(X) | | fst#(ok(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| fst#(mark(X)) | → | fst#(X) | | fst#(ok(X)) | → | fst#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| head#(ok(X)) | → | head#(X) | | head#(mark(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| head#(ok(X)) | → | head#(X) | | head#(mark(X)) | → | head#(X) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| natsFrom#(mark(X)) | → | natsFrom#(X) | | natsFrom#(ok(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| natsFrom#(mark(X)) | → | natsFrom#(X) | | natsFrom#(ok(X)) | → | natsFrom#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| snd#(mark(X)) | → | snd#(X) | | snd#(ok(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| snd#(mark(X)) | → | snd#(X) | | snd#(ok(X)) | → | snd#(X) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sel#(mark(X1), X2) | → | sel#(X1, X2) | | sel#(ok(X1), ok(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sel#(mark(X1), X2) | → | sel#(X1, X2) | | sel#(ok(X1), ok(X2)) | → | sel#(X1, X2) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(take(X1, X2)) | → | active#(X2) | | active#(fst(X)) | → | active#(X) |
| active#(take(X1, X2)) | → | active#(X1) | | active#(natsFrom(X)) | → | active#(X) |
| active#(afterNth(X1, X2)) | → | active#(X2) | | active#(u(X1, X2, X3, X4)) | → | active#(X1) |
| active#(afterNth(X1, X2)) | → | active#(X1) | | active#(sel(X1, X2)) | → | active#(X2) |
| active#(pair(X1, X2)) | → | active#(X2) | | active#(s(X)) | → | active#(X) |
| active#(sel(X1, X2)) | → | active#(X1) | | active#(splitAt(X1, X2)) | → | active#(X2) |
| active#(pair(X1, X2)) | → | active#(X1) | | active#(tail(X)) | → | active#(X) |
| active#(head(X)) | → | active#(X) | | active#(splitAt(X1, X2)) | → | active#(X1) |
| active#(snd(X)) | → | active#(X) | | active#(cons(X1, X2)) | → | active#(X1) |
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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(take(X1, X2)) | → | active#(X2) | | active#(fst(X)) | → | active#(X) |
| active#(take(X1, X2)) | → | active#(X1) | | active#(natsFrom(X)) | → | active#(X) |
| active#(afterNth(X1, X2)) | → | active#(X2) | | active#(u(X1, X2, X3, X4)) | → | active#(X1) |
| active#(afterNth(X1, X2)) | → | active#(X1) | | active#(sel(X1, X2)) | → | active#(X2) |
| active#(pair(X1, X2)) | → | active#(X2) | | active#(sel(X1, X2)) | → | active#(X1) |
| active#(splitAt(X1, X2)) | → | active#(X2) | | active#(s(X)) | → | active#(X) |
| active#(pair(X1, X2)) | → | active#(X1) | | active#(tail(X)) | → | active#(X) |
| active#(head(X)) | → | active#(X) | | active#(splitAt(X1, X2)) | → | active#(X1) |
| active#(snd(X)) | → | active#(X) | | active#(cons(X1, X2)) | → | active#(X1) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| afterNth#(X1, mark(X2)) | → | afterNth#(X1, X2) | | afterNth#(mark(X1), X2) | → | afterNth#(X1, X2) |
| afterNth#(ok(X1), ok(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| afterNth#(mark(X1), X2) | → | afterNth#(X1, X2) | | afterNth#(ok(X1), ok(X2)) | → | afterNth#(X1, X2) |
Problem 19: 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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, proper, afterNth, head, sel, top, cons, snd, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 0
- afterNth(x,y): 0
- afterNth#(x,y): 2y + x + 1
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- mark(x): x + 1
- natsFrom(x): 0
- nil: 0
- ok(x): 0
- pair(x,y): 0
- proper(x): 0
- s(x): 0
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- top(x): 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 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| pair#(mark(X1), X2) | → | pair#(X1, X2) | | pair#(ok(X1), ok(X2)) | → | pair#(X1, X2) |
| 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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| pair#(mark(X1), X2) | → | pair#(X1, X2) | | pair#(ok(X1), ok(X2)) | → | pair#(X1, X2) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| tail#(ok(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| tail#(ok(X)) | → | tail#(X) | | tail#(mark(X)) | → | tail#(X) |
Problem 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| u#(mark(X1), X2, X3, X4) | → | u#(X1, X2, X3, X4) | | u#(ok(X1), ok(X2), ok(X3), ok(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
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#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | u#(X1, X2, X3, X4) |
Problem 13: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| take#(mark(X1), X2) | → | take#(X1, X2) | | take#(X1, mark(X2)) | → | take#(X1, X2) |
| take#(ok(X1), ok(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| take#(mark(X1), X2) | → | take#(X1, X2) | | take#(ok(X1), ok(X2)) | → | take#(X1, X2) |
Problem 14: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(ok(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(ok(X)) | → | s#(X) |
Problem 15: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(u(X1, X2, X3, X4)) | → | proper#(X4) | | proper#(head(X)) | → | proper#(X) |
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(tail(X)) | → | proper#(X) | | proper#(natsFrom(X)) | → | proper#(X) |
| proper#(pair(X1, X2)) | → | proper#(X2) | | proper#(take(X1, X2)) | → | proper#(X2) |
| proper#(u(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(u(X1, X2, X3, X4)) | → | proper#(X3) |
| proper#(fst(X)) | → | proper#(X) | | proper#(afterNth(X1, X2)) | → | proper#(X2) |
| proper#(pair(X1, X2)) | → | proper#(X1) | | proper#(u(X1, X2, X3, X4)) | → | proper#(X1) |
| proper#(sel(X1, X2)) | → | proper#(X1) | | proper#(snd(X)) | → | proper#(X) |
| proper#(s(X)) | → | proper#(X) | | proper#(take(X1, X2)) | → | proper#(X1) |
| proper#(splitAt(X1, X2)) | → | proper#(X2) | | proper#(sel(X1, X2)) | → | proper#(X2) |
| proper#(splitAt(X1, X2)) | → | proper#(X1) | | proper#(afterNth(X1, X2)) | → | proper#(X1) |
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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(u(X1, X2, X3, X4)) | → | proper#(X4) | | proper#(head(X)) | → | proper#(X) |
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(tail(X)) | → | proper#(X) | | proper#(natsFrom(X)) | → | proper#(X) |
| proper#(pair(X1, X2)) | → | proper#(X2) | | proper#(take(X1, X2)) | → | proper#(X2) |
| proper#(u(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(fst(X)) | → | proper#(X) |
| proper#(u(X1, X2, X3, X4)) | → | proper#(X3) | | proper#(afterNth(X1, X2)) | → | proper#(X2) |
| proper#(u(X1, X2, X3, X4)) | → | proper#(X1) | | proper#(pair(X1, X2)) | → | proper#(X1) |
| proper#(sel(X1, X2)) | → | proper#(X1) | | proper#(s(X)) | → | proper#(X) |
| proper#(snd(X)) | → | proper#(X) | | proper#(take(X1, X2)) | → | proper#(X1) |
| proper#(splitAt(X1, X2)) | → | proper#(X2) | | proper#(sel(X1, X2)) | → | proper#(X2) |
| proper#(splitAt(X1, X2)) | → | proper#(X1) | | proper#(afterNth(X1, X2)) | → | proper#(X1) |
Problem 16: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Problem 17: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| splitAt#(ok(X1), ok(X2)) | → | splitAt#(X1, X2) | | splitAt#(X1, mark(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))) | | active(natsFrom(X)) | → | natsFrom(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(fst(X)) | → | fst(active(X)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(snd(X)) | → | snd(active(X)) |
| active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) |
| active(u(X1, X2, X3, X4)) | → | u(active(X1), X2, X3, X4) | | active(head(X)) | → | head(active(X)) |
| active(tail(X)) | → | tail(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | natsFrom(mark(X)) | → | mark(natsFrom(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| fst(mark(X)) | → | mark(fst(X)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | snd(mark(X)) | → | mark(snd(X)) |
| splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) | | splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) |
| u(mark(X1), X2, X3, X4) | → | mark(u(X1, X2, X3, X4)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) |
| afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(natsFrom(X)) | → | natsFrom(proper(X)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(nil) | → | ok(nil) |
| proper(u(X1, X2, X3, X4)) | → | u(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(head(X)) | → | head(proper(X)) |
| proper(tail(X)) | → | tail(proper(X)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| natsFrom(ok(X)) | → | ok(natsFrom(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | fst(ok(X)) | → | ok(fst(X)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) | | u(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(u(X1, X2, X3, X4)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) | | afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, ok, afterNth, proper, head, sel, nil, snd, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| splitAt#(ok(X1), ok(X2)) | → | splitAt#(X1, X2) | | splitAt#(mark(X1), X2) | → | splitAt#(X1, X2) |