Runtime Complexity (innermost) proof of /tmp/tmpaXX7Fc/ExIntrod_GM99

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS

↳1 DependencyGraphProof (BOTH BOUNDS(ID, ID), 3 ms)

↳2 CpxTRS

↳3 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CpxWeightedTrs

↳5 InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CpxWeightedTrs

↳7 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CpxTypedWeightedTrs

↳9 CompletionProof (UPPER BOUND(ID), 0 ms)

↳10 CpxTypedWeightedCompleteTrs

↳11 NarrowingProof (BOTH BOUNDS(ID, ID), 25 ms)

↳12 CpxTypedWeightedCompleteTrs

↳13 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)

↳14 CpxRNTS

↳15 InliningProof (UPPER BOUND(ID), 199 ms)

↳16 CpxRNTS

↳17 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)

↳18 CpxRNTS

↳19 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)

↳20 CpxRNTS

↳21 IntTrsBoundProof (UPPER BOUND(ID), 167 ms)

↳22 CpxRNTS

↳23 IntTrsBoundProof (UPPER BOUND(ID), 62 ms)

↳24 CpxRNTS

↳25 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳26 CpxRNTS

↳27 IntTrsBoundProof (UPPER BOUND(ID), 224 ms)

↳28 CpxRNTS

↳29 IntTrsBoundProof (UPPER BOUND(ID), 6 ms)

↳30 CpxRNTS

↳31 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳32 CpxRNTS

↳33 IntTrsBoundProof (UPPER BOUND(ID), 74 ms)

↳34 CpxRNTS

↳35 IntTrsBoundProof (UPPER BOUND(ID), 37 ms)

↳36 CpxRNTS

↳37 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳38 CpxRNTS

↳39 IntTrsBoundProof (UPPER BOUND(ID), 155 ms)

↳40 CpxRNTS

↳41 IntTrsBoundProof (UPPER BOUND(ID), 17 ms)

↳42 CpxRNTS

↳43 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳44 CpxRNTS

↳45 IntTrsBoundProof (UPPER BOUND(ID), 105 ms)

↳46 CpxRNTS

↳47 IntTrsBoundProof (UPPER BOUND(ID), 96 ms)

↳48 CpxRNTS

↳49 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳50 CpxRNTS

↳51 IntTrsBoundProof (UPPER BOUND(ID), 7632 ms)

↳52 CpxRNTS

↳53 IntTrsBoundProof (UPPER BOUND(ID), 856 ms)

↳54 CpxRNTS

↳55 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳56 CpxRNTS

↳57 IntTrsBoundProof (UPPER BOUND(ID), 76 ms)

↳58 CpxRNTS

↳59 IntTrsBoundProof (UPPER BOUND(ID), 34 ms)

↳60 CpxRNTS

↳61 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳62 CpxRNTS

↳63 IntTrsBoundProof (UPPER BOUND(ID), 1314 ms)

↳64 CpxRNTS

↳65 IntTrsBoundProof (UPPER BOUND(ID), 15 ms)

↳66 CpxRNTS

↳67 FinalProof (⇔, 0 ms)

↳68 BOUNDS(1, n^1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

primes → sieve(from(s(s(0))))
from(X) → cons(X, n__from(n__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(n__s(n__s(X)), activate(Z)), n__cons(Y, n__filter(X, n__sieve(Y))))
sieve(cons(X, Y)) → cons(X, n__filter(X, n__sieve(activate(Y))))
from(X) → n__from(X)
s(X) → n__s(X)
filter(X1, X2) → n__filter(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
sieve(X) → n__sieve(X)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__filter(X1, X2)) → filter(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__sieve(X)) → sieve(activate(X))
activate(X) → X

Rewrite Strategy: INNERMOST

(1) DependencyGraphProof (BOTH BOUNDS(ID, ID) transformation)

The following rules are not reachable from basic terms in the dependency graph and can be removed:
head(cons(X, Y)) → X
tail(cons(X, Y)) → activate(Y)

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

primes → sieve(from(s(s(0))))
activate(n__filter(X1, X2)) → filter(activate(X1), activate(X2))
sieve(cons(X, Y)) → cons(X, n__filter(X, n__sieve(activate(Y))))
sieve(X) → n__sieve(X)
if(true, X, Y) → activate(X)
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
activate(n__s(X)) → s(activate(X))
filter(X1, X2) → n__filter(X1, X2)
activate(n__from(X)) → from(activate(X))
from(X) → cons(X, n__from(n__s(X)))
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), n__filter(n__s(n__s(X)), activate(Z)), n__cons(Y, n__filter(X, n__sieve(Y))))
if(false, X, Y) → activate(Y)
from(X) → n__from(X)
s(X) → n__s(X)
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__sieve(X)) → sieve(activate(X))

Rewrite Strategy: INNERMOST

(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

primes → sieve(from(s(s(0)))) [1]
activate(n__filter(X1, X2)) → filter(activate(X1), activate(X2)) [1]
sieve(cons(X, Y)) → cons(X, n__filter(X, n__sieve(activate(Y)))) [1]
sieve(X) → n__sieve(X) [1]
if(true, X, Y) → activate(X) [1]
activate(X) → X [1]
cons(X1, X2) → n__cons(X1, X2) [1]
activate(n__s(X)) → s(activate(X)) [1]
filter(X1, X2) → n__filter(X1, X2) [1]
activate(n__from(X)) → from(activate(X)) [1]
from(X) → cons(X, n__from(n__s(X))) [1]
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), n__filter(n__s(n__s(X)), activate(Z)), n__cons(Y, n__filter(X, n__sieve(Y)))) [1]
if(false, X, Y) → activate(Y) [1]
from(X) → n__from(X) [1]
s(X) → n__s(X) [1]
activate(n__cons(X1, X2)) → cons(activate(X1), X2) [1]
activate(n__sieve(X)) → sieve(activate(X)) [1]

Rewrite Strategy: INNERMOST

(5) InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID) transformation)

Removed the following rules with non-basic left-hand side, as they cannot be used in innermost rewriting:

sieve(cons(X, Y)) → cons(X, n__filter(X, n__sieve(activate(Y)))) [1]
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), n__filter(n__s(n__s(X)), activate(Z)), n__cons(Y, n__filter(X, n__sieve(Y)))) [1]

Due to the following rules that have to be used instead:

cons(X1, X2) → n__cons(X1, X2) [1]
s(X) → n__s(X) [1]

(6) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

primes → sieve(from(s(s(0)))) [1]
activate(n__filter(X1, X2)) → filter(activate(X1), activate(X2)) [1]
sieve(X) → n__sieve(X) [1]
if(true, X, Y) → activate(X) [1]
activate(X) → X [1]
cons(X1, X2) → n__cons(X1, X2) [1]
activate(n__s(X)) → s(activate(X)) [1]
filter(X1, X2) → n__filter(X1, X2) [1]
activate(n__from(X)) → from(activate(X)) [1]
from(X) → cons(X, n__from(n__s(X))) [1]
if(false, X, Y) → activate(Y) [1]
from(X) → n__from(X) [1]
s(X) → n__s(X) [1]
activate(n__cons(X1, X2)) → cons(activate(X1), X2) [1]
activate(n__sieve(X)) → sieve(activate(X)) [1]

Rewrite Strategy: INNERMOST

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

primes → sieve(from(s(s(0)))) [1]
activate(n__filter(X1, X2)) → filter(activate(X1), activate(X2)) [1]
sieve(X) → n__sieve(X) [1]
if(true, X, Y) → activate(X) [1]
activate(X) → X [1]
cons(X1, X2) → n__cons(X1, X2) [1]
activate(n__s(X)) → s(activate(X)) [1]
filter(X1, X2) → n__filter(X1, X2) [1]
activate(n__from(X)) → from(activate(X)) [1]
from(X) → cons(X, n__from(n__s(X))) [1]
if(false, X, Y) → activate(Y) [1]
from(X) → n__from(X) [1]
s(X) → n__s(X) [1]
activate(n__cons(X1, X2)) → cons(activate(X1), X2) [1]
activate(n__sieve(X)) → sieve(activate(X)) [1]

The TRS has the following type information:

primes :: 0:n__filter:n__sieve:n__cons:n__s:n__from
sieve :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
from :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
s :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
0 :: 0:n__filter:n__sieve:n__cons:n__s:n__from
activate :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
n__filter :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
filter :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
n__sieve :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
if :: true:false → 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
true :: true:false
cons :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
n__cons :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
n__s :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
n__from :: 0:n__filter:n__sieve:n__cons:n__s:n__from → 0:n__filter:n__sieve:n__cons:n__s:n__from
false :: true:false

Rewrite Strategy: INNERMOST

(9) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

primes
if

from
s
activate
filter
cons
sieve

Due to the following rules being added:
none

And the following fresh constants: none

(10) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

primes → sieve(from(s(s(0)))) [1]
activate(n__filter(X1, X2)) → filter(activate(X1), activate(X2)) [1]
sieve(X) → n__sieve(X) [1]
if(true, X, Y) → activate(X) [1]
activate(X) → X [1]
cons(X1, X2) → n__cons(X1, X2) [1]
activate(n__s(X)) → s(activate(X)) [1]
filter(X1, X2) → n__filter(X1, X2) [1]
activate(n__from(X)) → from(activate(X)) [1]
from(X) → cons(X, n__from(n__s(X))) [1]
if(false, X, Y) → activate(Y) [1]
from(X) → n__from(X) [1]
s(X) → n__s(X) [1]
activate(n__cons(X1, X2)) → cons(activate(X1), X2) [1]
activate(n__sieve(X)) → sieve(activate(X)) [1]

The TRS has the following type information:

Rewrite Strategy: INNERMOST

(11) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(12) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

primes → sieve(from(s(n__s(0)))) [2]
activate(n__filter(X1, X2)) → filter(activate(X1), activate(X2)) [1]
sieve(X) → n__sieve(X) [1]
if(true, X, Y) → activate(X) [1]
activate(X) → X [1]
cons(X1, X2) → n__cons(X1, X2) [1]
activate(n__s(n__filter(X115, X214))) → s(filter(activate(X115), activate(X214))) [2]
activate(n__s(X)) → s(X) [2]
activate(n__s(n__s(X37))) → s(s(activate(X37))) [2]
activate(n__s(n__from(X38))) → s(from(activate(X38))) [2]
activate(n__s(n__cons(X116, X215))) → s(cons(activate(X116), X215)) [2]
activate(n__s(n__sieve(X39))) → s(sieve(activate(X39))) [2]
filter(X1, X2) → n__filter(X1, X2) [1]
activate(n__from(n__filter(X117, X216))) → from(filter(activate(X117), activate(X216))) [2]
activate(n__from(X)) → from(X) [2]
activate(n__from(n__s(X40))) → from(s(activate(X40))) [2]
activate(n__from(n__from(X41))) → from(from(activate(X41))) [2]
activate(n__from(n__cons(X118, X217))) → from(cons(activate(X118), X217)) [2]
activate(n__from(n__sieve(X42))) → from(sieve(activate(X42))) [2]
from(X) → cons(X, n__from(n__s(X))) [1]
if(false, X, Y) → activate(Y) [1]
from(X) → n__from(X) [1]
s(X) → n__s(X) [1]
activate(n__cons(n__filter(X119, X218), X2)) → cons(filter(activate(X119), activate(X218)), X2) [2]
activate(n__cons(X1, X2)) → cons(X1, X2) [2]
activate(n__cons(n__s(X43), X2)) → cons(s(activate(X43)), X2) [2]
activate(n__cons(n__from(X44), X2)) → cons(from(activate(X44)), X2) [2]
activate(n__cons(n__cons(X120, X219), X2)) → cons(cons(activate(X120), X219), X2) [2]
activate(n__cons(n__sieve(X45), X2)) → cons(sieve(activate(X45)), X2) [2]
activate(n__sieve(n__filter(X121, X220))) → sieve(filter(activate(X121), activate(X220))) [2]
activate(n__sieve(X)) → sieve(X) [2]
activate(n__sieve(n__s(X46))) → sieve(s(activate(X46))) [2]
activate(n__sieve(n__from(X47))) → sieve(from(activate(X47))) [2]
activate(n__sieve(n__cons(X122, X221))) → sieve(cons(activate(X122), X221)) [2]
activate(n__sieve(n__sieve(X48))) → sieve(sieve(activate(X48))) [2]

The TRS has the following type information:

Rewrite Strategy: INNERMOST

(13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
true => 1
false => 0

(14) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ sieve(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(X48))) :|: z = 1 + (1 + X48), X48 >= 0
activate(z) -{ 2 }→ sieve(s(activate(X46))) :|: X46 >= 0, z = 1 + (1 + X46)
activate(z) -{ 2 }→ sieve(from(activate(X47))) :|: X47 >= 0, z = 1 + (1 + X47)
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ s(sieve(activate(X39))) :|: z = 1 + (1 + X39), X39 >= 0
activate(z) -{ 2 }→ s(s(activate(X37))) :|: X37 >= 0, z = 1 + (1 + X37)
activate(z) -{ 2 }→ s(from(activate(X38))) :|: X38 >= 0, z = 1 + (1 + X38)
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ from(sieve(activate(X42))) :|: X42 >= 0, z = 1 + (1 + X42)
activate(z) -{ 2 }→ from(s(activate(X40))) :|: z = 1 + (1 + X40), X40 >= 0
activate(z) -{ 2 }→ from(from(activate(X41))) :|: X41 >= 0, z = 1 + (1 + X41)
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
filter(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
from(z) -{ 1 }→ cons(X, 1 + (1 + X)) :|: X >= 0, z = X
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
if(z, z', z'') -{ 1 }→ activate(X) :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0
if(z, z', z'') -{ 1 }→ activate(Y) :|: z' = X, Y >= 0, z'' = Y, X >= 0, z = 0
primes -{ 2 }→ sieve(from(s(1 + 0))) :|:
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sieve(z) -{ 1 }→ 1 + X :|: X >= 0, z = X

(15) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

sieve(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
filter(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
from(z) -{ 1 }→ cons(X, 1 + (1 + X)) :|: X >= 0, z = X
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X

(16) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ sieve(sieve(activate(X48))) :|: z = 1 + (1 + X48), X48 >= 0
activate(z) -{ 2 }→ sieve(s(activate(X46))) :|: X46 >= 0, z = 1 + (1 + X46)
activate(z) -{ 2 }→ sieve(from(activate(X47))) :|: X47 >= 0, z = 1 + (1 + X47)
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(X39))) :|: z = 1 + (1 + X39), X39 >= 0
activate(z) -{ 2 }→ s(s(activate(X37))) :|: X37 >= 0, z = 1 + (1 + X37)
activate(z) -{ 2 }→ s(from(activate(X38))) :|: X38 >= 0, z = 1 + (1 + X38)
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(X42))) :|: X42 >= 0, z = 1 + (1 + X42)
activate(z) -{ 2 }→ from(s(activate(X40))) :|: z = 1 + (1 + X40), X40 >= 0
activate(z) -{ 2 }→ from(from(activate(X41))) :|: X41 >= 0, z = 1 + (1 + X41)
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
filter(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
from(z) -{ 2 }→ 1 + X1 + X2 :|: X >= 0, z = X, X1 >= 0, X2 >= 0, X = X1, 1 + (1 + X) = X2
if(z, z', z'') -{ 1 }→ activate(X) :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0
if(z, z', z'') -{ 1 }→ activate(Y) :|: z' = X, Y >= 0, z'' = Y, X >= 0, z = 0
primes -{ 4 }→ sieve(cons(X', 1 + (1 + X'))) :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sieve(z) -{ 1 }→ 1 + X :|: X >= 0, z = X

(17) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(18) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 4 }→ sieve(cons(X', 1 + (1 + X'))) :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

(19) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ from }
{ cons }
{ sieve }
{ filter }
{ s }
{ activate }
{ primes }
{ if }

(20) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 4 }→ sieve(cons(X', 1 + (1 + X'))) :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {from}, {cons}, {sieve}, {filter}, {s}, {activate}, {primes}, {if}

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: from
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 3 + 2·z

(22) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 4 }→ sieve(cons(X', 1 + (1 + X'))) :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {from}, {cons}, {sieve}, {filter}, {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: ?, size: O(n¹) [3 + 2·z]

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: from
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 2

(24) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 4 }→ sieve(cons(X', 1 + (1 + X'))) :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {cons}, {sieve}, {filter}, {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 4 }→ sieve(cons(X', 1 + (1 + X'))) :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {cons}, {sieve}, {filter}, {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: cons
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z'

(28) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 4 }→ sieve(cons(X', 1 + (1 + X'))) :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {cons}, {sieve}, {filter}, {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]
cons: runtime: ?, size: O(n¹) [1 + z + z']

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: cons
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(30) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 4 }→ sieve(cons(X', 1 + (1 + X'))) :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {sieve}, {filter}, {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]
cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(32) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 5 }→ sieve(s') :|: s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {sieve}, {filter}, {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]
cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: sieve
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(34) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 5 }→ sieve(s') :|: s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {sieve}, {filter}, {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]
cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
sieve: runtime: ?, size: O(n¹) [1 + z]

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: sieve
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(36) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 5 }→ sieve(s') :|: s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 4 }→ sieve(1 + X') :|: X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {filter}, {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]
cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
sieve: runtime: O(1) [1], size: O(n¹) [1 + z]

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(38) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {filter}, {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]
cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
sieve: runtime: O(1) [1], size: O(n¹) [1 + z]

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: filter
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z'

(40) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {filter}, {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]
cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
sieve: runtime: O(1) [1], size: O(n¹) [1 + z]
filter: runtime: ?, size: O(n¹) [1 + z + z']

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: filter
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(42) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]
cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
sieve: runtime: O(1) [1], size: O(n¹) [1 + z]
filter: runtime: O(1) [1], size: O(n¹) [1 + z + z']

(43) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(44) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {s}, {activate}, {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]
cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
sieve: runtime: O(1) [1], size: O(n¹) [1 + z]
filter: runtime: O(1) [1], size: O(n¹) [1 + z + z']

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: s
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(46) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {s}, {activate}, {primes}, {if}
Previous analysis results are:

(47) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: s
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(48) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {activate}, {primes}, {if}
Previous analysis results are:

(49) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(50) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {activate}, {primes}, {if}
Previous analysis results are:

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: EXP with polynomial bound: ?

(52) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {activate}, {primes}, {if}
Previous analysis results are:

(53) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 75 + 150·z

(54) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ sieve(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sieve(filter(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 2 }→ sieve(cons(activate(X122), X221)) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ s(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(filter(activate(X115), activate(X214))) :|: z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ 2 }→ s(cons(activate(X116), X215)) :|: z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 2 }→ from(sieve(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(filter(activate(X117), activate(X216))) :|: X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ 2 }→ from(cons(activate(X118), X217)) :|: X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ 1 }→ filter(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(sieve(activate(X45)), X2) :|: X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 2 }→ cons(s(activate(X43)), X2) :|: z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X44)), X2) :|: z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 2 }→ cons(filter(activate(X119), activate(X218)), X2) :|: z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X120), X219), X2) :|: z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 1 }→ activate(z') :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 1 }→ activate(z'') :|: z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {primes}, {if}
Previous analysis results are:

from: runtime: O(1) [2], size: O(n¹) [3 + 2·z]
cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
sieve: runtime: O(1) [1], size: O(n¹) [1 + z]
filter: runtime: O(1) [1], size: O(n¹) [1 + z + z']
s: runtime: O(1) [1], size: O(n¹) [1 + z]
activate: runtime: O(n¹) [75 + 150·z], size: EXP

(55) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(56) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 79 + 150·X45 }→ s12 :|: s10 >= 0, s10 <= inf2, s11 >= 0, s11 <= 1 * s10 + 1, s12 >= 0, s12 <= 1 * s11 + 1 * X2 + 1, X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 79 + 150·X122 }→ s15 :|: s13 >= 0, s13 <= inf3, s14 >= 0, s14 <= 1 * s13 + 1 * X221 + 1, s15 >= 0, s15 <= 1 * s14 + 1, X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 152 + 150·X1 + 150·X2 }→ s18 :|: s16 >= 0, s16 <= inf4, s17 >= 0, s17 <= inf5, s18 >= 0, s18 <= 1 * s16 + 1 * s17 + 1, X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 154 + 150·X121 + 150·X220 }→ s22 :|: s19 >= 0, s19 <= inf6, s20 >= 0, s20 <= inf7, s21 >= 0, s21 <= 1 * s19 + 1 * s20 + 1, s22 >= 0, s22 <= 1 * s21 + 1, z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 154 + 150·X119 + 150·X218 }→ s26 :|: s23 >= 0, s23 <= inf8, s24 >= 0, s24 <= inf9, s25 >= 0, s25 <= 1 * s23 + 1 * s24 + 1, s26 >= 0, s26 <= 1 * s25 + 1 * X2 + 1, z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ -221 + 150·z }→ s29 :|: s27 >= 0, s27 <= inf10, s28 >= 0, s28 <= 1 * s27 + 1, s29 >= 0, s29 <= 1 * s28 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s32 :|: s30 >= 0, s30 <= inf11, s31 >= 0, s31 <= 1 * s30 + 1, s32 >= 0, s32 <= 1 * s31 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s35 :|: s33 >= 0, s33 <= inf12, s34 >= 0, s34 <= 1 * s33 + 1, s35 >= 0, s35 <= 1 * s34 + 1, z - 2 >= 0
activate(z) -{ 79 + 150·X116 }→ s38 :|: s36 >= 0, s36 <= inf13, s37 >= 0, s37 <= 1 * s36 + 1 * X215 + 1, s38 >= 0, s38 <= 1 * s37 + 1, z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 79 + 150·X43 }→ s41 :|: s39 >= 0, s39 <= inf14, s40 >= 0, s40 <= 1 * s39 + 1, s41 >= 0, s41 <= 1 * s40 + 1 * X2 + 1, z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 154 + 150·X115 + 150·X214 }→ s45 :|: s42 >= 0, s42 <= inf15, s43 >= 0, s43 <= inf16, s44 >= 0, s44 <= 1 * s42 + 1 * s43 + 1, s45 >= 0, s45 <= 1 * s44 + 1, z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ -219 + 150·z }→ s48 :|: s46 >= 0, s46 <= inf17, s47 >= 0, s47 <= 2 * s46 + 3, s48 >= 0, s48 <= 2 * s47 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s51 :|: s49 >= 0, s49 <= inf18, s50 >= 0, s50 <= 1 * s49 + 1, s51 >= 0, s51 <= 2 * s50 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s54 :|: s52 >= 0, s52 <= inf19, s53 >= 0, s53 <= 2 * s52 + 3, s54 >= 0, s54 <= 1 * s53 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X118 }→ s57 :|: s55 >= 0, s55 <= inf20, s56 >= 0, s56 <= 1 * s55 + 1 * X217 + 1, s57 >= 0, s57 <= 2 * s56 + 3, X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ -221 + 150·z }→ s6 :|: s4 >= 0, s4 <= inf'', s5 >= 0, s5 <= 1 * s4 + 1, s6 >= 0, s6 <= 1 * s5 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X44 }→ s60 :|: s58 >= 0, s58 <= inf21, s59 >= 0, s59 <= 2 * s58 + 3, s60 >= 0, s60 <= 1 * s59 + 1 * X2 + 1, z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 155 + 150·X117 + 150·X216 }→ s64 :|: s61 >= 0, s61 <= inf22, s62 >= 0, s62 <= inf23, s63 >= 0, s63 <= 1 * s61 + 1 * s62 + 1, s64 >= 0, s64 <= 2 * s63 + 3, X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ -220 + 150·z }→ s67 :|: s65 >= 0, s65 <= inf24, s66 >= 0, s66 <= 2 * s65 + 3, s67 >= 0, s67 <= 1 * s66 + 1, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s70 :|: s68 >= 0, s68 <= inf25, s69 >= 0, s69 <= 1 * s68 + 1, s70 >= 0, s70 <= 2 * s69 + 3, z - 2 >= 0
activate(z) -{ 79 + 150·X120 }→ s9 :|: s7 >= 0, s7 <= inf1, s8 >= 0, s8 <= 1 * s7 + 1 * X219 + 1, s9 >= 0, s9 <= 1 * s8 + 1 * X2 + 1, z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 76 + 150·z' }→ s2 :|: s2 >= 0, s2 <= inf, z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 76 + 150·z'' }→ s3 :|: s3 >= 0, s3 <= inf', z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {primes}, {if}
Previous analysis results are:

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: primes
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 8

(58) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 79 + 150·X45 }→ s12 :|: s10 >= 0, s10 <= inf2, s11 >= 0, s11 <= 1 * s10 + 1, s12 >= 0, s12 <= 1 * s11 + 1 * X2 + 1, X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 79 + 150·X122 }→ s15 :|: s13 >= 0, s13 <= inf3, s14 >= 0, s14 <= 1 * s13 + 1 * X221 + 1, s15 >= 0, s15 <= 1 * s14 + 1, X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 152 + 150·X1 + 150·X2 }→ s18 :|: s16 >= 0, s16 <= inf4, s17 >= 0, s17 <= inf5, s18 >= 0, s18 <= 1 * s16 + 1 * s17 + 1, X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 154 + 150·X121 + 150·X220 }→ s22 :|: s19 >= 0, s19 <= inf6, s20 >= 0, s20 <= inf7, s21 >= 0, s21 <= 1 * s19 + 1 * s20 + 1, s22 >= 0, s22 <= 1 * s21 + 1, z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 154 + 150·X119 + 150·X218 }→ s26 :|: s23 >= 0, s23 <= inf8, s24 >= 0, s24 <= inf9, s25 >= 0, s25 <= 1 * s23 + 1 * s24 + 1, s26 >= 0, s26 <= 1 * s25 + 1 * X2 + 1, z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ -221 + 150·z }→ s29 :|: s27 >= 0, s27 <= inf10, s28 >= 0, s28 <= 1 * s27 + 1, s29 >= 0, s29 <= 1 * s28 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s32 :|: s30 >= 0, s30 <= inf11, s31 >= 0, s31 <= 1 * s30 + 1, s32 >= 0, s32 <= 1 * s31 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s35 :|: s33 >= 0, s33 <= inf12, s34 >= 0, s34 <= 1 * s33 + 1, s35 >= 0, s35 <= 1 * s34 + 1, z - 2 >= 0
activate(z) -{ 79 + 150·X116 }→ s38 :|: s36 >= 0, s36 <= inf13, s37 >= 0, s37 <= 1 * s36 + 1 * X215 + 1, s38 >= 0, s38 <= 1 * s37 + 1, z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 79 + 150·X43 }→ s41 :|: s39 >= 0, s39 <= inf14, s40 >= 0, s40 <= 1 * s39 + 1, s41 >= 0, s41 <= 1 * s40 + 1 * X2 + 1, z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 154 + 150·X115 + 150·X214 }→ s45 :|: s42 >= 0, s42 <= inf15, s43 >= 0, s43 <= inf16, s44 >= 0, s44 <= 1 * s42 + 1 * s43 + 1, s45 >= 0, s45 <= 1 * s44 + 1, z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ -219 + 150·z }→ s48 :|: s46 >= 0, s46 <= inf17, s47 >= 0, s47 <= 2 * s46 + 3, s48 >= 0, s48 <= 2 * s47 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s51 :|: s49 >= 0, s49 <= inf18, s50 >= 0, s50 <= 1 * s49 + 1, s51 >= 0, s51 <= 2 * s50 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s54 :|: s52 >= 0, s52 <= inf19, s53 >= 0, s53 <= 2 * s52 + 3, s54 >= 0, s54 <= 1 * s53 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X118 }→ s57 :|: s55 >= 0, s55 <= inf20, s56 >= 0, s56 <= 1 * s55 + 1 * X217 + 1, s57 >= 0, s57 <= 2 * s56 + 3, X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ -221 + 150·z }→ s6 :|: s4 >= 0, s4 <= inf'', s5 >= 0, s5 <= 1 * s4 + 1, s6 >= 0, s6 <= 1 * s5 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X44 }→ s60 :|: s58 >= 0, s58 <= inf21, s59 >= 0, s59 <= 2 * s58 + 3, s60 >= 0, s60 <= 1 * s59 + 1 * X2 + 1, z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 155 + 150·X117 + 150·X216 }→ s64 :|: s61 >= 0, s61 <= inf22, s62 >= 0, s62 <= inf23, s63 >= 0, s63 <= 1 * s61 + 1 * s62 + 1, s64 >= 0, s64 <= 2 * s63 + 3, X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ -220 + 150·z }→ s67 :|: s65 >= 0, s65 <= inf24, s66 >= 0, s66 <= 2 * s65 + 3, s67 >= 0, s67 <= 1 * s66 + 1, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s70 :|: s68 >= 0, s68 <= inf25, s69 >= 0, s69 <= 1 * s68 + 1, s70 >= 0, s70 <= 2 * s69 + 3, z - 2 >= 0
activate(z) -{ 79 + 150·X120 }→ s9 :|: s7 >= 0, s7 <= inf1, s8 >= 0, s8 <= 1 * s7 + 1 * X219 + 1, s9 >= 0, s9 <= 1 * s8 + 1 * X2 + 1, z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 76 + 150·z' }→ s2 :|: s2 >= 0, s2 <= inf, z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 76 + 150·z'' }→ s3 :|: s3 >= 0, s3 <= inf', z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {primes}, {if}
Previous analysis results are:

(59) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: primes
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 11

(60) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 79 + 150·X45 }→ s12 :|: s10 >= 0, s10 <= inf2, s11 >= 0, s11 <= 1 * s10 + 1, s12 >= 0, s12 <= 1 * s11 + 1 * X2 + 1, X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 79 + 150·X122 }→ s15 :|: s13 >= 0, s13 <= inf3, s14 >= 0, s14 <= 1 * s13 + 1 * X221 + 1, s15 >= 0, s15 <= 1 * s14 + 1, X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 152 + 150·X1 + 150·X2 }→ s18 :|: s16 >= 0, s16 <= inf4, s17 >= 0, s17 <= inf5, s18 >= 0, s18 <= 1 * s16 + 1 * s17 + 1, X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 154 + 150·X121 + 150·X220 }→ s22 :|: s19 >= 0, s19 <= inf6, s20 >= 0, s20 <= inf7, s21 >= 0, s21 <= 1 * s19 + 1 * s20 + 1, s22 >= 0, s22 <= 1 * s21 + 1, z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 154 + 150·X119 + 150·X218 }→ s26 :|: s23 >= 0, s23 <= inf8, s24 >= 0, s24 <= inf9, s25 >= 0, s25 <= 1 * s23 + 1 * s24 + 1, s26 >= 0, s26 <= 1 * s25 + 1 * X2 + 1, z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ -221 + 150·z }→ s29 :|: s27 >= 0, s27 <= inf10, s28 >= 0, s28 <= 1 * s27 + 1, s29 >= 0, s29 <= 1 * s28 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s32 :|: s30 >= 0, s30 <= inf11, s31 >= 0, s31 <= 1 * s30 + 1, s32 >= 0, s32 <= 1 * s31 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s35 :|: s33 >= 0, s33 <= inf12, s34 >= 0, s34 <= 1 * s33 + 1, s35 >= 0, s35 <= 1 * s34 + 1, z - 2 >= 0
activate(z) -{ 79 + 150·X116 }→ s38 :|: s36 >= 0, s36 <= inf13, s37 >= 0, s37 <= 1 * s36 + 1 * X215 + 1, s38 >= 0, s38 <= 1 * s37 + 1, z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 79 + 150·X43 }→ s41 :|: s39 >= 0, s39 <= inf14, s40 >= 0, s40 <= 1 * s39 + 1, s41 >= 0, s41 <= 1 * s40 + 1 * X2 + 1, z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 154 + 150·X115 + 150·X214 }→ s45 :|: s42 >= 0, s42 <= inf15, s43 >= 0, s43 <= inf16, s44 >= 0, s44 <= 1 * s42 + 1 * s43 + 1, s45 >= 0, s45 <= 1 * s44 + 1, z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ -219 + 150·z }→ s48 :|: s46 >= 0, s46 <= inf17, s47 >= 0, s47 <= 2 * s46 + 3, s48 >= 0, s48 <= 2 * s47 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s51 :|: s49 >= 0, s49 <= inf18, s50 >= 0, s50 <= 1 * s49 + 1, s51 >= 0, s51 <= 2 * s50 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s54 :|: s52 >= 0, s52 <= inf19, s53 >= 0, s53 <= 2 * s52 + 3, s54 >= 0, s54 <= 1 * s53 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X118 }→ s57 :|: s55 >= 0, s55 <= inf20, s56 >= 0, s56 <= 1 * s55 + 1 * X217 + 1, s57 >= 0, s57 <= 2 * s56 + 3, X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ -221 + 150·z }→ s6 :|: s4 >= 0, s4 <= inf'', s5 >= 0, s5 <= 1 * s4 + 1, s6 >= 0, s6 <= 1 * s5 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X44 }→ s60 :|: s58 >= 0, s58 <= inf21, s59 >= 0, s59 <= 2 * s58 + 3, s60 >= 0, s60 <= 1 * s59 + 1 * X2 + 1, z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 155 + 150·X117 + 150·X216 }→ s64 :|: s61 >= 0, s61 <= inf22, s62 >= 0, s62 <= inf23, s63 >= 0, s63 <= 1 * s61 + 1 * s62 + 1, s64 >= 0, s64 <= 2 * s63 + 3, X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ -220 + 150·z }→ s67 :|: s65 >= 0, s65 <= inf24, s66 >= 0, s66 <= 2 * s65 + 3, s67 >= 0, s67 <= 1 * s66 + 1, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s70 :|: s68 >= 0, s68 <= inf25, s69 >= 0, s69 <= 1 * s68 + 1, s70 >= 0, s70 <= 2 * s69 + 3, z - 2 >= 0
activate(z) -{ 79 + 150·X120 }→ s9 :|: s7 >= 0, s7 <= inf1, s8 >= 0, s8 <= 1 * s7 + 1 * X219 + 1, s9 >= 0, s9 <= 1 * s8 + 1 * X2 + 1, z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 76 + 150·z' }→ s2 :|: s2 >= 0, s2 <= inf, z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 76 + 150·z'' }→ s3 :|: s3 >= 0, s3 <= inf', z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {if}
Previous analysis results are:

(61) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(62) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 79 + 150·X45 }→ s12 :|: s10 >= 0, s10 <= inf2, s11 >= 0, s11 <= 1 * s10 + 1, s12 >= 0, s12 <= 1 * s11 + 1 * X2 + 1, X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 79 + 150·X122 }→ s15 :|: s13 >= 0, s13 <= inf3, s14 >= 0, s14 <= 1 * s13 + 1 * X221 + 1, s15 >= 0, s15 <= 1 * s14 + 1, X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 152 + 150·X1 + 150·X2 }→ s18 :|: s16 >= 0, s16 <= inf4, s17 >= 0, s17 <= inf5, s18 >= 0, s18 <= 1 * s16 + 1 * s17 + 1, X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 154 + 150·X121 + 150·X220 }→ s22 :|: s19 >= 0, s19 <= inf6, s20 >= 0, s20 <= inf7, s21 >= 0, s21 <= 1 * s19 + 1 * s20 + 1, s22 >= 0, s22 <= 1 * s21 + 1, z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 154 + 150·X119 + 150·X218 }→ s26 :|: s23 >= 0, s23 <= inf8, s24 >= 0, s24 <= inf9, s25 >= 0, s25 <= 1 * s23 + 1 * s24 + 1, s26 >= 0, s26 <= 1 * s25 + 1 * X2 + 1, z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ -221 + 150·z }→ s29 :|: s27 >= 0, s27 <= inf10, s28 >= 0, s28 <= 1 * s27 + 1, s29 >= 0, s29 <= 1 * s28 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s32 :|: s30 >= 0, s30 <= inf11, s31 >= 0, s31 <= 1 * s30 + 1, s32 >= 0, s32 <= 1 * s31 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s35 :|: s33 >= 0, s33 <= inf12, s34 >= 0, s34 <= 1 * s33 + 1, s35 >= 0, s35 <= 1 * s34 + 1, z - 2 >= 0
activate(z) -{ 79 + 150·X116 }→ s38 :|: s36 >= 0, s36 <= inf13, s37 >= 0, s37 <= 1 * s36 + 1 * X215 + 1, s38 >= 0, s38 <= 1 * s37 + 1, z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 79 + 150·X43 }→ s41 :|: s39 >= 0, s39 <= inf14, s40 >= 0, s40 <= 1 * s39 + 1, s41 >= 0, s41 <= 1 * s40 + 1 * X2 + 1, z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 154 + 150·X115 + 150·X214 }→ s45 :|: s42 >= 0, s42 <= inf15, s43 >= 0, s43 <= inf16, s44 >= 0, s44 <= 1 * s42 + 1 * s43 + 1, s45 >= 0, s45 <= 1 * s44 + 1, z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ -219 + 150·z }→ s48 :|: s46 >= 0, s46 <= inf17, s47 >= 0, s47 <= 2 * s46 + 3, s48 >= 0, s48 <= 2 * s47 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s51 :|: s49 >= 0, s49 <= inf18, s50 >= 0, s50 <= 1 * s49 + 1, s51 >= 0, s51 <= 2 * s50 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s54 :|: s52 >= 0, s52 <= inf19, s53 >= 0, s53 <= 2 * s52 + 3, s54 >= 0, s54 <= 1 * s53 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X118 }→ s57 :|: s55 >= 0, s55 <= inf20, s56 >= 0, s56 <= 1 * s55 + 1 * X217 + 1, s57 >= 0, s57 <= 2 * s56 + 3, X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ -221 + 150·z }→ s6 :|: s4 >= 0, s4 <= inf'', s5 >= 0, s5 <= 1 * s4 + 1, s6 >= 0, s6 <= 1 * s5 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X44 }→ s60 :|: s58 >= 0, s58 <= inf21, s59 >= 0, s59 <= 2 * s58 + 3, s60 >= 0, s60 <= 1 * s59 + 1 * X2 + 1, z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 155 + 150·X117 + 150·X216 }→ s64 :|: s61 >= 0, s61 <= inf22, s62 >= 0, s62 <= inf23, s63 >= 0, s63 <= 1 * s61 + 1 * s62 + 1, s64 >= 0, s64 <= 2 * s63 + 3, X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ -220 + 150·z }→ s67 :|: s65 >= 0, s65 <= inf24, s66 >= 0, s66 <= 2 * s65 + 3, s67 >= 0, s67 <= 1 * s66 + 1, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s70 :|: s68 >= 0, s68 <= inf25, s69 >= 0, s69 <= 1 * s68 + 1, s70 >= 0, s70 <= 2 * s69 + 3, z - 2 >= 0
activate(z) -{ 79 + 150·X120 }→ s9 :|: s7 >= 0, s7 <= inf1, s8 >= 0, s8 <= 1 * s7 + 1 * X219 + 1, s9 >= 0, s9 <= 1 * s8 + 1 * X2 + 1, z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 76 + 150·z' }→ s2 :|: s2 >= 0, s2 <= inf, z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 76 + 150·z'' }→ s3 :|: s3 >= 0, s3 <= inf', z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {if}
Previous analysis results are:

(63) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: if
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

(64) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 79 + 150·X45 }→ s12 :|: s10 >= 0, s10 <= inf2, s11 >= 0, s11 <= 1 * s10 + 1, s12 >= 0, s12 <= 1 * s11 + 1 * X2 + 1, X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 79 + 150·X122 }→ s15 :|: s13 >= 0, s13 <= inf3, s14 >= 0, s14 <= 1 * s13 + 1 * X221 + 1, s15 >= 0, s15 <= 1 * s14 + 1, X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 152 + 150·X1 + 150·X2 }→ s18 :|: s16 >= 0, s16 <= inf4, s17 >= 0, s17 <= inf5, s18 >= 0, s18 <= 1 * s16 + 1 * s17 + 1, X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 154 + 150·X121 + 150·X220 }→ s22 :|: s19 >= 0, s19 <= inf6, s20 >= 0, s20 <= inf7, s21 >= 0, s21 <= 1 * s19 + 1 * s20 + 1, s22 >= 0, s22 <= 1 * s21 + 1, z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 154 + 150·X119 + 150·X218 }→ s26 :|: s23 >= 0, s23 <= inf8, s24 >= 0, s24 <= inf9, s25 >= 0, s25 <= 1 * s23 + 1 * s24 + 1, s26 >= 0, s26 <= 1 * s25 + 1 * X2 + 1, z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ -221 + 150·z }→ s29 :|: s27 >= 0, s27 <= inf10, s28 >= 0, s28 <= 1 * s27 + 1, s29 >= 0, s29 <= 1 * s28 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s32 :|: s30 >= 0, s30 <= inf11, s31 >= 0, s31 <= 1 * s30 + 1, s32 >= 0, s32 <= 1 * s31 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s35 :|: s33 >= 0, s33 <= inf12, s34 >= 0, s34 <= 1 * s33 + 1, s35 >= 0, s35 <= 1 * s34 + 1, z - 2 >= 0
activate(z) -{ 79 + 150·X116 }→ s38 :|: s36 >= 0, s36 <= inf13, s37 >= 0, s37 <= 1 * s36 + 1 * X215 + 1, s38 >= 0, s38 <= 1 * s37 + 1, z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 79 + 150·X43 }→ s41 :|: s39 >= 0, s39 <= inf14, s40 >= 0, s40 <= 1 * s39 + 1, s41 >= 0, s41 <= 1 * s40 + 1 * X2 + 1, z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 154 + 150·X115 + 150·X214 }→ s45 :|: s42 >= 0, s42 <= inf15, s43 >= 0, s43 <= inf16, s44 >= 0, s44 <= 1 * s42 + 1 * s43 + 1, s45 >= 0, s45 <= 1 * s44 + 1, z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ -219 + 150·z }→ s48 :|: s46 >= 0, s46 <= inf17, s47 >= 0, s47 <= 2 * s46 + 3, s48 >= 0, s48 <= 2 * s47 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s51 :|: s49 >= 0, s49 <= inf18, s50 >= 0, s50 <= 1 * s49 + 1, s51 >= 0, s51 <= 2 * s50 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s54 :|: s52 >= 0, s52 <= inf19, s53 >= 0, s53 <= 2 * s52 + 3, s54 >= 0, s54 <= 1 * s53 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X118 }→ s57 :|: s55 >= 0, s55 <= inf20, s56 >= 0, s56 <= 1 * s55 + 1 * X217 + 1, s57 >= 0, s57 <= 2 * s56 + 3, X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ -221 + 150·z }→ s6 :|: s4 >= 0, s4 <= inf'', s5 >= 0, s5 <= 1 * s4 + 1, s6 >= 0, s6 <= 1 * s5 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X44 }→ s60 :|: s58 >= 0, s58 <= inf21, s59 >= 0, s59 <= 2 * s58 + 3, s60 >= 0, s60 <= 1 * s59 + 1 * X2 + 1, z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 155 + 150·X117 + 150·X216 }→ s64 :|: s61 >= 0, s61 <= inf22, s62 >= 0, s62 <= inf23, s63 >= 0, s63 <= 1 * s61 + 1 * s62 + 1, s64 >= 0, s64 <= 2 * s63 + 3, X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ -220 + 150·z }→ s67 :|: s65 >= 0, s65 <= inf24, s66 >= 0, s66 <= 2 * s65 + 3, s67 >= 0, s67 <= 1 * s66 + 1, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s70 :|: s68 >= 0, s68 <= inf25, s69 >= 0, s69 <= 1 * s68 + 1, s70 >= 0, s70 <= 2 * s69 + 3, z - 2 >= 0
activate(z) -{ 79 + 150·X120 }→ s9 :|: s7 >= 0, s7 <= inf1, s8 >= 0, s8 <= 1 * s7 + 1 * X219 + 1, s9 >= 0, s9 <= 1 * s8 + 1 * X2 + 1, z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 76 + 150·z' }→ s2 :|: s2 >= 0, s2 <= inf, z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 76 + 150·z'' }→ s3 :|: s3 >= 0, s3 <= inf', z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {if}
Previous analysis results are:

(65) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: if
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 76 + 150·z' + 150·z''

(66) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 79 + 150·X45 }→ s12 :|: s10 >= 0, s10 <= inf2, s11 >= 0, s11 <= 1 * s10 + 1, s12 >= 0, s12 <= 1 * s11 + 1 * X2 + 1, X45 >= 0, X2 >= 0, z = 1 + (1 + X45) + X2
activate(z) -{ 79 + 150·X122 }→ s15 :|: s13 >= 0, s13 <= inf3, s14 >= 0, s14 <= 1 * s13 + 1 * X221 + 1, s15 >= 0, s15 <= 1 * s14 + 1, X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 152 + 150·X1 + 150·X2 }→ s18 :|: s16 >= 0, s16 <= inf4, s17 >= 0, s17 <= inf5, s18 >= 0, s18 <= 1 * s16 + 1 * s17 + 1, X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 154 + 150·X121 + 150·X220 }→ s22 :|: s19 >= 0, s19 <= inf6, s20 >= 0, s20 <= inf7, s21 >= 0, s21 <= 1 * s19 + 1 * s20 + 1, s22 >= 0, s22 <= 1 * s21 + 1, z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 154 + 150·X119 + 150·X218 }→ s26 :|: s23 >= 0, s23 <= inf8, s24 >= 0, s24 <= inf9, s25 >= 0, s25 <= 1 * s23 + 1 * s24 + 1, s26 >= 0, s26 <= 1 * s25 + 1 * X2 + 1, z = 1 + (1 + X119 + X218) + X2, X2 >= 0, X119 >= 0, X218 >= 0
activate(z) -{ -221 + 150·z }→ s29 :|: s27 >= 0, s27 <= inf10, s28 >= 0, s28 <= 1 * s27 + 1, s29 >= 0, s29 <= 1 * s28 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s32 :|: s30 >= 0, s30 <= inf11, s31 >= 0, s31 <= 1 * s30 + 1, s32 >= 0, s32 <= 1 * s31 + 1, z - 2 >= 0
activate(z) -{ -221 + 150·z }→ s35 :|: s33 >= 0, s33 <= inf12, s34 >= 0, s34 <= 1 * s33 + 1, s35 >= 0, s35 <= 1 * s34 + 1, z - 2 >= 0
activate(z) -{ 79 + 150·X116 }→ s38 :|: s36 >= 0, s36 <= inf13, s37 >= 0, s37 <= 1 * s36 + 1 * X215 + 1, s38 >= 0, s38 <= 1 * s37 + 1, z = 1 + (1 + X116 + X215), X116 >= 0, X215 >= 0
activate(z) -{ 79 + 150·X43 }→ s41 :|: s39 >= 0, s39 <= inf14, s40 >= 0, s40 <= 1 * s39 + 1, s41 >= 0, s41 <= 1 * s40 + 1 * X2 + 1, z = 1 + (1 + X43) + X2, X43 >= 0, X2 >= 0
activate(z) -{ 154 + 150·X115 + 150·X214 }→ s45 :|: s42 >= 0, s42 <= inf15, s43 >= 0, s43 <= inf16, s44 >= 0, s44 <= 1 * s42 + 1 * s43 + 1, s45 >= 0, s45 <= 1 * s44 + 1, z = 1 + (1 + X115 + X214), X214 >= 0, X115 >= 0
activate(z) -{ -219 + 150·z }→ s48 :|: s46 >= 0, s46 <= inf17, s47 >= 0, s47 <= 2 * s46 + 3, s48 >= 0, s48 <= 2 * s47 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s51 :|: s49 >= 0, s49 <= inf18, s50 >= 0, s50 <= 1 * s49 + 1, s51 >= 0, s51 <= 2 * s50 + 3, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s54 :|: s52 >= 0, s52 <= inf19, s53 >= 0, s53 <= 2 * s52 + 3, s54 >= 0, s54 <= 1 * s53 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X118 }→ s57 :|: s55 >= 0, s55 <= inf20, s56 >= 0, s56 <= 1 * s55 + 1 * X217 + 1, s57 >= 0, s57 <= 2 * s56 + 3, X118 >= 0, z = 1 + (1 + X118 + X217), X217 >= 0
activate(z) -{ -221 + 150·z }→ s6 :|: s4 >= 0, s4 <= inf'', s5 >= 0, s5 <= 1 * s4 + 1, s6 >= 0, s6 <= 1 * s5 + 1, z - 2 >= 0
activate(z) -{ 80 + 150·X44 }→ s60 :|: s58 >= 0, s58 <= inf21, s59 >= 0, s59 <= 2 * s58 + 3, s60 >= 0, s60 <= 1 * s59 + 1 * X2 + 1, z = 1 + (1 + X44) + X2, X2 >= 0, X44 >= 0
activate(z) -{ 155 + 150·X117 + 150·X216 }→ s64 :|: s61 >= 0, s61 <= inf22, s62 >= 0, s62 <= inf23, s63 >= 0, s63 <= 1 * s61 + 1 * s62 + 1, s64 >= 0, s64 <= 2 * s63 + 3, X216 >= 0, X117 >= 0, z = 1 + (1 + X117 + X216)
activate(z) -{ -220 + 150·z }→ s67 :|: s65 >= 0, s65 <= inf24, s66 >= 0, s66 <= 2 * s65 + 3, s67 >= 0, s67 <= 1 * s66 + 1, z - 2 >= 0
activate(z) -{ -220 + 150·z }→ s70 :|: s68 >= 0, s68 <= inf25, s69 >= 0, s69 <= 1 * s68 + 1, s70 >= 0, s70 <= 2 * s69 + 3, z - 2 >= 0
activate(z) -{ 79 + 150·X120 }→ s9 :|: s7 >= 0, s7 <= inf1, s8 >= 0, s8 <= 1 * s7 + 1 * X219 + 1, s9 >= 0, s9 <= 1 * s8 + 1 * X2 + 1, z = 1 + (1 + X120 + X219) + X2, X120 >= 0, X219 >= 0, X2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
filter(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
if(z, z', z'') -{ 76 + 150·z' }→ s2 :|: s2 >= 0, s2 <= inf, z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 76 + 150·z'' }→ s3 :|: s3 >= 0, s3 <= inf', z'' >= 0, z' >= 0, z = 0
primes -{ 6 }→ s'' :|: s'' >= 0, s'' <= 1 * s' + 1, s' >= 0, s' <= 1 * X' + 1 * (1 + (1 + X')) + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
primes -{ 5 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + X') + 1, X >= 0, 1 + 0 = X, X' >= 0, 1 + X = X'
s(z) -{ 1 }→ 1 + z :|: z >= 0
sieve(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed:
Previous analysis results are:

(67) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(0) Obligation:

(1) DependencyGraphProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CompletionProof (UPPER BOUND(ID) transformation)

(10) Obligation:

(11) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

(14) Obligation:

(15) InliningProof (UPPER BOUND(ID) transformation)

(16) Obligation:

(17) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

(20) Obligation:

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(22) Obligation:

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(24) Obligation:

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

(26) Obligation:

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(28) Obligation:

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(30) Obligation:

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

(32) Obligation:

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(34) Obligation:

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(36) Obligation:

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

(38) Obligation:

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(40) Obligation:

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(42) Obligation:

(43) ResultPropagationProof (UPPER BOUND(ID) transformation)

(44) Obligation:

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(46) Obligation:

(47) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(48) Obligation:

(49) ResultPropagationProof (UPPER BOUND(ID) transformation)

(50) Obligation:

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(52) Obligation:

(53) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(54) Obligation:

(55) ResultPropagationProof (UPPER BOUND(ID) transformation)

(56) Obligation:

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(58) Obligation:

(59) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(60) Obligation:

(61) ResultPropagationProof (UPPER BOUND(ID) transformation)

(62) Obligation:

(63) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(64) Obligation:

(65) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(66) Obligation:

(67) FinalProof (EQUIVALENT transformation)

(68) BOUNDS(1, n^1)