Termination Proof using AProVE

Term Rewriting System R:
[X, Y, M, N, X1, X2, X3]
filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)
SIEVE(cons(s(N), Y)) -> FILTER(activate(Y), N, N)
SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
ZPRIMES -> SIEVE(nats(s(s(0))))
ZPRIMES -> NATS(s(s(0)))
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
ACTIVATE(n_{_nats}(X)) -> NATS(X)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
SIEVE(cons(s(N), Y)) -> FILTER(activate(Y), N, N)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)
ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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

SIEVE(cons(s(N), Y)) -> FILTER(activate(Y), N, N)

four new Dependency Pairs are created:

SIEVE(cons(s(N), n_{_filter}(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
SIEVE(cons(s(N), n_{_sieve}(X'))) -> FILTER(sieve(X'), N, N)
SIEVE(cons(s(N), n_{_nats}(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Forward Instantiation Transformation

Dependency Pairs:

SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)
SIEVE(cons(s(N), n_{_nats}(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), n_{_sieve}(X'))) -> FILTER(sieve(X'), N, N)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)
SIEVE(cons(s(N), n_{_filter}(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)
ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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

FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)

two new Dependency Pairs are created:

FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), 0, M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
FILTER(cons(X, n_{_sieve}(X'')), 0, M) -> ACTIVATE(n_{_sieve}(X''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 3

                 ↳Forward Instantiation Transformation

Dependency Pairs:

SIEVE(cons(s(N), n_{_nats}(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), n_{_sieve}(X'))) -> FILTER(sieve(X'), N, N)
SIEVE(cons(s(N), n_{_filter}(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)
ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
FILTER(cons(X, n_{_sieve}(X'')), 0, M) -> ACTIVATE(n_{_sieve}(X''))
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), 0, M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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

FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)

two new Dependency Pairs are created:

FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
FILTER(cons(X, n_{_sieve}(X'')), s(N), M) -> ACTIVATE(n_{_sieve}(X''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 4

                 ↳Forward Instantiation Transformation

Dependency Pairs:

SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)
SIEVE(cons(s(N), n_{_sieve}(X'))) -> FILTER(sieve(X'), N, N)
FILTER(cons(X, n_{_sieve}(X'')), s(N), M) -> ACTIVATE(n_{_sieve}(X''))
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_filter}(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)
ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
FILTER(cons(X, n_{_sieve}(X'')), 0, M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), 0, M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_nats}(X'))) -> FILTER(nats(X'), N, N)

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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

SIEVE(cons(0, Y)) -> ACTIVATE(Y)

two new Dependency Pairs are created:

SIEVE(cons(0, n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(0, n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 5

                 ↳Forward Instantiation Transformation

Dependency Pairs:

SIEVE(cons(0, n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))
SIEVE(cons(0, n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_nats}(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), n_{_sieve}(X'))) -> FILTER(sieve(X'), N, N)
FILTER(cons(X, n_{_sieve}(X'')), s(N), M) -> ACTIVATE(n_{_sieve}(X''))
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_filter}(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
FILTER(cons(X, n_{_sieve}(X'')), 0, M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), 0, M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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

SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)

two new Dependency Pairs are created:

SIEVE(cons(s(N), n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 6

                 ↳Forward Instantiation Transformation

Dependency Pairs:

SIEVE(cons(s(N), n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))
SIEVE(cons(s(N), n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(0, n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)
SIEVE(cons(s(N), n_{_nats}(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), n_{_sieve}(X'))) -> FILTER(sieve(X'), N, N)
FILTER(cons(X, n_{_sieve}(X'')), s(N), M) -> ACTIVATE(n_{_sieve}(X''))
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
FILTER(cons(X, n_{_sieve}(X'')), 0, M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), 0, M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_filter}(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
SIEVE(cons(0, n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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

ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)

four new Dependency Pairs are created:

ACTIVATE(n_{_filter}(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, X3')) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, X3')
ACTIVATE(n_{_filter}(cons(X'', n_{_sieve}(X'''')), 0, X3')) -> FILTER(cons(X'', n_{_sieve}(X'''')), 0, X3')
ACTIVATE(n_{_filter}(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), X3')) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), X3')
ACTIVATE(n_{_filter}(cons(X'', n_{_sieve}(X'''')), s(N''), X3')) -> FILTER(cons(X'', n_{_sieve}(X'''')), s(N''), X3')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 7

                 ↳Forward Instantiation Transformation

Dependency Pairs:

SIEVE(cons(s(N), n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(0, n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))
SIEVE(cons(0, n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)
SIEVE(cons(s(N), n_{_nats}(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), n_{_sieve}(X'))) -> FILTER(sieve(X'), N, N)
FILTER(cons(X, n_{_sieve}(X'')), s(N), M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(cons(X'', n_{_sieve}(X'''')), s(N''), X3')) -> FILTER(cons(X'', n_{_sieve}(X'''')), s(N''), X3')
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
ACTIVATE(n_{_filter}(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), X3')) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), X3')
FILTER(cons(X, n_{_sieve}(X'')), 0, M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(cons(X'', n_{_sieve}(X'''')), 0, X3')) -> FILTER(cons(X'', n_{_sieve}(X'''')), 0, X3')
ACTIVATE(n_{_filter}(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, X3')) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, X3')
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), 0, M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_filter}(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
SIEVE(cons(s(N), n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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

ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)

eight new Dependency Pairs are created:

ACTIVATE(n_{_sieve}(cons(s(N''), n_{_filter}(X1''', X2''', X3''')))) -> SIEVE(cons(s(N''), n_{_filter}(X1''', X2''', X3''')))
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_sieve}(X''')))) -> SIEVE(cons(s(N''), n_{_sieve}(X''')))
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_nats}(X''')))) -> SIEVE(cons(s(N''), n_{_nats}(X''')))
ACTIVATE(n_{_sieve}(cons(s(N''), Y'''))) -> SIEVE(cons(s(N''), Y'''))
ACTIVATE(n_{_sieve}(cons(0, n_{_filter}(X1'''', X2'''', X3'''')))) -> SIEVE(cons(0, n_{_filter}(X1'''', X2'''', X3'''')))
ACTIVATE(n_{_sieve}(cons(0, n_{_sieve}(X'''')))) -> SIEVE(cons(0, n_{_sieve}(X'''')))
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_filter}(X1'''', X2'''', X3'''')))) -> SIEVE(cons(s(N''), n_{_filter}(X1'''', X2'''', X3'''')))
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_sieve}(X'''')))) -> SIEVE(cons(s(N''), n_{_sieve}(X'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 8

                 ↳Forward Instantiation Transformation

Dependency Pairs:

ACTIVATE(n_{_sieve}(cons(s(N''), n_{_sieve}(X'''')))) -> SIEVE(cons(s(N''), n_{_sieve}(X'''')))
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_filter}(X1'''', X2'''', X3'''')))) -> SIEVE(cons(s(N''), n_{_filter}(X1'''', X2'''', X3'''')))
SIEVE(cons(0, n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_sieve}(cons(0, n_{_sieve}(X'''')))) -> SIEVE(cons(0, n_{_sieve}(X'''')))
SIEVE(cons(0, n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
ACTIVATE(n_{_sieve}(cons(0, n_{_filter}(X1'''', X2'''', X3'''')))) -> SIEVE(cons(0, n_{_filter}(X1'''', X2'''', X3'''')))
ACTIVATE(n_{_sieve}(cons(s(N''), Y'''))) -> SIEVE(cons(s(N''), Y'''))
SIEVE(cons(s(N), n_{_nats}(X'))) -> FILTER(nats(X'), N, N)
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_nats}(X''')))) -> SIEVE(cons(s(N''), n_{_nats}(X''')))
SIEVE(cons(s(N), n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)
SIEVE(cons(s(N), n_{_sieve}(X'))) -> FILTER(sieve(X'), N, N)
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_sieve}(X''')))) -> SIEVE(cons(s(N''), n_{_sieve}(X''')))
FILTER(cons(X, n_{_sieve}(X'')), s(N), M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(cons(X'', n_{_sieve}(X'''')), s(N''), X3')) -> FILTER(cons(X'', n_{_sieve}(X'''')), s(N''), X3')
ACTIVATE(n_{_filter}(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), X3')) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), X3')
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_filter}(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_filter}(X1''', X2''', X3''')))) -> SIEVE(cons(s(N''), n_{_filter}(X1''', X2''', X3''')))
FILTER(cons(X, n_{_sieve}(X'')), 0, M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(cons(X'', n_{_sieve}(X'''')), 0, X3')) -> FILTER(cons(X'', n_{_sieve}(X'''')), 0, X3')
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), 0, M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
ACTIVATE(n_{_filter}(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, X3')) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, X3')
SIEVE(cons(s(N), n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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

SIEVE(cons(s(N), n_{_nats}(X'))) -> FILTER(nats(X'), N, N)

two new Dependency Pairs are created:

SIEVE(cons(s(0), n_{_nats}(X''))) -> FILTER(nats(X''), 0, 0)
SIEVE(cons(s(s(N'')), n_{_nats}(X''))) -> FILTER(nats(X''), s(N''), s(N''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 9

                 ↳Forward Instantiation Transformation

Dependency Pairs:

ACTIVATE(n_{_sieve}(cons(s(N''), n_{_filter}(X1'''', X2'''', X3'''')))) -> SIEVE(cons(s(N''), n_{_filter}(X1'''', X2'''', X3'''')))
SIEVE(cons(0, n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_sieve}(cons(0, n_{_sieve}(X'''')))) -> SIEVE(cons(0, n_{_sieve}(X'''')))
SIEVE(cons(0, n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
ACTIVATE(n_{_sieve}(cons(0, n_{_filter}(X1'''', X2'''', X3'''')))) -> SIEVE(cons(0, n_{_filter}(X1'''', X2'''', X3'''')))
SIEVE(cons(s(N), n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
ACTIVATE(n_{_sieve}(cons(s(N''), Y'''))) -> SIEVE(cons(s(N''), Y'''))
SIEVE(cons(s(s(N'')), n_{_nats}(X''))) -> FILTER(nats(X''), s(N''), s(N''))
SIEVE(cons(s(0), n_{_nats}(X''))) -> FILTER(nats(X''), 0, 0)
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_nats}(X''')))) -> SIEVE(cons(s(N''), n_{_nats}(X''')))
SIEVE(cons(s(N), n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_sieve}(X''')))) -> SIEVE(cons(s(N''), n_{_sieve}(X''')))
FILTER(cons(X, n_{_sieve}(X'')), s(N), M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(cons(X'', n_{_sieve}(X'''')), s(N''), X3')) -> FILTER(cons(X'', n_{_sieve}(X'''')), s(N''), X3')
ACTIVATE(n_{_filter}(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), X3')) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), X3')
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_filter}(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_filter}(X1''', X2''', X3''')))) -> SIEVE(cons(s(N''), n_{_filter}(X1''', X2''', X3''')))
FILTER(cons(X, n_{_sieve}(X'')), 0, M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(cons(X'', n_{_sieve}(X'''')), 0, X3')) -> FILTER(cons(X'', n_{_sieve}(X'''')), 0, X3')
ACTIVATE(n_{_filter}(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, X3')) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, X3')
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), 0, M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_sieve}(X'))) -> FILTER(sieve(X'), N, N)
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_sieve}(X'''')))) -> SIEVE(cons(s(N''), n_{_sieve}(X'''')))

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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

SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)

four new Dependency Pairs are created:

SIEVE(cons(s(0), cons(X'', n_{_filter}(X1'''', X2'''', X3'''')))) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, 0)
SIEVE(cons(s(0), cons(X'', n_{_sieve}(X'''')))) -> FILTER(cons(X'', n_{_sieve}(X'''')), 0, 0)
SIEVE(cons(s(s(N'')), cons(X'', n_{_filter}(X1'''', X2'''', X3'''')))) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), s(N''))
SIEVE(cons(s(s(N'')), cons(X'', n_{_sieve}(X'''')))) -> FILTER(cons(X'', n_{_sieve}(X'''')), s(N''), s(N''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 10

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

ACTIVATE(n_{_sieve}(cons(s(N''), n_{_sieve}(X'''')))) -> SIEVE(cons(s(N''), n_{_sieve}(X'''')))
SIEVE(cons(0, n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_sieve}(cons(0, n_{_sieve}(X'''')))) -> SIEVE(cons(0, n_{_sieve}(X'''')))
SIEVE(cons(0, n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
ACTIVATE(n_{_sieve}(cons(0, n_{_filter}(X1'''', X2'''', X3'''')))) -> SIEVE(cons(0, n_{_filter}(X1'''', X2'''', X3'''')))
SIEVE(cons(s(s(N'')), cons(X'', n_{_sieve}(X'''')))) -> FILTER(cons(X'', n_{_sieve}(X'''')), s(N''), s(N''))
SIEVE(cons(s(s(N'')), cons(X'', n_{_filter}(X1'''', X2'''', X3'''')))) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), s(N''))
SIEVE(cons(s(0), cons(X'', n_{_sieve}(X'''')))) -> FILTER(cons(X'', n_{_sieve}(X'''')), 0, 0)
SIEVE(cons(s(0), cons(X'', n_{_filter}(X1'''', X2'''', X3'''')))) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, 0)
ACTIVATE(n_{_sieve}(cons(s(N''), Y'''))) -> SIEVE(cons(s(N''), Y'''))
SIEVE(cons(s(s(N'')), n_{_nats}(X''))) -> FILTER(nats(X''), s(N''), s(N''))
SIEVE(cons(s(0), n_{_nats}(X''))) -> FILTER(nats(X''), 0, 0)
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_nats}(X''')))) -> SIEVE(cons(s(N''), n_{_nats}(X''')))
SIEVE(cons(s(N), n_{_sieve}(X''))) -> ACTIVATE(n_{_sieve}(X''))
SIEVE(cons(s(N), n_{_sieve}(X'))) -> FILTER(sieve(X'), N, N)
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_sieve}(X''')))) -> SIEVE(cons(s(N''), n_{_sieve}(X''')))
FILTER(cons(X, n_{_sieve}(X'')), s(N), M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(cons(X'', n_{_sieve}(X'''')), s(N''), X3')) -> FILTER(cons(X'', n_{_sieve}(X'''')), s(N''), X3')
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
ACTIVATE(n_{_filter}(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), X3')) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), s(N''), X3')
SIEVE(cons(s(N), n_{_filter}(X1'', X2'', X3''))) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_filter}(X1''', X2''', X3''')))) -> SIEVE(cons(s(N''), n_{_filter}(X1''', X2''', X3''')))
FILTER(cons(X, n_{_sieve}(X'')), 0, M) -> ACTIVATE(n_{_sieve}(X''))
ACTIVATE(n_{_filter}(cons(X'', n_{_sieve}(X'''')), 0, X3')) -> FILTER(cons(X'', n_{_sieve}(X'''')), 0, X3')
ACTIVATE(n_{_filter}(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, X3')) -> FILTER(cons(X'', n_{_filter}(X1'''', X2'''', X3'''')), 0, X3')
FILTER(cons(X, n_{_filter}(X1'', X2'', X3'')), 0, M) -> ACTIVATE(n_{_filter}(X1'', X2'', X3''))
SIEVE(cons(s(N), n_{_filter}(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
ACTIVATE(n_{_sieve}(cons(s(N''), n_{_filter}(X1'''', X2'''', X3'''')))) -> SIEVE(cons(s(N''), n_{_filter}(X1'''', X2'''', X3'''')))

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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