TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (2780ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| – Problem 3 was processed with processor SubtermCriterion (3ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (4810ms), DependencyGraph (26ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (5ms), ReductionPairSAT (8077ms), DependencyGraph (3ms), SizeChangePrinciple (timeout)].
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| – Problem 9 was processed with processor SubtermCriterion (3ms).
| – Problem 10 was processed with processor SubtermCriterion (1ms).
| – Problem 11 was processed with processor SubtermCriterion (1ms).
| – Problem 12 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 7
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(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, top, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(length(X)) | → | length#(proper(X)) |
| top#(ok(X)) | → | top#(active(X)) | | proper#(U11(X1, X2)) | → | proper#(X1) |
| U11#(ok(X1), ok(X2)) | → | U11#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
| proper#(isNatIList(X)) | → | isNatIList#(proper(X)) | | U11#(mark(X1), X2) | → | U11#(X1, X2) |
| proper#(U11(X1, X2)) | → | U11#(proper(X1), proper(X2)) | | proper#(and(X1, X2)) | → | and#(proper(X1), proper(X2)) |
| active#(cons(X1, X2)) | → | cons#(active(X1), X2) | | active#(length(cons(N, L))) | → | U11#(and(isNatList(L), isNat(N)), L) |
| proper#(U11(X1, X2)) | → | proper#(X2) | | active#(isNat(length(V1))) | → | isNatList#(V1) |
| proper#(and(X1, X2)) | → | proper#(X2) | | length#(ok(X)) | → | length#(X) |
| active#(isNatList(cons(V1, V2))) | → | isNatList#(V2) | | active#(U11(tt, L)) | → | s#(length(L)) |
| active#(U11(X1, X2)) | → | active#(X1) | | top#(mark(X)) | → | proper#(X) |
| length#(mark(X)) | → | length#(X) | | top#(mark(X)) | → | top#(proper(X)) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(isNatIList(X)) | → | proper#(X) |
| active#(length(X)) | → | active#(X) | | isNat#(ok(X)) | → | isNat#(X) |
| and#(mark(X1), X2) | → | and#(X1, X2) | | isNatList#(ok(X)) | → | isNatList#(X) |
| isNatIList#(ok(X)) | → | isNatIList#(X) | | active#(isNatIList(cons(V1, V2))) | → | isNat#(V1) |
| active#(U11(tt, L)) | → | length#(L) | | proper#(s(X)) | → | proper#(X) |
| proper#(isNatList(X)) | → | isNatList#(proper(X)) | | active#(isNatList(cons(V1, V2))) | → | isNat#(V1) |
| active#(cons(X1, X2)) | → | active#(X1) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| active#(isNatIList(cons(V1, V2))) | → | and#(isNat(V1), isNatIList(V2)) | | and#(ok(X1), ok(X2)) | → | and#(X1, X2) |
| proper#(and(X1, X2)) | → | proper#(X1) | | top#(ok(X)) | → | active#(X) |
| active#(length(cons(N, L))) | → | isNatList#(L) | | active#(and(X1, X2)) | → | and#(active(X1), X2) |
| active#(length(cons(N, L))) | → | isNat#(N) | | proper#(isNatList(X)) | → | proper#(X) |
| proper#(isNat(X)) | → | isNat#(proper(X)) | | active#(isNat(s(V1))) | → | isNat#(V1) |
| active#(isNatIList(cons(V1, V2))) | → | isNatIList#(V2) | | proper#(isNat(X)) | → | proper#(X) |
| active#(length(X)) | → | length#(active(X)) | | active#(isNatList(cons(V1, V2))) | → | and#(isNat(V1), isNatList(V2)) |
| active#(length(cons(N, L))) | → | and#(isNatList(L), isNat(N)) | | active#(U11(X1, X2)) | → | U11#(active(X1), X2) |
| active#(s(X)) | → | s#(active(X)) | | s#(ok(X)) | → | s#(X) |
| active#(isNatIList(V)) | → | isNatList#(V) | | s#(mark(X)) | → | s#(X) |
| proper#(length(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) |
| active#(s(X)) | → | active#(X) | | proper#(s(X)) | → | s#(proper(X)) |
| active#(zeros) | → | cons#(0, zeros) | | active#(and(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top
Strategy
The following SCCs where found
| 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) |
| U11#(ok(X1), ok(X2)) → U11#(X1, X2) | U11#(mark(X1), X2) → U11#(X1, X2) |
| isNat#(ok(X)) → isNat#(X) |
| active#(s(X)) → active#(X) | active#(length(X)) → active#(X) |
| active#(and(X1, X2)) → active#(X1) | active#(U11(X1, X2)) → active#(X1) |
| active#(cons(X1, X2)) → active#(X1) |
| isNatList#(ok(X)) → isNatList#(X) |
| and#(ok(X1), ok(X2)) → and#(X1, X2) | and#(mark(X1), X2) → and#(X1, X2) |
| proper#(length(X)) → proper#(X) | proper#(s(X)) → proper#(X) |
| proper#(isNat(X)) → proper#(X) | proper#(cons(X1, X2)) → proper#(X1) |
| proper#(U11(X1, X2)) → proper#(X2) | proper#(cons(X1, X2)) → proper#(X2) |
| proper#(and(X1, X2)) → proper#(X2) | proper#(U11(X1, X2)) → proper#(X1) |
| proper#(isNatIList(X)) → proper#(X) | proper#(isNatList(X)) → proper#(X) |
| proper#(and(X1, X2)) → proper#(X1) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
| s#(mark(X)) → s#(X) | s#(ok(X)) → s#(X) |
| isNatIList#(ok(X)) → isNatIList#(X) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(s(X)) | → | active#(X) | | active#(length(X)) | → | active#(X) |
| active#(and(X1, X2)) | → | 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(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(s(X)) | → | active#(X) | | active#(length(X)) | → | active#(X) |
| active#(and(X1, X2)) | → | active#(X1) | | active#(U11(X1, X2)) | → | active#(X1) |
| active#(cons(X1, X2)) | → | active#(X1) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isNatList#(ok(X)) | → | isNatList#(X) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isNatList#(ok(X)) | → | isNatList#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isNat#(ok(X)) | → | isNat#(X) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isNat#(ok(X)) | → | isNat#(X) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| and#(ok(X1), ok(X2)) | → | and#(X1, X2) | | and#(mark(X1), X2) | → | and#(X1, X2) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| and#(ok(X1), ok(X2)) | → | and#(X1, X2) | | and#(mark(X1), X2) | → | and#(X1, X2) |
Problem 6: 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(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, 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
| 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(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, 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 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isNatIList#(ok(X)) | → | isNatIList#(X) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isNatIList#(ok(X)) | → | isNatIList#(X) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(length(X)) | → | proper#(X) | | proper#(s(X)) | → | proper#(X) |
| proper#(isNat(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(U11(X1, X2)) | → | proper#(X2) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(and(X1, X2)) | → | proper#(X2) | | proper#(U11(X1, X2)) | → | proper#(X1) |
| proper#(isNatIList(X)) | → | proper#(X) | | proper#(isNatList(X)) | → | proper#(X) |
| proper#(and(X1, X2)) | → | proper#(X1) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(s(X)) | → | proper#(X) | | proper#(length(X)) | → | proper#(X) |
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(isNat(X)) | → | proper#(X) |
| proper#(U11(X1, X2)) | → | proper#(X2) | | proper#(and(X1, X2)) | → | proper#(X2) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(U11(X1, X2)) | → | proper#(X1) |
| proper#(isNatIList(X)) | → | proper#(X) | | proper#(isNatList(X)) | → | proper#(X) |
| proper#(and(X1, X2)) | → | proper#(X1) |
Problem 11: 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(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, 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
| length#(mark(X)) | → | length#(X) | | length#(ok(X)) | → | length#(X) |
Rewrite Rules
| active(zeros) | → | mark(cons(0, zeros)) | | active(U11(tt, L)) | → | mark(s(length(L))) |
| active(and(tt, X)) | → | mark(X) | | active(isNat(0)) | → | mark(tt) |
| active(isNat(length(V1))) | → | mark(isNatList(V1)) | | active(isNat(s(V1))) | → | mark(isNat(V1)) |
| active(isNatIList(V)) | → | mark(isNatList(V)) | | active(isNatIList(zeros)) | → | mark(tt) |
| active(isNatIList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatIList(V2))) | | active(isNatList(nil)) | → | mark(tt) |
| active(isNatList(cons(V1, V2))) | → | mark(and(isNat(V1), isNatList(V2))) | | active(length(nil)) | → | mark(0) |
| active(length(cons(N, L))) | → | mark(U11(and(isNatList(L), isNat(N)), L)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(U11(X1, X2)) | → | U11(active(X1), X2) | | active(s(X)) | → | s(active(X)) |
| active(length(X)) | → | length(active(X)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | U11(mark(X1), X2) | → | mark(U11(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | length(mark(X)) | → | mark(length(X)) |
| and(mark(X1), X2) | → | mark(and(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(s(X)) | → | s(proper(X)) | | proper(length(X)) | → | length(proper(X)) |
| proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) | | proper(isNat(X)) | → | isNat(proper(X)) |
| proper(isNatList(X)) | → | isNatList(proper(X)) | | proper(isNatIList(X)) | → | isNatIList(proper(X)) |
| proper(nil) | → | ok(nil) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| U11(ok(X1), ok(X2)) | → | ok(U11(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| length(ok(X)) | → | ok(length(X)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| isNat(ok(X)) | → | ok(isNat(X)) | | isNatList(ok(X)) | → | ok(isNatList(X)) |
| isNatIList(ok(X)) | → | ok(isNatIList(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, s, isNatList, zeros, tt, length, active, U11, ok, proper, 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) |