WORST_CASE(?,O(n^3))
proof of input_v3L9h91xZb.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CdtProblem
(9) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) CpxRelTRS
(11) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CpxWeightedTrs
(13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxTypedWeightedTrs
(15) CompletionProof [UPPER BOUND(ID), 0 ms]
(16) CpxTypedWeightedCompleteTrs
(17) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
(18) CpxTypedWeightedCompleteTrs
(19) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(20) CpxRNTS
(21) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
(22) CpxRNTS
(23) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
(24) CpxRNTS
(25) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(26) CpxRNTS
(27) IntTrsBoundProof [UPPER BOUND(ID), 87 ms]
(28) CpxRNTS
(29) IntTrsBoundProof [UPPER BOUND(ID), 74 ms]
(30) CpxRNTS
(31) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(32) CpxRNTS
(33) IntTrsBoundProof [UPPER BOUND(ID), 189 ms]
(34) CpxRNTS
(35) IntTrsBoundProof [UPPER BOUND(ID), 73 ms]
(36) CpxRNTS
(37) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(38) CpxRNTS
(39) IntTrsBoundProof [UPPER BOUND(ID), 191 ms]
(40) CpxRNTS
(41) IntTrsBoundProof [UPPER BOUND(ID), 65 ms]
(42) CpxRNTS
(43) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(44) CpxRNTS
(45) IntTrsBoundProof [UPPER BOUND(ID), 349 ms]
(46) CpxRNTS
(47) IntTrsBoundProof [UPPER BOUND(ID), 94 ms]
(48) CpxRNTS
(49) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(50) CpxRNTS
(51) IntTrsBoundProof [UPPER BOUND(ID), 737 ms]
(52) CpxRNTS
(53) IntTrsBoundProof [UPPER BOUND(ID), 55 ms]
(54) CpxRNTS
(55) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(56) CpxRNTS
(57) IntTrsBoundProof [UPPER BOUND(ID), 939 ms]
(58) CpxRNTS
(59) IntTrsBoundProof [UPPER BOUND(ID), 234 ms]
(60) CpxRNTS
(61) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(62) CpxRNTS
(63) IntTrsBoundProof [UPPER BOUND(ID), 98 ms]
(64) CpxRNTS
(65) IntTrsBoundProof [UPPER BOUND(ID), 3 ms]
(66) CpxRNTS
(67) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(68) CpxRNTS
(69) IntTrsBoundProof [UPPER BOUND(ID), 492 ms]
(70) CpxRNTS
(71) IntTrsBoundProof [UPPER BOUND(ID), 3 ms]
(72) CpxRNTS
(73) FinalProof [FINISHED, 0 ms]
(74) BOUNDS(1, n^3)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

   terms(N) -> cons(recip(sqr(N)), n__terms(s(N)))
   sqr(0) -> 0
   sqr(s(X)) -> s(add(sqr(X), dbl(X)))
   dbl(0) -> 0
   dbl(s(X)) -> s(s(dbl(X)))
   add(0, X) -> X
   add(s(X), Y) -> s(add(X, Y))
   first(0, X) -> nil
   first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
   terms(X) -> n__terms(X)
   first(X1, X2) -> n__first(X1, X2)
   activate(n__terms(X)) -> terms(X)
   activate(n__first(X1, X2)) -> first(X1, X2)
   activate(X) -> X

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   terms(z0) -> cons(recip(sqr(z0)), n__terms(s(z0)))
   terms(z0) -> n__terms(z0)
   sqr(0) -> 0
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
   dbl(0) -> 0
   dbl(s(z0)) -> s(s(dbl(z0)))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   first(0, z0) -> nil
   first(s(z0), cons(z1, z2)) -> cons(z1, n__first(z0, activate(z2)))
   first(z0, z1) -> n__first(z0, z1)
   activate(n__terms(z0)) -> terms(z0)
   activate(n__first(z0, z1)) -> first(z0, z1)
   activate(z0) -> z0
Tuples:
   TERMS(z0) -> c(SQR(z0))
   TERMS(z0) -> c1
   SQR(0) -> c2
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(0) -> c5
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(0, z0) -> c7
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(0, z0) -> c9
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2))
   FIRST(z0, z1) -> c11
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0))
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1))
   ACTIVATE(z0) -> c14
S tuples:
   TERMS(z0) -> c(SQR(z0))
   TERMS(z0) -> c1
   SQR(0) -> c2
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(0) -> c5
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(0, z0) -> c7
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(0, z0) -> c9
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2))
   FIRST(z0, z1) -> c11
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0))
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1))
   ACTIVATE(z0) -> c14
K tuples:none
Defined Rule Symbols:   terms_1, sqr_1, dbl_1, add_2, first_2, activate_1

Defined Pair Symbols:   TERMS_1, SQR_1, DBL_1, ADD_2, FIRST_2, ACTIVATE_1

Compound Symbols:   c_1, c1, c2, c3_2, c4_2, c5, c6_1, c7, c8_1, c9, c10_1, c11, c12_1, c13_1, c14


----------------------------------------

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 7 trailing nodes:
   FIRST(z0, z1) -> c11
   FIRST(0, z0) -> c9
   ACTIVATE(z0) -> c14
   ADD(0, z0) -> c7
   TERMS(z0) -> c1
   SQR(0) -> c2
   DBL(0) -> c5

----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   terms(z0) -> cons(recip(sqr(z0)), n__terms(s(z0)))
   terms(z0) -> n__terms(z0)
   sqr(0) -> 0
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
   dbl(0) -> 0
   dbl(s(z0)) -> s(s(dbl(z0)))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   first(0, z0) -> nil
   first(s(z0), cons(z1, z2)) -> cons(z1, n__first(z0, activate(z2)))
   first(z0, z1) -> n__first(z0, z1)
   activate(n__terms(z0)) -> terms(z0)
   activate(n__first(z0, z1)) -> first(z0, z1)
   activate(z0) -> z0
Tuples:
   TERMS(z0) -> c(SQR(z0))
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2))
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0))
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1))
S tuples:
   TERMS(z0) -> c(SQR(z0))
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2))
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0))
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1))
K tuples:none
Defined Rule Symbols:   terms_1, sqr_1, dbl_1, add_2, first_2, activate_1

Defined Pair Symbols:   TERMS_1, SQR_1, DBL_1, ADD_2, FIRST_2, ACTIVATE_1

Compound Symbols:   c_1, c3_2, c4_2, c6_1, c8_1, c10_1, c12_1, c13_1


----------------------------------------

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
Split RHS of tuples not part of any SCC
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   terms(z0) -> cons(recip(sqr(z0)), n__terms(s(z0)))
   terms(z0) -> n__terms(z0)
   sqr(0) -> 0
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
   dbl(0) -> 0
   dbl(s(z0)) -> s(s(dbl(z0)))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   first(0, z0) -> nil
   first(s(z0), cons(z1, z2)) -> cons(z1, n__first(z0, activate(z2)))
   first(z0, z1) -> n__first(z0, z1)
   activate(n__terms(z0)) -> terms(z0)
   activate(n__first(z0, z1)) -> first(z0, z1)
   activate(z0) -> z0
Tuples:
   TERMS(z0) -> c(SQR(z0))
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2))
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0))
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1))
   SQR(s(z0)) -> c1(ADD(sqr(z0), dbl(z0)))
   SQR(s(z0)) -> c1(DBL(z0))
S tuples:
   TERMS(z0) -> c(SQR(z0))
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2))
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0))
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1))
   SQR(s(z0)) -> c1(ADD(sqr(z0), dbl(z0)))
   SQR(s(z0)) -> c1(DBL(z0))
K tuples:none
Defined Rule Symbols:   terms_1, sqr_1, dbl_1, add_2, first_2, activate_1

Defined Pair Symbols:   TERMS_1, SQR_1, DBL_1, ADD_2, FIRST_2, ACTIVATE_1

Compound Symbols:   c_1, c3_2, c6_1, c8_1, c10_1, c12_1, c13_1, c1_1


----------------------------------------

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   terms(z0) -> cons(recip(sqr(z0)), n__terms(s(z0)))
   terms(z0) -> n__terms(z0)
   first(0, z0) -> nil
   first(s(z0), cons(z1, z2)) -> cons(z1, n__first(z0, activate(z2)))
   first(z0, z1) -> n__first(z0, z1)
   activate(n__terms(z0)) -> terms(z0)
   activate(n__first(z0, z1)) -> first(z0, z1)
   activate(z0) -> z0

----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   sqr(0) -> 0
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   dbl(0) -> 0
   dbl(s(z0)) -> s(s(dbl(z0)))
Tuples:
   TERMS(z0) -> c(SQR(z0))
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2))
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0))
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1))
   SQR(s(z0)) -> c1(ADD(sqr(z0), dbl(z0)))
   SQR(s(z0)) -> c1(DBL(z0))
S tuples:
   TERMS(z0) -> c(SQR(z0))
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2))
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0))
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1))
   SQR(s(z0)) -> c1(ADD(sqr(z0), dbl(z0)))
   SQR(s(z0)) -> c1(DBL(z0))
K tuples:none
Defined Rule Symbols:   sqr_1, add_2, dbl_1

Defined Pair Symbols:   TERMS_1, SQR_1, DBL_1, ADD_2, FIRST_2, ACTIVATE_1

Compound Symbols:   c_1, c3_2, c6_1, c8_1, c10_1, c12_1, c13_1, c1_1


----------------------------------------

(9) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(10)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

   TERMS(z0) -> c(SQR(z0))
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2))
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0))
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1))
   SQR(s(z0)) -> c1(ADD(sqr(z0), dbl(z0)))
   SQR(s(z0)) -> c1(DBL(z0))

The (relative) TRS S consists of the following rules:

   sqr(0) -> 0
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   dbl(0) -> 0
   dbl(s(z0)) -> s(s(dbl(z0)))

Rewrite Strategy: INNERMOST
----------------------------------------

(11) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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


The TRS R consists of the following rules:

   TERMS(z0) -> c(SQR(z0)) [1]
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0)) [1]
   DBL(s(z0)) -> c6(DBL(z0)) [1]
   ADD(s(z0), z1) -> c8(ADD(z0, z1)) [1]
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2)) [1]
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) [1]
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1)) [1]
   SQR(s(z0)) -> c1(ADD(sqr(z0), dbl(z0))) [1]
   SQR(s(z0)) -> c1(DBL(z0)) [1]
   sqr(0) -> 0 [0]
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0))) [0]
   add(0, z0) -> z0 [0]
   add(s(z0), z1) -> s(add(z0, z1)) [0]
   dbl(0) -> 0 [0]
   dbl(s(z0)) -> s(s(dbl(z0))) [0]

Rewrite Strategy: INNERMOST
----------------------------------------

(13) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(14)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   TERMS(z0) -> c(SQR(z0)) [1]
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0)) [1]
   DBL(s(z0)) -> c6(DBL(z0)) [1]
   ADD(s(z0), z1) -> c8(ADD(z0, z1)) [1]
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2)) [1]
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) [1]
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1)) [1]
   SQR(s(z0)) -> c1(ADD(sqr(z0), dbl(z0))) [1]
   SQR(s(z0)) -> c1(DBL(z0)) [1]
   sqr(0) -> 0 [0]
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0))) [0]
   add(0, z0) -> z0 [0]
   add(s(z0), z1) -> s(add(z0, z1)) [0]
   dbl(0) -> 0 [0]
   dbl(s(z0)) -> s(s(dbl(z0))) [0]

The TRS has the following type information:
TERMS :: s:0 -> c
c :: c3:c1 -> c
SQR :: s:0 -> c3:c1
s :: s:0 -> s:0
c3 :: c6:c8 -> c3:c1 -> c3:c1
ADD :: s:0 -> s:0 -> c6:c8
sqr :: s:0 -> s:0
dbl :: s:0 -> s:0
DBL :: s:0 -> c6:c8
c6 :: c6:c8 -> c6:c8
c8 :: c6:c8 -> c6:c8
FIRST :: s:0 -> cons -> c10
cons :: a -> n__terms:n__first -> cons
c10 :: c12:c13 -> c10
ACTIVATE :: n__terms:n__first -> c12:c13
n__terms :: s:0 -> n__terms:n__first
c12 :: c -> c12:c13
n__first :: s:0 -> cons -> n__terms:n__first
c13 :: c10 -> c12:c13
c1 :: c6:c8 -> c3:c1
0 :: s:0
add :: s:0 -> s:0 -> s:0

Rewrite Strategy: INNERMOST
----------------------------------------

(15) CompletionProof (UPPER BOUND(ID))
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:

   TERMS_1
   SQR_1
   DBL_1
   ADD_2
   FIRST_2
   ACTIVATE_1

(c) The following functions are completely defined:

   sqr_1
   add_2
   dbl_1

Due to the following rules being added:

   sqr(v0) -> 0 [0]
   add(v0, v1) -> 0 [0]
   dbl(v0) -> 0 [0]

And the following fresh constants:    const, const1, const2, const3, const4, const5, const6, const7

----------------------------------------

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

   TERMS(z0) -> c(SQR(z0)) [1]
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0)) [1]
   DBL(s(z0)) -> c6(DBL(z0)) [1]
   ADD(s(z0), z1) -> c8(ADD(z0, z1)) [1]
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2)) [1]
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) [1]
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1)) [1]
   SQR(s(z0)) -> c1(ADD(sqr(z0), dbl(z0))) [1]
   SQR(s(z0)) -> c1(DBL(z0)) [1]
   sqr(0) -> 0 [0]
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0))) [0]
   add(0, z0) -> z0 [0]
   add(s(z0), z1) -> s(add(z0, z1)) [0]
   dbl(0) -> 0 [0]
   dbl(s(z0)) -> s(s(dbl(z0))) [0]
   sqr(v0) -> 0 [0]
   add(v0, v1) -> 0 [0]
   dbl(v0) -> 0 [0]

The TRS has the following type information:
TERMS :: s:0 -> c
c :: c3:c1 -> c
SQR :: s:0 -> c3:c1
s :: s:0 -> s:0
c3 :: c6:c8 -> c3:c1 -> c3:c1
ADD :: s:0 -> s:0 -> c6:c8
sqr :: s:0 -> s:0
dbl :: s:0 -> s:0
DBL :: s:0 -> c6:c8
c6 :: c6:c8 -> c6:c8
c8 :: c6:c8 -> c6:c8
FIRST :: s:0 -> cons -> c10
cons :: a -> n__terms:n__first -> cons
c10 :: c12:c13 -> c10
ACTIVATE :: n__terms:n__first -> c12:c13
n__terms :: s:0 -> n__terms:n__first
c12 :: c -> c12:c13
n__first :: s:0 -> cons -> n__terms:n__first
c13 :: c10 -> c12:c13
c1 :: c6:c8 -> c3:c1
0 :: s:0
add :: s:0 -> s:0 -> s:0
const :: c
const1 :: c3:c1
const2 :: c6:c8
const3 :: c10
const4 :: cons
const5 :: a
const6 :: n__terms:n__first
const7 :: c12:c13

Rewrite Strategy: INNERMOST
----------------------------------------

(17) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

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

   TERMS(z0) -> c(SQR(z0)) [1]
   SQR(s(0)) -> c3(ADD(0, 0), SQR(0)) [1]
   SQR(s(0)) -> c3(ADD(0, 0), SQR(0)) [1]
   SQR(s(s(z0'))) -> c3(ADD(s(add(sqr(z0'), dbl(z0'))), s(s(dbl(z0')))), SQR(s(z0'))) [1]
   SQR(s(s(z0'))) -> c3(ADD(s(add(sqr(z0'), dbl(z0'))), 0), SQR(s(z0'))) [1]
   SQR(s(0)) -> c3(ADD(0, 0), SQR(0)) [1]
   SQR(s(s(z0''))) -> c3(ADD(0, s(s(dbl(z0'')))), SQR(s(z0''))) [1]
   SQR(s(z0)) -> c3(ADD(0, 0), SQR(z0)) [1]
   DBL(s(z0)) -> c6(DBL(z0)) [1]
   ADD(s(z0), z1) -> c8(ADD(z0, z1)) [1]
   FIRST(s(z0), cons(z1, z2)) -> c10(ACTIVATE(z2)) [1]
   ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) [1]
   ACTIVATE(n__first(z0, z1)) -> c13(FIRST(z0, z1)) [1]
   SQR(s(0)) -> c1(ADD(0, 0)) [1]
   SQR(s(0)) -> c1(ADD(0, 0)) [1]
   SQR(s(s(z01))) -> c1(ADD(s(add(sqr(z01), dbl(z01))), s(s(dbl(z01))))) [1]
   SQR(s(s(z01))) -> c1(ADD(s(add(sqr(z01), dbl(z01))), 0)) [1]
   SQR(s(0)) -> c1(ADD(0, 0)) [1]
   SQR(s(s(z02))) -> c1(ADD(0, s(s(dbl(z02))))) [1]
   SQR(s(z0)) -> c1(ADD(0, 0)) [1]
   SQR(s(z0)) -> c1(DBL(z0)) [1]
   sqr(0) -> 0 [0]
   sqr(s(0)) -> s(add(0, 0)) [0]
   sqr(s(0)) -> s(add(0, 0)) [0]
   sqr(s(s(z03))) -> s(add(s(add(sqr(z03), dbl(z03))), s(s(dbl(z03))))) [0]
   sqr(s(s(z03))) -> s(add(s(add(sqr(z03), dbl(z03))), 0)) [0]
   sqr(s(0)) -> s(add(0, 0)) [0]
   sqr(s(s(z04))) -> s(add(0, s(s(dbl(z04))))) [0]
   sqr(s(z0)) -> s(add(0, 0)) [0]
   add(0, z0) -> z0 [0]
   add(s(z0), z1) -> s(add(z0, z1)) [0]
   dbl(0) -> 0 [0]
   dbl(s(z0)) -> s(s(dbl(z0))) [0]
   sqr(v0) -> 0 [0]
   add(v0, v1) -> 0 [0]
   dbl(v0) -> 0 [0]

The TRS has the following type information:
TERMS :: s:0 -> c
c :: c3:c1 -> c
SQR :: s:0 -> c3:c1
s :: s:0 -> s:0
c3 :: c6:c8 -> c3:c1 -> c3:c1
ADD :: s:0 -> s:0 -> c6:c8
sqr :: s:0 -> s:0
dbl :: s:0 -> s:0
DBL :: s:0 -> c6:c8
c6 :: c6:c8 -> c6:c8
c8 :: c6:c8 -> c6:c8
FIRST :: s:0 -> cons -> c10
cons :: a -> n__terms:n__first -> cons
c10 :: c12:c13 -> c10
ACTIVATE :: n__terms:n__first -> c12:c13
n__terms :: s:0 -> n__terms:n__first
c12 :: c -> c12:c13
n__first :: s:0 -> cons -> n__terms:n__first
c13 :: c10 -> c12:c13
c1 :: c6:c8 -> c3:c1
0 :: s:0
add :: s:0 -> s:0 -> s:0
const :: c
const1 :: c3:c1
const2 :: c6:c8
const3 :: c10
const4 :: cons
const5 :: a
const6 :: n__terms:n__first
const7 :: c12:c13

Rewrite Strategy: INNERMOST
----------------------------------------

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

   0 => 0
   const => 0
   const1 => 0
   const2 => 0
   const3 => 0
   const4 => 0
   const5 => 0
   const6 => 0
   const7 => 0

----------------------------------------

(20)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z0) :|: z = 1 + z0, z0 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ 1 }-> 1 + ADD(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   DBL(z) -{ 1 }-> 1 + DBL(z0) :|: z = 1 + z0, z0 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0
   SQR(z) -{ 1 }-> 1 + DBL(z0) :|: z = 1 + z0, z0 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z = 1 + z0, z0 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z02))) :|: z = 1 + (1 + z02), z02 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z01), dbl(z01)), 0) :|: z = 1 + (1 + z01), z01 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z01), dbl(z01)), 1 + (1 + dbl(z01))) :|: z = 1 + (1 + z01), z01 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(z0) :|: z = 1 + z0, z0 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z0''))) + SQR(1 + z0'') :|: z = 1 + (1 + z0''), z0'' >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z0'), dbl(z0')), 0) + SQR(1 + z0') :|: z = 1 + (1 + z0'), z0' >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z0'), dbl(z0')), 1 + (1 + dbl(z0'))) + SQR(1 + z0') :|: z = 1 + (1 + z0'), z0' >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z0) :|: z = z0, z0 >= 0
   add(z, z') -{ 0 }-> z0 :|: z0 >= 0, z = 0, z' = z0
   add(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   add(z, z') -{ 0 }-> 1 + add(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z0)) :|: z = 1 + z0, z0 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + z0, z0 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z04))) :|: z04 >= 0, z = 1 + (1 + z04)
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z03), dbl(z03)), 0) :|: z = 1 + (1 + z03), z03 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z03), dbl(z03)), 1 + (1 + dbl(z03))) :|: z = 1 + (1 + z03), z03 >= 0


----------------------------------------

(21) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

(22)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0


----------------------------------------

(23) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { DBL }
   { ADD }
   { dbl }
   { add }
   { sqr }
   { SQR }
   { TERMS }
   { FIRST, ACTIVATE }

----------------------------------------

(24)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0

Function symbols to be analyzed: {DBL}, {ADD}, {dbl}, {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}

----------------------------------------

(25) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(26)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0

Function symbols to be analyzed: {DBL}, {ADD}, {dbl}, {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}

----------------------------------------

(27) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(28)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0

Function symbols to be analyzed: {DBL}, {ADD}, {dbl}, {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: ?, size: O(1) [0]

----------------------------------------

(29) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(30)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0

Function symbols to be analyzed: {ADD}, {dbl}, {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]

----------------------------------------

(31) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(32)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0

Function symbols to be analyzed: {ADD}, {dbl}, {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]

----------------------------------------

(33) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(34)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0

Function symbols to be analyzed: {ADD}, {dbl}, {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: ?, size: O(1) [0]

----------------------------------------

(35) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(36)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + SQR(z - 1) :|: z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0

Function symbols to be analyzed: {dbl}, {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]

----------------------------------------

(37) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(38)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0

Function symbols to be analyzed: {dbl}, {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]

----------------------------------------

(39) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 2*z

----------------------------------------

(40)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0

Function symbols to be analyzed: {dbl}, {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: ?, size: O(n^1) [2*z]

----------------------------------------

(41) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(42)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 0) :|: z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0

Function symbols to be analyzed: {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]

----------------------------------------

(43) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(44)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s10), 1 + (1 + s11)) :|: s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s12), 0) :|: s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s9 + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + s18)) :|: s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s15), 1 + (1 + s16)) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s17), 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]

----------------------------------------

(45) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(46)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s10), 1 + (1 + s11)) :|: s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s12), 0) :|: s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s9 + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + s18)) :|: s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s15), 1 + (1 + s16)) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s17), 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {add}, {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: ?, size: O(n^1) [z + z']

----------------------------------------

(47) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(48)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s10), 1 + (1 + s11)) :|: s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s12), 0) :|: s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s9 + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z = 1 + 0
   sqr(z) -{ 0 }-> 1 + add(0, 0) :|: z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(0, 1 + (1 + s18)) :|: s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s15), 1 + (1 + s16)) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s17), 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']

----------------------------------------

(49) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(50)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s10), 1 + (1 + s11)) :|: s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s12), 0) :|: s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s9 + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s15), 1 + (1 + s16)) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s17), 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']

----------------------------------------

(51) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(n^2) with polynomial bound: 3 + 8*z + 6*z^2

----------------------------------------

(52)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s10), 1 + (1 + s11)) :|: s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s12), 0) :|: s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s9 + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s15), 1 + (1 + s16)) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s17), 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {sqr}, {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: ?, size: O(n^2) [3 + 8*z + 6*z^2]

----------------------------------------

(53) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(54)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s10), 1 + (1 + s11)) :|: s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s12), 0) :|: s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s9 + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s15), 1 + (1 + s16)) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s17), 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: O(1) [0], size: O(n^2) [3 + 8*z + 6*z^2]

----------------------------------------

(55) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(56)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 2 + s31 }-> 1 + s32 :|: s30 >= 0, s30 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s31 >= 0, s31 <= s30 + s10, s32 >= 0, s32 <= 0, s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s34 }-> 1 + s35 :|: s33 >= 0, s33 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s34 >= 0, s34 <= s33 + s12, s35 >= 0, s35 <= 0, s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 2 + s25 }-> 1 + s26 + SQR(1 + (z - 2)) :|: s24 >= 0, s24 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s25 >= 0, s25 <= s24 + s5, s26 >= 0, s26 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s28 }-> 1 + s29 + SQR(1 + (z - 2)) :|: s27 >= 0, s27 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s28 >= 0, s28 <= s27 + s7, s29 >= 0, s29 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s9 + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s38 :|: s36 >= 0, s36 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s37 >= 0, s37 <= s36 + s15, s38 >= 0, s38 <= 1 + s37 + (1 + (1 + s16)), s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s41 :|: s39 >= 0, s39 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s40 >= 0, s40 <= s39 + s17, s41 >= 0, s41 <= 1 + s40 + 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: O(1) [0], size: O(n^2) [3 + 8*z + 6*z^2]

----------------------------------------

(57) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(58)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 2 + s31 }-> 1 + s32 :|: s30 >= 0, s30 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s31 >= 0, s31 <= s30 + s10, s32 >= 0, s32 <= 0, s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s34 }-> 1 + s35 :|: s33 >= 0, s33 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s34 >= 0, s34 <= s33 + s12, s35 >= 0, s35 <= 0, s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 2 + s25 }-> 1 + s26 + SQR(1 + (z - 2)) :|: s24 >= 0, s24 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s25 >= 0, s25 <= s24 + s5, s26 >= 0, s26 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s28 }-> 1 + s29 + SQR(1 + (z - 2)) :|: s27 >= 0, s27 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s28 >= 0, s28 <= s27 + s7, s29 >= 0, s29 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s9 + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s38 :|: s36 >= 0, s36 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s37 >= 0, s37 <= s36 + s15, s38 >= 0, s38 <= 1 + s37 + (1 + (1 + s16)), s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s41 :|: s39 >= 0, s39 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s40 >= 0, s40 <= s39 + s17, s41 >= 0, s41 <= 1 + s40 + 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {SQR}, {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: O(1) [0], size: O(n^2) [3 + 8*z + 6*z^2]
  SQR: runtime: ?, size: O(n^1) [z]

----------------------------------------

(59) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: SQR
after applying outer abstraction to obtain an ITS,
resulting in: O(n^3) with polynomial bound: 29 + 66*z + 48*z^2 + 12*z^3

----------------------------------------

(60)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 2 + s31 }-> 1 + s32 :|: s30 >= 0, s30 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s31 >= 0, s31 <= s30 + s10, s32 >= 0, s32 <= 0, s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s34 }-> 1 + s35 :|: s33 >= 0, s33 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s34 >= 0, s34 <= s33 + s12, s35 >= 0, s35 <= 0, s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s'' + SQR(0) :|: s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 1 }-> 1 + s1 + SQR(z - 1) :|: s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 2 + s25 }-> 1 + s26 + SQR(1 + (z - 2)) :|: s24 >= 0, s24 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s25 >= 0, s25 <= s24 + s5, s26 >= 0, s26 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s28 }-> 1 + s29 + SQR(1 + (z - 2)) :|: s27 >= 0, s27 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s28 >= 0, s28 <= s27 + s7, s29 >= 0, s29 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s9 + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   TERMS(z) -{ 1 }-> 1 + SQR(z) :|: z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s38 :|: s36 >= 0, s36 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s37 >= 0, s37 <= s36 + s15, s38 >= 0, s38 <= 1 + s37 + (1 + (1 + s16)), s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s41 :|: s39 >= 0, s39 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s40 >= 0, s40 <= s39 + s17, s41 >= 0, s41 <= 1 + s40 + 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: O(1) [0], size: O(n^2) [3 + 8*z + 6*z^2]
  SQR: runtime: O(n^3) [29 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [z]

----------------------------------------

(61) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(62)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 2 + s31 }-> 1 + s32 :|: s30 >= 0, s30 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s31 >= 0, s31 <= s30 + s10, s32 >= 0, s32 <= 0, s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s34 }-> 1 + s35 :|: s33 >= 0, s33 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s34 >= 0, s34 <= s33 + s12, s35 >= 0, s35 <= 0, s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 30 }-> 1 + s'' + s43 :|: s43 >= 0, s43 <= 0, s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s1 + s47 :|: s47 >= 0, s47 <= z - 1, s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 + s25 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s26 + s44 :|: s44 >= 0, s44 <= 1 + (z - 2), s24 >= 0, s24 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s25 >= 0, s25 <= s24 + s5, s26 >= 0, s26 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s28 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s29 + s45 :|: s45 >= 0, s45 <= 1 + (z - 2), s27 >= 0, s27 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s28 >= 0, s28 <= s27 + s7, s29 >= 0, s29 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s9 + s46 :|: s46 >= 0, s46 <= 1 + (z - 2), s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   TERMS(z) -{ 30 + 66*z + 48*z^2 + 12*z^3 }-> 1 + s42 :|: s42 >= 0, s42 <= z, z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s38 :|: s36 >= 0, s36 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s37 >= 0, s37 <= s36 + s15, s38 >= 0, s38 <= 1 + s37 + (1 + (1 + s16)), s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s41 :|: s39 >= 0, s39 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s40 >= 0, s40 <= s39 + s17, s41 >= 0, s41 <= 1 + s40 + 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: O(1) [0], size: O(n^2) [3 + 8*z + 6*z^2]
  SQR: runtime: O(n^3) [29 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [z]

----------------------------------------

(63) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(64)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 2 + s31 }-> 1 + s32 :|: s30 >= 0, s30 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s31 >= 0, s31 <= s30 + s10, s32 >= 0, s32 <= 0, s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s34 }-> 1 + s35 :|: s33 >= 0, s33 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s34 >= 0, s34 <= s33 + s12, s35 >= 0, s35 <= 0, s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 30 }-> 1 + s'' + s43 :|: s43 >= 0, s43 <= 0, s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s1 + s47 :|: s47 >= 0, s47 <= z - 1, s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 + s25 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s26 + s44 :|: s44 >= 0, s44 <= 1 + (z - 2), s24 >= 0, s24 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s25 >= 0, s25 <= s24 + s5, s26 >= 0, s26 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s28 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s29 + s45 :|: s45 >= 0, s45 <= 1 + (z - 2), s27 >= 0, s27 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s28 >= 0, s28 <= s27 + s7, s29 >= 0, s29 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s9 + s46 :|: s46 >= 0, s46 <= 1 + (z - 2), s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   TERMS(z) -{ 30 + 66*z + 48*z^2 + 12*z^3 }-> 1 + s42 :|: s42 >= 0, s42 <= z, z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s38 :|: s36 >= 0, s36 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s37 >= 0, s37 <= s36 + s15, s38 >= 0, s38 <= 1 + s37 + (1 + (1 + s16)), s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s41 :|: s39 >= 0, s39 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s40 >= 0, s40 <= s39 + s17, s41 >= 0, s41 <= 1 + s40 + 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {TERMS}, {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: O(1) [0], size: O(n^2) [3 + 8*z + 6*z^2]
  SQR: runtime: O(n^3) [29 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [z]
  TERMS: runtime: ?, size: O(n^1) [1 + z]

----------------------------------------

(65) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: TERMS
after applying outer abstraction to obtain an ITS,
resulting in: O(n^3) with polynomial bound: 30 + 66*z + 48*z^2 + 12*z^3

----------------------------------------

(66)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 }-> 1 + TERMS(z - 1) :|: z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 2 + s31 }-> 1 + s32 :|: s30 >= 0, s30 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s31 >= 0, s31 <= s30 + s10, s32 >= 0, s32 <= 0, s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s34 }-> 1 + s35 :|: s33 >= 0, s33 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s34 >= 0, s34 <= s33 + s12, s35 >= 0, s35 <= 0, s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 30 }-> 1 + s'' + s43 :|: s43 >= 0, s43 <= 0, s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s1 + s47 :|: s47 >= 0, s47 <= z - 1, s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 + s25 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s26 + s44 :|: s44 >= 0, s44 <= 1 + (z - 2), s24 >= 0, s24 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s25 >= 0, s25 <= s24 + s5, s26 >= 0, s26 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s28 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s29 + s45 :|: s45 >= 0, s45 <= 1 + (z - 2), s27 >= 0, s27 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s28 >= 0, s28 <= s27 + s7, s29 >= 0, s29 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s9 + s46 :|: s46 >= 0, s46 <= 1 + (z - 2), s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   TERMS(z) -{ 30 + 66*z + 48*z^2 + 12*z^3 }-> 1 + s42 :|: s42 >= 0, s42 <= z, z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s38 :|: s36 >= 0, s36 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s37 >= 0, s37 <= s36 + s15, s38 >= 0, s38 <= 1 + s37 + (1 + (1 + s16)), s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s41 :|: s39 >= 0, s39 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s40 >= 0, s40 <= s39 + s17, s41 >= 0, s41 <= 1 + s40 + 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: O(1) [0], size: O(n^2) [3 + 8*z + 6*z^2]
  SQR: runtime: O(n^3) [29 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [z]
  TERMS: runtime: O(n^3) [30 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [1 + z]

----------------------------------------

(67) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(68)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s48 :|: s48 >= 0, s48 <= z - 1 + 1, z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 2 + s31 }-> 1 + s32 :|: s30 >= 0, s30 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s31 >= 0, s31 <= s30 + s10, s32 >= 0, s32 <= 0, s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s34 }-> 1 + s35 :|: s33 >= 0, s33 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s34 >= 0, s34 <= s33 + s12, s35 >= 0, s35 <= 0, s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 30 }-> 1 + s'' + s43 :|: s43 >= 0, s43 <= 0, s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s1 + s47 :|: s47 >= 0, s47 <= z - 1, s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 + s25 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s26 + s44 :|: s44 >= 0, s44 <= 1 + (z - 2), s24 >= 0, s24 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s25 >= 0, s25 <= s24 + s5, s26 >= 0, s26 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s28 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s29 + s45 :|: s45 >= 0, s45 <= 1 + (z - 2), s27 >= 0, s27 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s28 >= 0, s28 <= s27 + s7, s29 >= 0, s29 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s9 + s46 :|: s46 >= 0, s46 <= 1 + (z - 2), s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   TERMS(z) -{ 30 + 66*z + 48*z^2 + 12*z^3 }-> 1 + s42 :|: s42 >= 0, s42 <= z, z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s38 :|: s36 >= 0, s36 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s37 >= 0, s37 <= s36 + s15, s38 >= 0, s38 <= 1 + s37 + (1 + (1 + s16)), s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s41 :|: s39 >= 0, s39 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s40 >= 0, s40 <= s39 + s17, s41 >= 0, s41 <= 1 + s40 + 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: O(1) [0], size: O(n^2) [3 + 8*z + 6*z^2]
  SQR: runtime: O(n^3) [29 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [z]
  TERMS: runtime: O(n^3) [30 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [1 + z]

----------------------------------------

(69) IntTrsBoundProof (UPPER BOUND(ID))

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

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

----------------------------------------

(70)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s48 :|: s48 >= 0, s48 <= z - 1 + 1, z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 2 + s31 }-> 1 + s32 :|: s30 >= 0, s30 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s31 >= 0, s31 <= s30 + s10, s32 >= 0, s32 <= 0, s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s34 }-> 1 + s35 :|: s33 >= 0, s33 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s34 >= 0, s34 <= s33 + s12, s35 >= 0, s35 <= 0, s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 30 }-> 1 + s'' + s43 :|: s43 >= 0, s43 <= 0, s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s1 + s47 :|: s47 >= 0, s47 <= z - 1, s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 + s25 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s26 + s44 :|: s44 >= 0, s44 <= 1 + (z - 2), s24 >= 0, s24 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s25 >= 0, s25 <= s24 + s5, s26 >= 0, s26 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s28 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s29 + s45 :|: s45 >= 0, s45 <= 1 + (z - 2), s27 >= 0, s27 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s28 >= 0, s28 <= s27 + s7, s29 >= 0, s29 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s9 + s46 :|: s46 >= 0, s46 <= 1 + (z - 2), s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   TERMS(z) -{ 30 + 66*z + 48*z^2 + 12*z^3 }-> 1 + s42 :|: s42 >= 0, s42 <= z, z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s38 :|: s36 >= 0, s36 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s37 >= 0, s37 <= s36 + s15, s38 >= 0, s38 <= 1 + s37 + (1 + (1 + s16)), s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s41 :|: s39 >= 0, s39 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s40 >= 0, s40 <= s39 + s17, s41 >= 0, s41 <= 1 + s40 + 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: {FIRST,ACTIVATE}
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: O(1) [0], size: O(n^2) [3 + 8*z + 6*z^2]
  SQR: runtime: O(n^3) [29 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [z]
  TERMS: runtime: O(n^3) [30 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [1 + z]
  FIRST: runtime: ?, size: O(n^1) [1 + z']
  ACTIVATE: runtime: ?, size: O(n^1) [1 + z]

----------------------------------------

(71) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: FIRST
after applying outer abstraction to obtain an ITS,
resulting in: O(n^3) with polynomial bound: 1 + 8*z' + 12*z'^2 + 12*z'^3

Computed RUNTIME bound using KoAT for: ACTIVATE
after applying outer abstraction to obtain an ITS,
resulting in: O(n^3) with polynomial bound: 3 + 14*z + 24*z^2 + 24*z^3

----------------------------------------

(72)
Obligation:
Complexity RNTS consisting of the following rules:

   ACTIVATE(z) -{ 1 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s48 :|: s48 >= 0, s48 <= z - 1 + 1, z - 1 >= 0
   ACTIVATE(z) -{ 1 }-> 1 + FIRST(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   ADD(z, z') -{ z }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z' >= 0, z - 1 >= 0
   DBL(z) -{ z }-> 1 + s :|: s >= 0, s <= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 + ACTIVATE(z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SQR(z) -{ z }-> 1 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + s14 :|: s13 >= 0, s13 <= 2 * (z - 2), s14 >= 0, s14 <= 0, z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 1 + 0
   SQR(z) -{ 2 + s31 }-> 1 + s32 :|: s30 >= 0, s30 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s31 >= 0, s31 <= s30 + s10, s32 >= 0, s32 <= 0, s10 >= 0, s10 <= 2 * (z - 2), s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 2 + s34 }-> 1 + s35 :|: s33 >= 0, s33 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s34 >= 0, s34 <= s33 + s12, s35 >= 0, s35 <= 0, s12 >= 0, s12 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z - 1 >= 0
   SQR(z) -{ 30 }-> 1 + s'' + s43 :|: s43 >= 0, s43 <= 0, s'' >= 0, s'' <= 0, z = 1 + 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s1 + s47 :|: s47 >= 0, s47 <= z - 1, s1 >= 0, s1 <= 0, z - 1 >= 0
   SQR(z) -{ 1 + s25 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s26 + s44 :|: s44 >= 0, s44 <= 1 + (z - 2), s24 >= 0, s24 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s25 >= 0, s25 <= s24 + s5, s26 >= 0, s26 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s28 + 6*z + 12*z^2 + 12*z^3 }-> 1 + s29 + s45 :|: s45 >= 0, s45 <= 1 + (z - 2), s27 >= 0, s27 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s28 >= 0, s28 <= s27 + s7, s29 >= 0, s29 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 6*z + 12*z^2 + 12*z^3 }-> 1 + s9 + s46 :|: s46 >= 0, s46 <= 1 + (z - 2), s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 0, z - 2 >= 0
   TERMS(z) -{ 30 + 66*z + 48*z^2 + 12*z^3 }-> 1 + s42 :|: s42 >= 0, s42 <= z, z >= 0
   add(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add(z, z') -{ 0 }-> 1 + s23 :|: s23 >= 0, s23 <= z - 1 + z', z' >= 0, z - 1 >= 0
   dbl(z) -{ 0 }-> 0 :|: z = 0
   dbl(z) -{ 0 }-> 0 :|: z >= 0
   dbl(z) -{ 0 }-> 1 + (1 + s19) :|: s19 >= 0, s19 <= 2 * (z - 1), z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s20 :|: s20 >= 0, s20 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s21 :|: s21 >= 0, s21 <= 0 + (1 + (1 + s18)), s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s22 :|: s22 >= 0, s22 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s38 :|: s36 >= 0, s36 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s37 >= 0, s37 <= s36 + s15, s38 >= 0, s38 <= 1 + s37 + (1 + (1 + s16)), s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s41 :|: s39 >= 0, s39 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s40 >= 0, s40 <= s39 + s17, s41 >= 0, s41 <= 1 + s40 + 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0

Function symbols to be analyzed: 
Previous analysis results are:
  DBL: runtime: O(n^1) [z], size: O(1) [0]
  ADD: runtime: O(n^1) [z], size: O(1) [0]
  dbl: runtime: O(1) [0], size: O(n^1) [2*z]
  add: runtime: O(1) [0], size: O(n^1) [z + z']
  sqr: runtime: O(1) [0], size: O(n^2) [3 + 8*z + 6*z^2]
  SQR: runtime: O(n^3) [29 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [z]
  TERMS: runtime: O(n^3) [30 + 66*z + 48*z^2 + 12*z^3], size: O(n^1) [1 + z]
  FIRST: runtime: O(n^3) [1 + 8*z' + 12*z'^2 + 12*z'^3], size: O(n^1) [1 + z']
  ACTIVATE: runtime: O(n^3) [3 + 14*z + 24*z^2 + 24*z^3], size: O(n^1) [1 + z]

----------------------------------------

(73) FinalProof (FINISHED)
Computed overall runtime complexity
----------------------------------------

(74)
BOUNDS(1, n^3)