0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 PisEmptyProof (⇔)
↳9 TRUE
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 PisEmptyProof (⇔)
↳14 TRUE
↳15 QDP
↳16 QDPOrderProof (⇔)
↳17 QDP
↳18 PisEmptyProof (⇔)
↳19 TRUE
↳20 QDP
↳21 QDPOrderProof (⇔)
↳22 QDP
↳23 QDPOrderProof (⇔)
↳24 QDP
↳25 QDPOrderProof (⇔)
↳26 QDP
↳27 PisEmptyProof (⇔)
↳28 TRUE
↳29 QDP
↳30 QDPOrderProof (⇔)
↳31 QDP
↳32 QDPOrderProof (⇔)
↳33 QDP
↳34 QDPOrderProof (⇔)
↳35 QDP
↳36 QDPOrderProof (⇔)
↳37 QDP
↳38 PisEmptyProof (⇔)
↳39 TRUE
↳40 QDP
↳41 QDPOrderProof (⇔)
↳42 QDP
↳43 DependencyGraphProof (⇔)
↳44 QDP
↳45 QDPOrderProof (⇔)
↳46 QDP
↳47 DependencyGraphProof (⇔)
↳48 TRUE
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
ACTIVE(filter(cons(X, Y), 0, M)) → MARK(cons(0, filter(Y, M, M)))
ACTIVE(filter(cons(X, Y), 0, M)) → CONS(0, filter(Y, M, M))
ACTIVE(filter(cons(X, Y), 0, M)) → FILTER(Y, M, M)
ACTIVE(filter(cons(X, Y), s(N), M)) → MARK(cons(X, filter(Y, N, M)))
ACTIVE(filter(cons(X, Y), s(N), M)) → CONS(X, filter(Y, N, M))
ACTIVE(filter(cons(X, Y), s(N), M)) → FILTER(Y, N, M)
ACTIVE(sieve(cons(0, Y))) → MARK(cons(0, sieve(Y)))
ACTIVE(sieve(cons(0, Y))) → CONS(0, sieve(Y))
ACTIVE(sieve(cons(0, Y))) → SIEVE(Y)
ACTIVE(sieve(cons(s(N), Y))) → MARK(cons(s(N), sieve(filter(Y, N, N))))
ACTIVE(sieve(cons(s(N), Y))) → CONS(s(N), sieve(filter(Y, N, N)))
ACTIVE(sieve(cons(s(N), Y))) → SIEVE(filter(Y, N, N))
ACTIVE(sieve(cons(s(N), Y))) → FILTER(Y, N, N)
ACTIVE(nats(N)) → MARK(cons(N, nats(s(N))))
ACTIVE(nats(N)) → CONS(N, nats(s(N)))
ACTIVE(nats(N)) → NATS(s(N))
ACTIVE(nats(N)) → S(N)
ACTIVE(zprimes) → MARK(sieve(nats(s(s(0)))))
ACTIVE(zprimes) → SIEVE(nats(s(s(0))))
ACTIVE(zprimes) → NATS(s(s(0)))
ACTIVE(zprimes) → S(s(0))
ACTIVE(zprimes) → S(0)
MARK(filter(X1, X2, X3)) → ACTIVE(filter(mark(X1), mark(X2), mark(X3)))
MARK(filter(X1, X2, X3)) → 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)) → ACTIVE(cons(mark(X1), X2))
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(0) → ACTIVE(0)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → S(mark(X))
MARK(s(X)) → MARK(X)
MARK(sieve(X)) → ACTIVE(sieve(mark(X)))
MARK(sieve(X)) → SIEVE(mark(X))
MARK(sieve(X)) → MARK(X)
MARK(nats(X)) → ACTIVE(nats(mark(X)))
MARK(nats(X)) → NATS(mark(X))
MARK(nats(X)) → MARK(X)
MARK(zprimes) → ACTIVE(zprimes)
FILTER(mark(X1), X2, X3) → FILTER(X1, X2, X3)
FILTER(X1, mark(X2), X3) → FILTER(X1, X2, X3)
FILTER(X1, X2, mark(X3)) → FILTER(X1, X2, X3)
FILTER(active(X1), X2, X3) → FILTER(X1, X2, X3)
FILTER(X1, active(X2), X3) → FILTER(X1, X2, X3)
FILTER(X1, X2, active(X3)) → FILTER(X1, X2, X3)
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)
S(mark(X)) → S(X)
S(active(X)) → S(X)
SIEVE(mark(X)) → SIEVE(X)
SIEVE(active(X)) → SIEVE(X)
NATS(mark(X)) → NATS(X)
NATS(active(X)) → NATS(X)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
NATS(active(X)) → NATS(X)
NATS(mark(X)) → NATS(X)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
NATS(active(X)) → NATS(X)
NATS(mark(X)) → NATS(X)
filter > [active1, mark1, cons, 0, s, sieve, nats]
zprimes > [active1, mark1, cons, 0, s, sieve, nats]
active1: multiset
mark1: multiset
filter: multiset
cons: multiset
0: multiset
s: []
sieve: multiset
nats: multiset
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
SIEVE(active(X)) → SIEVE(X)
SIEVE(mark(X)) → SIEVE(X)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SIEVE(active(X)) → SIEVE(X)
SIEVE(mark(X)) → SIEVE(X)
filter > [active1, mark1, cons, 0, s, sieve, nats]
zprimes > [active1, mark1, cons, 0, s, sieve, nats]
active1: multiset
mark1: multiset
filter: multiset
cons: multiset
0: multiset
s: []
sieve: multiset
nats: multiset
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
S(active(X)) → S(X)
S(mark(X)) → S(X)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(active(X)) → S(X)
S(mark(X)) → S(X)
filter > [active1, mark1, cons, 0, s, sieve, nats]
zprimes > [active1, mark1, cons, 0, s, sieve, nats]
active1: multiset
mark1: multiset
filter: multiset
cons: multiset
0: multiset
s: []
sieve: multiset
nats: multiset
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
zprimes > nats > [CONS2, mark1, filter2, cons, 0, s1, sieve1]
CONS2: [1,2]
mark1: [1]
filter2: [2,1]
cons: multiset
0: multiset
s1: [1]
sieve1: [1]
nats: []
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CONS(X1, active(X2)) → CONS(X1, X2)
zprimes > [0, sieve] > [filter2, mark1] > active1 > [cons, s1]
zprimes > nats > [filter2, mark1] > active1 > [cons, s1]
CONS1: [1]
active1: [1]
filter2: multiset
cons: multiset
0: multiset
mark1: multiset
s1: multiset
sieve: multiset
nats: []
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
CONS(active(X1), X2) → CONS(X1, X2)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CONS(active(X1), X2) → CONS(X1, X2)
0 > sieve > [filter2, mark1] > active1 > [cons, s1] > CONS2
zprimes > sieve > [filter2, mark1] > active1 > [cons, s1] > CONS2
zprimes > nats > [filter2, mark1] > active1 > [cons, s1] > CONS2
CONS2: [1,2]
active1: multiset
filter2: multiset
cons: []
0: multiset
mark1: multiset
s1: [1]
sieve: []
nats: []
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
FILTER(X1, mark(X2), X3) → FILTER(X1, X2, X3)
FILTER(mark(X1), X2, X3) → FILTER(X1, X2, X3)
FILTER(X1, X2, mark(X3)) → FILTER(X1, X2, X3)
FILTER(active(X1), X2, X3) → FILTER(X1, X2, X3)
FILTER(X1, active(X2), X3) → FILTER(X1, X2, X3)
FILTER(X1, X2, active(X3)) → FILTER(X1, X2, X3)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FILTER(mark(X1), X2, X3) → FILTER(X1, X2, X3)
zprimes > [mark1, filter2, sieve1, nats1] > 0 > [cons, s1]
mark1: multiset
filter2: multiset
cons: multiset
0: multiset
s1: multiset
sieve1: multiset
nats1: multiset
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
FILTER(X1, mark(X2), X3) → FILTER(X1, X2, X3)
FILTER(X1, X2, mark(X3)) → FILTER(X1, X2, X3)
FILTER(active(X1), X2, X3) → FILTER(X1, X2, X3)
FILTER(X1, active(X2), X3) → FILTER(X1, X2, X3)
FILTER(X1, X2, active(X3)) → FILTER(X1, X2, X3)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FILTER(X1, mark(X2), X3) → FILTER(X1, X2, X3)
FILTER(X1, active(X2), X3) → FILTER(X1, X2, X3)
filter > [mark1, active1, cons, 0, s, sieve, nats]
zprimes > [mark1, active1, cons, 0, s, sieve, nats]
mark1: multiset
active1: multiset
filter: multiset
cons: []
0: multiset
s: []
sieve: []
nats: []
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
FILTER(X1, X2, mark(X3)) → FILTER(X1, X2, X3)
FILTER(active(X1), X2, X3) → FILTER(X1, X2, X3)
FILTER(X1, X2, active(X3)) → FILTER(X1, X2, X3)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FILTER(X1, X2, mark(X3)) → FILTER(X1, X2, X3)
FILTER(X1, X2, active(X3)) → FILTER(X1, X2, X3)
filter > [FILTER1, mark1, active1, cons, 0, s, sieve, nats]
zprimes > [FILTER1, mark1, active1, cons, 0, s, sieve, nats]
FILTER1: [1]
mark1: multiset
active1: multiset
filter: multiset
cons: multiset
0: multiset
s: []
sieve: multiset
nats: multiset
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
FILTER(active(X1), X2, X3) → FILTER(X1, X2, X3)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FILTER(active(X1), X2, X3) → FILTER(X1, X2, X3)
filter > [FILTER2, active1, cons, 0, mark1, s, sieve, nats]
zprimes > [FILTER2, active1, cons, 0, mark1, s, sieve, nats]
FILTER2: [2,1]
active1: multiset
filter: multiset
cons: []
0: multiset
mark1: multiset
s: []
sieve: []
nats: []
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
MARK(filter(X1, X2, X3)) → ACTIVE(filter(mark(X1), mark(X2), mark(X3)))
ACTIVE(filter(cons(X, Y), 0, M)) → MARK(cons(0, filter(Y, M, M)))
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)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(filter(cons(X, Y), s(N), M)) → MARK(cons(X, filter(Y, N, M)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(s(X)) → ACTIVE(s(mark(X)))
ACTIVE(sieve(cons(0, Y))) → MARK(cons(0, sieve(Y)))
MARK(s(X)) → MARK(X)
MARK(sieve(X)) → ACTIVE(sieve(mark(X)))
ACTIVE(sieve(cons(s(N), Y))) → MARK(cons(s(N), sieve(filter(Y, N, N))))
MARK(sieve(X)) → MARK(X)
MARK(nats(X)) → ACTIVE(nats(mark(X)))
ACTIVE(nats(N)) → MARK(cons(N, nats(s(N))))
MARK(nats(X)) → MARK(X)
MARK(zprimes) → ACTIVE(zprimes)
ACTIVE(zprimes) → MARK(sieve(nats(s(s(0)))))
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(filter(cons(X, Y), 0, M)) → MARK(cons(0, filter(Y, M, M)))
MARK(filter(X1, X2, X3)) → MARK(X1)
MARK(filter(X1, X2, X3)) → MARK(X2)
MARK(filter(X1, X2, X3)) → MARK(X3)
ACTIVE(filter(cons(X, Y), s(N), M)) → MARK(cons(X, filter(Y, N, M)))
MARK(cons(X1, X2)) → MARK(X1)
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))))
MARK(sieve(X)) → MARK(X)
MARK(nats(X)) → MARK(X)
ACTIVE(zprimes) → MARK(sieve(nats(s(s(0)))))
zprimes > [MARK1, filter3, ACTIVE1, cons1, 0, sieve1, nats1]
MARK1: multiset
filter3: [1,2,3]
ACTIVE1: multiset
cons1: [1]
0: multiset
sieve1: multiset
nats1: [1]
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
MARK(filter(X1, X2, X3)) → ACTIVE(filter(mark(X1), mark(X2), mark(X3)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(sieve(X)) → ACTIVE(sieve(mark(X)))
MARK(nats(X)) → ACTIVE(nats(mark(X)))
ACTIVE(nats(N)) → MARK(cons(N, nats(s(N))))
MARK(zprimes) → ACTIVE(zprimes)
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
ACTIVE(nats(N)) → MARK(cons(N, nats(s(N))))
MARK(filter(X1, X2, X3)) → ACTIVE(filter(mark(X1), mark(X2), mark(X3)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(sieve(X)) → ACTIVE(sieve(mark(X)))
MARK(nats(X)) → ACTIVE(nats(mark(X)))
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(nats(N)) → MARK(cons(N, nats(s(N))))
MARK(s(X)) → MARK(X)
zprimes > [nats1, cons, s1, sieve1, 0]
nats1: [1]
cons: []
s1: multiset
sieve1: multiset
0: multiset
zprimes: multiset
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)
MARK(filter(X1, X2, X3)) → ACTIVE(filter(mark(X1), mark(X2), mark(X3)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(sieve(X)) → ACTIVE(sieve(mark(X)))
MARK(nats(X)) → ACTIVE(nats(mark(X)))
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)))))
mark(filter(X1, X2, X3)) → active(filter(mark(X1), mark(X2), mark(X3)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sieve(X)) → active(sieve(mark(X)))
mark(nats(X)) → active(nats(mark(X)))
mark(zprimes) → active(zprimes)
filter(mark(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, mark(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, mark(X3)) → filter(X1, X2, X3)
filter(active(X1), X2, X3) → filter(X1, X2, X3)
filter(X1, active(X2), X3) → filter(X1, X2, X3)
filter(X1, X2, active(X3)) → filter(X1, X2, X3)
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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
nats(mark(X)) → nats(X)
nats(active(X)) → nats(X)