TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60017 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (10107ms).
| – Problem 2 was processed with processor SubtermCriterion (5ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| | – Problem 16 was processed with processor PolynomialLinearRange4iUR (49ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| – Problem 5 was processed with processor SubtermCriterion (2ms).
| – Problem 6 remains open; application of the following processors failed [SubtermCriterion (3ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (3342ms), DependencyGraph (26ms), PolynomialLinearRange4iUR (9411ms), DependencyGraph (6ms), PolynomialLinearRange8NegiUR (30001ms), DependencyGraph (timeout), ReductionPairSAT (timeout)].
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor SubtermCriterion (2ms).
| – Problem 9 was processed with processor SubtermCriterion (1ms).
| – Problem 10 was processed with processor SubtermCriterion (3ms).
| – Problem 11 was processed with processor SubtermCriterion (2ms).
| | – Problem 17 was processed with processor PolynomialLinearRange4iUR (78ms).
| – Problem 12 was processed with processor SubtermCriterion (1ms).
| – Problem 13 was processed with processor SubtermCriterion (2ms).
| – Problem 14 was processed with processor SubtermCriterion (4ms).
| – Problem 15 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 6
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(X)) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, top, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(length(X)) | → | length#(proper(X)) |
| uTake1#(mark(X)) | → | uTake1#(X) | | active#(take(s(M), cons(N, IL))) | → | and#(isNat(M), and(isNat(N), isNatIList(IL))) |
| active#(uTake2(tt, M, N, IL)) | → | cons#(N, take(M, IL)) | | active#(uTake2(X1, X2, X3, X4)) | → | uTake2#(active(X1), X2, X3, X4) |
| uTake2#(mark(X1), X2, X3, X4) | → | uTake2#(X1, X2, X3, X4) | | active#(take(X1, X2)) | → | take#(active(X1), X2) |
| active#(uLength(X1, X2)) | → | active#(X1) | | top#(mark(X)) | → | proper#(X) |
| proper#(uLength(X1, X2)) | → | uLength#(proper(X1), proper(X2)) | | proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X4) |
| length#(mark(X)) | → | length#(X) | | proper#(uTake2(X1, X2, X3, X4)) | → | uTake2#(proper(X1), proper(X2), proper(X3), proper(X4)) |
| active#(take(X1, X2)) | → | active#(X2) | | active#(length(cons(N, L))) | → | and#(isNat(N), isNatList(L)) |
| active#(length(X)) | → | active#(X) | | isNat#(ok(X)) | → | isNat#(X) |
| and#(mark(X1), X2) | → | and#(X1, X2) | | active#(uTake1(X)) | → | uTake1#(active(X)) |
| isNatIList#(ok(X)) | → | isNatIList#(X) | | active#(take(s(M), cons(N, IL))) | → | isNat#(M) |
| active#(isNatIList(cons(N, IL))) | → | and#(isNat(N), isNatIList(IL)) | | active#(take(s(M), cons(N, IL))) | → | uTake2#(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL) |
| proper#(uTake1(X)) | → | proper#(X) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| active#(take(s(M), cons(N, IL))) | → | isNat#(N) | | top#(ok(X)) | → | active#(X) |
| active#(and(X1, X2)) | → | and#(active(X1), X2) | | active#(isNatList(take(N, IL))) | → | isNatIList#(IL) |
| active#(isNatIList(IL)) | → | isNatList#(IL) | | proper#(isNatList(X)) | → | proper#(X) |
| proper#(isNat(X)) | → | isNat#(proper(X)) | | take#(ok(X1), ok(X2)) | → | take#(X1, X2) |
| active#(uTake2(tt, M, N, IL)) | → | take#(M, IL) | | active#(and(X1, X2)) | → | active#(X2) |
| proper#(isNat(X)) | → | proper#(X) | | uLength#(mark(X1), X2) | → | uLength#(X1, X2) |
| active#(uTake1(X)) | → | active#(X) | | active#(s(X)) | → | s#(active(X)) |
| s#(ok(X)) | → | s#(X) | | proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X3) |
| active#(isNatList(cons(N, L))) | → | isNat#(N) | | proper#(length(X)) | → | proper#(X) |
| active#(take(X1, X2)) | → | take#(X1, active(X2)) | | proper#(s(X)) | → | s#(proper(X)) |
| active#(zeros) | → | cons#(0, zeros) | | top#(ok(X)) | → | top#(active(X)) |
| active#(take(s(M), cons(N, IL))) | → | isNatIList#(IL) | | proper#(isNatIList(X)) | → | isNatIList#(proper(X)) |
| proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
| proper#(and(X1, X2)) | → | and#(proper(X1), proper(X2)) | | active#(cons(X1, X2)) | → | cons#(active(X1), X2) |
| active#(uLength(X1, X2)) | → | uLength#(active(X1), X2) | | proper#(and(X1, X2)) | → | proper#(X2) |
| active#(isNat(s(N))) | → | isNat#(N) | | uTake2#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | uTake2#(X1, X2, X3, X4) |
| active#(isNatIList(cons(N, IL))) | → | isNat#(N) | | length#(ok(X)) | → | length#(X) |
| active#(length(cons(N, L))) | → | uLength#(and(isNat(N), isNatList(L)), L) | | active#(and(X1, X2)) | → | and#(X1, active(X2)) |
| top#(mark(X)) | → | top#(proper(X)) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| active#(isNatIList(cons(N, IL))) | → | isNatIList#(IL) | | proper#(isNatIList(X)) | → | proper#(X) |
| active#(uLength(tt, L)) | → | length#(L) | | take#(X1, mark(X2)) | → | take#(X1, X2) |
| isNatList#(ok(X)) | → | isNatList#(X) | | proper#(uLength(X1, X2)) | → | proper#(X1) |
| proper#(s(X)) | → | proper#(X) | | active#(isNatList(take(N, IL))) | → | isNat#(N) |
| active#(isNatList(cons(N, L))) | → | and#(isNat(N), isNatList(L)) | | proper#(isNatList(X)) | → | isNatList#(proper(X)) |
| proper#(take(X1, X2)) | → | take#(proper(X1), proper(X2)) | | active#(isNatList(cons(N, L))) | → | isNatList#(L) |
| active#(cons(X1, X2)) | → | active#(X1) | | take#(mark(X1), X2) | → | take#(X1, X2) |
| proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X1) | | and#(ok(X1), ok(X2)) | → | and#(X1, X2) |
| active#(isNat(length(L))) | → | isNatList#(L) | | proper#(and(X1, X2)) | → | proper#(X1) |
| active#(length(cons(N, L))) | → | isNatList#(L) | | active#(take(s(M), cons(N, IL))) | → | and#(isNat(N), isNatIList(IL)) |
| proper#(take(X1, X2)) | → | proper#(X1) | | active#(length(cons(N, L))) | → | isNat#(N) |
| active#(take(0, IL)) | → | uTake1#(isNatIList(IL)) | | proper#(uLength(X1, X2)) | → | proper#(X2) |
| and#(X1, mark(X2)) | → | and#(X1, X2) | | active#(length(X)) | → | length#(active(X)) |
| active#(isNatList(take(N, IL))) | → | and#(isNat(N), isNatIList(IL)) | | active#(take(X1, X2)) | → | active#(X1) |
| proper#(take(X1, X2)) | → | proper#(X2) | | active#(uTake2(X1, X2, X3, X4)) | → | active#(X1) |
| s#(mark(X)) | → | s#(X) | | uTake1#(ok(X)) | → | uTake1#(X) |
| proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) | | proper#(uTake1(X)) | → | uTake1#(proper(X)) |
| active#(uLength(tt, L)) | → | s#(length(L)) | | active#(s(X)) | → | active#(X) |
| active#(and(X1, X2)) | → | active#(X1) | | uLength#(ok(X1), ok(X2)) | → | uLength#(X1, X2) |
| active#(take(0, IL)) | → | isNatIList#(IL) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
The following SCCs where found
| and#(ok(X1), ok(X2)) → and#(X1, X2) | and#(mark(X1), X2) → and#(X1, X2) |
| and#(X1, mark(X2)) → and#(X1, X2) |
| uTake2#(mark(X1), X2, X3, X4) → uTake2#(X1, X2, X3, X4) | uTake2#(ok(X1), ok(X2), ok(X3), ok(X4)) → uTake2#(X1, X2, X3, X4) |
| isNat#(ok(X)) → isNat#(X) |
| take#(mark(X1), X2) → take#(X1, X2) | take#(X1, mark(X2)) → take#(X1, X2) |
| take#(ok(X1), ok(X2)) → take#(X1, X2) |
| isNatList#(ok(X)) → isNatList#(X) |
| s#(mark(X)) → s#(X) | s#(ok(X)) → s#(X) |
| isNatIList#(ok(X)) → isNatIList#(X) |
| cons#(mark(X1), X2) → cons#(X1, X2) | cons#(ok(X1), ok(X2)) → cons#(X1, X2) |
| length#(mark(X)) → length#(X) | length#(ok(X)) → length#(X) |
| active#(uLength(X1, X2)) → active#(X1) | active#(s(X)) → active#(X) |
| active#(uTake1(X)) → active#(X) | active#(take(X1, X2)) → active#(X2) |
| active#(take(X1, X2)) → active#(X1) | active#(length(X)) → active#(X) |
| active#(and(X1, X2)) → active#(X1) | active#(and(X1, X2)) → active#(X2) |
| active#(cons(X1, X2)) → active#(X1) | active#(uTake2(X1, X2, X3, X4)) → active#(X1) |
| uTake1#(ok(X)) → uTake1#(X) | uTake1#(mark(X)) → uTake1#(X) |
| uLength#(mark(X1), X2) → uLength#(X1, X2) | uLength#(ok(X1), ok(X2)) → uLength#(X1, X2) |
| proper#(uTake2(X1, X2, X3, X4)) → proper#(X4) | proper#(uTake1(X)) → proper#(X) |
| proper#(cons(X1, X2)) → proper#(X1) | proper#(isNat(X)) → proper#(X) |
| proper#(cons(X1, X2)) → proper#(X2) | proper#(isNatIList(X)) → proper#(X) |
| proper#(take(X1, X2)) → proper#(X2) | proper#(uTake2(X1, X2, X3, X4)) → proper#(X1) |
| proper#(uTake2(X1, X2, X3, X4)) → proper#(X2) | proper#(and(X1, X2)) → proper#(X1) |
| proper#(uTake2(X1, X2, X3, X4)) → proper#(X3) | proper#(uLength(X1, X2)) → proper#(X1) |
| proper#(length(X)) → proper#(X) | proper#(s(X)) → proper#(X) |
| proper#(and(X1, X2)) → proper#(X2) | proper#(take(X1, X2)) → proper#(X1) |
| proper#(isNatList(X)) → proper#(X) | proper#(uLength(X1, X2)) → proper#(X2) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isNat#(ok(X)) | → | isNat#(X) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isNat#(ok(X)) | → | isNat#(X) |
Problem 3: 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(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| take#(mark(X1), X2) | → | take#(X1, X2) | | take#(ok(X1), ok(X2)) | → | take#(X1, X2) |
Problem 16: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| take#(X1, mark(X2)) | → | take#(X1, X2) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, top, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 0
- and(x,y): 0
- cons(x,y): 0
- isNat(x): 0
- isNatIList(x): 0
- isNatList(x): 0
- length(x): 0
- mark(x): x + 2
- nil: 0
- ok(x): 0
- proper(x): 0
- s(x): 0
- take(x,y): 0
- take#(x,y): y + x + 1
- top(x): 0
- tt: 0
- uLength(x,y): 0
- uTake1(x): 0
- uTake2(x1,x2,x3,x4): 0
- zeros: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| take#(X1, mark(X2)) | → | take#(X1, X2) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X4) | | proper#(uTake1(X)) | → | proper#(X) |
| proper#(isNat(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(isNatIList(X)) | → | proper#(X) |
| proper#(take(X1, X2)) | → | proper#(X2) | | proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X2) |
| proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X1) | | proper#(and(X1, X2)) | → | proper#(X1) |
| proper#(uLength(X1, X2)) | → | proper#(X1) | | proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X3) |
| proper#(length(X)) | → | proper#(X) | | proper#(s(X)) | → | proper#(X) |
| proper#(and(X1, X2)) | → | proper#(X2) | | proper#(take(X1, X2)) | → | proper#(X1) |
| proper#(isNatList(X)) | → | proper#(X) | | proper#(uLength(X1, X2)) | → | proper#(X2) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X4) | | proper#(uTake1(X)) | → | proper#(X) |
| proper#(isNat(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(isNatIList(X)) | → | proper#(X) |
| proper#(take(X1, X2)) | → | proper#(X2) | | proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X1) |
| proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X2) | | proper#(and(X1, X2)) | → | proper#(X1) |
| proper#(uLength(X1, X2)) | → | proper#(X1) | | proper#(uTake2(X1, X2, X3, X4)) | → | proper#(X3) |
| proper#(s(X)) | → | proper#(X) | | proper#(length(X)) | → | proper#(X) |
| proper#(and(X1, X2)) | → | proper#(X2) | | proper#(take(X1, X2)) | → | proper#(X1) |
| proper#(isNatList(X)) | → | proper#(X) | | proper#(uLength(X1, X2)) | → | proper#(X2) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| uTake2#(mark(X1), X2, X3, X4) | → | uTake2#(X1, X2, X3, X4) | | uTake2#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | uTake2#(X1, X2, X3, X4) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| uTake2#(mark(X1), X2, X3, X4) | → | uTake2#(X1, X2, X3, X4) | | uTake2#(ok(X1), ok(X2), ok(X3), ok(X4)) | → | uTake2#(X1, X2, X3, X4) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isNatIList#(ok(X)) | → | isNatIList#(X) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isNatIList#(ok(X)) | → | isNatIList#(X) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| length#(mark(X)) | → | length#(X) | | length#(ok(X)) | → | length#(X) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, 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 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| uLength#(mark(X1), X2) | → | uLength#(X1, X2) | | uLength#(ok(X1), ok(X2)) | → | uLength#(X1, X2) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| uLength#(mark(X1), X2) | → | uLength#(X1, X2) | | uLength#(ok(X1), ok(X2)) | → | uLength#(X1, X2) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| and#(ok(X1), ok(X2)) | → | and#(X1, X2) | | and#(mark(X1), X2) | → | and#(X1, X2) |
| and#(X1, mark(X2)) | → | and#(X1, X2) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, 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) |
Problem 17: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| and#(X1, mark(X2)) | → | and#(X1, X2) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, top, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 0
- and(x,y): 0
- and#(x,y): y + x
- cons(x,y): 0
- isNat(x): 0
- isNatIList(x): 0
- isNatList(x): 0
- length(x): 0
- mark(x): x + 2
- nil: 0
- ok(x): 0
- proper(x): 0
- s(x): 0
- take(x,y): 0
- top(x): 0
- tt: 0
- uLength(x,y): 0
- uTake1(x): 0
- uTake2(x1,x2,x3,x4): 0
- zeros: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| and#(X1, mark(X2)) | → | and#(X1, X2) |
Problem 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(ok(X)) | → | s#(X) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(ok(X)) | → | s#(X) |
Problem 13: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(uLength(X1, X2)) | → | active#(X1) | | active#(s(X)) | → | active#(X) |
| active#(uTake1(X)) | → | active#(X) | | active#(take(X1, X2)) | → | active#(X2) |
| active#(take(X1, X2)) | → | active#(X1) | | active#(length(X)) | → | active#(X) |
| active#(and(X1, X2)) | → | active#(X1) | | active#(and(X1, X2)) | → | active#(X2) |
| active#(cons(X1, X2)) | → | active#(X1) | | active#(uTake2(X1, X2, X3, X4)) | → | active#(X1) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(uLength(X1, X2)) | → | active#(X1) | | active#(s(X)) | → | active#(X) |
| active#(uTake1(X)) | → | active#(X) | | active#(take(X1, X2)) | → | active#(X2) |
| active#(length(X)) | → | active#(X) | | active#(take(X1, X2)) | → | active#(X1) |
| active#(and(X1, X2)) | → | active#(X1) | | active#(and(X1, X2)) | → | active#(X2) |
| active#(uTake2(X1, X2, X3, X4)) | → | active#(X1) | | active#(cons(X1, X2)) | → | active#(X1) |
Problem 14: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| uTake1#(ok(X)) | → | uTake1#(X) | | uTake1#(mark(X)) | → | uTake1#(X) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| uTake1#(ok(X)) | → | uTake1#(X) | | uTake1#(mark(X)) | → | uTake1#(X) |
Problem 15: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isNatList#(ok(X)) | → | isNatList#(X) |
Rewrite Rules
| active(and(tt, T)) | → | mark(T) | | active(isNatIList(IL)) | → | mark(isNatList(IL)) |
| active(isNat(0)) | → | mark(tt) | | active(isNat(s(N))) | → | mark(isNat(N)) |
| active(isNat(length(L))) | → | mark(isNatList(L)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(N, L))) | → | mark(and(isNat(N), isNatList(L))) | | active(isNatList(take(N, IL))) | → | mark(and(isNat(N), isNatIList(IL))) |
| active(zeros) | → | mark(cons(0, zeros)) | | active(take(0, IL)) | → | mark(uTake1(isNatIList(IL))) |
| active(uTake1(tt)) | → | mark(nil) | | active(take(s(M), cons(N, IL))) | → | mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)) |
| active(uTake2(tt, M, N, IL)) | → | mark(cons(N, take(M, IL))) | | active(length(cons(N, L))) | → | mark(uLength(and(isNat(N), isNatList(L)), L)) |
| active(uLength(tt, L)) | → | mark(s(length(L))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(and(X1, X2)) | → | and(X1, active(X2)) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(take(X1, X2)) | → | take(active(X1), X2) | | active(take(X1, X2)) | → | take(X1, active(X2)) |
| active(uTake1(X)) | → | uTake1(active(X)) | | active(uTake2(X1, X2, X3, X4)) | → | uTake2(active(X1), X2, X3, X4) |
| active(uLength(X1, X2)) | → | uLength(active(X1), X2) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| and(X1, mark(X2)) | → | mark(and(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| length(mark(X)) | → | mark(length(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| take(mark(X1), X2) | → | mark(take(X1, X2)) | | take(X1, mark(X2)) | → | mark(take(X1, X2)) |
| uTake1(mark(X)) | → | mark(uTake1(X)) | | uTake2(mark(X1), X2, X3, X4) | → | mark(uTake2(X1, X2, X3, X4)) |
| uLength(mark(X1), X2) | → | mark(uLength(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(tt) | → | ok(tt) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(length(X)) | → | length(proper(X)) | | proper(zeros) | → | ok(zeros) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) | | proper(uTake1(X)) | → | uTake1(proper(X)) |
| proper(uTake2(X1, X2, X3, X4)) | → | uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) | | proper(uLength(X1, X2)) | → | uLength(proper(X1), proper(X2)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | isNatIList(ok(X)) | → | ok(isNatIList(X)) |
| isNatList(ok(X)) | → | ok(isNatList(X)) | | isNat(ok(X)) | → | ok(isNat(X)) |
| s(ok(X)) | → | ok(s(X)) | | length(ok(X)) | → | ok(length(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) |
| uTake1(ok(X)) | → | ok(uTake1(X)) | | uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) | → | ok(uTake2(X1, X2, X3, X4)) |
| uLength(ok(X1), ok(X2)) | → | ok(uLength(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: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, ok, proper, nil, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isNatList#(ok(X)) | → | isNatList#(X) |