(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
primes → sieve(from(s(s(0))))
from(X) → cons(X, n__from(s(X)))
head(cons(X, Y)) → X
tail(cons(X, Y)) → activate(Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), n__filter(s(s(X)), activate(Z)), n__cons(Y, n__filter(X, sieve(Y))))
sieve(cons(X, Y)) → cons(X, n__filter(X, sieve(activate(Y))))
from(X) → n__from(X)
filter(X1, X2) → n__filter(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(X)
activate(n__filter(X1, X2)) → filter(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
primes → sieve(from(s(s(0))))
from(z0) → cons(z0, n__from(s(z0)))
from(z0) → n__from(z0)
head(cons(z0, z1)) → z0
tail(cons(z0, z1)) → activate(z1)
if(true, z0, z1) → activate(z0)
if(false, z0, z1) → activate(z1)
filter(s(s(z0)), cons(z1, z2)) → if(divides(s(s(z0)), z1), n__filter(s(s(z0)), activate(z2)), n__cons(z1, n__filter(z0, sieve(z1))))
filter(z0, z1) → n__filter(z0, z1)
sieve(cons(z0, z1)) → cons(z0, n__filter(z0, sieve(activate(z1))))
cons(z0, z1) → n__cons(z0, z1)
activate(n__from(z0)) → from(z0)
activate(n__filter(z0, z1)) → filter(z0, z1)
activate(n__cons(z0, z1)) → cons(z0, z1)
activate(z0) → z0
Tuples:
PRIMES → c(SIEVE(from(s(s(0)))), FROM(s(s(0))))
FROM(z0) → c1(CONS(z0, n__from(s(z0))))
TAIL(cons(z0, z1)) → c4(ACTIVATE(z1))
IF(true, z0, z1) → c5(ACTIVATE(z0))
IF(false, z0, z1) → c6(ACTIVATE(z1))
FILTER(s(s(z0)), cons(z1, z2)) → c7(IF(divides(s(s(z0)), z1), n__filter(s(s(z0)), activate(z2)), n__cons(z1, n__filter(z0, sieve(z1)))), ACTIVATE(z2), SIEVE(z1))
SIEVE(cons(z0, z1)) → c9(CONS(z0, n__filter(z0, sieve(activate(z1)))), SIEVE(activate(z1)), ACTIVATE(z1))
ACTIVATE(n__from(z0)) → c11(FROM(z0))
ACTIVATE(n__filter(z0, z1)) → c12(FILTER(z0, z1))
ACTIVATE(n__cons(z0, z1)) → c13(CONS(z0, z1))
S tuples:
PRIMES → c(SIEVE(from(s(s(0)))), FROM(s(s(0))))
FROM(z0) → c1(CONS(z0, n__from(s(z0))))
TAIL(cons(z0, z1)) → c4(ACTIVATE(z1))
IF(true, z0, z1) → c5(ACTIVATE(z0))
IF(false, z0, z1) → c6(ACTIVATE(z1))
FILTER(s(s(z0)), cons(z1, z2)) → c7(IF(divides(s(s(z0)), z1), n__filter(s(s(z0)), activate(z2)), n__cons(z1, n__filter(z0, sieve(z1)))), ACTIVATE(z2), SIEVE(z1))
SIEVE(cons(z0, z1)) → c9(CONS(z0, n__filter(z0, sieve(activate(z1)))), SIEVE(activate(z1)), ACTIVATE(z1))
ACTIVATE(n__from(z0)) → c11(FROM(z0))
ACTIVATE(n__filter(z0, z1)) → c12(FILTER(z0, z1))
ACTIVATE(n__cons(z0, z1)) → c13(CONS(z0, z1))
K tuples:none
Defined Rule Symbols:
primes, from, head, tail, if, filter, sieve, cons, activate
Defined Pair Symbols:
PRIMES, FROM, TAIL, IF, FILTER, SIEVE, ACTIVATE
Compound Symbols:
c, c1, c4, c5, c6, c7, c9, c11, c12, c13
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
TAIL(cons(z0, z1)) → c4(ACTIVATE(z1))
FILTER(s(s(z0)), cons(z1, z2)) → c7(IF(divides(s(s(z0)), z1), n__filter(s(s(z0)), activate(z2)), n__cons(z1, n__filter(z0, sieve(z1)))), ACTIVATE(z2), SIEVE(z1))
SIEVE(cons(z0, z1)) → c9(CONS(z0, n__filter(z0, sieve(activate(z1)))), SIEVE(activate(z1)), ACTIVATE(z1))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
primes → sieve(from(s(s(0))))
from(z0) → cons(z0, n__from(s(z0)))
from(z0) → n__from(z0)
head(cons(z0, z1)) → z0
tail(cons(z0, z1)) → activate(z1)
if(true, z0, z1) → activate(z0)
if(false, z0, z1) → activate(z1)
filter(s(s(z0)), cons(z1, z2)) → if(divides(s(s(z0)), z1), n__filter(s(s(z0)), activate(z2)), n__cons(z1, n__filter(z0, sieve(z1))))
filter(z0, z1) → n__filter(z0, z1)
sieve(cons(z0, z1)) → cons(z0, n__filter(z0, sieve(activate(z1))))
cons(z0, z1) → n__cons(z0, z1)
activate(n__from(z0)) → from(z0)
activate(n__filter(z0, z1)) → filter(z0, z1)
activate(n__cons(z0, z1)) → cons(z0, z1)
activate(z0) → z0
Tuples:
PRIMES → c(SIEVE(from(s(s(0)))), FROM(s(s(0))))
FROM(z0) → c1(CONS(z0, n__from(s(z0))))
IF(true, z0, z1) → c5(ACTIVATE(z0))
IF(false, z0, z1) → c6(ACTIVATE(z1))
ACTIVATE(n__from(z0)) → c11(FROM(z0))
ACTIVATE(n__filter(z0, z1)) → c12(FILTER(z0, z1))
ACTIVATE(n__cons(z0, z1)) → c13(CONS(z0, z1))
S tuples:
PRIMES → c(SIEVE(from(s(s(0)))), FROM(s(s(0))))
FROM(z0) → c1(CONS(z0, n__from(s(z0))))
IF(true, z0, z1) → c5(ACTIVATE(z0))
IF(false, z0, z1) → c6(ACTIVATE(z1))
ACTIVATE(n__from(z0)) → c11(FROM(z0))
ACTIVATE(n__filter(z0, z1)) → c12(FILTER(z0, z1))
ACTIVATE(n__cons(z0, z1)) → c13(CONS(z0, z1))
K tuples:none
Defined Rule Symbols:
primes, from, head, tail, if, filter, sieve, cons, activate
Defined Pair Symbols:
PRIMES, FROM, IF, ACTIVATE
Compound Symbols:
c, c1, c5, c6, c11, c12, c13
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 7 trailing nodes:
IF(true, z0, z1) → c5(ACTIVATE(z0))
PRIMES → c(SIEVE(from(s(s(0)))), FROM(s(s(0))))
ACTIVATE(n__filter(z0, z1)) → c12(FILTER(z0, z1))
FROM(z0) → c1(CONS(z0, n__from(s(z0))))
IF(false, z0, z1) → c6(ACTIVATE(z1))
ACTIVATE(n__from(z0)) → c11(FROM(z0))
ACTIVATE(n__cons(z0, z1)) → c13(CONS(z0, z1))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
primes → sieve(from(s(s(0))))
from(z0) → cons(z0, n__from(s(z0)))
from(z0) → n__from(z0)
head(cons(z0, z1)) → z0
tail(cons(z0, z1)) → activate(z1)
if(true, z0, z1) → activate(z0)
if(false, z0, z1) → activate(z1)
filter(s(s(z0)), cons(z1, z2)) → if(divides(s(s(z0)), z1), n__filter(s(s(z0)), activate(z2)), n__cons(z1, n__filter(z0, sieve(z1))))
filter(z0, z1) → n__filter(z0, z1)
sieve(cons(z0, z1)) → cons(z0, n__filter(z0, sieve(activate(z1))))
cons(z0, z1) → n__cons(z0, z1)
activate(n__from(z0)) → from(z0)
activate(n__filter(z0, z1)) → filter(z0, z1)
activate(n__cons(z0, z1)) → cons(z0, z1)
activate(z0) → z0
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
primes, from, head, tail, if, filter, sieve, cons, activate
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))