Term Rewriting System R:

   [X, Y, M, N, X1, X2, X3]
   a__filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
   a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
   a__filter(X1, X2, X3) -> filter(X1, X2, X3)
   a__sieve(cons(0, Y)) -> cons(0, sieve(Y))
   a__sieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
   a__sieve(X) -> sieve(X)
   a__nats(N) -> cons(mark(N), nats(s(N)))
   a__nats(X) -> nats(X)
   a__zprimes -> a__sieve(a__nats(s(s(0))))
   a__zprimes -> zprimes
   mark(filter(X1, X2, X3)) -> a__filter(mark(X1), mark(X2), mark(X3))
   mark(sieve(X)) -> a__sieve(mark(X))
   mark(nats(X)) -> a__nats(mark(X))
   mark(zprimes) -> a__zprimes
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(0) -> 0
   mark(s(X)) -> s(mark(X))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   A__SIEVE(cons(s(N), Y)) -> MARK(N)
   MARK(s(X)) -> MARK(X)
   MARK(filter(X1, X2, X3)) -> A__FILTER(mark(X1), mark(X2), mark(X3))
   MARK(filter(X1, X2, X3)) -> MARK(X1)
   MARK(filter(X1, X2, X3)) -> MARK(X2)
   MARK(filter(X1, X2, X3)) -> MARK(X3)
   MARK(cons(X1, X2)) -> MARK(X1)
   MARK(zprimes) -> A__ZPRIMES
   MARK(nats(X)) -> A__NATS(mark(X))
   MARK(nats(X)) -> MARK(X)
   MARK(sieve(X)) -> A__SIEVE(mark(X))
   MARK(sieve(X)) -> MARK(X)
   A__FILTER(cons(X, Y), s(N), M) -> MARK(X)
   A__NATS(N) -> MARK(N)
   A__ZPRIMES -> A__SIEVE(a__nats(s(s(0))))
   A__ZPRIMES -> A__NATS(s(s(0)))

Furthermore, R contains one SCC.


SCC1:

MARK(sieve(X)) -> MARK(X)
MARK(sieve(X)) -> A__SIEVE(mark(X))
MARK(nats(X)) -> MARK(X)
MARK(nats(X)) -> A__NATS(mark(X))
A__NATS(N) -> MARK(N)
A__ZPRIMES -> A__NATS(s(s(0)))
A__ZPRIMES -> A__SIEVE(a__nats(s(s(0))))
MARK(zprimes) -> A__ZPRIMES
MARK(cons(X1, X2)) -> MARK(X1)
MARK(filter(X1, X2, X3)) -> MARK(X3)
MARK(filter(X1, X2, X3)) -> MARK(X2)
MARK(filter(X1, X2, X3)) -> MARK(X1)
A__FILTER(cons(X, Y), s(N), M) -> MARK(X)
MARK(filter(X1, X2, X3)) -> A__FILTER(mark(X1), mark(X2), mark(X3))
MARK(s(X)) -> MARK(X)
A__SIEVE(cons(s(N), Y)) -> MARK(N)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   a__zprimes -> zprimes
   a__zprimes -> a__sieve(a__nats(s(s(0))))
   a__filter(X1, X2, X3) -> filter(X1, X2, X3)
   a__filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
   a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
   mark(s(X)) -> s(mark(X))
   mark(filter(X1, X2, X3)) -> a__filter(mark(X1), mark(X2), mark(X3))
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(zprimes) -> a__zprimes
   mark(nats(X)) -> a__nats(mark(X))
   mark(sieve(X)) -> a__sieve(mark(X))
   mark(0) -> 0
   a__sieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
   a__sieve(X) -> sieve(X)
   a__sieve(cons(0, Y)) -> cons(0, sieve(Y))
   a__nats(X) -> nats(X)
   a__nats(N) -> cons(mark(N), nats(s(N)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(a__zprimes) = 1
POL(A__SIEVE(x_1)) = x_1
POL(s(x_1)) = x_1
POL(sieve(x_1)) = 1 + x_1
POL(nats(x_1)) = x_1
POL(zprimes) = 1
POL(A__FILTER(x_1, x_2, x_3)) = x_1
POL(mark(x_1)) = x_1
POL(a__filter(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(MARK(x_1)) = x_1
POL(A__NATS(x_1)) = x_1
POL(filter(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(0) = 0
POL(cons(x_1, x_2)) = x_1
POL(A__ZPRIMES) = 0
POL(a__sieve(x_1)) = 1 + x_1
POL(a__nats(x_1)) = x_1

 resulting in one subcycle.


SCC1.Polo1:

A__NATS(N) -> MARK(N)
MARK(nats(X)) -> A__NATS(mark(X))
MARK(cons(X1, X2)) -> MARK(X1)
MARK(filter(X1, X2, X3)) -> MARK(X3)
MARK(filter(X1, X2, X3)) -> MARK(X2)
MARK(filter(X1, X2, X3)) -> MARK(X1)
A__FILTER(cons(X, Y), s(N), M) -> MARK(X)
MARK(filter(X1, X2, X3)) -> A__FILTER(mark(X1), mark(X2), mark(X3))
MARK(s(X)) -> MARK(X)
MARK(nats(X)) -> MARK(X)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   a__zprimes -> zprimes
   a__zprimes -> a__sieve(a__nats(s(s(0))))
   a__filter(X1, X2, X3) -> filter(X1, X2, X3)
   a__filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
   a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
   mark(s(X)) -> s(mark(X))
   mark(filter(X1, X2, X3)) -> a__filter(mark(X1), mark(X2), mark(X3))
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(zprimes) -> a__zprimes
   mark(nats(X)) -> a__nats(mark(X))
   mark(sieve(X)) -> a__sieve(mark(X))
   mark(0) -> 0
   a__sieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
   a__sieve(X) -> sieve(X)
   a__sieve(cons(0, Y)) -> cons(0, sieve(Y))
   a__nats(X) -> nats(X)
   a__nats(N) -> cons(mark(N), nats(s(N)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(a__zprimes) = 1
POL(s(x_1)) = x_1
POL(sieve(x_1)) = x_1
POL(nats(x_1)) = 1 + x_1
POL(zprimes) = 1
POL(A__FILTER(x_1, x_2, x_3)) = x_1
POL(MARK(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(a__filter(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(filter(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(A__NATS(x_1)) = 1 + x_1
POL(0) = 0
POL(cons(x_1, x_2)) = x_1
POL(a__sieve(x_1)) = x_1
POL(a__nats(x_1)) = 1 + x_1

 resulting in one subcycle.


SCC1.Polo1.Polo1:

MARK(filter(X1, X2, X3)) -> MARK(X3)
MARK(filter(X1, X2, X3)) -> MARK(X2)
MARK(filter(X1, X2, X3)) -> MARK(X1)
A__FILTER(cons(X, Y), s(N), M) -> MARK(X)
MARK(filter(X1, X2, X3)) -> A__FILTER(mark(X1), mark(X2), mark(X3))
MARK(s(X)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   a__zprimes -> zprimes
   a__zprimes -> a__sieve(a__nats(s(s(0))))
   a__filter(X1, X2, X3) -> filter(X1, X2, X3)
   a__filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
   a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
   mark(s(X)) -> s(mark(X))
   mark(filter(X1, X2, X3)) -> a__filter(mark(X1), mark(X2), mark(X3))
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(zprimes) -> a__zprimes
   mark(nats(X)) -> a__nats(mark(X))
   mark(sieve(X)) -> a__sieve(mark(X))
   mark(0) -> 0
   a__sieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
   a__sieve(X) -> sieve(X)
   a__sieve(cons(0, Y)) -> cons(0, sieve(Y))
   a__nats(X) -> nats(X)
   a__nats(N) -> cons(mark(N), nats(s(N)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(a__zprimes) = 0
POL(s(x_1)) = x_1
POL(sieve(x_1)) = x_1
POL(nats(x_1)) = x_1
POL(zprimes) = 0
POL(A__FILTER(x_1, x_2, x_3)) = x_1
POL(mark(x_1)) = x_1
POL(a__filter(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3
POL(MARK(x_1)) = x_1
POL(filter(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3
POL(0) = 0
POL(cons(x_1, x_2)) = x_1
POL(a__sieve(x_1)) = x_1
POL(a__nats(x_1)) = x_1

 resulting in one subcycle.


SCC1.Polo1.Polo1.Polo1:

MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(MARK(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   MARK(cons(X1, X2)) -> MARK(X1)
   MARK(s(X)) -> MARK(X)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 3.651 seconds.