TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60002 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (23478ms).
| – Problem 2 was processed with processor SubtermCriterion (42ms).
| | – Problem 22 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (45ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (21ms), DependencyGraph (3ms)].
| – Problem 3 was processed with processor SubtermCriterion (4ms).
| – Problem 4 was processed with processor SubtermCriterion (3ms).
| – Problem 5 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (10ms), PolynomialLinearRange4iUR (1250ms), DependencyGraph (8ms), PolynomialLinearRange8NegiUR (3750ms), DependencyGraph (8ms), ReductionPairSAT (timeout)].
| – Problem 6 was processed with processor SubtermCriterion (2ms).
| | – Problem 23 remains open; application of the following processors failed [DependencyGraph (5ms), PolynomialLinearRange4iUR (15ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (20ms), DependencyGraph (2ms)].
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| | – Problem 24 remains open; application of the following processors failed [DependencyGraph (4ms), PolynomialLinearRange4iUR (8ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (2ms)].
| – Problem 8 was processed with processor SubtermCriterion (5ms).
| – Problem 9 was processed with processor SubtermCriterion (2ms).
| – Problem 10 was processed with processor DependencyGraph (938ms).
| | – Problem 27 remains open; application of the following processors failed [PolynomialLinearRange4iUR (37ms), DependencyGraph (573ms), PolynomialLinearRange8NegiUR (7ms), DependencyGraph (573ms)].
| – Problem 11 was processed with processor SubtermCriterion (3ms).
| – Problem 12 was processed with processor SubtermCriterion (2ms).
| – Problem 13 was processed with processor DependencyGraph (870ms).
| | – Problem 28 remains open; application of the following processors failed [PolynomialLinearRange4iUR (61ms), DependencyGraph (577ms), PolynomialLinearRange8NegiUR (4ms), DependencyGraph (550ms)].
| – Problem 14 was processed with processor SubtermCriterion (3ms).
| – Problem 15 was processed with processor SubtermCriterion (2ms).
| – Problem 16 was processed with processor SubtermCriterion (4ms).
| – Problem 17 was processed with processor SubtermCriterion (1ms).
| – Problem 18 was processed with processor SubtermCriterion (1ms).
| | – Problem 26 remains open; application of the following processors failed [DependencyGraph (5ms), PolynomialLinearRange4iUR (31ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (4ms)].
| – Problem 19 was processed with processor SubtermCriterion (2ms).
| | – Problem 25 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (4ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (25ms), DependencyGraph (3ms)].
| – Problem 20 was processed with processor SubtermCriterion (1ms).
| – Problem 21 was processed with processor SubtermCriterion (5ms).
The following open problems remain:
Open Dependency Pair Problem 5
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(X)) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, ok, U12, proper, afterNth, head, sel, top, nil, cons, snd
Open Dependency Pair Problem 23
Dependency Pairs
| afterNth#(X1, mark(X2)) | → | afterNth#(X1, X2) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Open Dependency Pair Problem 22
Dependency Pairs
| take#(X1, mark(X2)) | → | take#(X1, X2) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Open Dependency Pair Problem 25
Dependency Pairs
| splitAt#(X1, mark(X2)) | → | splitAt#(X1, X2) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Open Dependency Pair Problem 24
Dependency Pairs
| pair#(X1, mark(X2)) | → | pair#(X1, X2) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Open Dependency Pair Problem 27
Dependency Pairs
| active#(U12(X1, X2)) | → | active#(X1) | | 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#(U11(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#(and(X1, X2)) | → | active#(X1) |
| active#(snd(X)) | → | active#(X) | | active#(cons(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, ok, U12, proper, afterNth, head, sel, top, nil, cons, snd
Open Dependency Pair Problem 26
Dependency Pairs
| sel#(X1, mark(X2)) | → | sel#(X1, X2) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Open Dependency Pair Problem 28
Dependency Pairs
| active#(U12(X1, X2)) | → | active#(X1) | | 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#(U11(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#(and(X1, X2)) | → | active#(X1) |
| active#(snd(X)) | → | active#(X) | | active#(cons(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, ok, U12, proper, afterNth, head, sel, top, nil, cons, snd
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | active#(take(N, XS)) | → | splitAt#(N, XS) |
| proper#(tail(X)) | → | proper#(X) | | 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) | | and#(mark(X1), X2) | → | and#(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) |
| active#(U12(X1, X2)) | → | U12#(active(X1), X2) | | sel#(ok(X1), ok(X2)) | → | sel#(X1, X2) |
| proper#(splitAt(X1, X2)) | → | proper#(X2) | | U11#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U11#(X1, X2, X3, X4) |
| pair#(mark(X1), X2) | → | pair#(X1, X2) | | proper#(head(X)) | → | proper#(X) |
| active#(afterNth(N, XS)) | → | splitAt#(N, XS) | | natsFrom#(mark(X)) | → | natsFrom#(X) |
| proper#(U11(X1, X2, X3, X4)) | → | U11#(proper(X1), proper(X2), proper(X3), proper(X4)) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| active#(U12(pair(YS, ZS), X)) | → | pair#(cons(X, YS), ZS) | | active#(afterNth(X1, X2)) | → | afterNth#(X1, active(X2)) |
| top#(ok(X)) | → | active#(X) | | active#(and(X1, X2)) | → | and#(active(X1), X2) |
| 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) |
| active#(U12(X1, X2)) | → | active#(X1) | | 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)) | | s#(ok(X)) | → | s#(X) |
| proper#(pair(X1, X2)) | → | pair#(proper(X1), proper(X2)) | | 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)) |
| proper#(natsFrom(X)) | → | proper#(X) | | U12#(ok(X1), ok(X2)) | → | U12#(X1, X2) |
| afterNth#(X1, mark(X2)) | → | afterNth#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
| active#(U11(tt, N, X, XS)) | → | splitAt#(N, XS) | | proper#(U12(X1, X2)) | → | proper#(X2) |
| proper#(and(X1, X2)) | → | and#(proper(X1), proper(X2)) | | active#(cons(X1, X2)) | → | cons#(active(X1), X2) |
| active#(U11(X1, X2, X3, X4)) | → | U11#(active(X1), X2, X3, X4) | | active#(tail(X)) | → | tail#(active(X)) |
| active#(sel(N, XS)) | → | afterNth#(N, XS) | | active#(sel(X1, X2)) | → | active#(X2) |
| proper#(and(X1, X2)) | → | proper#(X2) | | active#(pair(X1, X2)) | → | active#(X2) |
| snd#(ok(X)) | → | snd#(X) | | U12#(mark(X1), X2) | → | U12#(X1, X2) |
| active#(head(X)) | → | active#(X) | | afterNth#(mark(X1), X2) | → | afterNth#(X1, X2) |
| proper#(afterNth(X1, X2)) | → | proper#(X1) | | top#(mark(X)) | → | top#(proper(X)) |
| proper#(fst(X)) | → | fst#(proper(X)) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| active#(U11(tt, N, X, XS)) | → | U12#(splitAt(N, XS), X) | | 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#(s(X)) | → | proper#(X) |
| proper#(snd(X)) | → | proper#(X) | | proper#(head(X)) | → | head#(proper(X)) |
| active#(U11(X1, X2, X3, X4)) | → | active#(X1) | | proper#(U11(X1, X2, X3, X4)) | → | proper#(X2) |
| 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) |
| proper#(U12(X1, X2)) | → | U12#(proper(X1), proper(X2)) | | active#(cons(X1, X2)) | → | active#(X1) |
| sel#(mark(X1), X2) | → | sel#(X1, X2) | | U11#(mark(X1), X2, X3, X4) | → | U11#(X1, X2, X3, X4) |
| take#(mark(X1), X2) | → | take#(X1, X2) | | active#(splitAt(s(N), cons(X, XS))) | → | U11#(tt, N, X, XS) |
| active#(natsFrom(N)) | → | s#(N) | | active#(pair(X1, X2)) | → | pair#(X1, active(X2)) |
| proper#(U11(X1, X2, X3, X4)) | → | proper#(X1) | | active#(natsFrom(X)) | → | active#(X) |
| and#(ok(X1), ok(X2)) | → | and#(X1, X2) | | proper#(U11(X1, X2, X3, X4)) | → | proper#(X4) |
| proper#(and(X1, X2)) | → | proper#(X1) | | proper#(fst(X)) | → | proper#(X) |
| proper#(sel(X1, X2)) | → | sel#(proper(X1), proper(X2)) | | afterNth#(ok(X1), ok(X2)) | → | afterNth#(X1, X2) |
| active#(U12(pair(YS, ZS), X)) | → | cons#(X, YS) | | 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)) |
| proper#(U11(X1, X2, X3, X4)) | → | proper#(X3) | | proper#(U12(X1, X2)) | → | proper#(X1) |
| active#(fst(X)) | → | fst#(active(X)) | | active#(fst(X)) | → | 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) | | proper#(afterNth(X1, X2)) | → | afterNth#(proper(X1), proper(X2)) |
| active#(natsFrom(N)) | → | cons#(N, natsFrom(s(N))) | | active#(and(X1, X2)) | → | active#(X1) |
| proper#(splitAt(X1, X2)) | → | proper#(X1) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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) |
| pair#(mark(X1), X2) → pair#(X1, X2) | pair#(ok(X1), ok(X2)) → pair#(X1, X2) |
| pair#(X1, mark(X2)) → pair#(X1, X2) |
| active#(natsFrom(N)) → natsFrom#(s(N)) | active#(splitAt(s(N), cons(X, XS))) → U11#(tt, N, X, XS) |
| active#(natsFrom(X)) → active#(X) | active#(afterNth(N, XS)) → snd#(splitAt(N, XS)) |
| 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#(pair(X1, X2)) → active#(X1) |
| active#(head(X)) → active#(X) | active#(splitAt(0, XS)) → pair#(nil, XS) |
| active#(natsFrom(X)) → natsFrom#(active(X)) | active#(U12(X1, X2)) → active#(X1) |
| active#(take(X1, X2)) → active#(X2) | active#(fst(X)) → fst#(active(X)) |
| active#(fst(X)) → active#(X) | active#(take(X1, X2)) → active#(X1) |
| active#(afterNth(X1, X2)) → active#(X2) | active#(U11(X1, X2, X3, X4)) → active#(X1) |
| active#(s(X)) → active#(X) | active#(tail(X)) → active#(X) |
| active#(and(X1, X2)) → active#(X1) | active#(splitAt(X1, X2)) → active#(X1) |
| active#(snd(X)) → active#(X) | active#(cons(X1, X2)) → active#(X1) |
| take#(mark(X1), X2) → take#(X1, X2) | take#(X1, mark(X2)) → take#(X1, X2) |
| take#(ok(X1), ok(X2)) → take#(X1, X2) |
| U11#(ok(X1), ok(X2), ok(X3), ok(X4)) → U11#(X1, X2, X3, X4) | U11#(mark(X1), X2, X3, X4) → U11#(X1, X2, X3, X4) |
| 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) |
| U12#(ok(X1), ok(X2)) → U12#(X1, X2) | U12#(mark(X1), X2) → U12#(X1, X2) |
| splitAt#(ok(X1), ok(X2)) → splitAt#(X1, X2) | splitAt#(X1, mark(X2)) → splitAt#(X1, X2) |
| splitAt#(mark(X1), X2) → splitAt#(X1, X2) |
| active#(natsFrom(N)) → natsFrom#(s(N)) | active#(splitAt(s(N), cons(X, XS))) → U11#(tt, N, X, XS) |
| active#(natsFrom(X)) → active#(X) | active#(afterNth(N, XS)) → snd#(splitAt(N, XS)) |
| 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#(pair(X1, X2)) → active#(X1) |
| active#(head(X)) → active#(X) | active#(splitAt(0, XS)) → pair#(nil, XS) |
| active#(U12(X1, X2)) → active#(X1) | active#(take(X1, X2)) → active#(X2) |
| active#(fst(X)) → fst#(active(X)) | active#(fst(X)) → active#(X) |
| active#(take(X1, X2)) → active#(X1) | active#(afterNth(X1, X2)) → active#(X2) |
| active#(U11(X1, X2, X3, X4)) → active#(X1) | active#(s(X)) → active#(X) |
| active#(tail(X)) → active#(X) | active#(and(X1, X2)) → active#(X1) |
| active#(splitAt(X1, X2)) → active#(X1) | active#(snd(X)) → active#(X) |
| active#(cons(X1, X2)) → active#(X1) |
| active#(U12(X1, X2)) → active#(X1) | 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#(U11(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#(pair(X1, X2)) → active#(X2) | active#(sel(X1, X2)) → active#(X1) |
| 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#(and(X1, X2)) → active#(X1) |
| active#(snd(X)) → active#(X) | active#(cons(X1, X2)) → active#(X1) |
| fst#(mark(X)) → fst#(X) | fst#(ok(X)) → fst#(X) |
| snd#(mark(X)) → snd#(X) | snd#(ok(X)) → snd#(X) |
| proper#(head(X)) → proper#(X) | proper#(cons(X1, X2)) → proper#(X1) |
| proper#(tail(X)) → proper#(X) | proper#(natsFrom(X)) → proper#(X) |
| proper#(U12(X1, X2)) → proper#(X2) | proper#(U11(X1, X2, X3, X4)) → proper#(X1) |
| proper#(U11(X1, X2, X3, X4)) → proper#(X4) | proper#(and(X1, X2)) → proper#(X1) |
| proper#(fst(X)) → proper#(X) | proper#(and(X1, X2)) → proper#(X2) |
| proper#(take(X1, X2)) → proper#(X1) | proper#(sel(X1, X2)) → proper#(X2) |
| proper#(afterNth(X1, X2)) → proper#(X1) | proper#(U11(X1, X2, X3, X4)) → proper#(X3) |
| proper#(U12(X1, X2)) → proper#(X1) | proper#(cons(X1, X2)) → proper#(X2) |
| proper#(pair(X1, X2)) → proper#(X2) | proper#(take(X1, X2)) → proper#(X2) |
| proper#(afterNth(X1, X2)) → proper#(X2) | proper#(pair(X1, X2)) → proper#(X1) |
| proper#(sel(X1, X2)) → proper#(X1) | proper#(snd(X)) → proper#(X) |
| proper#(s(X)) → proper#(X) | proper#(U11(X1, X2, X3, X4)) → proper#(X2) |
| proper#(splitAt(X1, X2)) → proper#(X2) | proper#(splitAt(X1, X2)) → proper#(X1) |
| afterNth#(X1, mark(X2)) → afterNth#(X1, X2) | afterNth#(mark(X1), X2) → afterNth#(X1, X2) |
| afterNth#(ok(X1), ok(X2)) → afterNth#(X1, X2) |
| and#(ok(X1), ok(X2)) → and#(X1, X2) | and#(mark(X1), X2) → and#(X1, X2) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
Problem 2: 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(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(head(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(tail(X)) | → | proper#(X) | | proper#(natsFrom(X)) | → | proper#(X) |
| proper#(U12(X1, X2)) | → | proper#(X2) | | proper#(U11(X1, X2, X3, X4)) | → | proper#(X1) |
| proper#(U11(X1, X2, X3, X4)) | → | proper#(X4) | | proper#(and(X1, X2)) | → | proper#(X1) |
| proper#(fst(X)) | → | proper#(X) | | proper#(and(X1, X2)) | → | proper#(X2) |
| proper#(take(X1, X2)) | → | proper#(X1) | | proper#(sel(X1, X2)) | → | proper#(X2) |
| proper#(afterNth(X1, X2)) | → | proper#(X1) | | proper#(U11(X1, X2, X3, X4)) | → | proper#(X3) |
| proper#(U12(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(pair(X1, X2)) | → | proper#(X2) | | proper#(take(X1, X2)) | → | proper#(X2) |
| proper#(afterNth(X1, X2)) | → | proper#(X2) | | proper#(pair(X1, X2)) | → | proper#(X1) |
| proper#(sel(X1, X2)) | → | proper#(X1) | | proper#(s(X)) | → | proper#(X) |
| proper#(snd(X)) | → | proper#(X) | | proper#(U11(X1, X2, X3, X4)) | → | proper#(X2) |
| proper#(splitAt(X1, X2)) | → | proper#(X2) | | proper#(splitAt(X1, X2)) | → | proper#(X1) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(head(X)) | → | proper#(X) |
| proper#(tail(X)) | → | proper#(X) | | proper#(natsFrom(X)) | → | proper#(X) |
| proper#(U11(X1, X2, X3, X4)) | → | proper#(X1) | | proper#(U12(X1, X2)) | → | proper#(X2) |
| proper#(U11(X1, X2, X3, X4)) | → | proper#(X4) | | proper#(fst(X)) | → | proper#(X) |
| proper#(and(X1, X2)) | → | proper#(X1) | | proper#(and(X1, X2)) | → | proper#(X2) |
| proper#(take(X1, X2)) | → | proper#(X1) | | proper#(sel(X1, X2)) | → | proper#(X2) |
| proper#(afterNth(X1, X2)) | → | proper#(X1) | | proper#(U11(X1, X2, X3, X4)) | → | proper#(X3) |
| proper#(U12(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(pair(X1, X2)) | → | proper#(X2) | | proper#(take(X1, X2)) | → | proper#(X2) |
| proper#(afterNth(X1, X2)) | → | proper#(X2) | | proper#(pair(X1, X2)) | → | proper#(X1) |
| proper#(sel(X1, X2)) | → | proper#(X1) | | proper#(s(X)) | → | proper#(X) |
| proper#(snd(X)) | → | proper#(X) | | proper#(U11(X1, X2, X3, X4)) | → | proper#(X2) |
| proper#(splitAt(X1, X2)) | → | proper#(X2) | | proper#(splitAt(X1, X2)) | → | proper#(X1) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| tail#(ok(X)) | → | tail#(X) | | tail#(mark(X)) | → | tail#(X) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 6: 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(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 7: 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(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(U12(X1, X2)) | → | active#(X1) | | 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#(U11(X1, X2, X3, X4)) | → | active#(X1) | | active#(afterNth(X1, X2)) | → | active#(X1) |
| active#(sel(X1, X2)) | → | active#(X2) | | active#(s(X)) | → | active#(X) |
| active#(sel(X1, X2)) | → | active#(X1) | | active#(pair(X1, X2)) | → | active#(X2) |
| 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#(and(X1, X2)) | → | active#(X1) |
| active#(snd(X)) | → | active#(X) | | active#(cons(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(U12(X1, X2)) | → | active#(X1) | | 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#(U11(X1, X2, X3, X4)) | → | active#(X1) | | active#(sel(X1, X2)) | → | active#(X2) |
| active#(afterNth(X1, X2)) | → | active#(X1) | | active#(sel(X1, X2)) | → | active#(X1) |
| active#(splitAt(X1, X2)) | → | active#(X2) | | active#(pair(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#(and(X1, X2)) | → | active#(X1) | | 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
| head#(ok(X)) | → | head#(X) | | head#(mark(X)) | → | head#(X) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 10: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| active#(natsFrom(N)) | → | natsFrom#(s(N)) | | active#(splitAt(s(N), cons(X, XS))) | → | U11#(tt, N, X, XS) |
| active#(natsFrom(X)) | → | active#(X) | | active#(afterNth(N, XS)) | → | snd#(splitAt(N, XS)) |
| 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#(pair(X1, X2)) | → | active#(X1) |
| active#(head(X)) | → | active#(X) | | active#(splitAt(0, XS)) | → | pair#(nil, XS) |
| active#(natsFrom(X)) | → | natsFrom#(active(X)) | | active#(U12(X1, X2)) | → | active#(X1) |
| active#(take(X1, X2)) | → | active#(X2) | | active#(fst(X)) | → | active#(X) |
| active#(fst(X)) | → | fst#(active(X)) | | active#(take(X1, X2)) | → | active#(X1) |
| active#(afterNth(X1, X2)) | → | active#(X2) | | active#(U11(X1, X2, X3, X4)) | → | active#(X1) |
| active#(s(X)) | → | active#(X) | | active#(tail(X)) | → | active#(X) |
| active#(splitAt(X1, X2)) | → | active#(X1) | | active#(and(X1, X2)) | → | active#(X1) |
| active#(snd(X)) | → | active#(X) | | active#(cons(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Strategy
The following SCCs where found
| active#(U12(X1, X2)) → active#(X1) | 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#(U11(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#(and(X1, X2)) → active#(X1) | active#(splitAt(X1, X2)) → active#(X1) |
| active#(snd(X)) → active#(X) | active#(cons(X1, X2)) → active#(X1) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| fst#(mark(X)) | → | fst#(X) | | fst#(ok(X)) | → | fst#(X) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U12#(ok(X1), ok(X2)) | → | U12#(X1, X2) | | U12#(mark(X1), X2) | → | U12#(X1, X2) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U12#(ok(X1), ok(X2)) | → | U12#(X1, X2) | | U12#(mark(X1), X2) | → | U12#(X1, X2) |
Problem 13: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| active#(natsFrom(N)) | → | natsFrom#(s(N)) | | active#(splitAt(s(N), cons(X, XS))) | → | U11#(tt, N, X, XS) |
| active#(natsFrom(X)) | → | active#(X) | | active#(afterNth(N, XS)) | → | snd#(splitAt(N, XS)) |
| 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#(pair(X1, X2)) | → | active#(X1) |
| active#(head(X)) | → | active#(X) | | active#(splitAt(0, XS)) | → | pair#(nil, XS) |
| active#(U12(X1, X2)) | → | active#(X1) | | active#(take(X1, X2)) | → | active#(X2) |
| active#(fst(X)) | → | active#(X) | | active#(fst(X)) | → | fst#(active(X)) |
| active#(take(X1, X2)) | → | active#(X1) | | active#(afterNth(X1, X2)) | → | active#(X2) |
| active#(U11(X1, X2, X3, X4)) | → | active#(X1) | | active#(s(X)) | → | active#(X) |
| active#(tail(X)) | → | active#(X) | | active#(splitAt(X1, X2)) | → | active#(X1) |
| active#(and(X1, X2)) | → | active#(X1) | | active#(snd(X)) | → | active#(X) |
| active#(cons(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Strategy
The following SCCs where found
| active#(U12(X1, X2)) → active#(X1) | 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#(U11(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#(and(X1, X2)) → active#(X1) | active#(splitAt(X1, X2)) → active#(X1) |
| active#(snd(X)) → active#(X) | active#(cons(X1, X2)) → active#(X1) |
Problem 14: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| snd#(mark(X)) | → | snd#(X) | | snd#(ok(X)) | → | snd#(X) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 15: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(ok(X)) | → | s#(X) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 16: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| natsFrom#(mark(X)) | → | natsFrom#(X) | | natsFrom#(ok(X)) | → | natsFrom#(X) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 17: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 18: 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(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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 19: 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(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, 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) |
Problem 20: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U11#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U11#(X1, X2, X3, X4) | | U11#(mark(X1), X2, X3, X4) | → | U11#(X1, X2, X3, X4) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U11#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U11#(X1, X2, X3, X4) | | U11#(mark(X1), X2, X3, X4) | → | U11#(X1, X2, X3, X4) |
Problem 21: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| and#(ok(X1), ok(X2)) | → | and#(X1, X2) | | and#(mark(X1), X2) | → | and#(X1, X2) |
Rewrite Rules
| active(U11(tt, N, X, XS)) | → | mark(U12(splitAt(N, XS), X)) | | active(U12(pair(YS, ZS), X)) | → | mark(pair(cons(X, YS), ZS)) |
| active(afterNth(N, XS)) | → | mark(snd(splitAt(N, XS))) | | active(and(tt, X)) | → | mark(X) |
| active(fst(pair(X, Y))) | → | mark(X) | | active(head(cons(N, XS))) | → | mark(N) |
| active(natsFrom(N)) | → | mark(cons(N, natsFrom(s(N)))) | | active(sel(N, XS)) | → | mark(head(afterNth(N, XS))) |
| active(snd(pair(X, Y))) | → | mark(Y) | | active(splitAt(0, XS)) | → | mark(pair(nil, XS)) |
| active(splitAt(s(N), cons(X, XS))) | → | mark(U11(tt, N, X, XS)) | | active(tail(cons(N, XS))) | → | mark(XS) |
| active(take(N, XS)) | → | mark(fst(splitAt(N, XS))) | | active(U11(X1, X2, X3, X4)) | → | U11(active(X1), X2, X3, X4) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(splitAt(X1, X2)) | → | splitAt(active(X1), X2) |
| active(splitAt(X1, X2)) | → | splitAt(X1, active(X2)) | | active(pair(X1, X2)) | → | pair(active(X1), X2) |
| active(pair(X1, X2)) | → | pair(X1, active(X2)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(afterNth(X1, X2)) | → | afterNth(active(X1), X2) | | active(afterNth(X1, X2)) | → | afterNth(X1, active(X2)) |
| active(snd(X)) | → | snd(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(fst(X)) | → | fst(active(X)) | | active(head(X)) | → | head(active(X)) |
| active(natsFrom(X)) | → | natsFrom(active(X)) | | active(s(X)) | → | s(active(X)) |
| active(sel(X1, X2)) | → | sel(active(X1), X2) | | active(sel(X1, X2)) | → | sel(X1, active(X2)) |
| active(tail(X)) | → | tail(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | U11(mark(X1), X2, X3, X4) | → | mark(U11(X1, X2, X3, X4)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | splitAt(mark(X1), X2) | → | mark(splitAt(X1, X2)) |
| splitAt(X1, mark(X2)) | → | mark(splitAt(X1, X2)) | | pair(mark(X1), X2) | → | mark(pair(X1, X2)) |
| pair(X1, mark(X2)) | → | mark(pair(X1, X2)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| afterNth(mark(X1), X2) | → | mark(afterNth(X1, X2)) | | afterNth(X1, mark(X2)) | → | mark(afterNth(X1, X2)) |
| snd(mark(X)) | → | mark(snd(X)) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| fst(mark(X)) | → | mark(fst(X)) | | head(mark(X)) | → | mark(head(X)) |
| natsFrom(mark(X)) | → | mark(natsFrom(X)) | | s(mark(X)) | → | mark(s(X)) |
| sel(mark(X1), X2) | → | mark(sel(X1, X2)) | | sel(X1, mark(X2)) | → | mark(sel(X1, X2)) |
| tail(mark(X)) | → | mark(tail(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | proper(U11(X1, X2, X3, X4)) | → | U11(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(splitAt(X1, X2)) | → | splitAt(proper(X1), proper(X2)) | | proper(pair(X1, X2)) | → | pair(proper(X1), proper(X2)) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(afterNth(X1, X2)) | → | afterNth(proper(X1), proper(X2)) |
| proper(snd(X)) | → | snd(proper(X)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(fst(X)) | → | fst(proper(X)) | | proper(head(X)) | → | head(proper(X)) |
| proper(natsFrom(X)) | → | natsFrom(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(nil) | → | ok(nil) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | U11(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U11(X1, X2, X3, X4)) |
| U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) | | splitAt(ok(X1), ok(X2)) | → | ok(splitAt(X1, X2)) |
| pair(ok(X1), ok(X2)) | → | ok(pair(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| afterNth(ok(X1), ok(X2)) | → | ok(afterNth(X1, X2)) | | snd(ok(X)) | → | ok(snd(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | fst(ok(X)) | → | ok(fst(X)) |
| head(ok(X)) | → | ok(head(X)) | | natsFrom(ok(X)) | → | ok(natsFrom(X)) |
| s(ok(X)) | → | ok(s(X)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| tail(ok(X)) | → | ok(tail(X)) | | 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, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| and#(ok(X1), ok(X2)) | → | and#(X1, X2) | | and#(mark(X1), X2) | → | and#(X1, X2) |