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 (874ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (2976ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (2ms), ReductionPairSAT (3019ms), DependencyGraph (44ms), SizeChangePrinciple (timeout)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (3ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (0ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| – Problem 9 was processed with processor SubtermCriterion (1ms).
| – Problem 10 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(X)) |
Rewrite Rules
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(incr(cons(X, Y))) | → | mark(cons(s(X), incr(Y))) | | active(adx(cons(X, Y))) | → | mark(incr(cons(X, adx(Y)))) |
| active(hd(cons(X, Y))) | → | mark(X) | | active(tl(cons(X, Y))) | → | mark(Y) |
| active(adx(X)) | → | adx(active(X)) | | active(incr(X)) | → | incr(active(X)) |
| active(hd(X)) | → | hd(active(X)) | | active(tl(X)) | → | tl(active(X)) |
| adx(mark(X)) | → | mark(adx(X)) | | incr(mark(X)) | → | mark(incr(X)) |
| hd(mark(X)) | → | mark(hd(X)) | | tl(mark(X)) | → | mark(tl(X)) |
| proper(nats) | → | ok(nats) | | proper(adx(X)) | → | adx(proper(X)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(incr(X)) | → | incr(proper(X)) |
| proper(s(X)) | → | s(proper(X)) | | proper(hd(X)) | → | hd(proper(X)) |
| proper(tl(X)) | → | tl(proper(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | incr(ok(X)) | → | ok(incr(X)) |
| s(ok(X)) | → | ok(s(X)) | | hd(ok(X)) | → | ok(hd(X)) |
| tl(ok(X)) | → | ok(tl(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: tl, mark, hd, nats, 0, s, zeros, adx, active, ok, incr, proper, top, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | active#(adx(cons(X, Y))) | → | cons#(X, adx(Y)) |
| active#(adx(X)) | → | active#(X) | | top#(ok(X)) | → | top#(active(X)) |
| active#(incr(cons(X, Y))) | → | cons#(s(X), incr(Y)) | | incr#(ok(X)) | → | incr#(X) |
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) | | tl#(ok(X)) | → | tl#(X) |
| proper#(incr(X)) | → | incr#(proper(X)) | | top#(ok(X)) | → | active#(X) |
| active#(tl(X)) | → | tl#(active(X)) | | proper#(adx(X)) | → | proper#(X) |
| proper#(incr(X)) | → | proper#(X) | | adx#(ok(X)) | → | adx#(X) |
| incr#(mark(X)) | → | incr#(X) | | proper#(hd(X)) | → | proper#(X) |
| active#(tl(X)) | → | active#(X) | | top#(mark(X)) | → | proper#(X) |
| active#(adx(cons(X, Y))) | → | adx#(Y) | | active#(incr(cons(X, Y))) | → | incr#(Y) |
| proper#(hd(X)) | → | hd#(proper(X)) | | top#(mark(X)) | → | top#(proper(X)) |
| active#(incr(X)) | → | active#(X) | | active#(adx(X)) | → | adx#(active(X)) |
| active#(adx(cons(X, Y))) | → | incr#(cons(X, adx(Y))) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| hd#(mark(X)) | → | hd#(X) | | active#(incr(X)) | → | incr#(active(X)) |
| active#(hd(X)) | → | hd#(active(X)) | | s#(ok(X)) | → | s#(X) |
| active#(nats) | → | adx#(zeros) | | proper#(adx(X)) | → | adx#(proper(X)) |
| adx#(mark(X)) | → | adx#(X) | | proper#(s(X)) | → | proper#(X) |
| proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) | | active#(incr(cons(X, Y))) | → | s#(X) |
| tl#(mark(X)) | → | tl#(X) | | proper#(s(X)) | → | s#(proper(X)) |
| active#(hd(X)) | → | active#(X) | | active#(zeros) | → | cons#(0, zeros) |
| proper#(tl(X)) | → | tl#(proper(X)) | | proper#(tl(X)) | → | proper#(X) |
| hd#(ok(X)) | → | hd#(X) |
Rewrite Rules
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(incr(cons(X, Y))) | → | mark(cons(s(X), incr(Y))) | | active(adx(cons(X, Y))) | → | mark(incr(cons(X, adx(Y)))) |
| active(hd(cons(X, Y))) | → | mark(X) | | active(tl(cons(X, Y))) | → | mark(Y) |
| active(adx(X)) | → | adx(active(X)) | | active(incr(X)) | → | incr(active(X)) |
| active(hd(X)) | → | hd(active(X)) | | active(tl(X)) | → | tl(active(X)) |
| adx(mark(X)) | → | mark(adx(X)) | | incr(mark(X)) | → | mark(incr(X)) |
| hd(mark(X)) | → | mark(hd(X)) | | tl(mark(X)) | → | mark(tl(X)) |
| proper(nats) | → | ok(nats) | | proper(adx(X)) | → | adx(proper(X)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(incr(X)) | → | incr(proper(X)) |
| proper(s(X)) | → | s(proper(X)) | | proper(hd(X)) | → | hd(proper(X)) |
| proper(tl(X)) | → | tl(proper(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | incr(ok(X)) | → | ok(incr(X)) |
| s(ok(X)) | → | ok(s(X)) | | hd(ok(X)) | → | ok(hd(X)) |
| tl(ok(X)) | → | ok(tl(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: tl, mark, hd, nats, 0, s, zeros, adx, active, ok, incr, proper, cons, top
Strategy
The following SCCs where found
| tl#(mark(X)) → tl#(X) | tl#(ok(X)) → tl#(X) |
| proper#(s(X)) → proper#(X) | proper#(adx(X)) → proper#(X) |
| proper#(cons(X1, X2)) → proper#(X1) | proper#(cons(X1, X2)) → proper#(X2) |
| proper#(incr(X)) → proper#(X) | proper#(hd(X)) → proper#(X) |
| proper#(tl(X)) → proper#(X) |
| hd#(mark(X)) → hd#(X) | hd#(ok(X)) → hd#(X) |
| active#(incr(X)) → active#(X) | active#(adx(X)) → active#(X) |
| active#(hd(X)) → active#(X) | active#(tl(X)) → active#(X) |
| incr#(ok(X)) → incr#(X) | incr#(mark(X)) → incr#(X) |
| cons#(ok(X1), ok(X2)) → cons#(X1, X2) |
| adx#(mark(X)) → adx#(X) | adx#(ok(X)) → adx#(X) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| incr#(ok(X)) | → | incr#(X) | | incr#(mark(X)) | → | incr#(X) |
Rewrite Rules
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(incr(cons(X, Y))) | → | mark(cons(s(X), incr(Y))) | | active(adx(cons(X, Y))) | → | mark(incr(cons(X, adx(Y)))) |
| active(hd(cons(X, Y))) | → | mark(X) | | active(tl(cons(X, Y))) | → | mark(Y) |
| active(adx(X)) | → | adx(active(X)) | | active(incr(X)) | → | incr(active(X)) |
| active(hd(X)) | → | hd(active(X)) | | active(tl(X)) | → | tl(active(X)) |
| adx(mark(X)) | → | mark(adx(X)) | | incr(mark(X)) | → | mark(incr(X)) |
| hd(mark(X)) | → | mark(hd(X)) | | tl(mark(X)) | → | mark(tl(X)) |
| proper(nats) | → | ok(nats) | | proper(adx(X)) | → | adx(proper(X)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(incr(X)) | → | incr(proper(X)) |
| proper(s(X)) | → | s(proper(X)) | | proper(hd(X)) | → | hd(proper(X)) |
| proper(tl(X)) | → | tl(proper(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | incr(ok(X)) | → | ok(incr(X)) |
| s(ok(X)) | → | ok(s(X)) | | hd(ok(X)) | → | ok(hd(X)) |
| tl(ok(X)) | → | ok(tl(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: tl, mark, hd, nats, 0, s, zeros, adx, active, ok, incr, proper, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| incr#(ok(X)) | → | incr#(X) | | incr#(mark(X)) | → | incr#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(incr(X)) | → | active#(X) | | active#(adx(X)) | → | active#(X) |
| active#(hd(X)) | → | active#(X) | | active#(tl(X)) | → | active#(X) |
Rewrite Rules
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(incr(cons(X, Y))) | → | mark(cons(s(X), incr(Y))) | | active(adx(cons(X, Y))) | → | mark(incr(cons(X, adx(Y)))) |
| active(hd(cons(X, Y))) | → | mark(X) | | active(tl(cons(X, Y))) | → | mark(Y) |
| active(adx(X)) | → | adx(active(X)) | | active(incr(X)) | → | incr(active(X)) |
| active(hd(X)) | → | hd(active(X)) | | active(tl(X)) | → | tl(active(X)) |
| adx(mark(X)) | → | mark(adx(X)) | | incr(mark(X)) | → | mark(incr(X)) |
| hd(mark(X)) | → | mark(hd(X)) | | tl(mark(X)) | → | mark(tl(X)) |
| proper(nats) | → | ok(nats) | | proper(adx(X)) | → | adx(proper(X)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(incr(X)) | → | incr(proper(X)) |
| proper(s(X)) | → | s(proper(X)) | | proper(hd(X)) | → | hd(proper(X)) |
| proper(tl(X)) | → | tl(proper(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | incr(ok(X)) | → | ok(incr(X)) |
| s(ok(X)) | → | ok(s(X)) | | hd(ok(X)) | → | ok(hd(X)) |
| tl(ok(X)) | → | ok(tl(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: tl, mark, hd, nats, 0, s, zeros, adx, active, ok, incr, proper, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(incr(X)) | → | active#(X) | | active#(adx(X)) | → | active#(X) |
| active#(hd(X)) | → | active#(X) | | active#(tl(X)) | → | active#(X) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| adx#(mark(X)) | → | adx#(X) | | adx#(ok(X)) | → | adx#(X) |
Rewrite Rules
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(incr(cons(X, Y))) | → | mark(cons(s(X), incr(Y))) | | active(adx(cons(X, Y))) | → | mark(incr(cons(X, adx(Y)))) |
| active(hd(cons(X, Y))) | → | mark(X) | | active(tl(cons(X, Y))) | → | mark(Y) |
| active(adx(X)) | → | adx(active(X)) | | active(incr(X)) | → | incr(active(X)) |
| active(hd(X)) | → | hd(active(X)) | | active(tl(X)) | → | tl(active(X)) |
| adx(mark(X)) | → | mark(adx(X)) | | incr(mark(X)) | → | mark(incr(X)) |
| hd(mark(X)) | → | mark(hd(X)) | | tl(mark(X)) | → | mark(tl(X)) |
| proper(nats) | → | ok(nats) | | proper(adx(X)) | → | adx(proper(X)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(incr(X)) | → | incr(proper(X)) |
| proper(s(X)) | → | s(proper(X)) | | proper(hd(X)) | → | hd(proper(X)) |
| proper(tl(X)) | → | tl(proper(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | incr(ok(X)) | → | ok(incr(X)) |
| s(ok(X)) | → | ok(s(X)) | | hd(ok(X)) | → | ok(hd(X)) |
| tl(ok(X)) | → | ok(tl(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: tl, mark, hd, nats, 0, s, zeros, adx, active, ok, incr, proper, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| adx#(mark(X)) | → | adx#(X) | | adx#(ok(X)) | → | adx#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| hd#(mark(X)) | → | hd#(X) | | hd#(ok(X)) | → | hd#(X) |
Rewrite Rules
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(incr(cons(X, Y))) | → | mark(cons(s(X), incr(Y))) | | active(adx(cons(X, Y))) | → | mark(incr(cons(X, adx(Y)))) |
| active(hd(cons(X, Y))) | → | mark(X) | | active(tl(cons(X, Y))) | → | mark(Y) |
| active(adx(X)) | → | adx(active(X)) | | active(incr(X)) | → | incr(active(X)) |
| active(hd(X)) | → | hd(active(X)) | | active(tl(X)) | → | tl(active(X)) |
| adx(mark(X)) | → | mark(adx(X)) | | incr(mark(X)) | → | mark(incr(X)) |
| hd(mark(X)) | → | mark(hd(X)) | | tl(mark(X)) | → | mark(tl(X)) |
| proper(nats) | → | ok(nats) | | proper(adx(X)) | → | adx(proper(X)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(incr(X)) | → | incr(proper(X)) |
| proper(s(X)) | → | s(proper(X)) | | proper(hd(X)) | → | hd(proper(X)) |
| proper(tl(X)) | → | tl(proper(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | incr(ok(X)) | → | ok(incr(X)) |
| s(ok(X)) | → | ok(s(X)) | | hd(ok(X)) | → | ok(hd(X)) |
| tl(ok(X)) | → | ok(tl(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: tl, mark, hd, nats, 0, s, zeros, adx, active, ok, incr, proper, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| hd#(mark(X)) | → | hd#(X) | | hd#(ok(X)) | → | hd#(X) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| tl#(mark(X)) | → | tl#(X) | | tl#(ok(X)) | → | tl#(X) |
Rewrite Rules
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(incr(cons(X, Y))) | → | mark(cons(s(X), incr(Y))) | | active(adx(cons(X, Y))) | → | mark(incr(cons(X, adx(Y)))) |
| active(hd(cons(X, Y))) | → | mark(X) | | active(tl(cons(X, Y))) | → | mark(Y) |
| active(adx(X)) | → | adx(active(X)) | | active(incr(X)) | → | incr(active(X)) |
| active(hd(X)) | → | hd(active(X)) | | active(tl(X)) | → | tl(active(X)) |
| adx(mark(X)) | → | mark(adx(X)) | | incr(mark(X)) | → | mark(incr(X)) |
| hd(mark(X)) | → | mark(hd(X)) | | tl(mark(X)) | → | mark(tl(X)) |
| proper(nats) | → | ok(nats) | | proper(adx(X)) | → | adx(proper(X)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(incr(X)) | → | incr(proper(X)) |
| proper(s(X)) | → | s(proper(X)) | | proper(hd(X)) | → | hd(proper(X)) |
| proper(tl(X)) | → | tl(proper(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | incr(ok(X)) | → | ok(incr(X)) |
| s(ok(X)) | → | ok(s(X)) | | hd(ok(X)) | → | ok(hd(X)) |
| tl(ok(X)) | → | ok(tl(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: tl, mark, hd, nats, 0, s, zeros, adx, active, ok, incr, proper, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| tl#(mark(X)) | → | tl#(X) | | tl#(ok(X)) | → | tl#(X) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(incr(cons(X, Y))) | → | mark(cons(s(X), incr(Y))) | | active(adx(cons(X, Y))) | → | mark(incr(cons(X, adx(Y)))) |
| active(hd(cons(X, Y))) | → | mark(X) | | active(tl(cons(X, Y))) | → | mark(Y) |
| active(adx(X)) | → | adx(active(X)) | | active(incr(X)) | → | incr(active(X)) |
| active(hd(X)) | → | hd(active(X)) | | active(tl(X)) | → | tl(active(X)) |
| adx(mark(X)) | → | mark(adx(X)) | | incr(mark(X)) | → | mark(incr(X)) |
| hd(mark(X)) | → | mark(hd(X)) | | tl(mark(X)) | → | mark(tl(X)) |
| proper(nats) | → | ok(nats) | | proper(adx(X)) | → | adx(proper(X)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(incr(X)) | → | incr(proper(X)) |
| proper(s(X)) | → | s(proper(X)) | | proper(hd(X)) | → | hd(proper(X)) |
| proper(tl(X)) | → | tl(proper(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | incr(ok(X)) | → | ok(incr(X)) |
| s(ok(X)) | → | ok(s(X)) | | hd(ok(X)) | → | ok(hd(X)) |
| tl(ok(X)) | → | ok(tl(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: tl, mark, hd, nats, 0, s, zeros, adx, active, ok, incr, proper, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(incr(cons(X, Y))) | → | mark(cons(s(X), incr(Y))) | | active(adx(cons(X, Y))) | → | mark(incr(cons(X, adx(Y)))) |
| active(hd(cons(X, Y))) | → | mark(X) | | active(tl(cons(X, Y))) | → | mark(Y) |
| active(adx(X)) | → | adx(active(X)) | | active(incr(X)) | → | incr(active(X)) |
| active(hd(X)) | → | hd(active(X)) | | active(tl(X)) | → | tl(active(X)) |
| adx(mark(X)) | → | mark(adx(X)) | | incr(mark(X)) | → | mark(incr(X)) |
| hd(mark(X)) | → | mark(hd(X)) | | tl(mark(X)) | → | mark(tl(X)) |
| proper(nats) | → | ok(nats) | | proper(adx(X)) | → | adx(proper(X)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(incr(X)) | → | incr(proper(X)) |
| proper(s(X)) | → | s(proper(X)) | | proper(hd(X)) | → | hd(proper(X)) |
| proper(tl(X)) | → | tl(proper(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | incr(ok(X)) | → | ok(incr(X)) |
| s(ok(X)) | → | ok(s(X)) | | hd(ok(X)) | → | ok(hd(X)) |
| tl(ok(X)) | → | ok(tl(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: tl, mark, hd, nats, 0, s, zeros, adx, active, ok, incr, proper, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(s(X)) | → | proper#(X) | | proper#(adx(X)) | → | proper#(X) |
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(incr(X)) | → | proper#(X) | | proper#(hd(X)) | → | proper#(X) |
| proper#(tl(X)) | → | proper#(X) |
Rewrite Rules
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(incr(cons(X, Y))) | → | mark(cons(s(X), incr(Y))) | | active(adx(cons(X, Y))) | → | mark(incr(cons(X, adx(Y)))) |
| active(hd(cons(X, Y))) | → | mark(X) | | active(tl(cons(X, Y))) | → | mark(Y) |
| active(adx(X)) | → | adx(active(X)) | | active(incr(X)) | → | incr(active(X)) |
| active(hd(X)) | → | hd(active(X)) | | active(tl(X)) | → | tl(active(X)) |
| adx(mark(X)) | → | mark(adx(X)) | | incr(mark(X)) | → | mark(incr(X)) |
| hd(mark(X)) | → | mark(hd(X)) | | tl(mark(X)) | → | mark(tl(X)) |
| proper(nats) | → | ok(nats) | | proper(adx(X)) | → | adx(proper(X)) |
| proper(zeros) | → | ok(zeros) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(incr(X)) | → | incr(proper(X)) |
| proper(s(X)) | → | s(proper(X)) | | proper(hd(X)) | → | hd(proper(X)) |
| proper(tl(X)) | → | tl(proper(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | incr(ok(X)) | → | ok(incr(X)) |
| s(ok(X)) | → | ok(s(X)) | | hd(ok(X)) | → | ok(hd(X)) |
| tl(ok(X)) | → | ok(tl(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: tl, mark, hd, nats, 0, s, zeros, adx, active, ok, incr, proper, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(adx(X)) | → | proper#(X) | | proper#(s(X)) | → | proper#(X) |
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(incr(X)) | → | proper#(X) | | proper#(hd(X)) | → | proper#(X) |
| proper#(tl(X)) | → | proper#(X) |