YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (114ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (114ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4 (43ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4 (136ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4 (98ms).
 |    |    |    |    | – Problem 6 was processed with processor PolynomialLinearRange4 (28ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

T(sieve(Y)) → sieve#(Y)T(filter(X, sieve(Y))) → filter#(X, sieve(Y))
if#(false, X, Y) → T(Y)T(filter(x_1, x_2)) → T(x_2)
T(cons(x_1, x_2)) → T(x_2)T(from(x_1)) → T(x_1)
T(cons(x_1, x_2)) → T(x_1)tail#(cons(X, Y)) → T(Y)
primes# → sieve#(from(s(s(0))))T(filter(s(s(X)), Z)) → filter#(s(s(X)), Z)
T(filter(x_1, x_2)) → T(x_1)T(s(x_1)) → T(x_1)
primes# → from#(s(s(0)))T(sieve(x_1)) → T(x_1)
filter#(s(s(X)), cons(Y, Z)) → if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))T(from(s(X))) → from#(s(X))
if#(true, X, Y) → T(X)

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Context-sensitive strategy:
μ(true) = μ(T) = μ(primes#) = μ(0) = μ(false) = μ(primes) = ∅
μ(from#) = μ(sieve) = μ(sieve#) = μ(from) = μ(tail#) = μ(tail) = μ(s) = μ(if) = μ(if#) = μ(head#) = μ(head) = μ(cons) = {1}
μ(divides) = μ(filter#) = μ(filter) = {1, 2}

The following SCCs where found

T(filter(x_1, x_2)) → T(x_2)T(cons(x_1, x_2)) → T(x_2)
T(s(x_1)) → T(x_1)T(from(x_1)) → T(x_1)
T(sieve(x_1)) → T(x_1)T(cons(x_1, x_2)) → T(x_1)
T(filter(x_1, x_2)) → T(x_1)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(filter(x_1, x_2)) → T(x_2)T(cons(x_1, x_2)) → T(x_2)
T(s(x_1)) → T(x_1)T(from(x_1)) → T(x_1)
T(sieve(x_1)) → T(x_1)T(cons(x_1, x_2)) → T(x_1)
T(filter(x_1, x_2)) → T(x_1)

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Context-sensitive strategy:
μ(true) = μ(T) = μ(primes#) = μ(0) = μ(false) = μ(primes) = ∅
μ(from#) = μ(sieve) = μ(sieve#) = μ(from) = μ(tail#) = μ(tail) = μ(s) = μ(if) = μ(if#) = μ(head#) = μ(head) = μ(cons) = {1}
μ(divides) = μ(filter#) = μ(filter) = {1, 2}

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:

T(sieve(x_1)) → T(x_1)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(filter(x_1, x_2)) → T(x_2)T(s(x_1)) → T(x_1)
T(cons(x_1, x_2)) → T(x_2)T(from(x_1)) → T(x_1)
T(cons(x_1, x_2)) → T(x_1)T(filter(x_1, x_2)) → T(x_1)

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Context-sensitive strategy:
μ(true) = μ(T) = μ(primes#) = μ(0) = μ(false) = μ(primes) = ∅
μ(from#) = μ(sieve) = μ(sieve#) = μ(from) = μ(tail#) = μ(tail) = μ(s) = μ(if) = μ(if#) = μ(head#) = μ(head) = μ(cons) = {1}
μ(divides) = μ(filter#) = μ(filter) = {1, 2}

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:

T(s(x_1)) → T(x_1)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(filter(x_1, x_2)) → T(x_2)T(cons(x_1, x_2)) → T(x_2)
T(from(x_1)) → T(x_1)T(cons(x_1, x_2)) → T(x_1)
T(filter(x_1, x_2)) → T(x_1)

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Context-sensitive strategy:
μ(true) = μ(T) = μ(primes#) = μ(0) = μ(false) = μ(primes) = ∅
μ(from#) = μ(sieve) = μ(sieve#) = μ(from) = μ(tail#) = μ(tail) = μ(s) = μ(if) = μ(if#) = μ(head#) = μ(head) = μ(cons) = {1}
μ(divides) = μ(filter#) = μ(filter) = {1, 2}

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:

T(filter(x_1, x_2)) → T(x_2)T(filter(x_1, x_2)) → T(x_1)

Problem 5: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(cons(x_1, x_2)) → T(x_2)T(from(x_1)) → T(x_1)
T(cons(x_1, x_2)) → T(x_1)

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Context-sensitive strategy:
μ(true) = μ(T) = μ(primes#) = μ(0) = μ(false) = μ(primes) = ∅
μ(from#) = μ(sieve) = μ(sieve#) = μ(from) = μ(tail#) = μ(tail) = μ(s) = μ(if) = μ(if#) = μ(head#) = μ(head) = μ(cons) = {1}
μ(divides) = μ(filter#) = μ(filter) = {1, 2}

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:

T(from(x_1)) → T(x_1)

Problem 6: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(cons(x_1, x_2)) → T(x_2)T(cons(x_1, x_2)) → T(x_1)

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Context-sensitive strategy:
μ(true) = μ(T) = μ(primes#) = μ(0) = μ(false) = μ(primes) = ∅
μ(from#) = μ(sieve) = μ(sieve#) = μ(from) = μ(tail#) = μ(tail) = μ(s) = μ(if) = μ(if#) = μ(head#) = μ(head) = μ(cons) = {1}
μ(divides) = μ(filter#) = μ(filter) = {1, 2}

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:

T(cons(x_1, x_2)) → T(x_2)T(cons(x_1, x_2)) → T(x_1)