Runtime Complexity (innermost) proof of /tmp/tmpLnHEDV/Ex5_DLMMU04

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), 4 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), 3 ms)

↳12 CpxTypedWeightedCompleteTrs

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

↳14 CpxRNTS

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

↳16 CpxRNTS

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

↳18 CpxRNTS

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

↳20 CpxRNTS

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

↳22 CpxRNTS

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

↳24 CpxRNTS

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

↳26 CpxRNTS

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

↳28 CpxRNTS

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

↳30 CpxRNTS

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

↳32 CpxRNTS

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

↳34 CpxRNTS

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

↳36 CpxRNTS

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

↳38 CpxRNTS

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

↳40 CpxRNTS

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

↳42 CpxRNTS

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

↳44 CpxRNTS

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

↳46 CpxRNTS

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

↳48 CpxRNTS

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

↳50 CpxRNTS

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

↳52 CpxRNTS

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

↳54 CpxRNTS

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

↳56 CpxRNTS

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

↳58 CpxRNTS

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

↳60 CpxRNTS

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

↳62 CpxRNTS

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

↳64 CpxRNTS

↳65 IntTrsBoundProof (UPPER BOUND(ID), 1039 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:

pairNs → cons(0, n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(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:
tail(cons(X, XS)) → activate(XS)

(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:

zip(nil, XS) → nil
zip(X, nil) → nil
repItems(X) → n__repItems(X)
activate(n__repItems(X)) → repItems(activate(X))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
activate(X) → X
activate(n__incr(X)) → incr(activate(X))
cons(X1, X2) → n__cons(X1, X2)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
incr(X) → n__incr(X)
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
repItems(nil) → nil
take(0, XS) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__oddNs) → oddNs
pairNs → cons(0, n__incr(n__oddNs))
oddNs → incr(pairNs)
zip(X1, X2) → n__zip(X1, X2)
activate(n__cons(X1, X2)) → cons(activate(X1), X2)

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:

zip(nil, XS) → nil [1]
zip(X, nil) → nil [1]
repItems(X) → n__repItems(X) [1]
activate(n__repItems(X)) → repItems(activate(X)) [1]
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS))) [1]
activate(X) → X [1]
activate(n__incr(X)) → incr(activate(X)) [1]
cons(X1, X2) → n__cons(X1, X2) [1]
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS))) [1]
oddNs → n__oddNs [1]
take(X1, X2) → n__take(X1, X2) [1]
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS)))) [1]
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS))) [1]
incr(X) → n__incr(X) [1]
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2)) [1]
repItems(nil) → nil [1]
take(0, XS) → nil [1]
activate(n__take(X1, X2)) → take(activate(X1), activate(X2)) [1]
activate(n__oddNs) → oddNs [1]
pairNs → cons(0, n__incr(n__oddNs)) [1]
oddNs → incr(pairNs) [1]
zip(X1, X2) → n__zip(X1, X2) [1]
activate(n__cons(X1, X2)) → cons(activate(X1), X2) [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:

take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS))) [1]
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS))) [1]
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS)))) [1]
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS))) [1]

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

cons(X1, X2) → n__cons(X1, X2) [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:

zip(nil, XS) → nil [1]
zip(X, nil) → nil [1]
repItems(X) → n__repItems(X) [1]
activate(n__repItems(X)) → repItems(activate(X)) [1]
activate(X) → X [1]
activate(n__incr(X)) → incr(activate(X)) [1]
cons(X1, X2) → n__cons(X1, X2) [1]
oddNs → n__oddNs [1]
take(X1, X2) → n__take(X1, X2) [1]
incr(X) → n__incr(X) [1]
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2)) [1]
repItems(nil) → nil [1]
take(0, XS) → nil [1]
activate(n__take(X1, X2)) → take(activate(X1), activate(X2)) [1]
activate(n__oddNs) → oddNs [1]
pairNs → cons(0, n__incr(n__oddNs)) [1]
oddNs → incr(pairNs) [1]
zip(X1, X2) → n__zip(X1, X2) [1]
activate(n__cons(X1, X2)) → cons(activate(X1), X2) [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:

zip(nil, XS) → nil [1]
zip(X, nil) → nil [1]
repItems(X) → n__repItems(X) [1]
activate(n__repItems(X)) → repItems(activate(X)) [1]
activate(X) → X [1]
activate(n__incr(X)) → incr(activate(X)) [1]
cons(X1, X2) → n__cons(X1, X2) [1]
oddNs → n__oddNs [1]
take(X1, X2) → n__take(X1, X2) [1]
incr(X) → n__incr(X) [1]
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2)) [1]
repItems(nil) → nil [1]
take(0, XS) → nil [1]
activate(n__take(X1, X2)) → take(activate(X1), activate(X2)) [1]
activate(n__oddNs) → oddNs [1]
pairNs → cons(0, n__incr(n__oddNs)) [1]
oddNs → incr(pairNs) [1]
zip(X1, X2) → n__zip(X1, X2) [1]
activate(n__cons(X1, X2)) → cons(activate(X1), X2) [1]

The TRS has the following type information:

zip :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
nil :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
repItems :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
n__repItems :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
activate :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
n__incr :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
incr :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
cons :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
n__cons :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
oddNs :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
n__oddNs :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
take :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
n__take :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
n__zip :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0 → nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
0 :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0
pairNs :: nil:n__repItems:n__incr:n__cons:n__oddNs:n__take:n__zip:0

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:
none

(c) The following functions are completely defined:

activate
pairNs
repItems
incr
zip
take
oddNs
cons

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:

zip(nil, XS) → nil [1]
zip(X, nil) → nil [1]
repItems(X) → n__repItems(X) [1]
activate(n__repItems(X)) → repItems(activate(X)) [1]
activate(X) → X [1]
activate(n__incr(X)) → incr(activate(X)) [1]
cons(X1, X2) → n__cons(X1, X2) [1]
oddNs → n__oddNs [1]
take(X1, X2) → n__take(X1, X2) [1]
incr(X) → n__incr(X) [1]
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2)) [1]
repItems(nil) → nil [1]
take(0, XS) → nil [1]
activate(n__take(X1, X2)) → take(activate(X1), activate(X2)) [1]
activate(n__oddNs) → oddNs [1]
pairNs → cons(0, n__incr(n__oddNs)) [1]
oddNs → incr(pairNs) [1]
zip(X1, X2) → n__zip(X1, X2) [1]
activate(n__cons(X1, X2)) → cons(activate(X1), X2) [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:

zip(nil, XS) → nil [1]
zip(X, nil) → nil [1]
repItems(X) → n__repItems(X) [1]
activate(n__repItems(n__repItems(X'))) → repItems(repItems(activate(X'))) [2]
activate(n__repItems(X)) → repItems(X) [2]
activate(n__repItems(n__incr(X''))) → repItems(incr(activate(X''))) [2]
activate(n__repItems(n__zip(X1', X2'))) → repItems(zip(activate(X1'), activate(X2'))) [2]
activate(n__repItems(n__take(X1'', X2''))) → repItems(take(activate(X1''), activate(X2''))) [2]
activate(n__repItems(n__oddNs)) → repItems(oddNs) [2]
activate(n__repItems(n__cons(X11, X21))) → repItems(cons(activate(X11), X21)) [2]
activate(X) → X [1]
activate(n__incr(n__repItems(X3))) → incr(repItems(activate(X3))) [2]
activate(n__incr(X)) → incr(X) [2]
activate(n__incr(n__incr(X4))) → incr(incr(activate(X4))) [2]
activate(n__incr(n__zip(X12, X22))) → incr(zip(activate(X12), activate(X22))) [2]
activate(n__incr(n__take(X13, X23))) → incr(take(activate(X13), activate(X23))) [2]
activate(n__incr(n__oddNs)) → incr(oddNs) [2]
activate(n__incr(n__cons(X14, X24))) → incr(cons(activate(X14), X24)) [2]
cons(X1, X2) → n__cons(X1, X2) [1]
oddNs → n__oddNs [1]
take(X1, X2) → n__take(X1, X2) [1]
incr(X) → n__incr(X) [1]
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2)) [1]
repItems(nil) → nil [1]
take(0, XS) → nil [1]
activate(n__take(X1, X2)) → take(activate(X1), activate(X2)) [1]
activate(n__oddNs) → oddNs [1]
pairNs → cons(0, n__incr(n__oddNs)) [1]
oddNs → incr(cons(0, n__incr(n__oddNs))) [2]
zip(X1, X2) → n__zip(X1, X2) [1]
activate(n__cons(n__repItems(X55), X2)) → cons(repItems(activate(X55)), X2) [2]
activate(n__cons(X1, X2)) → cons(X1, X2) [2]
activate(n__cons(n__incr(X56), X2)) → cons(incr(activate(X56)), X2) [2]
activate(n__cons(n__zip(X153, X253), X2)) → cons(zip(activate(X153), activate(X253)), X2) [2]
activate(n__cons(n__take(X154, X254), X2)) → cons(take(activate(X154), activate(X254)), X2) [2]
activate(n__cons(n__oddNs, X2)) → cons(oddNs, X2) [2]
activate(n__cons(n__cons(X155, X255), X2)) → cons(cons(activate(X155), X255), X2) [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:

nil => 2
n__oddNs => 1
0 => 0

(14) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ repItems(oddNs) :|: z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 1 }→ oddNs :|: z = 1
activate(z) -{ 2 }→ incr(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(X3))) :|: z = 1 + (1 + X3), X3 >= 0
activate(z) -{ 2 }→ incr(oddNs) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(X4))) :|: z = 1 + (1 + X4), X4 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(oddNs, X2) :|: z = 1 + 1 + X2, X2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
incr(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
oddNs -{ 2 }→ incr(cons(0, 1 + 1)) :|:
oddNs -{ 1 }→ 1 :|:
pairNs -{ 1 }→ cons(0, 1 + 1) :|:
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
take(z, z') -{ 1 }→ 2 :|: z' = XS, z = 0, XS >= 0
take(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' = XS, XS >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, X >= 0, z = X
zip(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2

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

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

zip(z, z') -{ 1 }→ 2 :|: z = 2, z' = XS, XS >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, X >= 0, z = X
zip(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
repItems(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
repItems(z) -{ 1 }→ 2 :|: z = 2
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
take(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
take(z, z') -{ 1 }→ 2 :|: z' = XS, z = 0, XS >= 0
incr(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
oddNs -{ 1 }→ 1 :|:
oddNs -{ 2 }→ incr(cons(0, 1 + 1)) :|:

(16) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 4 }→ repItems(incr(cons(0, 1 + 1))) :|: z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(X3))) :|: z = 1 + (1 + X3), X3 >= 0
activate(z) -{ 4 }→ incr(incr(cons(0, 1 + 1))) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(X4))) :|: z = 1 + (1 + X4), X4 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(cons(0, 1 + 1)) :|: z = 1
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 4 }→ cons(incr(cons(0, 1 + 1)), X2) :|: z = 1 + 1 + X2, X2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ cons(1, X2) :|: z = 1 + 1 + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z = 1 + X, X >= 0, X = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
take(z, z') -{ 1 }→ 2 :|: z' = XS, z = 0, XS >= 0
take(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' = XS, XS >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, X >= 0, z = X
zip(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2

(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) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 4 }→ repItems(incr(cons(0, 1 + 1))) :|: z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 4 }→ incr(incr(cons(0, 1 + 1))) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(cons(0, 1 + 1)) :|: z = 1
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 4 }→ cons(incr(cons(0, 1 + 1)), z - 2) :|: z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ cons(1, z - 2) :|: z - 2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

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

Found the following analysis order by SCC decomposition:

{ cons }
{ take }
{ zip }
{ incr }
{ repItems }
{ pairNs }
{ oddNs }
{ activate }

(20) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 4 }→ repItems(incr(cons(0, 1 + 1))) :|: z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 4 }→ incr(incr(cons(0, 1 + 1))) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(cons(0, 1 + 1)) :|: z = 1
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 4 }→ cons(incr(cons(0, 1 + 1)), z - 2) :|: z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ cons(1, z - 2) :|: z - 2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {cons}, {take}, {zip}, {incr}, {repItems}, {pairNs}, {oddNs}, {activate}

(21) 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'

(22) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 4 }→ repItems(incr(cons(0, 1 + 1))) :|: z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 4 }→ incr(incr(cons(0, 1 + 1))) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(cons(0, 1 + 1)) :|: z = 1
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 4 }→ cons(incr(cons(0, 1 + 1)), z - 2) :|: z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ cons(1, z - 2) :|: z - 2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {cons}, {take}, {zip}, {incr}, {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

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

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

(24) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 4 }→ repItems(incr(cons(0, 1 + 1))) :|: z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 4 }→ incr(incr(cons(0, 1 + 1))) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(cons(0, 1 + 1)) :|: z = 1
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 4 }→ cons(incr(cons(0, 1 + 1)), z - 2) :|: z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ cons(1, z - 2) :|: z - 2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {take}, {zip}, {incr}, {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

cons: runtime: O(1) [1], size: O(n¹) [1 + z + 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) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ repItems(incr(s')) :|: s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 4 }→ incr(s) :|: s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ incr(incr(s2)) :|: s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 5 }→ cons(incr(s1), z - 2) :|: s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {take}, {zip}, {incr}, {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

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

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

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

(28) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ repItems(incr(s')) :|: s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 4 }→ incr(s) :|: s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ incr(incr(s2)) :|: s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 5 }→ cons(incr(s1), z - 2) :|: s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {take}, {zip}, {incr}, {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

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

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

Computed RUNTIME bound using CoFloCo for: take
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) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ repItems(incr(s')) :|: s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 4 }→ incr(s) :|: s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ incr(incr(s2)) :|: s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 5 }→ cons(incr(s1), z - 2) :|: s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {zip}, {incr}, {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
take: runtime: O(1) [1], size: O(n¹) [2 + 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 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ repItems(incr(s')) :|: s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 4 }→ incr(s) :|: s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ incr(incr(s2)) :|: s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 5 }→ cons(incr(s1), z - 2) :|: s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {zip}, {incr}, {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

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

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

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

(34) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ repItems(incr(s')) :|: s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 4 }→ incr(s) :|: s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ incr(incr(s2)) :|: s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 5 }→ cons(incr(s1), z - 2) :|: s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {zip}, {incr}, {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
take: runtime: O(1) [1], size: O(n¹) [2 + z + z']
zip: runtime: ?, size: O(n¹) [1 + z + z']

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

Computed RUNTIME bound using CoFloCo for: zip
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 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ repItems(incr(s')) :|: s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 4 }→ incr(s) :|: s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ incr(incr(s2)) :|: s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 5 }→ cons(incr(s1), z - 2) :|: s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {incr}, {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
take: runtime: O(1) [1], size: O(n¹) [2 + z + z']
zip: runtime: O(1) [1], size: O(n¹) [1 + z + 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 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ repItems(incr(s')) :|: s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 4 }→ incr(s) :|: s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ incr(incr(s2)) :|: s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 5 }→ cons(incr(s1), z - 2) :|: s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {incr}, {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
take: runtime: O(1) [1], size: O(n¹) [2 + z + z']
zip: runtime: O(1) [1], size: O(n¹) [1 + z + z']

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

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

(40) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ repItems(incr(s')) :|: s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 4 }→ incr(s) :|: s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ incr(incr(s2)) :|: s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 5 }→ cons(incr(s1), z - 2) :|: s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {incr}, {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
take: runtime: O(1) [1], size: O(n¹) [2 + z + z']
zip: runtime: O(1) [1], size: O(n¹) [1 + z + z']
incr: runtime: ?, size: O(n¹) [1 + z]

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

Computed RUNTIME bound using CoFloCo for: incr
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 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ repItems(incr(s')) :|: s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 4 }→ incr(s) :|: s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 5 }→ incr(incr(s2)) :|: s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 3 }→ incr(1) :|: z = 1 + 1
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 5 }→ cons(incr(s1), z - 2) :|: s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
take: runtime: O(1) [1], size: O(n¹) [2 + z + z']
zip: runtime: O(1) [1], size: O(n¹) [1 + z + z']
incr: runtime: O(1) [1], size: O(n¹) [1 + 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 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 6 }→ repItems(s4) :|: s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
take: runtime: O(1) [1], size: O(n¹) [2 + z + z']
zip: runtime: O(1) [1], size: O(n¹) [1 + z + z']
incr: runtime: O(1) [1], size: O(n¹) [1 + z]

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

Computed SIZE bound using KoAT for: repItems
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 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 6 }→ repItems(s4) :|: s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {repItems}, {pairNs}, {oddNs}, {activate}
Previous analysis results are:

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

Computed RUNTIME bound using CoFloCo for: repItems
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 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 6 }→ repItems(s4) :|: s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 3 }→ repItems(1) :|: z = 1 + 1
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {pairNs}, {oddNs}, {activate}
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 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s10 :|: s10 >= 0, s10 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s11 :|: s11 >= 0, s11 <= 1 * s4 + 1, s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {pairNs}, {oddNs}, {activate}
Previous analysis results are:

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

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

(52) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s10 :|: s10 >= 0, s10 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s11 :|: s11 >= 0, s11 <= 1 * s4 + 1, s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {pairNs}, {oddNs}, {activate}
Previous analysis results are:

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

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

(54) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s10 :|: s10 >= 0, s10 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s11 :|: s11 >= 0, s11 <= 1 * s4 + 1, s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

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

cons: runtime: O(1) [1], size: O(n¹) [1 + z + z']
take: runtime: O(1) [1], size: O(n¹) [2 + z + z']
zip: runtime: O(1) [1], size: O(n¹) [1 + z + z']
incr: runtime: O(1) [1], size: O(n¹) [1 + z]
repItems: runtime: O(1) [1], size: O(n¹) [1 + z]
pairNs: runtime: O(1) [2], size: O(1) [3]

(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 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s10 :|: s10 >= 0, s10 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s11 :|: s11 >= 0, s11 <= 1 * s4 + 1, s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

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

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

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

(58) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s10 :|: s10 >= 0, s10 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s11 :|: s11 >= 0, s11 <= 1 * s4 + 1, s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

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

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

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

(60) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s10 :|: s10 >= 0, s10 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s11 :|: s11 >= 0, s11 <= 1 * s4 + 1, s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

Function symbols to be analyzed: {activate}
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 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s10 :|: s10 >= 0, s10 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s11 :|: s11 >= 0, s11 <= 1 * s4 + 1, s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

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

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

Computed SIZE bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 56 + 126·z + 28·z²

(64) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s10 :|: s10 >= 0, s10 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s11 :|: s11 >= 0, s11 <= 1 * s4 + 1, s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0

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

(65) 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: 100 + 200·z

(66) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s'' :|: s'' >= 0, s'' <= 1 * 1 + 1 * (z - 2) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s10 :|: s10 >= 0, s10 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s11 :|: s11 >= 0, s11 <= 1 * s4 + 1, s4 >= 0, s4 <= 1 * s' + 1, s' >= 0, s' <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 5 }→ s3 :|: s3 >= 0, s3 <= 1 * s + 1, s >= 0, s <= 1 * 0 + 1 * (1 + 1) + 1, z = 1
activate(z) -{ 7 }→ s6 :|: s5 >= 0, s5 <= 1 * s1 + 1, s6 >= 0, s6 <= 1 * s5 + 1 * (z - 2) + 1, s1 >= 0, s1 <= 1 * 0 + 1 * (1 + 1) + 1, z - 2 >= 0
activate(z) -{ 4 }→ s7 :|: s7 >= 0, s7 <= 1 * 1 + 1, z = 1 + 1
activate(z) -{ 7 }→ s9 :|: s8 >= 0, s8 <= 1 * s2 + 1, s9 >= 0, s9 <= 1 * s8 + 1, s2 >= 0, s2 <= 1 * 0 + 1 * (1 + 1) + 1, z = 1 + 1
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ zip(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ take(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ repItems(zip(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ repItems(take(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ repItems(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ repItems(cons(activate(X11), X21)) :|: z = 1 + (1 + X11 + X21), X11 >= 0, X21 >= 0
activate(z) -{ 2 }→ incr(zip(activate(X12), activate(X22))) :|: X12 >= 0, X22 >= 0, z = 1 + (1 + X12 + X22)
activate(z) -{ 2 }→ incr(take(activate(X13), activate(X23))) :|: z = 1 + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 2 }→ incr(repItems(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(incr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ incr(cons(activate(X14), X24)) :|: z = 1 + (1 + X14 + X24), X14 >= 0, X24 >= 0
activate(z) -{ 2 }→ cons(zip(activate(X153), activate(X253)), X2) :|: z = 1 + (1 + X153 + X253) + X2, X253 >= 0, X153 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(take(activate(X154), activate(X254)), X2) :|: X154 >= 0, X254 >= 0, z = 1 + (1 + X154 + X254) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(repItems(activate(X55)), X2) :|: X2 >= 0, z = 1 + (1 + X55) + X2, X55 >= 0
activate(z) -{ 2 }→ cons(incr(activate(X56)), X2) :|: z = 1 + (1 + X56) + X2, X56 >= 0, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X155), X255), X2) :|: X255 >= 0, X155 >= 0, z = 1 + (1 + X155 + X255) + X2, X2 >= 0
activate(z) -{ 3 }→ 2 :|: z - 1 >= 0, z - 1 = 2
activate(z) -{ 2 }→ 1 :|: z = 1
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
incr(z) -{ 1 }→ 1 + z :|: z >= 0
oddNs -{ 1 }→ 1 :|:
oddNs -{ 4 }→ 1 + X :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2, X >= 0, 1 + X1 + X2 = X
pairNs -{ 2 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, 0 = X1, 1 + 1 = X2
repItems(z) -{ 1 }→ 2 :|: z = 2
repItems(z) -{ 1 }→ 1 + z :|: z >= 0
take(z, z') -{ 1 }→ 2 :|: z = 0, z' >= 0
take(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z = 2, z' >= 0
zip(z, z') -{ 1 }→ 2 :|: z' = 2, z >= 0
zip(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, 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)