TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60078 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (6402ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (3333ms), DependencyGraph (26ms), PolynomialLinearRange8NegiUR (10000ms), DependencyGraph (5ms), ReductionPairSAT (timeout)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| | – Problem 14 remains open; application of the following processors failed [DependencyGraph (2ms), PolynomialLinearRange4iUR (11ms), DependencyGraph (5ms), PolynomialLinearRange8NegiUR (12ms), DependencyGraph (3ms)].
| – Problem 6 was processed with processor SubtermCriterion (3ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| | – Problem 15 remains open; application of the following processors failed [DependencyGraph (1ms), PolynomialLinearRange4iUR (12ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (19ms), DependencyGraph (1ms)].
| – Problem 9 was processed with processor SubtermCriterion (1ms).
| – Problem 10 was processed with processor SubtermCriterion (1ms).
| – Problem 11 was processed with processor SubtermCriterion (3ms).
| – Problem 12 was processed with processor SubtermCriterion (1ms).
| – Problem 13 was processed with processor SubtermCriterion (2ms).
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(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, proper, primes, head, filter, top, cons
Open Dependency Pair Problem 14
Dependency Pairs
| divides#(X1, mark(X2)) | → | divides#(X1, X2) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, top
Open Dependency Pair Problem 15
Dependency Pairs
| filter#(X1, mark(X2)) | → | filter#(X1, X2) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, top
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | top#(ok(X)) | → | top#(active(X)) |
| proper#(tail(X)) | → | proper#(X) | | active#(primes) | → | sieve#(from(s(s(0)))) |
| active#(sieve(X)) | → | active#(X) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
| active#(primes) | → | s#(s(0)) | | active#(filter(s(s(X)), cons(Y, Z))) | → | cons#(Y, filter(X, sieve(Y))) |
| from#(ok(X)) | → | from#(X) | | proper#(divides(X1, X2)) | → | proper#(X2) |
| sieve#(mark(X)) | → | sieve#(X) | | proper#(sieve(X)) | → | sieve#(proper(X)) |
| active#(filter(X1, X2)) | → | filter#(active(X1), X2) | | active#(cons(X1, X2)) | → | cons#(active(X1), X2) |
| active#(if(X1, X2, X3)) | → | active#(X1) | | active#(tail(X)) | → | tail#(active(X)) |
| tail#(ok(X)) | → | tail#(X) | | active#(filter(X1, X2)) | → | active#(X2) |
| active#(filter(s(s(X)), cons(Y, Z))) | → | filter#(X, sieve(Y)) | | active#(sieve(cons(X, Y))) | → | sieve#(Y) |
| filter#(X1, mark(X2)) | → | filter#(X1, X2) | | active#(filter(s(s(X)), cons(Y, Z))) | → | filter#(s(s(X)), Z) |
| active#(head(X)) | → | active#(X) | | top#(mark(X)) | → | proper#(X) |
| proper#(from(X)) | → | proper#(X) | | filter#(ok(X1), ok(X2)) | → | filter#(X1, X2) |
| top#(mark(X)) | → | top#(proper(X)) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| active#(divides(X1, X2)) | → | divides#(X1, active(X2)) | | active#(primes) | → | s#(0) |
| proper#(divides(X1, X2)) | → | divides#(proper(X1), proper(X2)) | | tail#(mark(X)) | → | tail#(X) |
| head#(ok(X)) | → | head#(X) | | active#(from(X)) | → | s#(X) |
| proper#(s(X)) | → | proper#(X) | | proper#(head(X)) | → | head#(proper(X)) |
| active#(divides(X1, X2)) | → | active#(X1) | | proper#(filter(X1, X2)) | → | filter#(proper(X1), proper(X2)) |
| divides#(mark(X1), X2) | → | divides#(X1, X2) | | active#(divides(X1, X2)) | → | active#(X2) |
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | proper#(filter(X1, X2)) | → | proper#(X1) |
| active#(cons(X1, X2)) | → | active#(X1) | | proper#(head(X)) | → | proper#(X) |
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | active#(from(X)) | → | from#(active(X)) |
| from#(mark(X)) | → | from#(X) | | top#(ok(X)) | → | active#(X) |
| active#(sieve(cons(X, Y))) | → | filter#(X, sieve(Y)) | | active#(filter(s(s(X)), cons(Y, Z))) | → | sieve#(Y) |
| divides#(X1, mark(X2)) | → | divides#(X1, X2) | | active#(sieve(cons(X, Y))) | → | cons#(X, filter(X, sieve(Y))) |
| active#(filter(s(s(X)), cons(Y, Z))) | → | if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))) | | active#(from(X)) | → | cons#(X, from(s(X))) |
| proper#(filter(X1, X2)) | → | proper#(X2) | | proper#(from(X)) | → | from#(proper(X)) |
| filter#(mark(X1), X2) | → | filter#(X1, X2) | | active#(sieve(X)) | → | sieve#(active(X)) |
| if#(ok(X1), ok(X2), ok(X3)) | → | if#(X1, X2, X3) | | active#(filter(s(s(X)), cons(Y, Z))) | → | s#(s(X)) |
| proper#(divides(X1, X2)) | → | proper#(X1) | | sieve#(ok(X)) | → | sieve#(X) |
| active#(filter(s(s(X)), cons(Y, Z))) | → | s#(X) | | proper#(if(X1, X2, X3)) | → | proper#(X1) |
| head#(mark(X)) | → | head#(X) | | active#(filter(X1, X2)) | → | filter#(X1, active(X2)) |
| active#(from(X)) | → | active#(X) | | proper#(if(X1, X2, X3)) | → | proper#(X2) |
| active#(head(X)) | → | head#(active(X)) | | active#(filter(X1, X2)) | → | active#(X1) |
| active#(s(X)) | → | s#(active(X)) | | divides#(ok(X1), ok(X2)) | → | divides#(X1, X2) |
| s#(ok(X)) | → | s#(X) | | s#(mark(X)) | → | s#(X) |
| proper#(tail(X)) | → | tail#(proper(X)) | | proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) |
| active#(filter(s(s(X)), cons(Y, Z))) | → | divides#(s(s(X)), Y) | | active#(s(X)) | → | active#(X) |
| proper#(s(X)) | → | s#(proper(X)) | | proper#(if(X1, X2, X3)) | → | proper#(X3) |
| active#(tail(X)) | → | active#(X) | | active#(if(X1, X2, X3)) | → | if#(active(X1), X2, X3) |
| proper#(sieve(X)) | → | proper#(X) | | active#(divides(X1, X2)) | → | divides#(active(X1), X2) |
| active#(primes) | → | from#(s(s(0))) | | proper#(if(X1, X2, X3)) | → | if#(proper(X1), proper(X2), proper(X3)) |
| active#(from(X)) | → | from#(s(X)) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, top
Strategy
The following SCCs where found
| active#(if(X1, X2, X3)) → active#(X1) | active#(filter(X1, X2)) → active#(X2) |
| active#(divides(X1, X2)) → active#(X1) | active#(from(X)) → active#(X) |
| active#(s(X)) → active#(X) | active#(tail(X)) → active#(X) |
| active#(divides(X1, X2)) → active#(X2) | active#(sieve(X)) → active#(X) |
| active#(filter(X1, X2)) → active#(X1) | active#(head(X)) → active#(X) |
| active#(cons(X1, X2)) → active#(X1) |
| sieve#(ok(X)) → sieve#(X) | sieve#(mark(X)) → sieve#(X) |
| 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) |
| divides#(X1, mark(X2)) → divides#(X1, X2) | divides#(mark(X1), X2) → divides#(X1, X2) |
| divides#(ok(X1), ok(X2)) → divides#(X1, X2) |
| tail#(ok(X)) → tail#(X) | tail#(mark(X)) → tail#(X) |
| filter#(ok(X1), ok(X2)) → filter#(X1, X2) | filter#(X1, mark(X2)) → filter#(X1, X2) |
| filter#(mark(X1), X2) → filter#(X1, X2) |
| if#(mark(X1), X2, X3) → if#(X1, X2, X3) | if#(ok(X1), ok(X2), ok(X3)) → if#(X1, X2, X3) |
| from#(mark(X)) → from#(X) | from#(ok(X)) → from#(X) |
| proper#(cons(X1, X2)) → proper#(X1) | proper#(head(X)) → proper#(X) |
| proper#(if(X1, X2, X3)) → proper#(X1) | proper#(cons(X1, X2)) → proper#(X2) |
| proper#(tail(X)) → proper#(X) | proper#(if(X1, X2, X3)) → proper#(X2) |
| proper#(divides(X1, X2)) → proper#(X2) | proper#(s(X)) → proper#(X) |
| proper#(if(X1, X2, X3)) → proper#(X3) | proper#(filter(X1, X2)) → proper#(X2) |
| proper#(sieve(X)) → proper#(X) | proper#(filter(X1, X2)) → proper#(X1) |
| proper#(from(X)) → proper#(X) | proper#(divides(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) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sieve#(ok(X)) | → | sieve#(X) | | sieve#(mark(X)) | → | sieve#(X) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sieve#(ok(X)) | → | sieve#(X) | | sieve#(mark(X)) | → | sieve#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | if#(ok(X1), ok(X2), ok(X3)) | → | if#(X1, X2, X3) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | if#(ok(X1), ok(X2), ok(X3)) | → | if#(X1, X2, X3) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| divides#(X1, mark(X2)) | → | divides#(X1, X2) | | divides#(mark(X1), X2) | → | divides#(X1, X2) |
| divides#(ok(X1), ok(X2)) | → | divides#(X1, X2) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| divides#(mark(X1), X2) | → | divides#(X1, X2) | | divides#(ok(X1), ok(X2)) | → | divides#(X1, X2) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(ok(X)) | → | s#(X) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, 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 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, 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 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| filter#(ok(X1), ok(X2)) | → | filter#(X1, X2) | | filter#(X1, mark(X2)) | → | filter#(X1, X2) |
| filter#(mark(X1), X2) | → | filter#(X1, X2) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| filter#(ok(X1), ok(X2)) | → | filter#(X1, X2) | | filter#(mark(X1), X2) | → | filter#(X1, X2) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(if(X1, X2, X3)) | → | active#(X1) | | active#(filter(X1, X2)) | → | active#(X2) |
| active#(divides(X1, X2)) | → | active#(X1) | | active#(from(X)) | → | active#(X) |
| active#(s(X)) | → | active#(X) | | active#(tail(X)) | → | active#(X) |
| active#(divides(X1, X2)) | → | active#(X2) | | active#(sieve(X)) | → | active#(X) |
| active#(filter(X1, X2)) | → | active#(X1) | | active#(head(X)) | → | active#(X) |
| active#(cons(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(if(X1, X2, X3)) | → | active#(X1) | | active#(filter(X1, X2)) | → | active#(X2) |
| active#(divides(X1, X2)) | → | active#(X1) | | active#(from(X)) | → | active#(X) |
| active#(s(X)) | → | active#(X) | | active#(tail(X)) | → | active#(X) |
| active#(divides(X1, X2)) | → | active#(X2) | | active#(sieve(X)) | → | active#(X) |
| active#(filter(X1, X2)) | → | active#(X1) | | active#(head(X)) | → | active#(X) |
| active#(cons(X1, X2)) | → | active#(X1) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| tail#(ok(X)) | → | tail#(X) | | tail#(mark(X)) | → | tail#(X) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, 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 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| head#(ok(X)) | → | head#(X) | | head#(mark(X)) | → | head#(X) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, 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 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| from#(mark(X)) | → | from#(X) | | from#(ok(X)) | → | from#(X) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| from#(mark(X)) | → | from#(X) | | from#(ok(X)) | → | from#(X) |
Problem 13: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(head(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(if(X1, X2, X3)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(if(X1, X2, X3)) | → | proper#(X2) | | proper#(tail(X)) | → | proper#(X) |
| proper#(divides(X1, X2)) | → | proper#(X2) | | proper#(s(X)) | → | proper#(X) |
| proper#(if(X1, X2, X3)) | → | proper#(X3) | | proper#(filter(X1, X2)) | → | proper#(X2) |
| proper#(sieve(X)) | → | proper#(X) | | proper#(filter(X1, X2)) | → | proper#(X1) |
| proper#(from(X)) | → | proper#(X) | | proper#(divides(X1, X2)) | → | proper#(X1) |
Rewrite Rules
| active(primes) | → | mark(sieve(from(s(s(0))))) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| active(head(cons(X, Y))) | → | mark(X) | | active(tail(cons(X, Y))) | → | mark(Y) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(filter(s(s(X)), cons(Y, Z))) | → | mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) | | active(sieve(cons(X, Y))) | → | mark(cons(X, filter(X, sieve(Y)))) |
| active(sieve(X)) | → | sieve(active(X)) | | active(from(X)) | → | from(active(X)) |
| active(s(X)) | → | s(active(X)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(head(X)) | → | head(active(X)) | | active(tail(X)) | → | tail(active(X)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(filter(X1, X2)) | → | filter(active(X1), X2) |
| active(filter(X1, X2)) | → | filter(X1, active(X2)) | | active(divides(X1, X2)) | → | divides(active(X1), X2) |
| active(divides(X1, X2)) | → | divides(X1, active(X2)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| from(mark(X)) | → | mark(from(X)) | | s(mark(X)) | → | mark(s(X)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | head(mark(X)) | → | mark(head(X)) |
| tail(mark(X)) | → | mark(tail(X)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| filter(mark(X1), X2) | → | mark(filter(X1, X2)) | | filter(X1, mark(X2)) | → | mark(filter(X1, X2)) |
| divides(mark(X1), X2) | → | mark(divides(X1, X2)) | | divides(X1, mark(X2)) | → | mark(divides(X1, X2)) |
| proper(primes) | → | ok(primes) | | proper(sieve(X)) | → | sieve(proper(X)) |
| proper(from(X)) | → | from(proper(X)) | | proper(s(X)) | → | s(proper(X)) |
| proper(0) | → | ok(0) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(head(X)) | → | head(proper(X)) | | proper(tail(X)) | → | tail(proper(X)) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(true) | → | ok(true) |
| proper(false) | → | ok(false) | | proper(filter(X1, X2)) | → | filter(proper(X1), proper(X2)) |
| proper(divides(X1, X2)) | → | divides(proper(X1), proper(X2)) | | sieve(ok(X)) | → | ok(sieve(X)) |
| from(ok(X)) | → | ok(from(X)) | | s(ok(X)) | → | ok(s(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | head(ok(X)) | → | ok(head(X)) |
| tail(ok(X)) | → | ok(tail(X)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| filter(ok(X1), ok(X2)) | → | ok(filter(X1, X2)) | | divides(ok(X1), ok(X2)) | → | ok(divides(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: sieve, true, divides, mark, from, tail, 0, s, if, active, false, ok, primes, proper, head, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(head(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(if(X1, X2, X3)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(if(X1, X2, X3)) | → | proper#(X2) | | proper#(tail(X)) | → | proper#(X) |
| proper#(divides(X1, X2)) | → | proper#(X2) | | proper#(s(X)) | → | proper#(X) |
| proper#(if(X1, X2, X3)) | → | proper#(X3) | | proper#(filter(X1, X2)) | → | proper#(X2) |
| proper#(sieve(X)) | → | proper#(X) | | proper#(filter(X1, X2)) | → | proper#(X1) |
| proper#(from(X)) | → | proper#(X) | | proper#(divides(X1, X2)) | → | proper#(X1) |