Termination Proof using AProVE

Term Rewriting System R:
[X, Y, X1, X2, X3, Z]
a_{_primes} -> a_{_sieve}(a_{_from}(s(s(0))))
a_{_primes} -> primes
a_{_from}(X) -> cons(mark(X), from(s(X)))
a_{_from}(X) -> from(X)
a_{_head}(cons(X, Y)) -> mark(X)
a_{_head}(X) -> head(X)
a_{_tail}(cons(X, Y)) -> mark(Y)
a_{_tail}(X) -> tail(X)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_filter}(s(s(X)), cons(Y, Z)) -> a_{_if}(divides(s(s(mark(X))), mark(Y)), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
a_{_filter}(X1, X2) -> filter(X1, X2)
a_{_sieve}(cons(X, Y)) -> cons(mark(X), filter(X, sieve(Y)))
a_{_sieve}(X) -> sieve(X)
mark(primes) -> a_{_primes}
mark(sieve(X)) -> a_{_sieve}(mark(X))
mark(from(X)) -> a_{_from}(mark(X))
mark(head(X)) -> a_{_head}(mark(X))
mark(tail(X)) -> a_{_tail}(mark(X))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(filter(X1, X2)) -> a_{_filter}(mark(X1), mark(X2))
mark(s(X)) -> s(mark(X))
mark(0) -> 0
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(true) -> true
mark(false) -> false
mark(divides(X1, X2)) -> divides(mark(X1), mark(X2))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A_{_PRIMES} -> A_{_SIEVE}(a_{_from}(s(s(0))))
A_{_PRIMES} -> A_{_FROM}(s(s(0)))
A_{_FROM}(X) -> MARK(X)
A_{_HEAD}(cons(X, Y)) -> MARK(X)
A_{_TAIL}(cons(X, Y)) -> MARK(Y)
A_{_IF}(true, X, Y) -> MARK(X)
A_{_IF}(false, X, Y) -> MARK(Y)
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> A_{_IF}(divides(s(s(mark(X))), mark(Y)), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> MARK(X)
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> MARK(Y)
A_{_SIEVE}(cons(X, Y)) -> MARK(X)
MARK(primes) -> A_{_PRIMES}
MARK(sieve(X)) -> A_{_SIEVE}(mark(X))
MARK(sieve(X)) -> MARK(X)
MARK(from(X)) -> A_{_FROM}(mark(X))
MARK(from(X)) -> MARK(X)
MARK(head(X)) -> A_{_HEAD}(mark(X))
MARK(head(X)) -> MARK(X)
MARK(tail(X)) -> A_{_TAIL}(mark(X))
MARK(tail(X)) -> MARK(X)
MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), X2, X3)
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(filter(X1, X2)) -> A_{_FILTER}(mark(X1), mark(X2))
MARK(filter(X1, X2)) -> MARK(X1)
MARK(filter(X1, X2)) -> MARK(X2)
MARK(s(X)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)
MARK(divides(X1, X2)) -> MARK(X1)
MARK(divides(X1, X2)) -> MARK(X2)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

A_{_IF}(false, X, Y) -> MARK(Y)
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> MARK(Y)
MARK(divides(X1, X2)) -> MARK(X2)
MARK(divides(X1, X2)) -> MARK(X1)
MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)
MARK(filter(X1, X2)) -> MARK(X2)
MARK(filter(X1, X2)) -> MARK(X1)
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> MARK(X)
MARK(filter(X1, X2)) -> A_{_FILTER}(mark(X1), mark(X2))
MARK(if(X1, X2, X3)) -> MARK(X1)
A_{_IF}(true, X, Y) -> MARK(X)
MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), X2, X3)
MARK(tail(X)) -> MARK(X)
A_{_TAIL}(cons(X, Y)) -> MARK(Y)
MARK(tail(X)) -> A_{_TAIL}(mark(X))
MARK(head(X)) -> MARK(X)
A_{_HEAD}(cons(X, Y)) -> MARK(X)
MARK(head(X)) -> A_{_HEAD}(mark(X))
MARK(from(X)) -> MARK(X)
MARK(from(X)) -> A_{_FROM}(mark(X))
MARK(sieve(X)) -> MARK(X)
MARK(sieve(X)) -> A_{_SIEVE}(mark(X))
A_{_FROM}(X) -> MARK(X)
A_{_PRIMES} -> A_{_FROM}(s(s(0)))
MARK(primes) -> A_{_PRIMES}
A_{_SIEVE}(cons(X, Y)) -> MARK(X)
A_{_PRIMES} -> A_{_SIEVE}(a_{_from}(s(s(0))))

Rules:

a_{_primes} -> a_{_sieve}(a_{_from}(s(s(0))))
a_{_primes} -> primes
a_{_from}(X) -> cons(mark(X), from(s(X)))
a_{_from}(X) -> from(X)
a_{_head}(cons(X, Y)) -> mark(X)
a_{_head}(X) -> head(X)
a_{_tail}(cons(X, Y)) -> mark(Y)
a_{_tail}(X) -> tail(X)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_filter}(s(s(X)), cons(Y, Z)) -> a_{_if}(divides(s(s(mark(X))), mark(Y)), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
a_{_filter}(X1, X2) -> filter(X1, X2)
a_{_sieve}(cons(X, Y)) -> cons(mark(X), filter(X, sieve(Y)))
a_{_sieve}(X) -> sieve(X)
mark(primes) -> a_{_primes}
mark(sieve(X)) -> a_{_sieve}(mark(X))
mark(from(X)) -> a_{_from}(mark(X))
mark(head(X)) -> a_{_head}(mark(X))
mark(tail(X)) -> a_{_tail}(mark(X))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(filter(X1, X2)) -> a_{_filter}(mark(X1), mark(X2))
mark(s(X)) -> s(mark(X))
mark(0) -> 0
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(true) -> true
mark(false) -> false
mark(divides(X1, X2)) -> divides(mark(X1), mark(X2))

Strategy:

innermost

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