Term Rewriting System R:
[X, Y, M, N, X1, X2, X3]
afilter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
afilter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
afilter(X1, X2, X3) -> filter(X1, X2, X3)
asieve(cons(0, Y)) -> cons(0, sieve(Y))
asieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
asieve(X) -> sieve(X)
anats(N) -> cons(mark(N), nats(s(N)))
anats(X) -> nats(X)
azprimes -> asieve(anats(s(s(0))))
azprimes -> zprimes
mark(filter(X1, X2, X3)) -> afilter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) -> asieve(mark(X))
mark(nats(X)) -> anats(mark(X))
mark(zprimes) -> azprimes
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(0) -> 0
mark(s(X)) -> s(mark(X))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

AFILTER(cons(X, Y), s(N), M) -> MARK(X)
ASIEVE(cons(s(N), Y)) -> MARK(N)
ANATS(N) -> MARK(N)
AZPRIMES -> ASIEVE(anats(s(s(0))))
AZPRIMES -> ANATS(s(s(0)))
MARK(filter(X1, X2, X3)) -> AFILTER(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(sieve(X)) -> ASIEVE(mark(X))
MARK(sieve(X)) -> MARK(X)
MARK(nats(X)) -> ANATS(mark(X))
MARK(nats(X)) -> MARK(X)
MARK(zprimes) -> AZPRIMES
MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)

Furthermore, R contains one SCC.


   R
DPs
       →DP Problem 1
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

MARK(s(X)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)
AZPRIMES -> ANATS(s(s(0)))
AZPRIMES -> ASIEVE(anats(s(s(0))))
MARK(zprimes) -> AZPRIMES
MARK(nats(X)) -> MARK(X)
ANATS(N) -> MARK(N)
MARK(nats(X)) -> ANATS(mark(X))
MARK(sieve(X)) -> MARK(X)
ASIEVE(cons(s(N), Y)) -> MARK(N)
MARK(sieve(X)) -> ASIEVE(mark(X))
MARK(filter(X1, X2, X3)) -> MARK(X3)
MARK(filter(X1, X2, X3)) -> MARK(X2)
MARK(filter(X1, X2, X3)) -> MARK(X1)
MARK(filter(X1, X2, X3)) -> AFILTER(mark(X1), mark(X2), mark(X3))
AFILTER(cons(X, Y), s(N), M) -> MARK(X)


Rules:


afilter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
afilter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
afilter(X1, X2, X3) -> filter(X1, X2, X3)
asieve(cons(0, Y)) -> cons(0, sieve(Y))
asieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
asieve(X) -> sieve(X)
anats(N) -> cons(mark(N), nats(s(N)))
anats(X) -> nats(X)
azprimes -> asieve(anats(s(s(0))))
azprimes -> zprimes
mark(filter(X1, X2, X3)) -> afilter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) -> asieve(mark(X))
mark(nats(X)) -> anats(mark(X))
mark(zprimes) -> azprimes
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(0) -> 0
mark(s(X)) -> s(mark(X))


Strategy:

innermost



Innermost Termination of R could not be shown.
Duration:
0:05 minutes