TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60044 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (7138ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (3ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (2ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| | – Problem 14 remains open; application of the following processors failed [DependencyGraph (4ms), PolynomialLinearRange4iUR (17ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (32ms), DependencyGraph (2ms)].
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor SubtermCriterion (5ms).
| – Problem 9 was processed with processor SubtermCriterion (2ms).
| – Problem 10 was processed with processor SubtermCriterion (1ms).
| – Problem 11 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (9ms), ReductionPairSAT (timeout)].
| – Problem 12 was processed with processor SubtermCriterion (3ms).
| – Problem 13 was processed with processor SubtermCriterion (2ms).
The following open problems remain:
Open Dependency Pair Problem 11
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(X)) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, top, nil, cons, U22
Open Dependency Pair Problem 14
Dependency Pairs
| take#(X1, mark(X2)) | → | take#(X1, X2) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, cons, nil, top
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(U22(X1, X2, X3, X4)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(length(X)) | → | length#(proper(X)) | | top#(ok(X)) | → | top#(active(X)) |
| proper#(U22(X1, X2, X3, X4)) | → | proper#(X2) | | active#(U21(X1, X2, X3, X4)) | → | active#(X1) |
| proper#(U11(X1, X2)) | → | proper#(X1) | | U12#(ok(X1), ok(X2)) | → | U12#(X1, X2) |
| U11#(ok(X1), ok(X2)) | → | U11#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
| proper#(U12(X1, X2)) | → | proper#(X2) | | U11#(mark(X1), X2) | → | U11#(X1, X2) |
| proper#(U11(X1, X2)) | → | U11#(proper(X1), proper(X2)) | | active#(U23(tt, IL, M, N)) | → | cons#(N, take(M, IL)) |
| active#(cons(X1, X2)) | → | cons#(active(X1), X2) | | active#(take(X1, X2)) | → | take#(active(X1), X2) |
| proper#(U11(X1, X2)) | → | proper#(X2) | | active#(U11(tt, L)) | → | U12#(tt, L) |
| proper#(U21(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(U22(X1, X2, X3, X4)) | → | proper#(X4) |
| U12#(mark(X1), X2) | → | U12#(X1, X2) | | length#(ok(X)) | → | length#(X) |
| active#(U11(X1, X2)) | → | active#(X1) | | top#(mark(X)) | → | proper#(X) |
| length#(mark(X)) | → | length#(X) | | top#(mark(X)) | → | top#(proper(X)) |
| active#(U22(X1, X2, X3, X4)) | → | U22#(active(X1), X2, X3, X4) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| active#(length(cons(N, L))) | → | U11#(tt, L) | | U23#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U23#(X1, X2, X3, X4) |
| active#(take(X1, X2)) | → | active#(X2) | | U21#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U21#(X1, X2, X3, X4) |
| active#(length(X)) | → | active#(X) | | active#(U21(tt, IL, M, N)) | → | U22#(tt, IL, M, N) |
| take#(X1, mark(X2)) | → | take#(X1, X2) | | active#(U12(X1, X2)) | → | U12#(active(X1), X2) |
| proper#(s(X)) | → | proper#(X) | | U22#(mark(X1), X2, X3, X4) | → | U22#(X1, X2, X3, X4) |
| U23#(mark(X1), X2, X3, X4) | → | U23#(X1, X2, X3, X4) | | proper#(take(X1, X2)) | → | take#(proper(X1), proper(X2)) |
| proper#(U23(X1, X2, X3, X4)) | → | U23#(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper#(U21(X1, X2, X3, X4)) | → | proper#(X1) |
| active#(U21(X1, X2, X3, X4)) | → | U21#(active(X1), X2, X3, X4) | | proper#(U12(X1, X2)) | → | U12#(proper(X1), proper(X2)) |
| proper#(U21(X1, X2, X3, X4)) | → | U21#(proper(X1), proper(X2), proper(X3), proper(X4)) | | active#(cons(X1, X2)) | → | active#(X1) |
| proper#(U23(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(U21(X1, X2, X3, X4)) | → | proper#(X4) |
| take#(mark(X1), X2) | → | take#(X1, X2) | | active#(U22(X1, X2, X3, X4)) | → | active#(X1) |
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | proper#(U23(X1, X2, X3, X4)) | → | proper#(X3) |
| active#(U23(X1, X2, X3, X4)) | → | active#(X1) | | top#(ok(X)) | → | active#(X) |
| U21#(mark(X1), X2, X3, X4) | → | U21#(X1, X2, X3, X4) | | active#(U23(tt, IL, M, N)) | → | take#(M, IL) |
| proper#(U23(X1, X2, X3, X4)) | → | proper#(X1) | | proper#(take(X1, X2)) | → | proper#(X1) |
| active#(U22(tt, IL, M, N)) | → | U23#(tt, IL, M, N) | | proper#(U21(X1, X2, X3, X4)) | → | proper#(X3) |
| take#(ok(X1), ok(X2)) | → | take#(X1, X2) | | proper#(U22(X1, X2, X3, X4)) | → | proper#(X3) |
| proper#(U12(X1, X2)) | → | proper#(X1) | | active#(length(X)) | → | length#(active(X)) |
| active#(U12(tt, L)) | → | length#(L) | | active#(U12(X1, X2)) | → | active#(X1) |
| active#(U23(X1, X2, X3, X4)) | → | U23#(active(X1), X2, X3, X4) | | active#(take(X1, X2)) | → | active#(X1) |
| proper#(take(X1, X2)) | → | proper#(X2) | | U22#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U22#(X1, X2, X3, X4) |
| active#(U11(X1, X2)) | → | U11#(active(X1), X2) | | active#(s(X)) | → | s#(active(X)) |
| proper#(U22(X1, X2, X3, X4)) | → | U22#(proper(X1), proper(X2), proper(X3), proper(X4)) | | s#(ok(X)) | → | s#(X) |
| s#(mark(X)) | → | s#(X) | | active#(U12(tt, L)) | → | s#(length(L)) |
| proper#(length(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) |
| active#(take(X1, X2)) | → | take#(X1, active(X2)) | | active#(take(s(M), cons(N, IL))) | → | U21#(tt, IL, M, N) |
| active#(s(X)) | → | active#(X) | | proper#(s(X)) | → | s#(proper(X)) |
| active#(zeros) | → | cons#(0, zeros) | | proper#(U23(X1, X2, X3, X4)) | → | proper#(X4) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, cons, nil, top
Strategy
The following SCCs where found
| length#(mark(X)) → length#(X) | length#(ok(X)) → length#(X) |
| cons#(mark(X1), X2) → cons#(X1, X2) | cons#(ok(X1), ok(X2)) → cons#(X1, X2) |
| proper#(U23(X1, X2, X3, X4)) → proper#(X2) | proper#(U12(X1, X2)) → proper#(X1) |
| proper#(U22(X1, X2, X3, X4)) → proper#(X1) | proper#(cons(X1, X2)) → proper#(X1) |
| proper#(U21(X1, X2, X3, X4)) → proper#(X4) | proper#(U11(X1, X2)) → proper#(X1) |
| proper#(U22(X1, X2, X3, X4)) → proper#(X2) | proper#(cons(X1, X2)) → proper#(X2) |
| proper#(U23(X1, X2, X3, X4)) → proper#(X3) | proper#(take(X1, X2)) → proper#(X2) |
| proper#(U12(X1, X2)) → proper#(X2) | proper#(length(X)) → proper#(X) |
| proper#(s(X)) → proper#(X) | proper#(U11(X1, X2)) → proper#(X2) |
| proper#(U21(X1, X2, X3, X4)) → proper#(X2) | proper#(U23(X1, X2, X3, X4)) → proper#(X1) |
| proper#(take(X1, X2)) → proper#(X1) | proper#(U22(X1, X2, X3, X4)) → proper#(X4) |
| proper#(U23(X1, X2, X3, X4)) → proper#(X4) | proper#(U21(X1, X2, X3, X4)) → proper#(X3) |
| proper#(U21(X1, X2, X3, X4)) → proper#(X1) | proper#(U22(X1, X2, X3, X4)) → proper#(X3) |
| U12#(ok(X1), ok(X2)) → U12#(X1, X2) | U12#(mark(X1), X2) → U12#(X1, X2) |
| U11#(ok(X1), ok(X2)) → U11#(X1, X2) | U11#(mark(X1), X2) → U11#(X1, X2) |
| U23#(ok(X1), ok(X2), ok(X3), ok(X4)) → U23#(X1, X2, X3, X4) | U23#(mark(X1), X2, X3, X4) → U23#(X1, X2, X3, X4) |
| U21#(ok(X1), ok(X2), ok(X3), ok(X4)) → U21#(X1, X2, X3, X4) | U21#(mark(X1), X2, X3, X4) → U21#(X1, X2, X3, X4) |
| U22#(mark(X1), X2, X3, X4) → U22#(X1, X2, X3, X4) | U22#(ok(X1), ok(X2), ok(X3), ok(X4)) → U22#(X1, X2, X3, X4) |
| take#(mark(X1), X2) → take#(X1, X2) | take#(X1, mark(X2)) → take#(X1, X2) |
| take#(ok(X1), ok(X2)) → take#(X1, X2) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
| s#(mark(X)) → s#(X) | s#(ok(X)) → s#(X) |
| active#(U21(X1, X2, X3, X4)) → active#(X1) | active#(U12(X1, X2)) → active#(X1) |
| active#(U22(X1, X2, X3, X4)) → active#(X1) | active#(s(X)) → active#(X) |
| active#(take(X1, X2)) → active#(X2) | active#(take(X1, X2)) → active#(X1) |
| active#(length(X)) → active#(X) | active#(U23(X1, X2, X3, X4)) → active#(X1) |
| active#(U11(X1, X2)) → active#(X1) | active#(cons(X1, X2)) → active#(X1) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U21#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U21#(X1, X2, X3, X4) | | U21#(mark(X1), X2, X3, X4) | → | U21#(X1, X2, X3, X4) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U21#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U21#(X1, X2, X3, X4) | | U21#(mark(X1), X2, X3, X4) | → | U21#(X1, X2, X3, X4) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U23#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U23#(X1, X2, X3, X4) | | U23#(mark(X1), X2, X3, X4) | → | U23#(X1, X2, X3, X4) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U23#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U23#(X1, X2, X3, X4) | | U23#(mark(X1), X2, X3, X4) | → | U23#(X1, X2, X3, X4) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| length#(mark(X)) | → | length#(X) | | length#(ok(X)) | → | length#(X) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| length#(mark(X)) | → | length#(X) | | length#(ok(X)) | → | length#(X) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, 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 6: 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(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, 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 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U11#(ok(X1), ok(X2)) | → | U11#(X1, X2) | | U11#(mark(X1), X2) | → | U11#(X1, X2) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U11#(ok(X1), ok(X2)) | → | U11#(X1, X2) | | U11#(mark(X1), X2) | → | U11#(X1, X2) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(U23(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(U21(X1, X2, X3, X4)) | → | proper#(X4) |
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(U22(X1, X2, X3, X4)) | → | proper#(X1) |
| proper#(U12(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(U22(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(U11(X1, X2)) | → | proper#(X1) |
| proper#(U23(X1, X2, X3, X4)) | → | proper#(X3) | | proper#(take(X1, X2)) | → | proper#(X2) |
| proper#(U12(X1, X2)) | → | proper#(X2) | | proper#(s(X)) | → | proper#(X) |
| proper#(length(X)) | → | proper#(X) | | proper#(U11(X1, X2)) | → | proper#(X2) |
| proper#(U21(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(U23(X1, X2, X3, X4)) | → | proper#(X1) |
| proper#(take(X1, X2)) | → | proper#(X1) | | proper#(U22(X1, X2, X3, X4)) | → | proper#(X4) |
| proper#(U23(X1, X2, X3, X4)) | → | proper#(X4) | | proper#(U21(X1, X2, X3, X4)) | → | proper#(X3) |
| proper#(U21(X1, X2, X3, X4)) | → | proper#(X1) | | proper#(U22(X1, X2, X3, X4)) | → | proper#(X3) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(U23(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(U21(X1, X2, X3, X4)) | → | proper#(X4) |
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(U22(X1, X2, X3, X4)) | → | proper#(X1) |
| proper#(U12(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(U22(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(U11(X1, X2)) | → | proper#(X1) |
| proper#(U23(X1, X2, X3, X4)) | → | proper#(X3) | | proper#(take(X1, X2)) | → | proper#(X2) |
| proper#(U12(X1, X2)) | → | proper#(X2) | | proper#(length(X)) | → | proper#(X) |
| proper#(s(X)) | → | proper#(X) | | proper#(U11(X1, X2)) | → | proper#(X2) |
| proper#(U23(X1, X2, X3, X4)) | → | proper#(X1) | | proper#(take(X1, X2)) | → | proper#(X1) |
| proper#(U21(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(U22(X1, X2, X3, X4)) | → | proper#(X4) |
| proper#(U23(X1, X2, X3, X4)) | → | proper#(X4) | | proper#(U21(X1, X2, X3, X4)) | → | proper#(X3) |
| proper#(U21(X1, X2, X3, X4)) | → | proper#(X1) | | proper#(U22(X1, X2, X3, X4)) | → | proper#(X3) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(U21(X1, X2, X3, X4)) | → | active#(X1) | | active#(U12(X1, X2)) | → | active#(X1) |
| active#(U22(X1, X2, X3, X4)) | → | active#(X1) | | active#(s(X)) | → | active#(X) |
| active#(take(X1, X2)) | → | active#(X2) | | active#(take(X1, X2)) | → | active#(X1) |
| active#(length(X)) | → | active#(X) | | active#(U23(X1, X2, X3, X4)) | → | active#(X1) |
| active#(U11(X1, X2)) | → | active#(X1) | | active#(cons(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(U12(X1, X2)) | → | active#(X1) | | active#(U21(X1, X2, X3, X4)) | → | active#(X1) |
| active#(s(X)) | → | active#(X) | | active#(U22(X1, X2, X3, X4)) | → | active#(X1) |
| active#(take(X1, X2)) | → | active#(X2) | | active#(take(X1, X2)) | → | active#(X1) |
| active#(length(X)) | → | active#(X) | | active#(U23(X1, X2, X3, X4)) | → | active#(X1) |
| active#(U11(X1, X2)) | → | active#(X1) | | active#(cons(X1, X2)) | → | active#(X1) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(ok(X)) | → | s#(X) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, 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 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(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, 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: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U22#(mark(X1), X2, X3, X4) | → | U22#(X1, X2, X3, X4) | | U22#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U22#(X1, X2, X3, X4) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(U12(tt, L)) |
| active(U12(tt, L)) | → | mark(s(length(L))) | | active(U21(tt, IL, M, N)) | → | mark(U22(tt, IL, M, N)) |
| active(U22(tt, IL, M, N)) | → | mark(U23(tt, IL, M, N)) | | active(U23(tt, IL, M, N)) | → | mark(cons(N, take(M, IL))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(N, L))) | → | mark(U11(tt, L)) |
| active(take(0, IL)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(U21(tt, IL, M, N)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(U11(X1, X2)) | → | U11(active(X1), X2) |
| active(U12(X1, X2)) | → | U12(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(U21(X1, X2, X3, X4)) | → | U21(active(X1), X2, X3, X4) |
| active(U22(X1, X2, X3, X4)) | → | U22(active(X1), X2, X3, X4) | | active(U23(X1, X2, X3, X4)) | → | U23(active(X1), X2, X3, X4) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| U12(mark(X1), X2) | → | mark(U12(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | U21(mark(X1), X2, X3, X4) | → | mark(U21(X1, X2, X3, X4)) |
| U22(mark(X1), X2, X3, X4) | → | mark(U22(X1, X2, X3, X4)) | | U23(mark(X1), X2, X3, X4) | → | mark(U23(X1, X2, X3, X4)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(U11(X1, X2)) | → | U11(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(U12(X1, X2)) | → | U12(proper(X1), proper(X2)) |
| proper(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(U21(X1, X2, X3, X4)) | → | U21(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(U22(X1, X2, X3, X4)) | → | U22(proper(X1), proper(X2), proper(X3), proper(X4)) |
| proper(U23(X1, X2, X3, X4)) | → | U23(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | U12(ok(X1), ok(X2)) | → | ok(U12(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| U21(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U21(X1, X2, X3, X4)) | | U22(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U22(X1, X2, X3, X4)) |
| U23(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(U23(X1, X2, X3, X4)) | | 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: mark, 0, s, zeros, tt, take, length, active, U11, ok, U12, proper, U23, U21, U22, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U22#(mark(X1), X2, X3, X4) | → | U22#(X1, X2, X3, X4) | | U22#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | U22#(X1, X2, X3, X4) |