R
↳Dependency Pair Analysis
FILTER(cons(X, Y), 0, M) -> FILTER(Y, M, M)
FILTER(cons(X, Y), s(N), M) -> FILTER(Y, N, M)
SIEVE(cons(0, Y)) -> SIEVE(Y)
SIEVE(cons(s(N), Y)) -> SIEVE(filter(Y, N, N))
SIEVE(cons(s(N), Y)) -> FILTER(Y, N, N)
NATS(N) -> NATS(s(N))
ZPRIMES -> SIEVE(nats(s(s(0))))
ZPRIMES -> NATS(s(s(0)))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Remaining
→DP Problem 3
↳Remaining
FILTER(cons(X, Y), s(N), M) -> FILTER(Y, N, M)
FILTER(cons(X, Y), 0, M) -> FILTER(Y, M, M)
filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
sieve(cons(0, Y)) -> cons(0, sieve(Y))
sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
nats(N) -> cons(N, nats(s(N)))
zprimes -> sieve(nats(s(s(0))))
FILTER(cons(X, Y), s(N), M) -> FILTER(Y, N, M)
FILTER(cons(X, Y), 0, M) -> FILTER(Y, M, M)
POL(cons(x1, x2)) = 1 + x1 + x2
FILTER(x1, x2, x3) -> x1
cons(x1, x2) -> cons(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳Remaining
→DP Problem 3
↳Remaining
filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
sieve(cons(0, Y)) -> cons(0, sieve(Y))
sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
nats(N) -> cons(N, nats(s(N)))
zprimes -> sieve(nats(s(s(0))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
NATS(N) -> NATS(s(N))
filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
sieve(cons(0, Y)) -> cons(0, sieve(Y))
sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
nats(N) -> cons(N, nats(s(N)))
zprimes -> sieve(nats(s(s(0))))
SIEVE(cons(s(N), Y)) -> SIEVE(filter(Y, N, N))
SIEVE(cons(0, Y)) -> SIEVE(Y)
filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
sieve(cons(0, Y)) -> cons(0, sieve(Y))
sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
nats(N) -> cons(N, nats(s(N)))
zprimes -> sieve(nats(s(s(0))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
NATS(N) -> NATS(s(N))
filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
sieve(cons(0, Y)) -> cons(0, sieve(Y))
sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
nats(N) -> cons(N, nats(s(N)))
zprimes -> sieve(nats(s(s(0))))
SIEVE(cons(s(N), Y)) -> SIEVE(filter(Y, N, N))
SIEVE(cons(0, Y)) -> SIEVE(Y)
filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
sieve(cons(0, Y)) -> cons(0, sieve(Y))
sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
nats(N) -> cons(N, nats(s(N)))
zprimes -> sieve(nats(s(s(0))))