YES

The TRS could be proven terminating. The proof took 5260 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (688ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (2800ms).
 |    | – Problem 12 was processed with processor PolynomialLinearRange4iUR (1676ms).
 | – Problem 3 was processed with processor SubtermCriterion (2ms).
 | – Problem 4 was processed with processor SubtermCriterion (2ms).
 | – Problem 5 was processed with processor SubtermCriterion (2ms).
 | – Problem 6 was processed with processor SubtermCriterion (2ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 was processed with processor SubtermCriterion (4ms).
 | – Problem 9 was processed with processor SubtermCriterion (8ms).
 |    | – Problem 10 was processed with processor SubtermCriterion (0ms).
 |    |    | – Problem 11 was processed with processor PolynomialLinearRange4iUR (9ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2))proper#(X1)top#(ok(X))top#(active(X))
active#(sieve(cons(s(N), Y)))sieve#(filter(Y, N, N))active#(nats(X))active#(X)
active#(filter(cons(X, Y), s(N), M))filter#(Y, N, M)active#(zprimes)nats#(s(s(0)))
active#(sieve(X))active#(X)cons#(ok(X1), ok(X2))cons#(X1, X2)
sieve#(mark(X))sieve#(X)active#(nats(X))nats#(active(X))
proper#(sieve(X))sieve#(proper(X))active#(cons(X1, X2))cons#(active(X1), X2)
active#(filter(X1, X2, X3))active#(X1)active#(sieve(cons(s(N), Y)))cons#(s(N), sieve(filter(Y, N, N)))
active#(zprimes)s#(s(0))proper#(filter(X1, X2, X3))proper#(X1)
top#(mark(X))proper#(X)nats#(ok(X))nats#(X)
active#(zprimes)s#(0)top#(mark(X))top#(proper(X))
proper#(cons(X1, X2))proper#(X2)filter#(ok(X1), ok(X2), ok(X3))filter#(X1, X2, X3)
nats#(mark(X))nats#(X)active#(sieve(cons(0, Y)))cons#(0, sieve(Y))
active#(sieve(cons(s(N), Y)))filter#(Y, N, N)active#(nats(N))nats#(s(N))
proper#(s(X))proper#(X)active#(filter(X1, X2, X3))filter#(X1, active(X2), X3)
filter#(X1, X2, mark(X3))filter#(X1, X2, X3)proper#(filter(X1, X2, X3))proper#(X3)
active#(nats(N))s#(N)proper#(filter(X1, X2, X3))proper#(X2)
proper#(filter(X1, X2, X3))filter#(proper(X1), proper(X2), proper(X3))proper#(nats(X))nats#(proper(X))
active#(cons(X1, X2))active#(X1)active#(filter(cons(X, Y), 0, M))filter#(Y, M, M)
cons#(mark(X1), X2)cons#(X1, X2)filter#(mark(X1), X2, X3)filter#(X1, X2, X3)
top#(ok(X))active#(X)active#(filter(X1, X2, X3))filter#(active(X1), X2, X3)
filter#(X1, mark(X2), X3)filter#(X1, X2, X3)active#(filter(X1, X2, X3))active#(X2)
active#(sieve(X))sieve#(active(X))active#(filter(X1, X2, X3))active#(X3)
active#(sieve(cons(s(N), Y)))s#(N)sieve#(ok(X))sieve#(X)
active#(filter(X1, X2, X3))filter#(X1, X2, active(X3))active#(filter(cons(X, Y), s(N), M))cons#(X, filter(Y, N, M))
active#(nats(N))cons#(N, nats(s(N)))active#(sieve(cons(0, Y)))sieve#(Y)
active#(s(X))s#(active(X))active#(zprimes)sieve#(nats(s(s(0))))
s#(ok(X))s#(X)s#(mark(X))s#(X)
active#(filter(cons(X, Y), 0, M))cons#(0, filter(Y, M, M))proper#(cons(X1, X2))cons#(proper(X1), proper(X2))
active#(s(X))active#(X)proper#(s(X))s#(proper(X))
proper#(nats(X))proper#(X)proper#(sieve(X))proper#(X)

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top

Strategy


The following SCCs where found

active#(nats(X)) → active#(X)active#(s(X)) → active#(X)
active#(sieve(X)) → active#(X)active#(filter(X1, X2, X3)) → active#(X2)
active#(filter(X1, X2, X3)) → active#(X1)active#(cons(X1, X2)) → active#(X1)
active#(filter(X1, X2, X3)) → active#(X3)

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)

proper#(s(X)) → proper#(X)proper#(cons(X1, X2)) → proper#(X1)
proper#(filter(X1, X2, X3)) → proper#(X3)proper#(cons(X1, X2)) → proper#(X2)
proper#(filter(X1, X2, X3)) → proper#(X1)proper#(filter(X1, X2, X3)) → proper#(X2)
proper#(nats(X)) → proper#(X)proper#(sieve(X)) → proper#(X)

filter#(X1, X2, mark(X3)) → filter#(X1, X2, X3)filter#(ok(X1), ok(X2), ok(X3)) → filter#(X1, X2, X3)
filter#(X1, mark(X2), X3) → filter#(X1, X2, X3)filter#(mark(X1), X2, X3) → filter#(X1, X2, X3)

nats#(ok(X)) → nats#(X)nats#(mark(X)) → nats#(X)

top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))

s#(mark(X)) → s#(X)s#(ok(X)) → s#(X)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

top#(mark(X))top#(proper(X))top#(ok(X))top#(active(X))

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top

Strategy


Polynomial Interpretation

Improved Usable rules

sieve(mark(X))mark(sieve(X))nats(ok(X))ok(nats(X))
active(s(X))s(active(X))active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))
filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))cons(mark(X1), X2)mark(cons(X1, X2))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))
s(mark(X))mark(s(X))proper(s(X))s(proper(X))
active(nats(X))nats(active(X))nats(mark(X))mark(nats(X))
proper(sieve(X))sieve(proper(X))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
sieve(ok(X))ok(sieve(X))active(sieve(X))sieve(active(X))
filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(filter(X1, X2, X3))filter(X1, X2, active(X3))s(ok(X))ok(s(X))
filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))
cons(ok(X1), ok(X2))ok(cons(X1, X2))active(nats(N))mark(cons(N, nats(s(N))))
active(zprimes)mark(sieve(nats(s(s(0)))))active(cons(X1, X2))cons(active(X1), X2)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(nats(X))nats(proper(X))
active(filter(X1, X2, X3))filter(X1, active(X2), X3)proper(zprimes)ok(zprimes)
active(filter(X1, X2, X3))filter(active(X1), X2, X3)proper(0)ok(0)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

top#(mark(X))top#(proper(X))

Problem 12: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

top#(ok(X))top#(active(X))

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, sieve, s, active, ok, mark, proper, zprimes, filter, top, cons

Strategy


Polynomial Interpretation

Improved Usable rules

nats(ok(X))ok(nats(X))sieve(mark(X))mark(sieve(X))
active(s(X))s(active(X))active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))
filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))cons(mark(X1), X2)mark(cons(X1, X2))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))s(mark(X))mark(s(X))
nats(mark(X))mark(nats(X))active(nats(X))nats(active(X))
active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))sieve(ok(X))ok(sieve(X))
active(sieve(X))sieve(active(X))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))active(filter(X1, X2, X3))filter(X1, X2, active(X3))
s(ok(X))ok(s(X))filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))cons(ok(X1), ok(X2))ok(cons(X1, X2))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(cons(X1, X2))cons(active(X1), X2)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(active(X1), X2, X3)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

top#(ok(X))top#(active(X))

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

proper#(s(X))proper#(X)proper#(cons(X1, X2))proper#(X1)
proper#(filter(X1, X2, X3))proper#(X3)proper#(cons(X1, X2))proper#(X2)
proper#(filter(X1, X2, X3))proper#(X1)proper#(filter(X1, X2, X3))proper#(X2)
proper#(nats(X))proper#(X)proper#(sieve(X))proper#(X)

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(s(X))proper#(X)proper#(cons(X1, X2))proper#(X1)
proper#(cons(X1, X2))proper#(X2)proper#(filter(X1, X2, X3))proper#(X3)
proper#(filter(X1, X2, X3))proper#(X2)proper#(filter(X1, X2, X3))proper#(X1)
proper#(nats(X))proper#(X)proper#(sieve(X))proper#(X)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

cons#(mark(X1), X2)cons#(X1, X2)cons#(ok(X1), ok(X2))cons#(X1, X2)

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, 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 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

nats#(ok(X))nats#(X)nats#(mark(X))nats#(X)

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

nats#(ok(X))nats#(X)nats#(mark(X))nats#(X)

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

active#(nats(X))active#(X)active#(s(X))active#(X)
active#(sieve(X))active#(X)active#(filter(X1, X2, X3))active#(X2)
active#(filter(X1, X2, X3))active#(X1)active#(cons(X1, X2))active#(X1)
active#(filter(X1, X2, X3))active#(X3)

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(nats(X))active#(X)active#(s(X))active#(X)
active#(sieve(X))active#(X)active#(filter(X1, X2, X3))active#(X2)
active#(filter(X1, X2, X3))active#(X3)active#(filter(X1, X2, X3))active#(X1)
active#(cons(X1, X2))active#(X1)

Problem 7: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

s#(mark(X))s#(X)s#(ok(X))s#(X)

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, 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 8: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

sieve#(ok(X))sieve#(X)sieve#(mark(X))sieve#(X)

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, 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 9: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

filter#(X1, X2, mark(X3))filter#(X1, X2, X3)filter#(ok(X1), ok(X2), ok(X3))filter#(X1, X2, X3)
filter#(X1, mark(X2), X3)filter#(X1, X2, X3)filter#(mark(X1), X2, X3)filter#(X1, X2, X3)

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

filter#(ok(X1), ok(X2), ok(X3))filter#(X1, X2, X3)filter#(mark(X1), X2, X3)filter#(X1, X2, X3)

Problem 10: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

filter#(X1, X2, mark(X3))filter#(X1, X2, X3)filter#(X1, mark(X2), X3)filter#(X1, X2, X3)

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, sieve, s, active, ok, mark, proper, zprimes, filter, top, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

filter#(X1, mark(X2), X3)filter#(X1, X2, X3)

Problem 11: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

filter#(X1, X2, mark(X3))filter#(X1, X2, X3)

Rewrite Rules

active(filter(cons(X, Y), 0, M))mark(cons(0, filter(Y, M, M)))active(filter(cons(X, Y), s(N), M))mark(cons(X, filter(Y, N, M)))
active(sieve(cons(0, Y)))mark(cons(0, sieve(Y)))active(sieve(cons(s(N), Y)))mark(cons(s(N), sieve(filter(Y, N, N))))
active(nats(N))mark(cons(N, nats(s(N))))active(zprimes)mark(sieve(nats(s(s(0)))))
active(filter(X1, X2, X3))filter(active(X1), X2, X3)active(filter(X1, X2, X3))filter(X1, active(X2), X3)
active(filter(X1, X2, X3))filter(X1, X2, active(X3))active(cons(X1, X2))cons(active(X1), X2)
active(s(X))s(active(X))active(sieve(X))sieve(active(X))
active(nats(X))nats(active(X))filter(mark(X1), X2, X3)mark(filter(X1, X2, X3))
filter(X1, mark(X2), X3)mark(filter(X1, X2, X3))filter(X1, X2, mark(X3))mark(filter(X1, X2, X3))
cons(mark(X1), X2)mark(cons(X1, X2))s(mark(X))mark(s(X))
sieve(mark(X))mark(sieve(X))nats(mark(X))mark(nats(X))
proper(filter(X1, X2, X3))filter(proper(X1), proper(X2), proper(X3))proper(cons(X1, X2))cons(proper(X1), proper(X2))
proper(0)ok(0)proper(s(X))s(proper(X))
proper(sieve(X))sieve(proper(X))proper(nats(X))nats(proper(X))
proper(zprimes)ok(zprimes)filter(ok(X1), ok(X2), ok(X3))ok(filter(X1, X2, X3))
cons(ok(X1), ok(X2))ok(cons(X1, X2))s(ok(X))ok(s(X))
sieve(ok(X))ok(sieve(X))nats(ok(X))ok(nats(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top

Strategy


Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

filter#(X1, X2, mark(X3))filter#(X1, X2, X3)