WORST_CASE(Omega(n^3),O(n^3))
proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 275 ms]
(2) CpxRelTRS
(3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxWeightedTrs
    (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CpxTypedWeightedTrs
    (7) CompletionProof [UPPER BOUND(ID), 0 ms]
    (8) CpxTypedWeightedCompleteTrs
    (9) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxTypedWeightedCompleteTrs
    (11) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (12) CpxRNTS
    (13) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CpxRNTS
    (15) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) CpxRNTS
    (17) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (18) CpxRNTS
    (19) IntTrsBoundProof [UPPER BOUND(ID), 148 ms]
    (20) CpxRNTS
    (21) IntTrsBoundProof [UPPER BOUND(ID), 6 ms]
    (22) CpxRNTS
    (23) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (24) CpxRNTS
    (25) IntTrsBoundProof [UPPER BOUND(ID), 83 ms]
    (26) CpxRNTS
    (27) IntTrsBoundProof [UPPER BOUND(ID), 0 ms]
    (28) CpxRNTS
    (29) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (30) CpxRNTS
    (31) IntTrsBoundProof [UPPER BOUND(ID), 292 ms]
    (32) CpxRNTS
    (33) IntTrsBoundProof [UPPER BOUND(ID), 4 ms]
    (34) CpxRNTS
    (35) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (36) CpxRNTS
    (37) IntTrsBoundProof [UPPER BOUND(ID), 143 ms]
    (38) CpxRNTS
    (39) IntTrsBoundProof [UPPER BOUND(ID), 34 ms]
    (40) CpxRNTS
    (41) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (42) CpxRNTS
    (43) IntTrsBoundProof [UPPER BOUND(ID), 89 ms]
    (44) CpxRNTS
    (45) IntTrsBoundProof [UPPER BOUND(ID), 53 ms]
    (46) CpxRNTS
    (47) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (48) CpxRNTS
    (49) IntTrsBoundProof [UPPER BOUND(ID), 380 ms]
    (50) CpxRNTS
    (51) IntTrsBoundProof [UPPER BOUND(ID), 34 ms]
    (52) CpxRNTS
    (53) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (54) CpxRNTS
    (55) IntTrsBoundProof [UPPER BOUND(ID), 843 ms]
    (56) CpxRNTS
    (57) IntTrsBoundProof [UPPER BOUND(ID), 49 ms]
    (58) CpxRNTS
    (59) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (60) CpxRNTS
    (61) IntTrsBoundProof [UPPER BOUND(ID), 1915 ms]
    (62) CpxRNTS
    (63) IntTrsBoundProof [UPPER BOUND(ID), 459 ms]
    (64) CpxRNTS
    (65) ResultPropagationProof [UPPER BOUND(ID), 3 ms]
    (66) CpxRNTS
    (67) IntTrsBoundProof [UPPER BOUND(ID), 540 ms]
    (68) CpxRNTS
    (69) IntTrsBoundProof [UPPER BOUND(ID), 32 ms]
    (70) CpxRNTS
    (71) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (72) CpxRNTS
    (73) IntTrsBoundProof [UPPER BOUND(ID), 379 ms]
    (74) CpxRNTS
    (75) IntTrsBoundProof [UPPER BOUND(ID), 0 ms]
    (76) CpxRNTS
    (77) FinalProof [FINISHED, 0 ms]
    (78) BOUNDS(1, n^3)
(79) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(80) CpxRelTRS
    (81) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (82) typed CpxTrs
    (83) OrderProof [LOWER BOUND(ID), 17 ms]
    (84) typed CpxTrs
    (85) RewriteLemmaProof [LOWER BOUND(ID), 260 ms]
    (86) BEST
        (87) proven lower bound
            (88) LowerBoundPropagationProof [FINISHED, 0 ms]
            (89) BOUNDS(n^1, INF)
        (90) typed CpxTrs
            (91) RewriteLemmaProof [LOWER BOUND(ID), 130 ms]
            (92) typed CpxTrs
            (93) RewriteLemmaProof [LOWER BOUND(ID), 34 ms]
            (94) typed CpxTrs
            (95) RewriteLemmaProof [LOWER BOUND(ID), 55 ms]
            (96) typed CpxTrs
            (97) RewriteLemmaProof [LOWER BOUND(ID), 102 ms]
            (98) typed CpxTrs
            (99) RewriteLemmaProof [LOWER BOUND(ID), 464 ms]
            (100) proven lower bound
            (101) LowerBoundPropagationProof [FINISHED, 0 ms]
            (102) BOUNDS(n^3, INF)


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

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


The TRS R consists of the following rules:

   TERMS(z0) -> c(SQR(z0))
   SQR(0) -> c1
   SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(0) -> c4
   DBL(s(z0)) -> c5(DBL(z0))
   ADD(0, z0) -> c6
   ADD(s(z0), z1) -> c7(ADD(z0, z1))
   FIRST(0, z0) -> c8
   FIRST(s(z0), cons(z1)) -> c9

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

   terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

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

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

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


The TRS R consists of the following rules:

   TERMS(z0) -> c(SQR(z0))
   SQR(0) -> c1
   SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(0) -> c4
   DBL(s(z0)) -> c5(DBL(z0))
   ADD(0, z0) -> c6
   ADD(s(z0), z1) -> c7(ADD(z0, z1))
   FIRST(0, z0) -> c8
   FIRST(s(z0), cons(z1)) -> c9

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

   terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

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

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

(4)
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(0) -> c1 [1]
   SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0)) [1]
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0)) [1]
   DBL(0) -> c4 [1]
   DBL(s(z0)) -> c5(DBL(z0)) [1]
   ADD(0, z0) -> c6 [1]
   ADD(s(z0), z1) -> c7(ADD(z0, z1)) [1]
   FIRST(0, z0) -> c8 [1]
   FIRST(s(z0), cons(z1)) -> c9 [1]
   terms(z0) -> cons(recip(sqr(z0))) [0]
   sqr(0) -> 0 [0]
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0))) [0]
   dbl(0) -> 0 [0]
   dbl(s(z0)) -> s(s(dbl(z0))) [0]
   add(0, z0) -> z0 [0]
   add(s(z0), z1) -> s(add(z0, z1)) [0]
   first(0, z0) -> nil [0]
   first(s(z0), cons(z1)) -> cons(z1) [0]

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

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

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

   TERMS(z0) -> c(SQR(z0)) [1]
   SQR(0) -> c1 [1]
   SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0)) [1]
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0)) [1]
   DBL(0) -> c4 [1]
   DBL(s(z0)) -> c5(DBL(z0)) [1]
   ADD(0, z0) -> c6 [1]
   ADD(s(z0), z1) -> c7(ADD(z0, z1)) [1]
   FIRST(0, z0) -> c8 [1]
   FIRST(s(z0), cons(z1)) -> c9 [1]
   terms(z0) -> cons(recip(sqr(z0))) [0]
   sqr(0) -> 0 [0]
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0))) [0]
   dbl(0) -> 0 [0]
   dbl(s(z0)) -> s(s(dbl(z0))) [0]
   add(0, z0) -> z0 [0]
   add(s(z0), z1) -> s(add(z0, z1)) [0]
   first(0, z0) -> nil [0]
   first(s(z0), cons(z1)) -> cons(z1) [0]

The TRS has the following type information:
TERMS :: 0:s -> c
c :: c1:c2:c3 -> c
SQR :: 0:s -> c1:c2:c3
0 :: 0:s
c1 :: c1:c2:c3
s :: 0:s -> 0:s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0:s -> 0:s -> c6:c7
sqr :: 0:s -> 0:s
dbl :: 0:s -> 0:s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0:s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0:s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0:s -> cons:nil
recip :: 0:s -> recip
add :: 0:s -> 0:s -> 0:s
first :: 0:s -> cons:nil -> cons:nil
nil :: cons:nil

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

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

(c) The following functions are completely defined:

   terms_1
   sqr_1
   dbl_1
   add_2
   first_2

Due to the following rules being added:

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

And the following fresh constants:    const, const1

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

(8)
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(0) -> c1 [1]
   SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0)) [1]
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0)) [1]
   DBL(0) -> c4 [1]
   DBL(s(z0)) -> c5(DBL(z0)) [1]
   ADD(0, z0) -> c6 [1]
   ADD(s(z0), z1) -> c7(ADD(z0, z1)) [1]
   FIRST(0, z0) -> c8 [1]
   FIRST(s(z0), cons(z1)) -> c9 [1]
   terms(z0) -> cons(recip(sqr(z0))) [0]
   sqr(0) -> 0 [0]
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0))) [0]
   dbl(0) -> 0 [0]
   dbl(s(z0)) -> s(s(dbl(z0))) [0]
   add(0, z0) -> z0 [0]
   add(s(z0), z1) -> s(add(z0, z1)) [0]
   first(0, z0) -> nil [0]
   first(s(z0), cons(z1)) -> cons(z1) [0]
   terms(v0) -> nil [0]
   sqr(v0) -> 0 [0]
   dbl(v0) -> 0 [0]
   add(v0, v1) -> 0 [0]
   first(v0, v1) -> nil [0]

The TRS has the following type information:
TERMS :: 0:s -> c
c :: c1:c2:c3 -> c
SQR :: 0:s -> c1:c2:c3
0 :: 0:s
c1 :: c1:c2:c3
s :: 0:s -> 0:s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0:s -> 0:s -> c6:c7
sqr :: 0:s -> 0:s
dbl :: 0:s -> 0:s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0:s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0:s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0:s -> cons:nil
recip :: 0:s -> recip
add :: 0:s -> 0:s -> 0:s
first :: 0:s -> cons:nil -> cons:nil
nil :: cons:nil
const :: c
const1 :: recip

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

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

(10)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

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

   TERMS(z0) -> c(SQR(z0)) [1]
   SQR(0) -> c1 [1]
   SQR(s(0)) -> c2(ADD(0, 0), SQR(0)) [1]
   SQR(s(0)) -> c2(ADD(0, 0), SQR(0)) [1]
   SQR(s(s(z0'))) -> c2(ADD(s(add(sqr(z0'), dbl(z0'))), s(s(dbl(z0')))), SQR(s(z0'))) [1]
   SQR(s(s(z0'))) -> c2(ADD(s(add(sqr(z0'), dbl(z0'))), 0), SQR(s(z0'))) [1]
   SQR(s(0)) -> c2(ADD(0, 0), SQR(0)) [1]
   SQR(s(s(z0''))) -> c2(ADD(0, s(s(dbl(z0'')))), SQR(s(z0''))) [1]
   SQR(s(z0)) -> c2(ADD(0, 0), SQR(z0)) [1]
   SQR(s(0)) -> c3(ADD(0, 0), DBL(0)) [1]
   SQR(s(0)) -> c3(ADD(0, 0), DBL(0)) [1]
   SQR(s(s(z01))) -> c3(ADD(s(add(sqr(z01), dbl(z01))), s(s(dbl(z01)))), DBL(s(z01))) [1]
   SQR(s(s(z01))) -> c3(ADD(s(add(sqr(z01), dbl(z01))), 0), DBL(s(z01))) [1]
   SQR(s(0)) -> c3(ADD(0, 0), DBL(0)) [1]
   SQR(s(s(z02))) -> c3(ADD(0, s(s(dbl(z02)))), DBL(s(z02))) [1]
   SQR(s(z0)) -> c3(ADD(0, 0), DBL(z0)) [1]
   DBL(0) -> c4 [1]
   DBL(s(z0)) -> c5(DBL(z0)) [1]
   ADD(0, z0) -> c6 [1]
   ADD(s(z0), z1) -> c7(ADD(z0, z1)) [1]
   FIRST(0, z0) -> c8 [1]
   FIRST(s(z0), cons(z1)) -> c9 [1]
   terms(z0) -> cons(recip(sqr(z0))) [0]
   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]
   dbl(0) -> 0 [0]
   dbl(s(z0)) -> s(s(dbl(z0))) [0]
   add(0, z0) -> z0 [0]
   add(s(z0), z1) -> s(add(z0, z1)) [0]
   first(0, z0) -> nil [0]
   first(s(z0), cons(z1)) -> cons(z1) [0]
   terms(v0) -> nil [0]
   sqr(v0) -> 0 [0]
   dbl(v0) -> 0 [0]
   add(v0, v1) -> 0 [0]
   first(v0, v1) -> nil [0]

The TRS has the following type information:
TERMS :: 0:s -> c
c :: c1:c2:c3 -> c
SQR :: 0:s -> c1:c2:c3
0 :: 0:s
c1 :: c1:c2:c3
s :: 0:s -> 0:s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0:s -> 0:s -> c6:c7
sqr :: 0:s -> 0:s
dbl :: 0:s -> 0:s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0:s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0:s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0:s -> cons:nil
recip :: 0:s -> recip
add :: 0:s -> 0:s -> 0:s
first :: 0:s -> cons:nil -> cons:nil
nil :: cons:nil
const :: c
const1 :: recip

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

(11) 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
   c1 => 0
   c4 => 0
   c6 => 0
   c8 => 0
   c9 => 1
   nil => 0
   const => 0
   const1 => 0

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   ADD(z, z') -{ 1 }-> 1 + ADD(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 }-> 1 + DBL(z0) :|: z = 1 + z0, z0 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   FIRST(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   SQR(z) -{ 1 }-> 0 :|: z = 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, 0) + DBL(z0) :|: z = 1 + z0, z0 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + DBL(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(0, 1 + (1 + dbl(z02))) + DBL(1 + z02) :|: z = 1 + (1 + z02), z02 >= 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
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z01), dbl(z01)), 0) + DBL(1 + z01) :|: z = 1 + (1 + z01), z01 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z01), dbl(z01)), 1 + (1 + dbl(z01))) + DBL(1 + z01) :|: z = 1 + (1 + z01), z01 >= 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
   first(z, z') -{ 0 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   first(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   first(z, z') -{ 0 }-> 1 + z1 :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   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
   terms(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z0)) :|: z = z0, z0 >= 0


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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 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, 0) + DBL(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + DBL(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(0, 1 + (1 + dbl(z - 2))) + DBL(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)), 0) + DBL(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
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + DBL(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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0


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

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

   { DBL }
   { FIRST }
   { ADD }
   { first }
   { dbl }
   { add }
   { sqr }
   { SQR }
   { terms }
   { TERMS }

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 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, 0) + DBL(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + DBL(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(0, 1 + (1 + dbl(z - 2))) + DBL(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)), 0) + DBL(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
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + DBL(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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 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, 0) + DBL(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + DBL(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(0, 1 + (1 + dbl(z - 2))) + DBL(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)), 0) + DBL(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
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + DBL(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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

(19) 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: z

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 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, 0) + DBL(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + DBL(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(0, 1 + (1 + dbl(z - 2))) + DBL(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)), 0) + DBL(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
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + DBL(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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

(21) 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: 1 + z

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 }-> 1 + DBL(z - 1) :|: z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 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, 0) + DBL(0) :|: z = 1 + 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 0) + DBL(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(0, 1 + (1 + dbl(z - 2))) + DBL(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)), 0) + DBL(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
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + DBL(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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + ADD(0, 0) + s :|: s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 0) + s2 :|: s2 >= 0, s2 <= z - 1, z - 1 >= 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 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

(25) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + ADD(0, 0) + s :|: s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 0) + s2 :|: s2 >= 0, s2 <= z - 1, z - 1 >= 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 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

(27) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + ADD(0, 0) + s :|: s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 0) + s2 :|: s2 >= 0, s2 <= z - 1, z - 1 >= 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 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + ADD(0, 0) + s :|: s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 0) + s2 :|: s2 >= 0, s2 <= z - 1, z - 1 >= 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 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + ADD(0, 0) + s :|: s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 0) + s2 :|: s2 >= 0, s2 <= z - 1, z - 1 >= 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 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

(33) 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: 1 + z

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 }-> 1 + ADD(z - 1, z') :|: z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + ADD(0, 0) + s :|: s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 0) + s2 :|: s2 >= 0, s2 <= z - 1, z - 1 >= 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 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

(37) 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: z'

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

(39) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + s1 :|: s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(0, 1 + (1 + dbl(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 0) + s'' :|: s'' >= 0, s'' <= 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 + z }-> 1 + ADD(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) + s' :|: s' >= 0, s' <= 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
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s13 + SQR(1 + (z - 2)) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s11), 0) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s14), 1 + (1 + s15)) + s' :|: s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s16), 0) + s'' :|: s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s9), 1 + (1 + s10)) + SQR(1 + (z - 2)) :|: s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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 + s22)) :|: s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s13 + SQR(1 + (z - 2)) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s11), 0) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s14), 1 + (1 + s15)) + s' :|: s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s16), 0) + s'' :|: s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s9), 1 + (1 + s10)) + SQR(1 + (z - 2)) :|: s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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 + s22)) :|: s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s13 + SQR(1 + (z - 2)) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s11), 0) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s14), 1 + (1 + s15)) + s' :|: s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s16), 0) + s'' :|: s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s9), 1 + (1 + s10)) + SQR(1 + (z - 2)) :|: s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, 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 + s22)) :|: s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s13 + SQR(1 + (z - 2)) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s11), 0) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s14), 1 + (1 + s15)) + s' :|: s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s16), 0) + s'' :|: s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s9), 1 + (1 + s10)) + SQR(1 + (z - 2)) :|: s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

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

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s13 + SQR(1 + (z - 2)) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s11), 0) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s14), 1 + (1 + s15)) + s' :|: s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s16), 0) + s'' :|: s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s9), 1 + (1 + s10)) + SQR(1 + (z - 2)) :|: s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {SQR}, {terms}, {TERMS}
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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]

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

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s13 + SQR(1 + (z - 2)) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s11), 0) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s14), 1 + (1 + s15)) + s' :|: s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + z }-> 1 + ADD(1 + add(sqr(z - 2), s16), 0) + s'' :|: s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 }-> 1 + ADD(1 + add(sqr(z - 2), s9), 1 + (1 + s10)) + SQR(1 + (z - 2)) :|: s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + add(1 + add(sqr(z - 2), s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {SQR}, {terms}, {TERMS}
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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]

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s13 + SQR(1 + (z - 2)) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s29 }-> 1 + s30 + SQR(1 + (z - 2)) :|: s28 >= 0, s28 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s29 >= 0, s29 <= s28 + s9, s30 >= 0, s30 <= 1 + s29, s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s32 }-> 1 + s33 + SQR(1 + (z - 2)) :|: s31 >= 0, s31 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s32 >= 0, s32 <= s31 + s11, s33 >= 0, s33 <= 1 + s32, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s35 + z }-> 1 + s36 + s' :|: s34 >= 0, s34 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s35 >= 0, s35 <= s34 + s14, s36 >= 0, s36 <= 1 + s35, s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s38 + z }-> 1 + s39 + s'' :|: s37 >= 0, s37 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s38 >= 0, s38 <= s37 + s16, s39 >= 0, s39 <= 1 + s38, s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s43 :|: s41 >= 0, s41 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s42 >= 0, s42 <= s41 + s19, s43 >= 0, s43 <= 1 + s42 + (1 + (1 + s20)), s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s46 :|: s44 >= 0, s44 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s45 >= 0, s45 <= s44 + s21, s46 >= 0, s46 <= 1 + s45 + 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 6 * (z * z) + 8 * z + 3, z >= 0

Function symbols to be analyzed: {SQR}, {terms}, {TERMS}
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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]

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

(61) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s13 + SQR(1 + (z - 2)) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s29 }-> 1 + s30 + SQR(1 + (z - 2)) :|: s28 >= 0, s28 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s29 >= 0, s29 <= s28 + s9, s30 >= 0, s30 <= 1 + s29, s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s32 }-> 1 + s33 + SQR(1 + (z - 2)) :|: s31 >= 0, s31 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s32 >= 0, s32 <= s31 + s11, s33 >= 0, s33 <= 1 + s32, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s35 + z }-> 1 + s36 + s' :|: s34 >= 0, s34 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s35 >= 0, s35 <= s34 + s14, s36 >= 0, s36 <= 1 + s35, s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s38 + z }-> 1 + s39 + s'' :|: s37 >= 0, s37 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s38 >= 0, s38 <= s37 + s16, s39 >= 0, s39 <= 1 + s38, s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s43 :|: s41 >= 0, s41 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s42 >= 0, s42 <= s41 + s19, s43 >= 0, s43 <= 1 + s42 + (1 + (1 + s20)), s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s46 :|: s44 >= 0, s44 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s45 >= 0, s45 <= s44 + s21, s46 >= 0, s46 <= 1 + s45 + 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 6 * (z * z) + 8 * z + 3, z >= 0

Function symbols to be analyzed: {SQR}, {terms}, {TERMS}
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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: INF

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

(63) 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: 36 + 74*z + 48*z^2 + 12*z^3

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 2 }-> 1 + s13 + SQR(1 + (z - 2)) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s29 }-> 1 + s30 + SQR(1 + (z - 2)) :|: s28 >= 0, s28 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s29 >= 0, s29 <= s28 + s9, s30 >= 0, s30 <= 1 + s29, s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s32 }-> 1 + s33 + SQR(1 + (z - 2)) :|: s31 >= 0, s31 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s32 >= 0, s32 <= s31 + s11, s33 >= 0, s33 <= 1 + s32, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s35 + z }-> 1 + s36 + s' :|: s34 >= 0, s34 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s35 >= 0, s35 <= s34 + s14, s36 >= 0, s36 <= 1 + s35, s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s38 + z }-> 1 + s39 + s'' :|: s37 >= 0, s37 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s38 >= 0, s38 <= s37 + s16, s39 >= 0, s39 <= 1 + s38, s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 2 }-> 1 + s4 + SQR(0) :|: s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 2 }-> 1 + s5 + SQR(z - 1) :|: s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s43 :|: s41 >= 0, s41 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s42 >= 0, s42 <= s41 + s19, s43 >= 0, s43 <= 1 + s42 + (1 + (1 + s20)), s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s46 :|: s44 >= 0, s44 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s45 >= 0, s45 <= s44 + s21, s46 >= 0, s46 <= 1 + s45 + 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 6 * (z * z) + 8 * z + 3, z >= 0

Function symbols to be analyzed: {terms}, {TERMS}
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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) [36 + 74*z + 48*z^2 + 12*z^3], size: INF

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s13 + s51 :|: s51 >= 0, s51 <= inf2, s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s29 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s30 + s49 :|: s49 >= 0, s49 <= inf'', s28 >= 0, s28 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s29 >= 0, s29 <= s28 + s9, s30 >= 0, s30 <= 1 + s29, s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s32 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s33 + s50 :|: s50 >= 0, s50 <= inf1, s31 >= 0, s31 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s32 >= 0, s32 <= s31 + s11, s33 >= 0, s33 <= 1 + s32, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s35 + z }-> 1 + s36 + s' :|: s34 >= 0, s34 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s35 >= 0, s35 <= s34 + s14, s36 >= 0, s36 <= 1 + s35, s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s38 + z }-> 1 + s39 + s'' :|: s37 >= 0, s37 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s38 >= 0, s38 <= s37 + s16, s39 >= 0, s39 <= 1 + s38, s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 38 }-> 1 + s4 + s48 :|: s48 >= 0, s48 <= inf', s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s5 + s52 :|: s52 >= 0, s52 <= inf3, s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   TERMS(z) -{ 37 + 74*z + 48*z^2 + 12*z^3 }-> 1 + s47 :|: s47 >= 0, s47 <= inf, 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s43 :|: s41 >= 0, s41 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s42 >= 0, s42 <= s41 + s19, s43 >= 0, s43 <= 1 + s42 + (1 + (1 + s20)), s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s46 :|: s44 >= 0, s44 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s45 >= 0, s45 <= s44 + s21, s46 >= 0, s46 <= 1 + s45 + 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 6 * (z * z) + 8 * z + 3, z >= 0

Function symbols to be analyzed: {terms}, {TERMS}
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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) [36 + 74*z + 48*z^2 + 12*z^3], size: INF

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

(67) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s13 + s51 :|: s51 >= 0, s51 <= inf2, s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s29 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s30 + s49 :|: s49 >= 0, s49 <= inf'', s28 >= 0, s28 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s29 >= 0, s29 <= s28 + s9, s30 >= 0, s30 <= 1 + s29, s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s32 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s33 + s50 :|: s50 >= 0, s50 <= inf1, s31 >= 0, s31 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s32 >= 0, s32 <= s31 + s11, s33 >= 0, s33 <= 1 + s32, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s35 + z }-> 1 + s36 + s' :|: s34 >= 0, s34 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s35 >= 0, s35 <= s34 + s14, s36 >= 0, s36 <= 1 + s35, s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s38 + z }-> 1 + s39 + s'' :|: s37 >= 0, s37 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s38 >= 0, s38 <= s37 + s16, s39 >= 0, s39 <= 1 + s38, s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 38 }-> 1 + s4 + s48 :|: s48 >= 0, s48 <= inf', s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s5 + s52 :|: s52 >= 0, s52 <= inf3, s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   TERMS(z) -{ 37 + 74*z + 48*z^2 + 12*z^3 }-> 1 + s47 :|: s47 >= 0, s47 <= inf, 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s43 :|: s41 >= 0, s41 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s42 >= 0, s42 <= s41 + s19, s43 >= 0, s43 <= 1 + s42 + (1 + (1 + s20)), s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s46 :|: s44 >= 0, s44 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s45 >= 0, s45 <= s44 + s21, s46 >= 0, s46 <= 1 + s45 + 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 6 * (z * z) + 8 * z + 3, z >= 0

Function symbols to be analyzed: {terms}, {TERMS}
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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) [36 + 74*z + 48*z^2 + 12*z^3], size: INF
  terms: runtime: ?, size: O(n^2) [5 + 8*z + 6*z^2]

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

(69) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s13 + s51 :|: s51 >= 0, s51 <= inf2, s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s29 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s30 + s49 :|: s49 >= 0, s49 <= inf'', s28 >= 0, s28 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s29 >= 0, s29 <= s28 + s9, s30 >= 0, s30 <= 1 + s29, s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s32 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s33 + s50 :|: s50 >= 0, s50 <= inf1, s31 >= 0, s31 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s32 >= 0, s32 <= s31 + s11, s33 >= 0, s33 <= 1 + s32, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s35 + z }-> 1 + s36 + s' :|: s34 >= 0, s34 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s35 >= 0, s35 <= s34 + s14, s36 >= 0, s36 <= 1 + s35, s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s38 + z }-> 1 + s39 + s'' :|: s37 >= 0, s37 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s38 >= 0, s38 <= s37 + s16, s39 >= 0, s39 <= 1 + s38, s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 38 }-> 1 + s4 + s48 :|: s48 >= 0, s48 <= inf', s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s5 + s52 :|: s52 >= 0, s52 <= inf3, s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   TERMS(z) -{ 37 + 74*z + 48*z^2 + 12*z^3 }-> 1 + s47 :|: s47 >= 0, s47 <= inf, 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s43 :|: s41 >= 0, s41 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s42 >= 0, s42 <= s41 + s19, s43 >= 0, s43 <= 1 + s42 + (1 + (1 + s20)), s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s46 :|: s44 >= 0, s44 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s45 >= 0, s45 <= s44 + s21, s46 >= 0, s46 <= 1 + s45 + 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 6 * (z * z) + 8 * z + 3, z >= 0

Function symbols to be analyzed: {TERMS}
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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) [36 + 74*z + 48*z^2 + 12*z^3], size: INF
  terms: runtime: O(1) [0], size: O(n^2) [5 + 8*z + 6*z^2]

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s13 + s51 :|: s51 >= 0, s51 <= inf2, s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s29 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s30 + s49 :|: s49 >= 0, s49 <= inf'', s28 >= 0, s28 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s29 >= 0, s29 <= s28 + s9, s30 >= 0, s30 <= 1 + s29, s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s32 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s33 + s50 :|: s50 >= 0, s50 <= inf1, s31 >= 0, s31 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s32 >= 0, s32 <= s31 + s11, s33 >= 0, s33 <= 1 + s32, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s35 + z }-> 1 + s36 + s' :|: s34 >= 0, s34 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s35 >= 0, s35 <= s34 + s14, s36 >= 0, s36 <= 1 + s35, s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s38 + z }-> 1 + s39 + s'' :|: s37 >= 0, s37 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s38 >= 0, s38 <= s37 + s16, s39 >= 0, s39 <= 1 + s38, s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 38 }-> 1 + s4 + s48 :|: s48 >= 0, s48 <= inf', s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s5 + s52 :|: s52 >= 0, s52 <= inf3, s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   TERMS(z) -{ 37 + 74*z + 48*z^2 + 12*z^3 }-> 1 + s47 :|: s47 >= 0, s47 <= inf, 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s43 :|: s41 >= 0, s41 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s42 >= 0, s42 <= s41 + s19, s43 >= 0, s43 <= 1 + s42 + (1 + (1 + s20)), s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s46 :|: s44 >= 0, s44 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s45 >= 0, s45 <= s44 + s21, s46 >= 0, s46 <= 1 + s45 + 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 6 * (z * z) + 8 * z + 3, z >= 0

Function symbols to be analyzed: {TERMS}
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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) [36 + 74*z + 48*z^2 + 12*z^3], size: INF
  terms: runtime: O(1) [0], size: O(n^2) [5 + 8*z + 6*z^2]

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

(73) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s13 + s51 :|: s51 >= 0, s51 <= inf2, s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s29 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s30 + s49 :|: s49 >= 0, s49 <= inf'', s28 >= 0, s28 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s29 >= 0, s29 <= s28 + s9, s30 >= 0, s30 <= 1 + s29, s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s32 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s33 + s50 :|: s50 >= 0, s50 <= inf1, s31 >= 0, s31 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s32 >= 0, s32 <= s31 + s11, s33 >= 0, s33 <= 1 + s32, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s35 + z }-> 1 + s36 + s' :|: s34 >= 0, s34 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s35 >= 0, s35 <= s34 + s14, s36 >= 0, s36 <= 1 + s35, s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s38 + z }-> 1 + s39 + s'' :|: s37 >= 0, s37 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s38 >= 0, s38 <= s37 + s16, s39 >= 0, s39 <= 1 + s38, s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 38 }-> 1 + s4 + s48 :|: s48 >= 0, s48 <= inf', s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s5 + s52 :|: s52 >= 0, s52 <= inf3, s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   TERMS(z) -{ 37 + 74*z + 48*z^2 + 12*z^3 }-> 1 + s47 :|: s47 >= 0, s47 <= inf, 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s43 :|: s41 >= 0, s41 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s42 >= 0, s42 <= s41 + s19, s43 >= 0, s43 <= 1 + s42 + (1 + (1 + s20)), s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s46 :|: s44 >= 0, s44 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s45 >= 0, s45 <= s44 + s21, s46 >= 0, s46 <= 1 + s45 + 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 6 * (z * z) + 8 * z + 3, z >= 0

Function symbols to be analyzed: {TERMS}
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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) [36 + 74*z + 48*z^2 + 12*z^3], size: INF
  terms: runtime: O(1) [0], size: O(n^2) [5 + 8*z + 6*z^2]
  TERMS: runtime: ?, size: INF

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

(75) 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: 37 + 74*z + 48*z^2 + 12*z^3

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

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

   ADD(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   ADD(z, z') -{ 1 + z }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1, z' >= 0, z - 1 >= 0
   DBL(z) -{ 1 }-> 0 :|: z = 0
   DBL(z) -{ 1 + z }-> 1 + s3 :|: s3 >= 0, s3 <= z - 1, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 1 :|: z' - 1 >= 0, z - 1 >= 0
   FIRST(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   SQR(z) -{ 1 }-> 0 :|: z = 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s13 + s51 :|: s51 >= 0, s51 <= inf2, s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 0, z - 2 >= 0
   SQR(z) -{ 2 + z }-> 1 + s18 + s1 :|: s17 >= 0, s17 <= 2 * (z - 2), s18 >= 0, s18 <= 0, s1 >= 0, s1 <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s29 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s30 + s49 :|: s49 >= 0, s49 <= inf'', s28 >= 0, s28 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s29 >= 0, s29 <= s28 + s9, s30 >= 0, s30 <= 1 + s29, s9 >= 0, s9 <= 2 * (z - 2), s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 1 + s32 + 14*z + 12*z^2 + 12*z^3 }-> 1 + s33 + s50 :|: s50 >= 0, s50 <= inf1, s31 >= 0, s31 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s32 >= 0, s32 <= s31 + s11, s33 >= 0, s33 <= 1 + s32, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s35 + z }-> 1 + s36 + s' :|: s34 >= 0, s34 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s35 >= 0, s35 <= s34 + s14, s36 >= 0, s36 <= 1 + s35, s14 >= 0, s14 <= 2 * (z - 2), s15 >= 0, s15 <= 2 * (z - 2), s' >= 0, s' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 3 + s38 + z }-> 1 + s39 + s'' :|: s37 >= 0, s37 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s38 >= 0, s38 <= s37 + s16, s39 >= 0, s39 <= 1 + s38, s16 >= 0, s16 <= 2 * (z - 2), s'' >= 0, s'' <= 1 + (z - 2), z - 2 >= 0
   SQR(z) -{ 38 }-> 1 + s4 + s48 :|: s48 >= 0, s48 <= inf', s4 >= 0, s4 <= 0, z = 1 + 0
   SQR(z) -{ 14*z + 12*z^2 + 12*z^3 }-> 1 + s5 + s52 :|: s52 >= 0, s52 <= inf3, s5 >= 0, s5 <= 0, z - 1 >= 0
   SQR(z) -{ 3 }-> 1 + s6 + s :|: s6 >= 0, s6 <= 0, s >= 0, s <= 0, z = 1 + 0
   SQR(z) -{ 2 + z }-> 1 + s7 + s2 :|: s7 >= 0, s7 <= 0, s2 >= 0, s2 <= z - 1, z - 1 >= 0
   TERMS(z) -{ 37 + 74*z + 48*z^2 + 12*z^3 }-> 1 + s47 :|: s47 >= 0, s47 <= inf, 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 + s27 :|: s27 >= 0, s27 <= 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 + s23) :|: s23 >= 0, s23 <= 2 * (z - 1), z - 1 >= 0
   first(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   first(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   first(z, z') -{ 0 }-> 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 0 :|: z = 0
   sqr(z) -{ 0 }-> 0 :|: z >= 0
   sqr(z) -{ 0 }-> 1 + s24 :|: s24 >= 0, s24 <= 0 + 0, z = 1 + 0
   sqr(z) -{ 0 }-> 1 + s25 :|: s25 >= 0, s25 <= 0 + (1 + (1 + s22)), s22 >= 0, s22 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s26 :|: s26 >= 0, s26 <= 0 + 0, z - 1 >= 0
   sqr(z) -{ 0 }-> 1 + s43 :|: s41 >= 0, s41 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s42 >= 0, s42 <= s41 + s19, s43 >= 0, s43 <= 1 + s42 + (1 + (1 + s20)), s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0
   sqr(z) -{ 0 }-> 1 + s46 :|: s44 >= 0, s44 <= 6 * ((z - 2) * (z - 2)) + 8 * (z - 2) + 3, s45 >= 0, s45 <= s44 + s21, s46 >= 0, s46 <= 1 + s45 + 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0
   terms(z) -{ 0 }-> 0 :|: z >= 0
   terms(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 6 * (z * z) + 8 * z + 3, z >= 0

Function symbols to be analyzed: 
Previous analysis results are:
  DBL: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  FIRST: runtime: O(1) [1], size: O(1) [1]
  ADD: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  first: runtime: O(1) [0], size: O(n^1) [z']
  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) [36 + 74*z + 48*z^2 + 12*z^3], size: INF
  terms: runtime: O(1) [0], size: O(n^2) [5 + 8*z + 6*z^2]
  TERMS: runtime: O(n^3) [37 + 74*z + 48*z^2 + 12*z^3], size: INF

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

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

(78)
BOUNDS(1, n^3)

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

(79) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

   TERMS(z0) -> c(SQR(z0))
   SQR(0') -> c1
   SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(0') -> c4
   DBL(s(z0)) -> c5(DBL(z0))
   ADD(0', z0) -> c6
   ADD(s(z0), z1) -> c7(ADD(z0, z1))
   FIRST(0', z0) -> c8
   FIRST(s(z0), cons(z1)) -> c9

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

   terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

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

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

(82)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
SQR(0') -> c1
SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c4
DBL(s(z0)) -> c5(DBL(z0))
ADD(0', z0) -> c6
ADD(s(z0), z1) -> c7(ADD(z0, z1))
FIRST(0', z0) -> c8
FIRST(s(z0), cons(z1)) -> c9
terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

Types:
TERMS :: 0':s -> c
c :: c1:c2:c3 -> c
SQR :: 0':s -> c1:c2:c3
0' :: 0':s
c1 :: c1:c2:c3
s :: 0':s -> 0':s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0':s -> 0':s -> c6:c7
sqr :: 0':s -> 0':s
dbl :: 0':s -> 0':s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0':s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0':s -> cons:nil
recip :: 0':s -> recip
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_10 :: c
hole_0':s2_10 :: 0':s
hole_c1:c2:c33_10 :: c1:c2:c3
hole_c6:c74_10 :: c6:c7
hole_c4:c55_10 :: c4:c5
hole_c8:c96_10 :: c8:c9
hole_cons:nil7_10 :: cons:nil
hole_recip8_10 :: recip
gen_0':s9_10 :: Nat -> 0':s
gen_c1:c2:c310_10 :: Nat -> c1:c2:c3
gen_c6:c711_10 :: Nat -> c6:c7
gen_c4:c512_10 :: Nat -> c4:c5

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

(83) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
SQR, ADD, sqr, dbl, DBL, add

They will be analysed ascendingly in the following order:
ADD < SQR
sqr < SQR
dbl < SQR
DBL < SQR
dbl < sqr
add < sqr

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

(84)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
SQR(0') -> c1
SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c4
DBL(s(z0)) -> c5(DBL(z0))
ADD(0', z0) -> c6
ADD(s(z0), z1) -> c7(ADD(z0, z1))
FIRST(0', z0) -> c8
FIRST(s(z0), cons(z1)) -> c9
terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

Types:
TERMS :: 0':s -> c
c :: c1:c2:c3 -> c
SQR :: 0':s -> c1:c2:c3
0' :: 0':s
c1 :: c1:c2:c3
s :: 0':s -> 0':s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0':s -> 0':s -> c6:c7
sqr :: 0':s -> 0':s
dbl :: 0':s -> 0':s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0':s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0':s -> cons:nil
recip :: 0':s -> recip
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_10 :: c
hole_0':s2_10 :: 0':s
hole_c1:c2:c33_10 :: c1:c2:c3
hole_c6:c74_10 :: c6:c7
hole_c4:c55_10 :: c4:c5
hole_c8:c96_10 :: c8:c9
hole_cons:nil7_10 :: cons:nil
hole_recip8_10 :: recip
gen_0':s9_10 :: Nat -> 0':s
gen_c1:c2:c310_10 :: Nat -> c1:c2:c3
gen_c6:c711_10 :: Nat -> c6:c7
gen_c4:c512_10 :: Nat -> c4:c5


Generator Equations:
gen_0':s9_10(0) <=> 0'
gen_0':s9_10(+(x, 1)) <=> s(gen_0':s9_10(x))
gen_c1:c2:c310_10(0) <=> c1
gen_c1:c2:c310_10(+(x, 1)) <=> c2(c6, gen_c1:c2:c310_10(x))
gen_c6:c711_10(0) <=> c6
gen_c6:c711_10(+(x, 1)) <=> c7(gen_c6:c711_10(x))
gen_c4:c512_10(0) <=> c4
gen_c4:c512_10(+(x, 1)) <=> c5(gen_c4:c512_10(x))


The following defined symbols remain to be analysed:
ADD, SQR, sqr, dbl, DBL, add

They will be analysed ascendingly in the following order:
ADD < SQR
sqr < SQR
dbl < SQR
DBL < SQR
dbl < sqr
add < sqr

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

(85) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ADD(gen_0':s9_10(n14_10), gen_0':s9_10(b)) -> gen_c6:c711_10(n14_10), rt in Omega(1 + n14_10)

Induction Base:
ADD(gen_0':s9_10(0), gen_0':s9_10(b)) ->_R^Omega(1)
c6

Induction Step:
ADD(gen_0':s9_10(+(n14_10, 1)), gen_0':s9_10(b)) ->_R^Omega(1)
c7(ADD(gen_0':s9_10(n14_10), gen_0':s9_10(b))) ->_IH
c7(gen_c6:c711_10(c15_10))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(86)
Complex Obligation (BEST)

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

(87)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
SQR(0') -> c1
SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c4
DBL(s(z0)) -> c5(DBL(z0))
ADD(0', z0) -> c6
ADD(s(z0), z1) -> c7(ADD(z0, z1))
FIRST(0', z0) -> c8
FIRST(s(z0), cons(z1)) -> c9
terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

Types:
TERMS :: 0':s -> c
c :: c1:c2:c3 -> c
SQR :: 0':s -> c1:c2:c3
0' :: 0':s
c1 :: c1:c2:c3
s :: 0':s -> 0':s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0':s -> 0':s -> c6:c7
sqr :: 0':s -> 0':s
dbl :: 0':s -> 0':s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0':s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0':s -> cons:nil
recip :: 0':s -> recip
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_10 :: c
hole_0':s2_10 :: 0':s
hole_c1:c2:c33_10 :: c1:c2:c3
hole_c6:c74_10 :: c6:c7
hole_c4:c55_10 :: c4:c5
hole_c8:c96_10 :: c8:c9
hole_cons:nil7_10 :: cons:nil
hole_recip8_10 :: recip
gen_0':s9_10 :: Nat -> 0':s
gen_c1:c2:c310_10 :: Nat -> c1:c2:c3
gen_c6:c711_10 :: Nat -> c6:c7
gen_c4:c512_10 :: Nat -> c4:c5


Generator Equations:
gen_0':s9_10(0) <=> 0'
gen_0':s9_10(+(x, 1)) <=> s(gen_0':s9_10(x))
gen_c1:c2:c310_10(0) <=> c1
gen_c1:c2:c310_10(+(x, 1)) <=> c2(c6, gen_c1:c2:c310_10(x))
gen_c6:c711_10(0) <=> c6
gen_c6:c711_10(+(x, 1)) <=> c7(gen_c6:c711_10(x))
gen_c4:c512_10(0) <=> c4
gen_c4:c512_10(+(x, 1)) <=> c5(gen_c4:c512_10(x))


The following defined symbols remain to be analysed:
ADD, SQR, sqr, dbl, DBL, add

They will be analysed ascendingly in the following order:
ADD < SQR
sqr < SQR
dbl < SQR
DBL < SQR
dbl < sqr
add < sqr

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

(88) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(89)
BOUNDS(n^1, INF)

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

(90)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
SQR(0') -> c1
SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c4
DBL(s(z0)) -> c5(DBL(z0))
ADD(0', z0) -> c6
ADD(s(z0), z1) -> c7(ADD(z0, z1))
FIRST(0', z0) -> c8
FIRST(s(z0), cons(z1)) -> c9
terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

Types:
TERMS :: 0':s -> c
c :: c1:c2:c3 -> c
SQR :: 0':s -> c1:c2:c3
0' :: 0':s
c1 :: c1:c2:c3
s :: 0':s -> 0':s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0':s -> 0':s -> c6:c7
sqr :: 0':s -> 0':s
dbl :: 0':s -> 0':s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0':s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0':s -> cons:nil
recip :: 0':s -> recip
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_10 :: c
hole_0':s2_10 :: 0':s
hole_c1:c2:c33_10 :: c1:c2:c3
hole_c6:c74_10 :: c6:c7
hole_c4:c55_10 :: c4:c5
hole_c8:c96_10 :: c8:c9
hole_cons:nil7_10 :: cons:nil
hole_recip8_10 :: recip
gen_0':s9_10 :: Nat -> 0':s
gen_c1:c2:c310_10 :: Nat -> c1:c2:c3
gen_c6:c711_10 :: Nat -> c6:c7
gen_c4:c512_10 :: Nat -> c4:c5


Lemmas:
ADD(gen_0':s9_10(n14_10), gen_0':s9_10(b)) -> gen_c6:c711_10(n14_10), rt in Omega(1 + n14_10)


Generator Equations:
gen_0':s9_10(0) <=> 0'
gen_0':s9_10(+(x, 1)) <=> s(gen_0':s9_10(x))
gen_c1:c2:c310_10(0) <=> c1
gen_c1:c2:c310_10(+(x, 1)) <=> c2(c6, gen_c1:c2:c310_10(x))
gen_c6:c711_10(0) <=> c6
gen_c6:c711_10(+(x, 1)) <=> c7(gen_c6:c711_10(x))
gen_c4:c512_10(0) <=> c4
gen_c4:c512_10(+(x, 1)) <=> c5(gen_c4:c512_10(x))


The following defined symbols remain to be analysed:
dbl, SQR, sqr, DBL, add

They will be analysed ascendingly in the following order:
sqr < SQR
dbl < SQR
DBL < SQR
dbl < sqr
add < sqr

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

(91) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
dbl(gen_0':s9_10(n602_10)) -> gen_0':s9_10(*(2, n602_10)), rt in Omega(0)

Induction Base:
dbl(gen_0':s9_10(0)) ->_R^Omega(0)
0'

Induction Step:
dbl(gen_0':s9_10(+(n602_10, 1))) ->_R^Omega(0)
s(s(dbl(gen_0':s9_10(n602_10)))) ->_IH
s(s(gen_0':s9_10(*(2, c603_10))))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(92)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
SQR(0') -> c1
SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c4
DBL(s(z0)) -> c5(DBL(z0))
ADD(0', z0) -> c6
ADD(s(z0), z1) -> c7(ADD(z0, z1))
FIRST(0', z0) -> c8
FIRST(s(z0), cons(z1)) -> c9
terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

Types:
TERMS :: 0':s -> c
c :: c1:c2:c3 -> c
SQR :: 0':s -> c1:c2:c3
0' :: 0':s
c1 :: c1:c2:c3
s :: 0':s -> 0':s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0':s -> 0':s -> c6:c7
sqr :: 0':s -> 0':s
dbl :: 0':s -> 0':s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0':s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0':s -> cons:nil
recip :: 0':s -> recip
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_10 :: c
hole_0':s2_10 :: 0':s
hole_c1:c2:c33_10 :: c1:c2:c3
hole_c6:c74_10 :: c6:c7
hole_c4:c55_10 :: c4:c5
hole_c8:c96_10 :: c8:c9
hole_cons:nil7_10 :: cons:nil
hole_recip8_10 :: recip
gen_0':s9_10 :: Nat -> 0':s
gen_c1:c2:c310_10 :: Nat -> c1:c2:c3
gen_c6:c711_10 :: Nat -> c6:c7
gen_c4:c512_10 :: Nat -> c4:c5


Lemmas:
ADD(gen_0':s9_10(n14_10), gen_0':s9_10(b)) -> gen_c6:c711_10(n14_10), rt in Omega(1 + n14_10)
dbl(gen_0':s9_10(n602_10)) -> gen_0':s9_10(*(2, n602_10)), rt in Omega(0)


Generator Equations:
gen_0':s9_10(0) <=> 0'
gen_0':s9_10(+(x, 1)) <=> s(gen_0':s9_10(x))
gen_c1:c2:c310_10(0) <=> c1
gen_c1:c2:c310_10(+(x, 1)) <=> c2(c6, gen_c1:c2:c310_10(x))
gen_c6:c711_10(0) <=> c6
gen_c6:c711_10(+(x, 1)) <=> c7(gen_c6:c711_10(x))
gen_c4:c512_10(0) <=> c4
gen_c4:c512_10(+(x, 1)) <=> c5(gen_c4:c512_10(x))


The following defined symbols remain to be analysed:
DBL, SQR, sqr, add

They will be analysed ascendingly in the following order:
sqr < SQR
DBL < SQR
add < sqr

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

(93) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DBL(gen_0':s9_10(n934_10)) -> gen_c4:c512_10(n934_10), rt in Omega(1 + n934_10)

Induction Base:
DBL(gen_0':s9_10(0)) ->_R^Omega(1)
c4

Induction Step:
DBL(gen_0':s9_10(+(n934_10, 1))) ->_R^Omega(1)
c5(DBL(gen_0':s9_10(n934_10))) ->_IH
c5(gen_c4:c512_10(c935_10))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(94)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
SQR(0') -> c1
SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c4
DBL(s(z0)) -> c5(DBL(z0))
ADD(0', z0) -> c6
ADD(s(z0), z1) -> c7(ADD(z0, z1))
FIRST(0', z0) -> c8
FIRST(s(z0), cons(z1)) -> c9
terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

Types:
TERMS :: 0':s -> c
c :: c1:c2:c3 -> c
SQR :: 0':s -> c1:c2:c3
0' :: 0':s
c1 :: c1:c2:c3
s :: 0':s -> 0':s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0':s -> 0':s -> c6:c7
sqr :: 0':s -> 0':s
dbl :: 0':s -> 0':s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0':s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0':s -> cons:nil
recip :: 0':s -> recip
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_10 :: c
hole_0':s2_10 :: 0':s
hole_c1:c2:c33_10 :: c1:c2:c3
hole_c6:c74_10 :: c6:c7
hole_c4:c55_10 :: c4:c5
hole_c8:c96_10 :: c8:c9
hole_cons:nil7_10 :: cons:nil
hole_recip8_10 :: recip
gen_0':s9_10 :: Nat -> 0':s
gen_c1:c2:c310_10 :: Nat -> c1:c2:c3
gen_c6:c711_10 :: Nat -> c6:c7
gen_c4:c512_10 :: Nat -> c4:c5


Lemmas:
ADD(gen_0':s9_10(n14_10), gen_0':s9_10(b)) -> gen_c6:c711_10(n14_10), rt in Omega(1 + n14_10)
dbl(gen_0':s9_10(n602_10)) -> gen_0':s9_10(*(2, n602_10)), rt in Omega(0)
DBL(gen_0':s9_10(n934_10)) -> gen_c4:c512_10(n934_10), rt in Omega(1 + n934_10)


Generator Equations:
gen_0':s9_10(0) <=> 0'
gen_0':s9_10(+(x, 1)) <=> s(gen_0':s9_10(x))
gen_c1:c2:c310_10(0) <=> c1
gen_c1:c2:c310_10(+(x, 1)) <=> c2(c6, gen_c1:c2:c310_10(x))
gen_c6:c711_10(0) <=> c6
gen_c6:c711_10(+(x, 1)) <=> c7(gen_c6:c711_10(x))
gen_c4:c512_10(0) <=> c4
gen_c4:c512_10(+(x, 1)) <=> c5(gen_c4:c512_10(x))


The following defined symbols remain to be analysed:
add, SQR, sqr

They will be analysed ascendingly in the following order:
sqr < SQR
add < sqr

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

(95) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
add(gen_0':s9_10(n1310_10), gen_0':s9_10(b)) -> gen_0':s9_10(+(n1310_10, b)), rt in Omega(0)

Induction Base:
add(gen_0':s9_10(0), gen_0':s9_10(b)) ->_R^Omega(0)
gen_0':s9_10(b)

Induction Step:
add(gen_0':s9_10(+(n1310_10, 1)), gen_0':s9_10(b)) ->_R^Omega(0)
s(add(gen_0':s9_10(n1310_10), gen_0':s9_10(b))) ->_IH
s(gen_0':s9_10(+(b, c1311_10)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(96)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
SQR(0') -> c1
SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c4
DBL(s(z0)) -> c5(DBL(z0))
ADD(0', z0) -> c6
ADD(s(z0), z1) -> c7(ADD(z0, z1))
FIRST(0', z0) -> c8
FIRST(s(z0), cons(z1)) -> c9
terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

Types:
TERMS :: 0':s -> c
c :: c1:c2:c3 -> c
SQR :: 0':s -> c1:c2:c3
0' :: 0':s
c1 :: c1:c2:c3
s :: 0':s -> 0':s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0':s -> 0':s -> c6:c7
sqr :: 0':s -> 0':s
dbl :: 0':s -> 0':s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0':s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0':s -> cons:nil
recip :: 0':s -> recip
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_10 :: c
hole_0':s2_10 :: 0':s
hole_c1:c2:c33_10 :: c1:c2:c3
hole_c6:c74_10 :: c6:c7
hole_c4:c55_10 :: c4:c5
hole_c8:c96_10 :: c8:c9
hole_cons:nil7_10 :: cons:nil
hole_recip8_10 :: recip
gen_0':s9_10 :: Nat -> 0':s
gen_c1:c2:c310_10 :: Nat -> c1:c2:c3
gen_c6:c711_10 :: Nat -> c6:c7
gen_c4:c512_10 :: Nat -> c4:c5


Lemmas:
ADD(gen_0':s9_10(n14_10), gen_0':s9_10(b)) -> gen_c6:c711_10(n14_10), rt in Omega(1 + n14_10)
dbl(gen_0':s9_10(n602_10)) -> gen_0':s9_10(*(2, n602_10)), rt in Omega(0)
DBL(gen_0':s9_10(n934_10)) -> gen_c4:c512_10(n934_10), rt in Omega(1 + n934_10)
add(gen_0':s9_10(n1310_10), gen_0':s9_10(b)) -> gen_0':s9_10(+(n1310_10, b)), rt in Omega(0)


Generator Equations:
gen_0':s9_10(0) <=> 0'
gen_0':s9_10(+(x, 1)) <=> s(gen_0':s9_10(x))
gen_c1:c2:c310_10(0) <=> c1
gen_c1:c2:c310_10(+(x, 1)) <=> c2(c6, gen_c1:c2:c310_10(x))
gen_c6:c711_10(0) <=> c6
gen_c6:c711_10(+(x, 1)) <=> c7(gen_c6:c711_10(x))
gen_c4:c512_10(0) <=> c4
gen_c4:c512_10(+(x, 1)) <=> c5(gen_c4:c512_10(x))


The following defined symbols remain to be analysed:
sqr, SQR

They will be analysed ascendingly in the following order:
sqr < SQR

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

(97) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sqr(gen_0':s9_10(n2387_10)) -> gen_0':s9_10(*(n2387_10, n2387_10)), rt in Omega(0)

Induction Base:
sqr(gen_0':s9_10(0)) ->_R^Omega(0)
0'

Induction Step:
sqr(gen_0':s9_10(+(n2387_10, 1))) ->_R^Omega(0)
s(add(sqr(gen_0':s9_10(n2387_10)), dbl(gen_0':s9_10(n2387_10)))) ->_IH
s(add(gen_0':s9_10(*(c2388_10, c2388_10)), dbl(gen_0':s9_10(n2387_10)))) ->_L^Omega(0)
s(add(gen_0':s9_10(*(n2387_10, n2387_10)), gen_0':s9_10(*(2, n2387_10)))) ->_L^Omega(0)
s(gen_0':s9_10(+(*(n2387_10, n2387_10), *(2, n2387_10))))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(98)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
SQR(0') -> c1
SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c4
DBL(s(z0)) -> c5(DBL(z0))
ADD(0', z0) -> c6
ADD(s(z0), z1) -> c7(ADD(z0, z1))
FIRST(0', z0) -> c8
FIRST(s(z0), cons(z1)) -> c9
terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

Types:
TERMS :: 0':s -> c
c :: c1:c2:c3 -> c
SQR :: 0':s -> c1:c2:c3
0' :: 0':s
c1 :: c1:c2:c3
s :: 0':s -> 0':s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0':s -> 0':s -> c6:c7
sqr :: 0':s -> 0':s
dbl :: 0':s -> 0':s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0':s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0':s -> cons:nil
recip :: 0':s -> recip
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_10 :: c
hole_0':s2_10 :: 0':s
hole_c1:c2:c33_10 :: c1:c2:c3
hole_c6:c74_10 :: c6:c7
hole_c4:c55_10 :: c4:c5
hole_c8:c96_10 :: c8:c9
hole_cons:nil7_10 :: cons:nil
hole_recip8_10 :: recip
gen_0':s9_10 :: Nat -> 0':s
gen_c1:c2:c310_10 :: Nat -> c1:c2:c3
gen_c6:c711_10 :: Nat -> c6:c7
gen_c4:c512_10 :: Nat -> c4:c5


Lemmas:
ADD(gen_0':s9_10(n14_10), gen_0':s9_10(b)) -> gen_c6:c711_10(n14_10), rt in Omega(1 + n14_10)
dbl(gen_0':s9_10(n602_10)) -> gen_0':s9_10(*(2, n602_10)), rt in Omega(0)
DBL(gen_0':s9_10(n934_10)) -> gen_c4:c512_10(n934_10), rt in Omega(1 + n934_10)
add(gen_0':s9_10(n1310_10), gen_0':s9_10(b)) -> gen_0':s9_10(+(n1310_10, b)), rt in Omega(0)
sqr(gen_0':s9_10(n2387_10)) -> gen_0':s9_10(*(n2387_10, n2387_10)), rt in Omega(0)


Generator Equations:
gen_0':s9_10(0) <=> 0'
gen_0':s9_10(+(x, 1)) <=> s(gen_0':s9_10(x))
gen_c1:c2:c310_10(0) <=> c1
gen_c1:c2:c310_10(+(x, 1)) <=> c2(c6, gen_c1:c2:c310_10(x))
gen_c6:c711_10(0) <=> c6
gen_c6:c711_10(+(x, 1)) <=> c7(gen_c6:c711_10(x))
gen_c4:c512_10(0) <=> c4
gen_c4:c512_10(+(x, 1)) <=> c5(gen_c4:c512_10(x))


The following defined symbols remain to be analysed:
SQR
----------------------------------------

(99) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SQR(gen_0':s9_10(n2856_10)) -> *13_10, rt in Omega(n2856_10 + n2856_10^3)

Induction Base:
SQR(gen_0':s9_10(0))

Induction Step:
SQR(gen_0':s9_10(+(n2856_10, 1))) ->_R^Omega(1)
c2(ADD(sqr(gen_0':s9_10(n2856_10)), dbl(gen_0':s9_10(n2856_10))), SQR(gen_0':s9_10(n2856_10))) ->_L^Omega(0)
c2(ADD(gen_0':s9_10(*(n2856_10, n2856_10)), dbl(gen_0':s9_10(n2856_10))), SQR(gen_0':s9_10(n2856_10))) ->_L^Omega(0)
c2(ADD(gen_0':s9_10(*(n2856_10, n2856_10)), gen_0':s9_10(*(2, n2856_10))), SQR(gen_0':s9_10(n2856_10))) ->_L^Omega(1 + n2856_10^2)
c2(gen_c6:c711_10(*(n2856_10, n2856_10)), SQR(gen_0':s9_10(n2856_10))) ->_IH
c2(gen_c6:c711_10(*(n2856_10, n2856_10)), *13_10)

We have rt in Omega(n^3) and sz in O(n). Thus, we have irc_R in Omega(n^3).
----------------------------------------

(100)
Obligation:
Proved the lower bound n^3 for the following obligation:

Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
SQR(0') -> c1
SQR(s(z0)) -> c2(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c4
DBL(s(z0)) -> c5(DBL(z0))
ADD(0', z0) -> c6
ADD(s(z0), z1) -> c7(ADD(z0, z1))
FIRST(0', z0) -> c8
FIRST(s(z0), cons(z1)) -> c9
terms(z0) -> cons(recip(sqr(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)) -> cons(z1)

Types:
TERMS :: 0':s -> c
c :: c1:c2:c3 -> c
SQR :: 0':s -> c1:c2:c3
0' :: 0':s
c1 :: c1:c2:c3
s :: 0':s -> 0':s
c2 :: c6:c7 -> c1:c2:c3 -> c1:c2:c3
ADD :: 0':s -> 0':s -> c6:c7
sqr :: 0':s -> 0':s
dbl :: 0':s -> 0':s
c3 :: c6:c7 -> c4:c5 -> c1:c2:c3
DBL :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
FIRST :: 0':s -> cons:nil -> c8:c9
c8 :: c8:c9
cons :: recip -> cons:nil
c9 :: c8:c9
terms :: 0':s -> cons:nil
recip :: 0':s -> recip
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_10 :: c
hole_0':s2_10 :: 0':s
hole_c1:c2:c33_10 :: c1:c2:c3
hole_c6:c74_10 :: c6:c7
hole_c4:c55_10 :: c4:c5
hole_c8:c96_10 :: c8:c9
hole_cons:nil7_10 :: cons:nil
hole_recip8_10 :: recip
gen_0':s9_10 :: Nat -> 0':s
gen_c1:c2:c310_10 :: Nat -> c1:c2:c3
gen_c6:c711_10 :: Nat -> c6:c7
gen_c4:c512_10 :: Nat -> c4:c5


Lemmas:
ADD(gen_0':s9_10(n14_10), gen_0':s9_10(b)) -> gen_c6:c711_10(n14_10), rt in Omega(1 + n14_10)
dbl(gen_0':s9_10(n602_10)) -> gen_0':s9_10(*(2, n602_10)), rt in Omega(0)
DBL(gen_0':s9_10(n934_10)) -> gen_c4:c512_10(n934_10), rt in Omega(1 + n934_10)
add(gen_0':s9_10(n1310_10), gen_0':s9_10(b)) -> gen_0':s9_10(+(n1310_10, b)), rt in Omega(0)
sqr(gen_0':s9_10(n2387_10)) -> gen_0':s9_10(*(n2387_10, n2387_10)), rt in Omega(0)


Generator Equations:
gen_0':s9_10(0) <=> 0'
gen_0':s9_10(+(x, 1)) <=> s(gen_0':s9_10(x))
gen_c1:c2:c310_10(0) <=> c1
gen_c1:c2:c310_10(+(x, 1)) <=> c2(c6, gen_c1:c2:c310_10(x))
gen_c6:c711_10(0) <=> c6
gen_c6:c711_10(+(x, 1)) <=> c7(gen_c6:c711_10(x))
gen_c4:c512_10(0) <=> c4
gen_c4:c512_10(+(x, 1)) <=> c5(gen_c4:c512_10(x))


The following defined symbols remain to be analysed:
SQR
----------------------------------------

(101) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(102)
BOUNDS(n^3, INF)