TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60164 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1354ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (4ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (3661ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (3ms), ReductionPairSAT (4885ms), DependencyGraph (3ms), SizeChangePrinciple (timeout)].
| – Problem 3 was processed with processor SubtermCriterion (2ms).
| – Problem 4 was processed with processor SubtermCriterion (0ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| – Problem 9 was processed with processor SubtermCriterion (2ms).
| – 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(incr(nil)) | → | mark(nil) | | active(incr(cons(X, L))) | → | mark(cons(s(X), incr(L))) |
| active(adx(nil)) | → | mark(nil) | | active(adx(cons(X, L))) | → | mark(incr(cons(X, adx(L)))) |
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(head(cons(X, L))) | → | mark(X) | | active(tail(cons(X, L))) | → | mark(L) |
| active(incr(X)) | → | incr(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(adx(X)) | → | adx(active(X)) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| incr(mark(X)) | → | mark(incr(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | adx(mark(X)) | → | mark(adx(X)) |
| head(mark(X)) | → | mark(head(X)) | | tail(mark(X)) | → | mark(tail(X)) |
| proper(incr(X)) | → | incr(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(adx(X)) | → | adx(proper(X)) | | proper(nats) | → | ok(nats) |
| proper(zeros) | → | ok(zeros) | | proper(0) | → | ok(0) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| incr(ok(X)) | → | ok(incr(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: mark, tail, nats, 0, s, zeros, active, adx, ok, incr, proper, head, top, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | active#(adx(X)) | → | active#(X) |
| top#(ok(X)) | → | top#(active(X)) | | proper#(tail(X)) | → | proper#(X) |
| incr#(ok(X)) | → | incr#(X) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
| active#(incr(cons(X, L))) | → | incr#(L) | | active#(cons(X1, X2)) | → | cons#(active(X1), X2) |
| active#(tail(X)) | → | tail#(active(X)) | | tail#(ok(X)) | → | tail#(X) |
| active#(incr(cons(X, L))) | → | cons#(s(X), incr(L)) | | proper#(incr(X)) | → | proper#(X) |
| adx#(ok(X)) | → | adx#(X) | | active#(head(X)) | → | active#(X) |
| top#(mark(X)) | → | proper#(X) | | top#(mark(X)) | → | top#(proper(X)) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | tail#(mark(X)) | → | tail#(X) |
| head#(ok(X)) | → | head#(X) | | proper#(adx(X)) | → | adx#(proper(X)) |
| proper#(s(X)) | → | proper#(X) | | proper#(head(X)) | → | head#(proper(X)) |
| active#(adx(cons(X, L))) | → | incr#(cons(X, adx(L))) | | active#(cons(X1, X2)) | → | active#(X1) |
| proper#(head(X)) | → | proper#(X) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| proper#(incr(X)) | → | incr#(proper(X)) | | top#(ok(X)) | → | active#(X) |
| proper#(adx(X)) | → | proper#(X) | | active#(incr(cons(X, L))) | → | s#(X) |
| incr#(mark(X)) | → | incr#(X) | | active#(adx(X)) | → | adx#(active(X)) |
| active#(incr(X)) | → | active#(X) | | head#(mark(X)) | → | head#(X) |
| active#(adx(cons(X, L))) | → | cons#(X, adx(L)) | | active#(incr(X)) | → | incr#(active(X)) |
| active#(head(X)) | → | head#(active(X)) | | active#(adx(cons(X, L))) | → | adx#(L) |
| active#(s(X)) | → | s#(active(X)) | | s#(ok(X)) | → | s#(X) |
| s#(mark(X)) | → | s#(X) | | active#(nats) | → | adx#(zeros) |
| adx#(mark(X)) | → | adx#(X) | | proper#(tail(X)) | → | tail#(proper(X)) |
| proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) | | active#(s(X)) | → | active#(X) |
| proper#(s(X)) | → | s#(proper(X)) | | active#(tail(X)) | → | active#(X) |
| active#(zeros) | → | cons#(0, zeros) |
Rewrite Rules
| active(incr(nil)) | → | mark(nil) | | active(incr(cons(X, L))) | → | mark(cons(s(X), incr(L))) |
| active(adx(nil)) | → | mark(nil) | | active(adx(cons(X, L))) | → | mark(incr(cons(X, adx(L)))) |
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(head(cons(X, L))) | → | mark(X) | | active(tail(cons(X, L))) | → | mark(L) |
| active(incr(X)) | → | incr(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(adx(X)) | → | adx(active(X)) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| incr(mark(X)) | → | mark(incr(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | adx(mark(X)) | → | mark(adx(X)) |
| head(mark(X)) | → | mark(head(X)) | | tail(mark(X)) | → | mark(tail(X)) |
| proper(incr(X)) | → | incr(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(adx(X)) | → | adx(proper(X)) | | proper(nats) | → | ok(nats) |
| proper(zeros) | → | ok(zeros) | | proper(0) | → | ok(0) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| incr(ok(X)) | → | ok(incr(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: mark, tail, nats, 0, s, zeros, active, adx, ok, incr, proper, head, cons, nil, top
Strategy
The following SCCs where found
| cons#(mark(X1), X2) → cons#(X1, X2) | cons#(ok(X1), ok(X2)) → cons#(X1, X2) |
| head#(ok(X)) → head#(X) | head#(mark(X)) → head#(X) |
| tail#(ok(X)) → tail#(X) | tail#(mark(X)) → tail#(X) |
| incr#(ok(X)) → incr#(X) | incr#(mark(X)) → incr#(X) |
| adx#(mark(X)) → adx#(X) | adx#(ok(X)) → adx#(X) |
| proper#(adx(X)) → proper#(X) | proper#(s(X)) → proper#(X) |
| proper#(head(X)) → proper#(X) | proper#(cons(X1, X2)) → proper#(X1) |
| proper#(cons(X1, X2)) → proper#(X2) | proper#(tail(X)) → proper#(X) |
| proper#(incr(X)) → proper#(X) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
| active#(incr(X)) → active#(X) | active#(adx(X)) → active#(X) |
| active#(s(X)) → active#(X) | active#(tail(X)) → active#(X) |
| active#(head(X)) → active#(X) | active#(cons(X1, X2)) → active#(X1) |
| s#(mark(X)) → s#(X) | s#(ok(X)) → s#(X) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| incr#(ok(X)) | → | incr#(X) | | incr#(mark(X)) | → | incr#(X) |
Rewrite Rules
| active(incr(nil)) | → | mark(nil) | | active(incr(cons(X, L))) | → | mark(cons(s(X), incr(L))) |
| active(adx(nil)) | → | mark(nil) | | active(adx(cons(X, L))) | → | mark(incr(cons(X, adx(L)))) |
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(head(cons(X, L))) | → | mark(X) | | active(tail(cons(X, L))) | → | mark(L) |
| active(incr(X)) | → | incr(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(adx(X)) | → | adx(active(X)) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| incr(mark(X)) | → | mark(incr(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | adx(mark(X)) | → | mark(adx(X)) |
| head(mark(X)) | → | mark(head(X)) | | tail(mark(X)) | → | mark(tail(X)) |
| proper(incr(X)) | → | incr(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(adx(X)) | → | adx(proper(X)) | | proper(nats) | → | ok(nats) |
| proper(zeros) | → | ok(zeros) | | proper(0) | → | ok(0) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| incr(ok(X)) | → | ok(incr(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: mark, tail, nats, 0, s, zeros, active, adx, ok, incr, proper, head, cons, nil, 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
| adx#(mark(X)) | → | adx#(X) | | adx#(ok(X)) | → | adx#(X) |
Rewrite Rules
| active(incr(nil)) | → | mark(nil) | | active(incr(cons(X, L))) | → | mark(cons(s(X), incr(L))) |
| active(adx(nil)) | → | mark(nil) | | active(adx(cons(X, L))) | → | mark(incr(cons(X, adx(L)))) |
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(head(cons(X, L))) | → | mark(X) | | active(tail(cons(X, L))) | → | mark(L) |
| active(incr(X)) | → | incr(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(adx(X)) | → | adx(active(X)) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| incr(mark(X)) | → | mark(incr(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | adx(mark(X)) | → | mark(adx(X)) |
| head(mark(X)) | → | mark(head(X)) | | tail(mark(X)) | → | mark(tail(X)) |
| proper(incr(X)) | → | incr(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(adx(X)) | → | adx(proper(X)) | | proper(nats) | → | ok(nats) |
| proper(zeros) | → | ok(zeros) | | proper(0) | → | ok(0) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| incr(ok(X)) | → | ok(incr(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: mark, tail, nats, 0, s, zeros, active, adx, ok, incr, proper, head, cons, nil, 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 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(adx(X)) | → | proper#(X) | | proper#(s(X)) | → | proper#(X) |
| proper#(head(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(tail(X)) | → | proper#(X) |
| proper#(incr(X)) | → | proper#(X) |
Rewrite Rules
| active(incr(nil)) | → | mark(nil) | | active(incr(cons(X, L))) | → | mark(cons(s(X), incr(L))) |
| active(adx(nil)) | → | mark(nil) | | active(adx(cons(X, L))) | → | mark(incr(cons(X, adx(L)))) |
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(head(cons(X, L))) | → | mark(X) | | active(tail(cons(X, L))) | → | mark(L) |
| active(incr(X)) | → | incr(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(adx(X)) | → | adx(active(X)) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| incr(mark(X)) | → | mark(incr(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | adx(mark(X)) | → | mark(adx(X)) |
| head(mark(X)) | → | mark(head(X)) | | tail(mark(X)) | → | mark(tail(X)) |
| proper(incr(X)) | → | incr(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(adx(X)) | → | adx(proper(X)) | | proper(nats) | → | ok(nats) |
| proper(zeros) | → | ok(zeros) | | proper(0) | → | ok(0) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| incr(ok(X)) | → | ok(incr(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: mark, tail, nats, 0, s, zeros, active, adx, ok, incr, proper, head, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(s(X)) | → | proper#(X) | | proper#(adx(X)) | → | proper#(X) |
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(head(X)) | → | proper#(X) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(tail(X)) | → | proper#(X) |
| proper#(incr(X)) | → | proper#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| tail#(ok(X)) | → | tail#(X) | | tail#(mark(X)) | → | tail#(X) |
Rewrite Rules
| active(incr(nil)) | → | mark(nil) | | active(incr(cons(X, L))) | → | mark(cons(s(X), incr(L))) |
| active(adx(nil)) | → | mark(nil) | | active(adx(cons(X, L))) | → | mark(incr(cons(X, adx(L)))) |
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(head(cons(X, L))) | → | mark(X) | | active(tail(cons(X, L))) | → | mark(L) |
| active(incr(X)) | → | incr(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(adx(X)) | → | adx(active(X)) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| incr(mark(X)) | → | mark(incr(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | adx(mark(X)) | → | mark(adx(X)) |
| head(mark(X)) | → | mark(head(X)) | | tail(mark(X)) | → | mark(tail(X)) |
| proper(incr(X)) | → | incr(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(adx(X)) | → | adx(proper(X)) | | proper(nats) | → | ok(nats) |
| proper(zeros) | → | ok(zeros) | | proper(0) | → | ok(0) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| incr(ok(X)) | → | ok(incr(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: mark, tail, nats, 0, s, zeros, active, adx, ok, incr, proper, head, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| tail#(ok(X)) | → | tail#(X) | | tail#(mark(X)) | → | tail#(X) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| head#(ok(X)) | → | head#(X) | | head#(mark(X)) | → | head#(X) |
Rewrite Rules
| active(incr(nil)) | → | mark(nil) | | active(incr(cons(X, L))) | → | mark(cons(s(X), incr(L))) |
| active(adx(nil)) | → | mark(nil) | | active(adx(cons(X, L))) | → | mark(incr(cons(X, adx(L)))) |
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(head(cons(X, L))) | → | mark(X) | | active(tail(cons(X, L))) | → | mark(L) |
| active(incr(X)) | → | incr(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(adx(X)) | → | adx(active(X)) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| incr(mark(X)) | → | mark(incr(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | adx(mark(X)) | → | mark(adx(X)) |
| head(mark(X)) | → | mark(head(X)) | | tail(mark(X)) | → | mark(tail(X)) |
| proper(incr(X)) | → | incr(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(adx(X)) | → | adx(proper(X)) | | proper(nats) | → | ok(nats) |
| proper(zeros) | → | ok(zeros) | | proper(0) | → | ok(0) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| incr(ok(X)) | → | ok(incr(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: mark, tail, nats, 0, s, zeros, active, adx, ok, incr, proper, head, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| head#(ok(X)) | → | head#(X) | | head#(mark(X)) | → | head#(X) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(ok(X)) | → | s#(X) |
Rewrite Rules
| active(incr(nil)) | → | mark(nil) | | active(incr(cons(X, L))) | → | mark(cons(s(X), incr(L))) |
| active(adx(nil)) | → | mark(nil) | | active(adx(cons(X, L))) | → | mark(incr(cons(X, adx(L)))) |
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(head(cons(X, L))) | → | mark(X) | | active(tail(cons(X, L))) | → | mark(L) |
| active(incr(X)) | → | incr(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(adx(X)) | → | adx(active(X)) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| incr(mark(X)) | → | mark(incr(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | adx(mark(X)) | → | mark(adx(X)) |
| head(mark(X)) | → | mark(head(X)) | | tail(mark(X)) | → | mark(tail(X)) |
| proper(incr(X)) | → | incr(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(adx(X)) | → | adx(proper(X)) | | proper(nats) | → | ok(nats) |
| proper(zeros) | → | ok(zeros) | | proper(0) | → | ok(0) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| incr(ok(X)) | → | ok(incr(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: mark, tail, nats, 0, s, zeros, active, adx, ok, incr, proper, head, 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 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(incr(X)) | → | active#(X) | | active#(adx(X)) | → | active#(X) |
| active#(s(X)) | → | active#(X) | | active#(tail(X)) | → | active#(X) |
| active#(head(X)) | → | active#(X) | | active#(cons(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(incr(nil)) | → | mark(nil) | | active(incr(cons(X, L))) | → | mark(cons(s(X), incr(L))) |
| active(adx(nil)) | → | mark(nil) | | active(adx(cons(X, L))) | → | mark(incr(cons(X, adx(L)))) |
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(head(cons(X, L))) | → | mark(X) | | active(tail(cons(X, L))) | → | mark(L) |
| active(incr(X)) | → | incr(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(adx(X)) | → | adx(active(X)) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| incr(mark(X)) | → | mark(incr(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | adx(mark(X)) | → | mark(adx(X)) |
| head(mark(X)) | → | mark(head(X)) | | tail(mark(X)) | → | mark(tail(X)) |
| proper(incr(X)) | → | incr(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(adx(X)) | → | adx(proper(X)) | | proper(nats) | → | ok(nats) |
| proper(zeros) | → | ok(zeros) | | proper(0) | → | ok(0) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| incr(ok(X)) | → | ok(incr(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: mark, tail, nats, 0, s, zeros, active, adx, ok, incr, proper, head, cons, nil, 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#(s(X)) | → | active#(X) | | active#(tail(X)) | → | active#(X) |
| active#(head(X)) | → | active#(X) | | active#(cons(X1, X2)) | → | active#(X1) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(incr(nil)) | → | mark(nil) | | active(incr(cons(X, L))) | → | mark(cons(s(X), incr(L))) |
| active(adx(nil)) | → | mark(nil) | | active(adx(cons(X, L))) | → | mark(incr(cons(X, adx(L)))) |
| active(nats) | → | mark(adx(zeros)) | | active(zeros) | → | mark(cons(0, zeros)) |
| active(head(cons(X, L))) | → | mark(X) | | active(tail(cons(X, L))) | → | mark(L) |
| active(incr(X)) | → | incr(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(adx(X)) | → | adx(active(X)) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| incr(mark(X)) | → | mark(incr(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| s(mark(X)) | → | mark(s(X)) | | adx(mark(X)) | → | mark(adx(X)) |
| head(mark(X)) | → | mark(head(X)) | | tail(mark(X)) | → | mark(tail(X)) |
| proper(incr(X)) | → | incr(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(s(X)) | → | s(proper(X)) |
| proper(adx(X)) | → | adx(proper(X)) | | proper(nats) | → | ok(nats) |
| proper(zeros) | → | ok(zeros) | | proper(0) | → | ok(0) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| incr(ok(X)) | → | ok(incr(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | adx(ok(X)) | → | ok(adx(X)) |
| head(ok(X)) | → | ok(head(X)) | | tail(ok(X)) | → | ok(tail(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: mark, tail, nats, 0, s, zeros, active, adx, ok, incr, proper, head, 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) |