TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60056 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (6524ms).
| – Problem 2 was processed with processor SubtermCriterion (5ms).
| | – Problem 12 remains open; application of the following processors failed [DependencyGraph (4ms), PolynomialLinearRange4iUR (18ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (20ms), DependencyGraph (4ms), ReductionPairSAT (timeout)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| | – Problem 13 remains open; application of the following processors failed [DependencyGraph (4ms), PolynomialLinearRange4iUR (2ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (26ms), DependencyGraph (5ms)].
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| | – Problem 14 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (17ms), DependencyGraph (5ms), PolynomialLinearRange8NegiUR (62ms), DependencyGraph (4ms)].
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (3ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| | – Problem 15 remains open; application of the following processors failed [DependencyGraph (11ms), PolynomialLinearRange4iUR (11ms), DependencyGraph (11ms), PolynomialLinearRange8NegiUR (3ms), DependencyGraph (11ms)].
| – Problem 9 was processed with processor SubtermCriterion (1ms).
| – Problem 10 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (878ms), PolynomialLinearRange4iUR (2000ms), DependencyGraph (921ms), PolynomialLinearRange8NegiUR (6000ms), DependencyGraph (920ms), ReductionPairSAT (42296ms)].
| – Problem 11 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 10
Dependency Pairs
| mark#(filter(X1, X2)) | → | mark#(X1) | | mark#(false) | → | active#(false) |
| mark#(head(X)) | → | active#(head(mark(X))) | | mark#(cons(X1, X2)) | → | active#(cons(mark(X1), X2)) |
| active#(head(cons(X, Y))) | → | mark#(X) | | mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) |
| active#(if(false, X, Y)) | → | mark#(Y) | | mark#(divides(X1, X2)) | → | mark#(X1) |
| active#(if(true, X, Y)) | → | mark#(X) | | mark#(filter(X1, X2)) | → | mark#(X2) |
| mark#(tail(X)) | → | active#(tail(mark(X))) | | mark#(head(X)) | → | mark#(X) |
| 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))))) | | mark#(primes) | → | active#(primes) |
| mark#(s(X)) | → | mark#(X) | | mark#(sieve(X)) | → | active#(sieve(mark(X))) |
| mark#(0) | → | active#(0) | | mark#(s(X)) | → | active#(s(mark(X))) |
| mark#(true) | → | active#(true) | | active#(sieve(cons(X, Y))) | → | mark#(cons(X, filter(X, sieve(Y)))) |
| mark#(from(X)) | → | mark#(X) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(filter(X1, X2)) | → | active#(filter(mark(X1), mark(X2))) | | active#(from(X)) | → | mark#(cons(X, from(s(X)))) |
| mark#(from(X)) | → | active#(from(mark(X))) | | active#(primes) | → | mark#(sieve(from(s(s(0))))) |
| active#(tail(cons(X, Y))) | → | mark#(Y) | | mark#(tail(X)) | → | mark#(X) |
| mark#(if(X1, X2, X3)) | → | mark#(X1) | | mark#(divides(X1, X2)) | → | active#(divides(mark(X1), mark(X2))) |
| mark#(divides(X1, X2)) | → | mark#(X2) | | mark#(sieve(X)) | → | mark#(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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Open Dependency Pair Problem 12
Dependency Pairs
| divides#(X1, mark(X2)) | → | divides#(X1, X2) | | divides#(X1, active(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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Open Dependency Pair Problem 13
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(X1, mark(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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Open Dependency Pair Problem 14
Dependency Pairs
| filter#(X1, active(X2)) | → | filter#(X1, X2) | | 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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Open Dependency Pair Problem 15
Dependency Pairs
| if#(X1, mark(X2), X3) | → | if#(X1, X2, X3) | | if#(X1, X2, mark(X3)) | → | if#(X1, X2, X3) |
| if#(X1, active(X2), X3) | → | if#(X1, X2, X3) | | if#(X1, X2, active(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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(filter(X1, X2)) | → | mark#(X1) | | mark#(cons(X1, X2)) | → | active#(cons(mark(X1), X2)) |
| active#(primes) | → | sieve#(from(s(s(0)))) | | mark#(divides(X1, X2)) | → | mark#(X1) |
| if#(X1, X2, active(X3)) | → | if#(X1, X2, X3) | | active#(filter(s(s(X)), cons(Y, Z))) | → | cons#(Y, filter(X, sieve(Y))) |
| active#(primes) | → | s#(s(0)) | | sieve#(mark(X)) | → | sieve#(X) |
| mark#(s(X)) | → | s#(mark(X)) | | active#(if(true, X, Y)) | → | mark#(X) |
| mark#(tail(X)) | → | active#(tail(mark(X))) | | active#(filter(s(s(X)), cons(Y, Z))) | → | filter#(X, sieve(Y)) |
| active#(sieve(cons(X, Y))) | → | sieve#(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))))) |
| filter#(X1, mark(X2)) | → | filter#(X1, X2) | | active#(filter(s(s(X)), cons(Y, Z))) | → | filter#(s(s(X)), Z) |
| mark#(s(X)) | → | mark#(X) | | mark#(sieve(X)) | → | active#(sieve(mark(X))) |
| mark#(true) | → | active#(true) | | active#(primes) | → | s#(0) |
| active#(sieve(cons(X, Y))) | → | mark#(cons(X, filter(X, sieve(Y)))) | | mark#(from(X)) | → | mark#(X) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(filter(X1, X2)) | → | active#(filter(mark(X1), mark(X2))) |
| tail#(mark(X)) | → | tail#(X) | | active#(from(X)) | → | mark#(cons(X, from(s(X)))) |
| active#(from(X)) | → | s#(X) | | cons#(X1, active(X2)) | → | cons#(X1, X2) |
| mark#(from(X)) | → | from#(mark(X)) | | sieve#(active(X)) | → | sieve#(X) |
| if#(X1, mark(X2), X3) | → | if#(X1, X2, X3) | | mark#(from(X)) | → | active#(from(mark(X))) |
| mark#(tail(X)) | → | mark#(X) | | if#(X1, X2, mark(X3)) | → | if#(X1, X2, X3) |
| from#(active(X)) | → | from#(X) | | divides#(mark(X1), X2) | → | divides#(X1, X2) |
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | mark#(divides(X1, X2)) | → | divides#(mark(X1), mark(X2)) |
| head#(active(X)) | → | head#(X) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(divides(X1, X2)) | → | active#(divides(mark(X1), mark(X2))) | | divides#(active(X1), X2) | → | divides#(X1, X2) |
| mark#(sieve(X)) | → | mark#(X) | | mark#(false) | → | active#(false) |
| mark#(head(X)) | → | active#(head(mark(X))) | | active#(head(cons(X, Y))) | → | mark#(X) |
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) | | active#(if(false, X, Y)) | → | mark#(Y) |
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | mark#(tail(X)) | → | tail#(mark(X)) |
| if#(X1, active(X2), X3) | → | if#(X1, X2, X3) | | from#(mark(X)) | → | from#(X) |
| active#(sieve(cons(X, Y))) | → | filter#(X, sieve(Y)) | | active#(filter(s(s(X)), cons(Y, Z))) | → | sieve#(Y) |
| mark#(filter(X1, X2)) | → | mark#(X2) | | divides#(X1, mark(X2)) | → | divides#(X1, X2) |
| mark#(head(X)) | → | mark#(X) | | 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)))) | | tail#(active(X)) | → | tail#(X) |
| active#(from(X)) | → | cons#(X, from(s(X))) | | mark#(primes) | → | active#(primes) |
| mark#(sieve(X)) | → | sieve#(mark(X)) | | filter#(mark(X1), X2) | → | filter#(X1, X2) |
| cons#(X1, mark(X2)) | → | cons#(X1, X2) | | mark#(cons(X1, X2)) | → | cons#(mark(X1), X2) |
| active#(filter(s(s(X)), cons(Y, Z))) | → | s#(s(X)) | | mark#(if(X1, X2, X3)) | → | if#(mark(X1), X2, X3) |
| mark#(0) | → | active#(0) | | active#(filter(s(s(X)), cons(Y, Z))) | → | s#(X) |
| mark#(s(X)) | → | active#(s(mark(X))) | | head#(mark(X)) | → | head#(X) |
| divides#(X1, active(X2)) | → | divides#(X1, X2) | | filter#(active(X1), X2) | → | filter#(X1, X2) |
| cons#(active(X1), X2) | → | cons#(X1, X2) | | mark#(head(X)) | → | head#(mark(X)) |
| if#(active(X1), X2, X3) | → | if#(X1, X2, X3) | | s#(mark(X)) | → | s#(X) |
| filter#(X1, active(X2)) | → | filter#(X1, X2) | | active#(primes) | → | mark#(sieve(from(s(s(0))))) |
| active#(tail(cons(X, Y))) | → | mark#(Y) | | active#(filter(s(s(X)), cons(Y, Z))) | → | divides#(s(s(X)), Y) |
| mark#(filter(X1, X2)) | → | filter#(mark(X1), mark(X2)) | | s#(active(X)) | → | s#(X) |
| active#(primes) | → | from#(s(s(0))) | | mark#(divides(X1, X2)) | → | mark#(X2) |
| 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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Strategy
The following SCCs where found
| filter#(X1, active(X2)) → filter#(X1, X2) | filter#(X1, mark(X2)) → filter#(X1, X2) |
| filter#(active(X1), X2) → filter#(X1, X2) | filter#(mark(X1), X2) → filter#(X1, X2) |
| sieve#(active(X)) → sieve#(X) | sieve#(mark(X)) → sieve#(X) |
| from#(active(X)) → from#(X) | from#(mark(X)) → from#(X) |
| tail#(active(X)) → tail#(X) | tail#(mark(X)) → tail#(X) |
| if#(X1, mark(X2), X3) → if#(X1, X2, X3) | if#(X1, X2, mark(X3)) → if#(X1, X2, X3) |
| if#(mark(X1), X2, X3) → if#(X1, X2, X3) | if#(X1, active(X2), X3) → if#(X1, X2, X3) |
| if#(X1, X2, active(X3)) → if#(X1, X2, X3) | if#(active(X1), X2, X3) → if#(X1, X2, X3) |
| cons#(X1, active(X2)) → cons#(X1, X2) | cons#(mark(X1), X2) → cons#(X1, X2) |
| cons#(X1, mark(X2)) → cons#(X1, X2) | cons#(active(X1), X2) → cons#(X1, X2) |
| s#(mark(X)) → s#(X) | s#(active(X)) → s#(X) |
| divides#(X1, mark(X2)) → divides#(X1, X2) | divides#(X1, active(X2)) → divides#(X1, X2) |
| divides#(mark(X1), X2) → divides#(X1, X2) | divides#(active(X1), X2) → divides#(X1, X2) |
| mark#(filter(X1, X2)) → mark#(X1) | mark#(cons(X1, X2)) → active#(cons(mark(X1), X2)) |
| mark#(head(X)) → active#(head(mark(X))) | mark#(false) → active#(false) |
| mark#(if(X1, X2, X3)) → active#(if(mark(X1), X2, X3)) | active#(head(cons(X, Y))) → mark#(X) |
| active#(if(false, X, Y)) → mark#(Y) | mark#(divides(X1, X2)) → mark#(X1) |
| mark#(filter(X1, X2)) → mark#(X2) | active#(if(true, X, Y)) → mark#(X) |
| mark#(tail(X)) → active#(tail(mark(X))) | mark#(head(X)) → mark#(X) |
| mark#(primes) → active#(primes) | 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))))) |
| mark#(s(X)) → mark#(X) | mark#(sieve(X)) → active#(sieve(mark(X))) |
| mark#(0) → active#(0) | mark#(s(X)) → active#(s(mark(X))) |
| mark#(true) → active#(true) | active#(sieve(cons(X, Y))) → mark#(cons(X, filter(X, sieve(Y)))) |
| mark#(from(X)) → mark#(X) | mark#(cons(X1, X2)) → mark#(X1) |
| mark#(filter(X1, X2)) → active#(filter(mark(X1), mark(X2))) | active#(from(X)) → mark#(cons(X, from(s(X)))) |
| active#(primes) → mark#(sieve(from(s(s(0))))) | mark#(from(X)) → active#(from(mark(X))) |
| mark#(tail(X)) → mark#(X) | active#(tail(cons(X, Y))) → mark#(Y) |
| mark#(if(X1, X2, X3)) → mark#(X1) | mark#(divides(X1, X2)) → active#(divides(mark(X1), mark(X2))) |
| mark#(divides(X1, X2)) → mark#(X2) | mark#(sieve(X)) → mark#(X) |
| head#(mark(X)) → head#(X) | head#(active(X)) → head#(X) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| divides#(X1, mark(X2)) | → | divides#(X1, X2) | | divides#(X1, active(X2)) | → | divides#(X1, X2) |
| divides#(mark(X1), X2) | → | divides#(X1, X2) | | divides#(active(X1), 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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| divides#(mark(X1), X2) | → | divides#(X1, X2) | | divides#(active(X1), X2) | → | divides#(X1, X2) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| head#(mark(X)) | → | head#(X) | | head#(active(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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| head#(mark(X)) | → | head#(X) | | head#(active(X)) | → | head#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| cons#(X1, mark(X2)) | → | cons#(X1, X2) | | cons#(active(X1), 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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(active(X1), X2) | → | cons#(X1, X2) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| filter#(X1, active(X2)) | → | filter#(X1, X2) | | filter#(X1, mark(X2)) | → | filter#(X1, X2) |
| filter#(active(X1), 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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| filter#(mark(X1), X2) | → | filter#(X1, X2) | | filter#(active(X1), X2) | → | filter#(X1, X2) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(active(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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sieve#(active(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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sieve#(active(X)) | → | sieve#(X) | | sieve#(mark(X)) | → | sieve#(X) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| if#(X1, mark(X2), X3) | → | if#(X1, X2, X3) | | if#(X1, X2, mark(X3)) | → | if#(X1, X2, X3) |
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | if#(X1, active(X2), X3) | → | if#(X1, X2, X3) |
| if#(X1, X2, active(X3)) | → | if#(X1, X2, X3) | | if#(active(X1), X2, 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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | if#(active(X1), X2, X3) | → | if#(X1, X2, X3) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| tail#(active(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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| tail#(active(X)) | → | tail#(X) | | tail#(mark(X)) | → | tail#(X) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| from#(active(X)) | → | from#(X) | | from#(mark(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)))) |
| mark(primes) | → | active(primes) | | mark(sieve(X)) | → | active(sieve(mark(X))) |
| mark(from(X)) | → | active(from(mark(X))) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(0) | → | active(0) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(head(X)) | → | active(head(mark(X))) | | mark(tail(X)) | → | active(tail(mark(X))) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(filter(X1, X2)) | → | active(filter(mark(X1), mark(X2))) |
| mark(divides(X1, X2)) | → | active(divides(mark(X1), mark(X2))) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | head(mark(X)) | → | head(X) |
| head(active(X)) | → | head(X) | | tail(mark(X)) | → | tail(X) |
| tail(active(X)) | → | tail(X) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | filter(mark(X1), X2) | → | filter(X1, X2) |
| filter(X1, mark(X2)) | → | filter(X1, X2) | | filter(active(X1), X2) | → | filter(X1, X2) |
| filter(X1, active(X2)) | → | filter(X1, X2) | | divides(mark(X1), X2) | → | divides(X1, X2) |
| divides(X1, mark(X2)) | → | divides(X1, X2) | | divides(active(X1), X2) | → | divides(X1, X2) |
| divides(X1, active(X2)) | → | divides(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, mark, from, tail, 0, s, if, active, false, primes, head, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| from#(active(X)) | → | from#(X) | | from#(mark(X)) | → | from#(X) |