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))

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

         ↳Narrowing Transformation

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))

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A_{_PRIMES} -> A_{_SIEVE}(a_{_from}(s(s(0))))

two new Dependency Pairs are created:

A_{_PRIMES} -> A_{_SIEVE}(cons(mark(s(s(0))), from(s(s(s(0))))))
A_{_PRIMES} -> A_{_SIEVE}(from(s(s(0))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

A_{_PRIMES} -> A_{_SIEVE}(cons(mark(s(s(0))), from(s(s(s(0))))))
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)
A_{_SIEVE}(cons(X, Y)) -> 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_{_IF}(false, X, Y) -> MARK(Y)

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))

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(sieve(X)) -> A_{_SIEVE}(mark(X))

13 new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Narrowing Transformation

Dependency Pairs:

A_{_IF}(false, X, Y) -> MARK(Y)
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> MARK(Y)
MARK(sieve(cons(X1', X2'))) -> A_{_SIEVE}(cons(mark(X1'), X2'))
MARK(sieve(filter(X1', X2'))) -> A_{_SIEVE}(a_{_filter}(mark(X1'), mark(X2')))
MARK(sieve(if(X1', X2', X3'))) -> A_{_SIEVE}(a_{_if}(mark(X1'), X2', X3'))
MARK(sieve(tail(X''))) -> A_{_SIEVE}(a_{_tail}(mark(X'')))
MARK(sieve(head(X''))) -> A_{_SIEVE}(a_{_head}(mark(X'')))
MARK(sieve(from(X''))) -> A_{_SIEVE}(a_{_from}(mark(X'')))
MARK(sieve(sieve(X''))) -> A_{_SIEVE}(a_{_sieve}(mark(X'')))
MARK(sieve(primes)) -> A_{_SIEVE}(a_{_primes})
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)
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}(cons(mark(s(s(0))), from(s(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))

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(head(X)) -> A_{_HEAD}(mark(X))

13 new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 4

                 ↳Narrowing Transformation

Dependency Pairs:

A_{_PRIMES} -> A_{_SIEVE}(cons(mark(s(s(0))), from(s(s(s(0))))))
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> MARK(Y)
MARK(head(cons(X1', X2'))) -> A_{_HEAD}(cons(mark(X1'), X2'))
MARK(head(filter(X1', X2'))) -> A_{_HEAD}(a_{_filter}(mark(X1'), mark(X2')))
MARK(head(if(X1', X2', X3'))) -> A_{_HEAD}(a_{_if}(mark(X1'), X2', X3'))
MARK(head(tail(X''))) -> A_{_HEAD}(a_{_tail}(mark(X'')))
MARK(head(head(X''))) -> A_{_HEAD}(a_{_head}(mark(X'')))
MARK(head(from(X''))) -> A_{_HEAD}(a_{_from}(mark(X'')))
MARK(head(sieve(X''))) -> A_{_HEAD}(a_{_sieve}(mark(X'')))
A_{_HEAD}(cons(X, Y)) -> MARK(X)
MARK(head(primes)) -> A_{_HEAD}(a_{_primes})
MARK(sieve(cons(X1', X2'))) -> A_{_SIEVE}(cons(mark(X1'), X2'))
MARK(sieve(filter(X1', X2'))) -> A_{_SIEVE}(a_{_filter}(mark(X1'), mark(X2')))
MARK(sieve(if(X1', X2', X3'))) -> A_{_SIEVE}(a_{_if}(mark(X1'), X2', X3'))
MARK(sieve(tail(X''))) -> A_{_SIEVE}(a_{_tail}(mark(X'')))
MARK(sieve(head(X''))) -> A_{_SIEVE}(a_{_head}(mark(X'')))
MARK(sieve(from(X''))) -> A_{_SIEVE}(a_{_from}(mark(X'')))
MARK(sieve(sieve(X''))) -> A_{_SIEVE}(a_{_sieve}(mark(X'')))
A_{_SIEVE}(cons(X, Y)) -> MARK(X)
MARK(sieve(primes)) -> A_{_SIEVE}(a_{_primes})
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)
MARK(from(X)) -> MARK(X)
MARK(from(X)) -> A_{_FROM}(mark(X))
MARK(sieve(X)) -> MARK(X)
A_{_FROM}(X) -> MARK(X)
A_{_PRIMES} -> A_{_FROM}(s(s(0)))
MARK(primes) -> A_{_PRIMES}
A_{_IF}(false, X, Y) -> MARK(Y)

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))

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(tail(X)) -> A_{_TAIL}(mark(X))

13 new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 5

                 ↳Narrowing Transformation

Dependency Pairs:

A_{_IF}(false, X, Y) -> MARK(Y)
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> MARK(Y)
MARK(tail(cons(X1', X2'))) -> A_{_TAIL}(cons(mark(X1'), X2'))
MARK(tail(filter(X1', X2'))) -> A_{_TAIL}(a_{_filter}(mark(X1'), mark(X2')))
MARK(tail(if(X1', X2', X3'))) -> A_{_TAIL}(a_{_if}(mark(X1'), X2', X3'))
MARK(tail(tail(X''))) -> A_{_TAIL}(a_{_tail}(mark(X'')))
MARK(tail(head(X''))) -> A_{_TAIL}(a_{_head}(mark(X'')))
MARK(tail(from(X''))) -> A_{_TAIL}(a_{_from}(mark(X'')))
MARK(tail(sieve(X''))) -> A_{_TAIL}(a_{_sieve}(mark(X'')))
A_{_TAIL}(cons(X, Y)) -> MARK(Y)
MARK(tail(primes)) -> A_{_TAIL}(a_{_primes})
MARK(head(cons(X1', X2'))) -> A_{_HEAD}(cons(mark(X1'), X2'))
MARK(head(filter(X1', X2'))) -> A_{_HEAD}(a_{_filter}(mark(X1'), mark(X2')))
MARK(head(if(X1', X2', X3'))) -> A_{_HEAD}(a_{_if}(mark(X1'), X2', X3'))
MARK(head(tail(X''))) -> A_{_HEAD}(a_{_tail}(mark(X'')))
MARK(head(head(X''))) -> A_{_HEAD}(a_{_head}(mark(X'')))
MARK(head(from(X''))) -> A_{_HEAD}(a_{_from}(mark(X'')))
MARK(head(sieve(X''))) -> A_{_HEAD}(a_{_sieve}(mark(X'')))
A_{_HEAD}(cons(X, Y)) -> MARK(X)
MARK(head(primes)) -> A_{_HEAD}(a_{_primes})
MARK(sieve(cons(X1', X2'))) -> A_{_SIEVE}(cons(mark(X1'), X2'))
MARK(sieve(filter(X1', X2'))) -> A_{_SIEVE}(a_{_filter}(mark(X1'), mark(X2')))
MARK(sieve(if(X1', X2', X3'))) -> A_{_SIEVE}(a_{_if}(mark(X1'), X2', X3'))
MARK(sieve(tail(X''))) -> A_{_SIEVE}(a_{_tail}(mark(X'')))
MARK(sieve(head(X''))) -> A_{_SIEVE}(a_{_head}(mark(X'')))
MARK(sieve(from(X''))) -> A_{_SIEVE}(a_{_from}(mark(X'')))
MARK(sieve(sieve(X''))) -> A_{_SIEVE}(a_{_sieve}(mark(X'')))
MARK(sieve(primes)) -> A_{_SIEVE}(a_{_primes})
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)
MARK(head(X)) -> MARK(X)
MARK(from(X)) -> MARK(X)
MARK(from(X)) -> A_{_FROM}(mark(X))
MARK(sieve(X)) -> 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}(cons(mark(s(s(0))), from(s(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))

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), X2, X3)

13 new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 6

                 ↳Narrowing Transformation

Dependency Pairs:

A_{_PRIMES} -> A_{_SIEVE}(cons(mark(s(s(0))), from(s(s(s(0))))))
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> MARK(Y)
MARK(if(false, X2, X3)) -> A_{_IF}(false, X2, X3)
MARK(if(true, X2, X3)) -> A_{_IF}(true, X2, X3)
MARK(if(filter(X1'', X2''), X2, X3)) -> A_{_IF}(a_{_filter}(mark(X1''), mark(X2'')), X2, X3)
MARK(if(if(X1'', X2'', X3''), X2, X3)) -> A_{_IF}(a_{_if}(mark(X1''), X2'', X3''), X2, X3)
MARK(if(tail(X'), X2, X3)) -> A_{_IF}(a_{_tail}(mark(X')), X2, X3)
MARK(if(head(X'), X2, X3)) -> A_{_IF}(a_{_head}(mark(X')), X2, X3)
MARK(if(from(X'), X2, X3)) -> A_{_IF}(a_{_from}(mark(X')), X2, X3)
MARK(if(sieve(X'), X2, X3)) -> A_{_IF}(a_{_sieve}(mark(X')), X2, X3)
A_{_IF}(true, X, Y) -> MARK(X)
MARK(if(primes, X2, X3)) -> A_{_IF}(a_{_primes}, X2, X3)
MARK(tail(cons(X1', X2'))) -> A_{_TAIL}(cons(mark(X1'), X2'))
MARK(tail(filter(X1', X2'))) -> A_{_TAIL}(a_{_filter}(mark(X1'), mark(X2')))
MARK(tail(if(X1', X2', X3'))) -> A_{_TAIL}(a_{_if}(mark(X1'), X2', X3'))
MARK(tail(tail(X''))) -> A_{_TAIL}(a_{_tail}(mark(X'')))
MARK(tail(head(X''))) -> A_{_TAIL}(a_{_head}(mark(X'')))
MARK(tail(from(X''))) -> A_{_TAIL}(a_{_from}(mark(X'')))
MARK(tail(sieve(X''))) -> A_{_TAIL}(a_{_sieve}(mark(X'')))
A_{_TAIL}(cons(X, Y)) -> MARK(Y)
MARK(tail(primes)) -> A_{_TAIL}(a_{_primes})
MARK(head(cons(X1', X2'))) -> A_{_HEAD}(cons(mark(X1'), X2'))
MARK(head(filter(X1', X2'))) -> A_{_HEAD}(a_{_filter}(mark(X1'), mark(X2')))
MARK(head(if(X1', X2', X3'))) -> A_{_HEAD}(a_{_if}(mark(X1'), X2', X3'))
MARK(head(tail(X''))) -> A_{_HEAD}(a_{_tail}(mark(X'')))
MARK(head(head(X''))) -> A_{_HEAD}(a_{_head}(mark(X'')))
MARK(head(from(X''))) -> A_{_HEAD}(a_{_from}(mark(X'')))
MARK(head(sieve(X''))) -> A_{_HEAD}(a_{_sieve}(mark(X'')))
A_{_HEAD}(cons(X, Y)) -> MARK(X)
MARK(head(primes)) -> A_{_HEAD}(a_{_primes})
MARK(sieve(cons(X1', X2'))) -> A_{_SIEVE}(cons(mark(X1'), X2'))
MARK(sieve(filter(X1', X2'))) -> A_{_SIEVE}(a_{_filter}(mark(X1'), mark(X2')))
MARK(sieve(if(X1', X2', X3'))) -> A_{_SIEVE}(a_{_if}(mark(X1'), X2', X3'))
MARK(sieve(tail(X''))) -> A_{_SIEVE}(a_{_tail}(mark(X'')))
MARK(sieve(head(X''))) -> A_{_SIEVE}(a_{_head}(mark(X'')))
MARK(sieve(from(X''))) -> A_{_SIEVE}(a_{_from}(mark(X'')))
MARK(sieve(sieve(X''))) -> A_{_SIEVE}(a_{_sieve}(mark(X'')))
A_{_SIEVE}(cons(X, Y)) -> MARK(X)
MARK(sieve(primes)) -> A_{_SIEVE}(a_{_primes})
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)
MARK(tail(X)) -> MARK(X)
MARK(head(X)) -> MARK(X)
MARK(from(X)) -> MARK(X)
MARK(from(X)) -> A_{_FROM}(mark(X))
MARK(sieve(X)) -> MARK(X)
A_{_FROM}(X) -> MARK(X)
A_{_PRIMES} -> A_{_FROM}(s(s(0)))
MARK(primes) -> A_{_PRIMES}
A_{_IF}(false, X, Y) -> MARK(Y)

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))

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(filter(X1, X2)) -> A_{_FILTER}(mark(X1), mark(X2))

26 new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 7

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

MARK(filter(X1, cons(X1'', X2''))) -> A_{_FILTER}(mark(X1), cons(mark(X1''), X2''))
MARK(filter(X1, filter(X1'', X2''))) -> A_{_FILTER}(mark(X1), a_{_filter}(mark(X1''), mark(X2'')))
MARK(filter(X1, if(X1'', X2'', X3'))) -> A_{_FILTER}(mark(X1), a_{_if}(mark(X1''), X2'', X3'))
MARK(filter(X1, tail(X'))) -> A_{_FILTER}(mark(X1), a_{_tail}(mark(X')))
MARK(filter(X1, head(X'))) -> A_{_FILTER}(mark(X1), a_{_head}(mark(X')))
MARK(filter(X1, from(X'))) -> A_{_FILTER}(mark(X1), a_{_from}(mark(X')))
MARK(filter(X1, sieve(X'))) -> A_{_FILTER}(mark(X1), a_{_sieve}(mark(X')))
MARK(filter(X1, primes)) -> A_{_FILTER}(mark(X1), a_{_primes})
MARK(filter(s(X'), X2)) -> A_{_FILTER}(s(mark(X')), mark(X2))
MARK(filter(filter(X1'', X2''), X2)) -> A_{_FILTER}(a_{_filter}(mark(X1''), mark(X2'')), mark(X2))
MARK(filter(if(X1'', X2'', X3'), X2)) -> A_{_FILTER}(a_{_if}(mark(X1''), X2'', X3'), mark(X2))
MARK(filter(tail(X'), X2)) -> A_{_FILTER}(a_{_tail}(mark(X')), mark(X2))
MARK(filter(head(X'), X2)) -> A_{_FILTER}(a_{_head}(mark(X')), mark(X2))
MARK(filter(from(X'), X2)) -> A_{_FILTER}(a_{_from}(mark(X')), mark(X2))
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> MARK(Y)
MARK(filter(sieve(X'), X2)) -> A_{_FILTER}(a_{_sieve}(mark(X')), mark(X2))
A_{_FILTER}(s(s(X)), cons(Y, Z)) -> MARK(X)
MARK(filter(primes, X2)) -> A_{_FILTER}(a_{_primes}, mark(X2))
MARK(if(false, X2, X3)) -> A_{_IF}(false, X2, X3)
MARK(if(true, X2, X3)) -> A_{_IF}(true, X2, X3)
MARK(if(filter(X1'', X2''), X2, X3)) -> A_{_IF}(a_{_filter}(mark(X1''), mark(X2'')), X2, X3)
MARK(if(if(X1'', X2'', X3''), X2, X3)) -> A_{_IF}(a_{_if}(mark(X1''), X2'', X3''), X2, X3)
MARK(if(tail(X'), X2, X3)) -> A_{_IF}(a_{_tail}(mark(X')), X2, X3)
MARK(if(head(X'), X2, X3)) -> A_{_IF}(a_{_head}(mark(X')), X2, X3)
MARK(if(from(X'), X2, X3)) -> A_{_IF}(a_{_from}(mark(X')), X2, X3)
A_{_IF}(false, X, Y) -> MARK(Y)
MARK(if(sieve(X'), X2, X3)) -> A_{_IF}(a_{_sieve}(mark(X')), X2, X3)
A_{_IF}(true, X, Y) -> MARK(X)
MARK(if(primes, X2, X3)) -> A_{_IF}(a_{_primes}, X2, X3)
MARK(tail(cons(X1', X2'))) -> A_{_TAIL}(cons(mark(X1'), X2'))
MARK(tail(filter(X1', X2'))) -> A_{_TAIL}(a_{_filter}(mark(X1'), mark(X2')))
MARK(tail(if(X1', X2', X3'))) -> A_{_TAIL}(a_{_if}(mark(X1'), X2', X3'))
MARK(tail(tail(X''))) -> A_{_TAIL}(a_{_tail}(mark(X'')))
MARK(tail(head(X''))) -> A_{_TAIL}(a_{_head}(mark(X'')))
MARK(tail(from(X''))) -> A_{_TAIL}(a_{_from}(mark(X'')))
MARK(tail(sieve(X''))) -> A_{_TAIL}(a_{_sieve}(mark(X'')))
A_{_TAIL}(cons(X, Y)) -> MARK(Y)
MARK(tail(primes)) -> A_{_TAIL}(a_{_primes})
MARK(head(cons(X1', X2'))) -> A_{_HEAD}(cons(mark(X1'), X2'))
MARK(head(filter(X1', X2'))) -> A_{_HEAD}(a_{_filter}(mark(X1'), mark(X2')))
MARK(head(if(X1', X2', X3'))) -> A_{_HEAD}(a_{_if}(mark(X1'), X2', X3'))
MARK(head(tail(X''))) -> A_{_HEAD}(a_{_tail}(mark(X'')))
MARK(head(head(X''))) -> A_{_HEAD}(a_{_head}(mark(X'')))
MARK(head(from(X''))) -> A_{_HEAD}(a_{_from}(mark(X'')))
MARK(head(sieve(X''))) -> A_{_HEAD}(a_{_sieve}(mark(X'')))
A_{_HEAD}(cons(X, Y)) -> MARK(X)
MARK(head(primes)) -> A_{_HEAD}(a_{_primes})
MARK(sieve(cons(X1', X2'))) -> A_{_SIEVE}(cons(mark(X1'), X2'))
MARK(sieve(filter(X1', X2'))) -> A_{_SIEVE}(a_{_filter}(mark(X1'), mark(X2')))
MARK(sieve(if(X1', X2', X3'))) -> A_{_SIEVE}(a_{_if}(mark(X1'), X2', X3'))
MARK(sieve(tail(X''))) -> A_{_SIEVE}(a_{_tail}(mark(X'')))
MARK(sieve(head(X''))) -> A_{_SIEVE}(a_{_head}(mark(X'')))
MARK(sieve(from(X''))) -> A_{_SIEVE}(a_{_from}(mark(X'')))
MARK(sieve(sieve(X''))) -> A_{_SIEVE}(a_{_sieve}(mark(X'')))
MARK(sieve(primes)) -> A_{_SIEVE}(a_{_primes})
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)
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(tail(X)) -> MARK(X)
MARK(head(X)) -> MARK(X)
MARK(from(X)) -> MARK(X)
MARK(from(X)) -> A_{_FROM}(mark(X))
MARK(sieve(X)) -> 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}(cons(mark(s(s(0))), from(s(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))

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