(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, n__filter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) → cons(X, n__filter(activate(Y), N, M))
sieve(cons(0, Y)) → cons(0, n__sieve(activate(Y)))
sieve(cons(s(N), Y)) → cons(s(N), n__sieve(filter(activate(Y), N, N)))
nats(N) → cons(N, n__nats(s(N)))
zprimessieve(nats(s(s(0))))
filter(X1, X2, X3) → n__filter(X1, X2, X3)
sieve(X) → n__sieve(X)
nats(X) → n__nats(X)
activate(n__filter(X1, X2, X3)) → filter(X1, X2, X3)
activate(n__sieve(X)) → sieve(X)
activate(n__nats(X)) → nats(X)
activate(X) → X

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FILTER(cons(X, Y), 0, M) → ACTIVATE(Y)
FILTER(cons(X, Y), s(N), M) → ACTIVATE(Y)
SIEVE(cons(0, Y)) → ACTIVATE(Y)
SIEVE(cons(s(N), Y)) → FILTER(activate(Y), N, N)
SIEVE(cons(s(N), Y)) → ACTIVATE(Y)
ZPRIMESSIEVE(nats(s(s(0))))
ZPRIMESNATS(s(s(0)))
ACTIVATE(n__filter(X1, X2, X3)) → FILTER(X1, X2, X3)
ACTIVATE(n__sieve(X)) → SIEVE(X)
ACTIVATE(n__nats(X)) → NATS(X)

The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, n__filter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) → cons(X, n__filter(activate(Y), N, M))
sieve(cons(0, Y)) → cons(0, n__sieve(activate(Y)))
sieve(cons(s(N), Y)) → cons(s(N), n__sieve(filter(activate(Y), N, N)))
nats(N) → cons(N, n__nats(s(N)))
zprimessieve(nats(s(s(0))))
filter(X1, X2, X3) → n__filter(X1, X2, X3)
sieve(X) → n__sieve(X)
nats(X) → n__nats(X)
activate(n__filter(X1, X2, X3)) → filter(X1, X2, X3)
activate(n__sieve(X)) → sieve(X)
activate(n__nats(X)) → nats(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__filter(X1, X2, X3)) → FILTER(X1, X2, X3)
FILTER(cons(X, Y), 0, M) → ACTIVATE(Y)
ACTIVATE(n__sieve(X)) → SIEVE(X)
SIEVE(cons(0, Y)) → ACTIVATE(Y)
SIEVE(cons(s(N), Y)) → FILTER(activate(Y), N, N)
FILTER(cons(X, Y), s(N), M) → ACTIVATE(Y)
SIEVE(cons(s(N), Y)) → ACTIVATE(Y)

The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, n__filter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) → cons(X, n__filter(activate(Y), N, M))
sieve(cons(0, Y)) → cons(0, n__sieve(activate(Y)))
sieve(cons(s(N), Y)) → cons(s(N), n__sieve(filter(activate(Y), N, N)))
nats(N) → cons(N, n__nats(s(N)))
zprimessieve(nats(s(s(0))))
filter(X1, X2, X3) → n__filter(X1, X2, X3)
sieve(X) → n__sieve(X)
nats(X) → n__nats(X)
activate(n__filter(X1, X2, X3)) → filter(X1, X2, X3)
activate(n__sieve(X)) → sieve(X)
activate(n__nats(X)) → nats(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(5) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ACTIVATE(n__sieve(X)) → SIEVE(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVATE(x1)  =  ACTIVATE(x1)
n__filter(x1, x2, x3)  =  x1
FILTER(x1, x2, x3)  =  FILTER(x1)
cons(x1, x2)  =  x2
0  =  0
n__sieve(x1)  =  n__sieve(x1)
SIEVE(x1)  =  SIEVE(x1)
s(x1)  =  s
activate(x1)  =  x1
filter(x1, x2, x3)  =  x1
sieve(x1)  =  sieve(x1)
nats(x1)  =  x1
n__nats(x1)  =  x1
zprimes  =  zprimes

Recursive path order with status [RPO].
Quasi-Precedence:
[0, zprimes] > [ACTIVATE1, FILTER1, SIEVE1] > s
[0, zprimes] > [nsieve1, sieve1] > s

Status:
ACTIVATE1: multiset
FILTER1: multiset
0: multiset
nsieve1: multiset
SIEVE1: multiset
s: multiset
sieve1: multiset
zprimes: multiset


The following usable rules [FROCOS05] were oriented:

filter(cons(X, Y), 0, M) → cons(0, n__filter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) → cons(X, n__filter(activate(Y), N, M))
sieve(cons(0, Y)) → cons(0, n__sieve(activate(Y)))
sieve(cons(s(N), Y)) → cons(s(N), n__sieve(filter(activate(Y), N, N)))
nats(N) → cons(N, n__nats(s(N)))
zprimessieve(nats(s(s(0))))
filter(X1, X2, X3) → n__filter(X1, X2, X3)
sieve(X) → n__sieve(X)
nats(X) → n__nats(X)
activate(n__filter(X1, X2, X3)) → filter(X1, X2, X3)
activate(n__sieve(X)) → sieve(X)
activate(n__nats(X)) → nats(X)
activate(X) → X

(6) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__filter(X1, X2, X3)) → FILTER(X1, X2, X3)
FILTER(cons(X, Y), 0, M) → ACTIVATE(Y)
SIEVE(cons(0, Y)) → ACTIVATE(Y)
SIEVE(cons(s(N), Y)) → FILTER(activate(Y), N, N)
FILTER(cons(X, Y), s(N), M) → ACTIVATE(Y)
SIEVE(cons(s(N), Y)) → ACTIVATE(Y)

The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, n__filter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) → cons(X, n__filter(activate(Y), N, M))
sieve(cons(0, Y)) → cons(0, n__sieve(activate(Y)))
sieve(cons(s(N), Y)) → cons(s(N), n__sieve(filter(activate(Y), N, N)))
nats(N) → cons(N, n__nats(s(N)))
zprimessieve(nats(s(s(0))))
filter(X1, X2, X3) → n__filter(X1, X2, X3)
sieve(X) → n__sieve(X)
nats(X) → n__nats(X)
activate(n__filter(X1, X2, X3)) → filter(X1, X2, X3)
activate(n__sieve(X)) → sieve(X)
activate(n__nats(X)) → nats(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FILTER(cons(X, Y), 0, M) → ACTIVATE(Y)
ACTIVATE(n__filter(X1, X2, X3)) → FILTER(X1, X2, X3)
FILTER(cons(X, Y), s(N), M) → ACTIVATE(Y)

The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, n__filter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) → cons(X, n__filter(activate(Y), N, M))
sieve(cons(0, Y)) → cons(0, n__sieve(activate(Y)))
sieve(cons(s(N), Y)) → cons(s(N), n__sieve(filter(activate(Y), N, N)))
nats(N) → cons(N, n__nats(s(N)))
zprimessieve(nats(s(s(0))))
filter(X1, X2, X3) → n__filter(X1, X2, X3)
sieve(X) → n__sieve(X)
nats(X) → n__nats(X)
activate(n__filter(X1, X2, X3)) → filter(X1, X2, X3)
activate(n__sieve(X)) → sieve(X)
activate(n__nats(X)) → nats(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(9) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


FILTER(cons(X, Y), 0, M) → ACTIVATE(Y)
FILTER(cons(X, Y), s(N), M) → ACTIVATE(Y)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
FILTER(x1, x2, x3)  =  FILTER(x1, x2, x3)
cons(x1, x2)  =  x2
0  =  0
ACTIVATE(x1)  =  x1
n__filter(x1, x2, x3)  =  n__filter(x1, x2, x3)
s(x1)  =  s(x1)
filter(x1, x2, x3)  =  filter(x1, x2, x3)
activate(x1)  =  activate(x1)
sieve(x1)  =  sieve
n__sieve(x1)  =  n__sieve
nats(x1)  =  nats(x1)
n__nats(x1)  =  x1
zprimes  =  zprimes

Recursive path order with status [RPO].
Quasi-Precedence:
zprimes > [0, filter3, activate1] > [FILTER3, nfilter3]
zprimes > [0, filter3, activate1] > sieve > s1
zprimes > [0, filter3, activate1] > sieve > nsieve
zprimes > [0, filter3, activate1] > nats1 > s1

Status:
FILTER3: multiset
0: multiset
nfilter3: multiset
s1: multiset
filter3: multiset
activate1: multiset
sieve: multiset
nsieve: []
nats1: [1]
zprimes: multiset


The following usable rules [FROCOS05] were oriented:

filter(cons(X, Y), 0, M) → cons(0, n__filter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) → cons(X, n__filter(activate(Y), N, M))
sieve(cons(0, Y)) → cons(0, n__sieve(activate(Y)))
sieve(cons(s(N), Y)) → cons(s(N), n__sieve(filter(activate(Y), N, N)))
nats(N) → cons(N, n__nats(s(N)))
zprimessieve(nats(s(s(0))))
filter(X1, X2, X3) → n__filter(X1, X2, X3)
sieve(X) → n__sieve(X)
nats(X) → n__nats(X)
activate(n__filter(X1, X2, X3)) → filter(X1, X2, X3)
activate(n__sieve(X)) → sieve(X)
activate(n__nats(X)) → nats(X)
activate(X) → X

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__filter(X1, X2, X3)) → FILTER(X1, X2, X3)

The TRS R consists of the following rules:

filter(cons(X, Y), 0, M) → cons(0, n__filter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) → cons(X, n__filter(activate(Y), N, M))
sieve(cons(0, Y)) → cons(0, n__sieve(activate(Y)))
sieve(cons(s(N), Y)) → cons(s(N), n__sieve(filter(activate(Y), N, N)))
nats(N) → cons(N, n__nats(s(N)))
zprimessieve(nats(s(s(0))))
filter(X1, X2, X3) → n__filter(X1, X2, X3)
sieve(X) → n__sieve(X)
nats(X) → n__nats(X)
activate(n__filter(X1, X2, X3)) → filter(X1, X2, X3)
activate(n__sieve(X)) → sieve(X)
activate(n__nats(X)) → nats(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(11) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(12) TRUE