Term Rewriting System R:
[X, Y, M, N, X1, X2, X3]
filter(cons(X, Y), 0, M) -> cons(0, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(X)) -> nats(X)
activate(X) -> X

Innermost Termination of R to be shown.



   R
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(nfilter(X1, X2, X3)) -> FILTER(X1, X2, X3)
ACTIVATE(nsieve(X)) -> SIEVE(X)
ACTIVATE(nnats(X)) -> NATS(X)

Furthermore, R contains one SCC.


   R
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(nsieve(X)) -> SIEVE(X)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)
ACTIVATE(nfilter(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)


Rules:


filter(cons(X, Y), 0, M) -> cons(0, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(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), nfilter(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
SIEVE(cons(s(N), nsieve(X'))) -> FILTER(sieve(X'), N, N)
SIEVE(cons(s(N), nnats(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)

The transformation is resulting in one new DP problem:



   R
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), nnats(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), nsieve(X'))) -> FILTER(sieve(X'), N, N)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)
SIEVE(cons(s(N), nfilter(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)
ACTIVATE(nsieve(X)) -> SIEVE(X)
FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)
ACTIVATE(nfilter(X1, X2, X3)) -> FILTER(X1, X2, X3)
SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)


Rules:


filter(cons(X, Y), 0, M) -> cons(0, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(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, nfilter(X1'', X2'', X3'')), 0, M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
FILTER(cons(X, nsieve(X'')), 0, M) -> ACTIVATE(nsieve(X''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
FwdInst
             ...
               →DP Problem 3
Forward Instantiation Transformation


Dependency Pairs:

SIEVE(cons(s(N), nnats(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), nsieve(X'))) -> FILTER(sieve(X'), N, N)
SIEVE(cons(s(N), nfilter(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)
ACTIVATE(nsieve(X)) -> SIEVE(X)
FILTER(cons(X, nsieve(X'')), 0, M) -> ACTIVATE(nsieve(X''))
FILTER(cons(X, nfilter(X1'', X2'', X3'')), 0, M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
ACTIVATE(nfilter(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, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(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, nfilter(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
FILTER(cons(X, nsieve(X'')), s(N), M) -> ACTIVATE(nsieve(X''))

The transformation is resulting in one new DP problem:



   R
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), nsieve(X'))) -> FILTER(sieve(X'), N, N)
FILTER(cons(X, nsieve(X'')), s(N), M) -> ACTIVATE(nsieve(X''))
FILTER(cons(X, nfilter(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nfilter(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)
ACTIVATE(nsieve(X)) -> SIEVE(X)
FILTER(cons(X, nsieve(X'')), 0, M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, nfilter(X1'', X2'', X3'')), 0, M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nnats(X'))) -> FILTER(nats(X'), N, N)


Rules:


filter(cons(X, Y), 0, M) -> cons(0, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(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, nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(0, nsieve(X''))) -> ACTIVATE(nsieve(X''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
FwdInst
             ...
               →DP Problem 5
Forward Instantiation Transformation


Dependency Pairs:

SIEVE(cons(0, nsieve(X''))) -> ACTIVATE(nsieve(X''))
SIEVE(cons(0, nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nnats(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), nsieve(X'))) -> FILTER(sieve(X'), N, N)
FILTER(cons(X, nsieve(X'')), s(N), M) -> ACTIVATE(nsieve(X''))
FILTER(cons(X, nfilter(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nfilter(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
ACTIVATE(nsieve(X)) -> SIEVE(X)
FILTER(cons(X, nsieve(X'')), 0, M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, nfilter(X1'', X2'', X3'')), 0, M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)


Rules:


filter(cons(X, Y), 0, M) -> cons(0, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(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), nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nsieve(X''))) -> ACTIVATE(nsieve(X''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
FwdInst
             ...
               →DP Problem 6
Forward Instantiation Transformation


Dependency Pairs:

SIEVE(cons(s(N), nsieve(X''))) -> ACTIVATE(nsieve(X''))
SIEVE(cons(s(N), nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(0, nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)
SIEVE(cons(s(N), nnats(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), nsieve(X'))) -> FILTER(sieve(X'), N, N)
FILTER(cons(X, nsieve(X'')), s(N), M) -> ACTIVATE(nsieve(X''))
FILTER(cons(X, nfilter(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
FILTER(cons(X, nsieve(X'')), 0, M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, nfilter(X1'', X2'', X3'')), 0, M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nfilter(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
ACTIVATE(nsieve(X)) -> SIEVE(X)
SIEVE(cons(0, nsieve(X''))) -> ACTIVATE(nsieve(X''))


Rules:


filter(cons(X, Y), 0, M) -> cons(0, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(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(nfilter(X1, X2, X3)) -> FILTER(X1, X2, X3)
four new Dependency Pairs are created:

ACTIVATE(nfilter(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, X3')) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, X3')
ACTIVATE(nfilter(cons(X'', nsieve(X'''')), 0, X3')) -> FILTER(cons(X'', nsieve(X'''')), 0, X3')
ACTIVATE(nfilter(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), X3')) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), X3')
ACTIVATE(nfilter(cons(X'', nsieve(X'''')), s(N''), X3')) -> FILTER(cons(X'', nsieve(X'''')), s(N''), X3')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
FwdInst
             ...
               →DP Problem 7
Forward Instantiation Transformation


Dependency Pairs:

SIEVE(cons(s(N), nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(0, nsieve(X''))) -> ACTIVATE(nsieve(X''))
SIEVE(cons(0, nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)
SIEVE(cons(s(N), nnats(X'))) -> FILTER(nats(X'), N, N)
SIEVE(cons(s(N), nsieve(X'))) -> FILTER(sieve(X'), N, N)
FILTER(cons(X, nsieve(X'')), s(N), M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(cons(X'', nsieve(X'''')), s(N''), X3')) -> FILTER(cons(X'', nsieve(X'''')), s(N''), X3')
FILTER(cons(X, nfilter(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
ACTIVATE(nfilter(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), X3')) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), X3')
FILTER(cons(X, nsieve(X'')), 0, M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(cons(X'', nsieve(X'''')), 0, X3')) -> FILTER(cons(X'', nsieve(X'''')), 0, X3')
ACTIVATE(nfilter(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, X3')) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, X3')
FILTER(cons(X, nfilter(X1'', X2'', X3'')), 0, M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nfilter(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
ACTIVATE(nsieve(X)) -> SIEVE(X)
SIEVE(cons(s(N), nsieve(X''))) -> ACTIVATE(nsieve(X''))


Rules:


filter(cons(X, Y), 0, M) -> cons(0, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(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(nsieve(X)) -> SIEVE(X)
eight new Dependency Pairs are created:

ACTIVATE(nsieve(cons(s(N''), nfilter(X1''', X2''', X3''')))) -> SIEVE(cons(s(N''), nfilter(X1''', X2''', X3''')))
ACTIVATE(nsieve(cons(s(N''), nsieve(X''')))) -> SIEVE(cons(s(N''), nsieve(X''')))
ACTIVATE(nsieve(cons(s(N''), nnats(X''')))) -> SIEVE(cons(s(N''), nnats(X''')))
ACTIVATE(nsieve(cons(s(N''), Y'''))) -> SIEVE(cons(s(N''), Y'''))
ACTIVATE(nsieve(cons(0, nfilter(X1'''', X2'''', X3'''')))) -> SIEVE(cons(0, nfilter(X1'''', X2'''', X3'''')))
ACTIVATE(nsieve(cons(0, nsieve(X'''')))) -> SIEVE(cons(0, nsieve(X'''')))
ACTIVATE(nsieve(cons(s(N''), nfilter(X1'''', X2'''', X3'''')))) -> SIEVE(cons(s(N''), nfilter(X1'''', X2'''', X3'''')))
ACTIVATE(nsieve(cons(s(N''), nsieve(X'''')))) -> SIEVE(cons(s(N''), nsieve(X'''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
FwdInst
             ...
               →DP Problem 8
Forward Instantiation Transformation


Dependency Pairs:

ACTIVATE(nsieve(cons(s(N''), nsieve(X'''')))) -> SIEVE(cons(s(N''), nsieve(X'''')))
ACTIVATE(nsieve(cons(s(N''), nfilter(X1'''', X2'''', X3'''')))) -> SIEVE(cons(s(N''), nfilter(X1'''', X2'''', X3'''')))
SIEVE(cons(0, nsieve(X''))) -> ACTIVATE(nsieve(X''))
ACTIVATE(nsieve(cons(0, nsieve(X'''')))) -> SIEVE(cons(0, nsieve(X'''')))
SIEVE(cons(0, nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
ACTIVATE(nsieve(cons(0, nfilter(X1'''', X2'''', X3'''')))) -> SIEVE(cons(0, nfilter(X1'''', X2'''', X3'''')))
ACTIVATE(nsieve(cons(s(N''), Y'''))) -> SIEVE(cons(s(N''), Y'''))
SIEVE(cons(s(N), nnats(X'))) -> FILTER(nats(X'), N, N)
ACTIVATE(nsieve(cons(s(N''), nnats(X''')))) -> SIEVE(cons(s(N''), nnats(X''')))
SIEVE(cons(s(N), nsieve(X''))) -> ACTIVATE(nsieve(X''))
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)
SIEVE(cons(s(N), nsieve(X'))) -> FILTER(sieve(X'), N, N)
ACTIVATE(nsieve(cons(s(N''), nsieve(X''')))) -> SIEVE(cons(s(N''), nsieve(X''')))
FILTER(cons(X, nsieve(X'')), s(N), M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(cons(X'', nsieve(X'''')), s(N''), X3')) -> FILTER(cons(X'', nsieve(X'''')), s(N''), X3')
ACTIVATE(nfilter(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), X3')) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), X3')
FILTER(cons(X, nfilter(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nfilter(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
ACTIVATE(nsieve(cons(s(N''), nfilter(X1''', X2''', X3''')))) -> SIEVE(cons(s(N''), nfilter(X1''', X2''', X3''')))
FILTER(cons(X, nsieve(X'')), 0, M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(cons(X'', nsieve(X'''')), 0, X3')) -> FILTER(cons(X'', nsieve(X'''')), 0, X3')
FILTER(cons(X, nfilter(X1'', X2'', X3'')), 0, M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
ACTIVATE(nfilter(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, X3')) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, X3')
SIEVE(cons(s(N), nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))


Rules:


filter(cons(X, Y), 0, M) -> cons(0, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(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), nnats(X'))) -> FILTER(nats(X'), N, N)
two new Dependency Pairs are created:

SIEVE(cons(s(0), nnats(X''))) -> FILTER(nats(X''), 0, 0)
SIEVE(cons(s(s(N'')), nnats(X''))) -> FILTER(nats(X''), s(N''), s(N''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
FwdInst
             ...
               →DP Problem 9
Forward Instantiation Transformation


Dependency Pairs:

ACTIVATE(nsieve(cons(s(N''), nfilter(X1'''', X2'''', X3'''')))) -> SIEVE(cons(s(N''), nfilter(X1'''', X2'''', X3'''')))
SIEVE(cons(0, nsieve(X''))) -> ACTIVATE(nsieve(X''))
ACTIVATE(nsieve(cons(0, nsieve(X'''')))) -> SIEVE(cons(0, nsieve(X'''')))
SIEVE(cons(0, nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
ACTIVATE(nsieve(cons(0, nfilter(X1'''', X2'''', X3'''')))) -> SIEVE(cons(0, nfilter(X1'''', X2'''', X3'''')))
SIEVE(cons(s(N), nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
ACTIVATE(nsieve(cons(s(N''), Y'''))) -> SIEVE(cons(s(N''), Y'''))
SIEVE(cons(s(s(N'')), nnats(X''))) -> FILTER(nats(X''), s(N''), s(N''))
SIEVE(cons(s(0), nnats(X''))) -> FILTER(nats(X''), 0, 0)
ACTIVATE(nsieve(cons(s(N''), nnats(X''')))) -> SIEVE(cons(s(N''), nnats(X''')))
SIEVE(cons(s(N), nsieve(X''))) -> ACTIVATE(nsieve(X''))
SIEVE(cons(s(N), Y')) -> FILTER(Y', N, N)
ACTIVATE(nsieve(cons(s(N''), nsieve(X''')))) -> SIEVE(cons(s(N''), nsieve(X''')))
FILTER(cons(X, nsieve(X'')), s(N), M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(cons(X'', nsieve(X'''')), s(N''), X3')) -> FILTER(cons(X'', nsieve(X'''')), s(N''), X3')
ACTIVATE(nfilter(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), X3')) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), X3')
FILTER(cons(X, nfilter(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nfilter(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
ACTIVATE(nsieve(cons(s(N''), nfilter(X1''', X2''', X3''')))) -> SIEVE(cons(s(N''), nfilter(X1''', X2''', X3''')))
FILTER(cons(X, nsieve(X'')), 0, M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(cons(X'', nsieve(X'''')), 0, X3')) -> FILTER(cons(X'', nsieve(X'''')), 0, X3')
ACTIVATE(nfilter(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, X3')) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, X3')
FILTER(cons(X, nfilter(X1'', X2'', X3'')), 0, M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nsieve(X'))) -> FILTER(sieve(X'), N, N)
ACTIVATE(nsieve(cons(s(N''), nsieve(X'''')))) -> SIEVE(cons(s(N''), nsieve(X'''')))


Rules:


filter(cons(X, Y), 0, M) -> cons(0, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(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'', nfilter(X1'''', X2'''', X3'''')))) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, 0)
SIEVE(cons(s(0), cons(X'', nsieve(X'''')))) -> FILTER(cons(X'', nsieve(X'''')), 0, 0)
SIEVE(cons(s(s(N'')), cons(X'', nfilter(X1'''', X2'''', X3'''')))) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), s(N''))
SIEVE(cons(s(s(N'')), cons(X'', nsieve(X'''')))) -> FILTER(cons(X'', nsieve(X'''')), s(N''), s(N''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
FwdInst
             ...
               →DP Problem 10
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

ACTIVATE(nsieve(cons(s(N''), nsieve(X'''')))) -> SIEVE(cons(s(N''), nsieve(X'''')))
SIEVE(cons(0, nsieve(X''))) -> ACTIVATE(nsieve(X''))
ACTIVATE(nsieve(cons(0, nsieve(X'''')))) -> SIEVE(cons(0, nsieve(X'''')))
SIEVE(cons(0, nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
ACTIVATE(nsieve(cons(0, nfilter(X1'''', X2'''', X3'''')))) -> SIEVE(cons(0, nfilter(X1'''', X2'''', X3'''')))
SIEVE(cons(s(s(N'')), cons(X'', nsieve(X'''')))) -> FILTER(cons(X'', nsieve(X'''')), s(N''), s(N''))
SIEVE(cons(s(s(N'')), cons(X'', nfilter(X1'''', X2'''', X3'''')))) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), s(N''))
SIEVE(cons(s(0), cons(X'', nsieve(X'''')))) -> FILTER(cons(X'', nsieve(X'''')), 0, 0)
SIEVE(cons(s(0), cons(X'', nfilter(X1'''', X2'''', X3'''')))) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, 0)
ACTIVATE(nsieve(cons(s(N''), Y'''))) -> SIEVE(cons(s(N''), Y'''))
SIEVE(cons(s(s(N'')), nnats(X''))) -> FILTER(nats(X''), s(N''), s(N''))
SIEVE(cons(s(0), nnats(X''))) -> FILTER(nats(X''), 0, 0)
ACTIVATE(nsieve(cons(s(N''), nnats(X''')))) -> SIEVE(cons(s(N''), nnats(X''')))
SIEVE(cons(s(N), nsieve(X''))) -> ACTIVATE(nsieve(X''))
SIEVE(cons(s(N), nsieve(X'))) -> FILTER(sieve(X'), N, N)
ACTIVATE(nsieve(cons(s(N''), nsieve(X''')))) -> SIEVE(cons(s(N''), nsieve(X''')))
FILTER(cons(X, nsieve(X'')), s(N), M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(cons(X'', nsieve(X'''')), s(N''), X3')) -> FILTER(cons(X'', nsieve(X'''')), s(N''), X3')
FILTER(cons(X, nfilter(X1'', X2'', X3'')), s(N), M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
ACTIVATE(nfilter(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), X3')) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), s(N''), X3')
SIEVE(cons(s(N), nfilter(X1'', X2'', X3''))) -> ACTIVATE(nfilter(X1'', X2'', X3''))
ACTIVATE(nsieve(cons(s(N''), nfilter(X1''', X2''', X3''')))) -> SIEVE(cons(s(N''), nfilter(X1''', X2''', X3''')))
FILTER(cons(X, nsieve(X'')), 0, M) -> ACTIVATE(nsieve(X''))
ACTIVATE(nfilter(cons(X'', nsieve(X'''')), 0, X3')) -> FILTER(cons(X'', nsieve(X'''')), 0, X3')
ACTIVATE(nfilter(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, X3')) -> FILTER(cons(X'', nfilter(X1'''', X2'''', X3'''')), 0, X3')
FILTER(cons(X, nfilter(X1'', X2'', X3'')), 0, M) -> ACTIVATE(nfilter(X1'', X2'', X3''))
SIEVE(cons(s(N), nfilter(X1', X2', X3'))) -> FILTER(filter(X1', X2', X3'), N, N)
ACTIVATE(nsieve(cons(s(N''), nfilter(X1'''', X2'''', X3'''')))) -> SIEVE(cons(s(N''), nfilter(X1'''', X2'''', X3'''')))


Rules:


filter(cons(X, Y), 0, M) -> cons(0, nfilter(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, nfilter(activate(Y), N, M))
filter(X1, X2, X3) -> nfilter(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, nsieve(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), nsieve(filter(activate(Y), N, N)))
sieve(X) -> nsieve(X)
nats(N) -> cons(N, nnats(s(N)))
nats(X) -> nnats(X)
zprimes -> sieve(nats(s(s(0))))
activate(nfilter(X1, X2, X3)) -> filter(X1, X2, X3)
activate(nsieve(X)) -> sieve(X)
activate(nnats(X)) -> nats(X)
activate(X) -> X


Strategy:

innermost



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