WORST_CASE(Omega(n^1),O(n^2))
proof of /export/starexec/sandbox/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^1, n^2).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 219 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), 7 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), 398 ms]
    (20) CpxRNTS
    (21) IntTrsBoundProof [UPPER BOUND(ID), 20 ms]
    (22) CpxRNTS
    (23) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (24) CpxRNTS
    (25) IntTrsBoundProof [UPPER BOUND(ID), 245 ms]
    (26) CpxRNTS
    (27) IntTrsBoundProof [UPPER BOUND(ID), 66 ms]
    (28) CpxRNTS
    (29) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (30) CpxRNTS
    (31) IntTrsBoundProof [UPPER BOUND(ID), 2048 ms]
    (32) CpxRNTS
    (33) IntTrsBoundProof [UPPER BOUND(ID), 617 ms]
    (34) CpxRNTS
    (35) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (36) CpxRNTS
    (37) IntTrsBoundProof [UPPER BOUND(ID), 6882 ms]
    (38) CpxRNTS
    (39) IntTrsBoundProof [UPPER BOUND(ID), 2335 ms]
    (40) CpxRNTS
    (41) FinalProof [FINISHED, 0 ms]
    (42) BOUNDS(1, n^2)
(43) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(44) CpxRelTRS
    (45) SlicingProof [LOWER BOUND(ID), 0 ms]
    (46) CpxRelTRS
    (47) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (48) typed CpxTrs
    (49) OrderProof [LOWER BOUND(ID), 7 ms]
    (50) typed CpxTrs
    (51) RewriteLemmaProof [LOWER BOUND(ID), 301 ms]
    (52) BEST
        (53) proven lower bound
            (54) LowerBoundPropagationProof [FINISHED, 0 ms]
            (55) BOUNDS(n^1, INF)
        (56) typed CpxTrs
            (57) RewriteLemmaProof [LOWER BOUND(ID), 89 ms]
            (58) typed CpxTrs
            (59) RewriteLemmaProof [LOWER BOUND(ID), 163 ms]
            (60) typed CpxTrs
            (61) RewriteLemmaProof [LOWER BOUND(ID), 31 ms]
            (62) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   CONCAT(leaf, z0) -> c
   CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2))
   LESSLEAVES(z0, leaf) -> c2
   LESSLEAVES(leaf, cons(z0, z1)) -> c3
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1))
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3))

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

   concat(leaf, z0) -> z0
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
   lessleaves(z0, leaf) -> false
   lessleaves(leaf, cons(z0, z1)) -> true
   lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3))

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^1, n^2).


The TRS R consists of the following rules:

   CONCAT(leaf, z0) -> c
   CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2))
   LESSLEAVES(z0, leaf) -> c2
   LESSLEAVES(leaf, cons(z0, z1)) -> c3
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1))
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3))

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

   concat(leaf, z0) -> z0
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
   lessleaves(z0, leaf) -> false
   lessleaves(leaf, cons(z0, z1)) -> true
   lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3))

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^2).


The TRS R consists of the following rules:

   CONCAT(leaf, z0) -> c [1]
   CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) [1]
   LESSLEAVES(z0, leaf) -> c2 [1]
   LESSLEAVES(leaf, cons(z0, z1)) -> c3 [1]
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) [1]
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) [1]
   concat(leaf, z0) -> z0 [0]
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) [0]
   lessleaves(z0, leaf) -> false [0]
   lessleaves(leaf, cons(z0, z1)) -> true [0]
   lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) [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:

   CONCAT(leaf, z0) -> c [1]
   CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) [1]
   LESSLEAVES(z0, leaf) -> c2 [1]
   LESSLEAVES(leaf, cons(z0, z1)) -> c3 [1]
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) [1]
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) [1]
   concat(leaf, z0) -> z0 [0]
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) [0]
   lessleaves(z0, leaf) -> false [0]
   lessleaves(leaf, cons(z0, z1)) -> true [0]
   lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) [0]

The TRS has the following type information:
CONCAT :: leaf:cons -> leaf:cons -> c:c1
leaf :: leaf:cons
c :: c:c1
cons :: leaf:cons -> leaf:cons -> leaf:cons
c1 :: c:c1 -> c:c1
LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5
c2 :: c2:c3:c4:c5
c3 :: c2:c3:c4:c5
c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
concat :: leaf:cons -> leaf:cons -> leaf:cons
c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
lessleaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true

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:

   CONCAT_2
   LESSLEAVES_2

(c) The following functions are completely defined:

   concat_2
   lessleaves_2

Due to the following rules being added:

   concat(v0, v1) -> leaf [0]
   lessleaves(v0, v1) -> null_lessleaves [0]

And the following fresh constants:    null_lessleaves

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

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

   CONCAT(leaf, z0) -> c [1]
   CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) [1]
   LESSLEAVES(z0, leaf) -> c2 [1]
   LESSLEAVES(leaf, cons(z0, z1)) -> c3 [1]
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) [1]
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) [1]
   concat(leaf, z0) -> z0 [0]
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) [0]
   lessleaves(z0, leaf) -> false [0]
   lessleaves(leaf, cons(z0, z1)) -> true [0]
   lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) [0]
   concat(v0, v1) -> leaf [0]
   lessleaves(v0, v1) -> null_lessleaves [0]

The TRS has the following type information:
CONCAT :: leaf:cons -> leaf:cons -> c:c1
leaf :: leaf:cons
c :: c:c1
cons :: leaf:cons -> leaf:cons -> leaf:cons
c1 :: c:c1 -> c:c1
LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5
c2 :: c2:c3:c4:c5
c3 :: c2:c3:c4:c5
c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
concat :: leaf:cons -> leaf:cons -> leaf:cons
c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
lessleaves :: leaf:cons -> leaf:cons -> false:true:null_lessleaves
false :: false:true:null_lessleaves
true :: false:true:null_lessleaves
null_lessleaves :: false:true:null_lessleaves

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:

   CONCAT(leaf, z0) -> c [1]
   CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) [1]
   LESSLEAVES(z0, leaf) -> c2 [1]
   LESSLEAVES(leaf, cons(z0, z1)) -> c3 [1]
   LESSLEAVES(cons(leaf, z1), cons(leaf, z3)) -> c4(LESSLEAVES(z1, z3), CONCAT(leaf, z1)) [1]
   LESSLEAVES(cons(leaf, z1), cons(cons(z0'', z1''), z3)) -> c4(LESSLEAVES(z1, cons(z0'', concat(z1'', z3))), CONCAT(leaf, z1)) [1]
   LESSLEAVES(cons(leaf, z1), cons(z2, z3)) -> c4(LESSLEAVES(z1, leaf), CONCAT(leaf, z1)) [1]
   LESSLEAVES(cons(cons(z0', z1'), z1), cons(leaf, z3)) -> c4(LESSLEAVES(cons(z0', concat(z1', z1)), z3), CONCAT(cons(z0', z1'), z1)) [1]
   LESSLEAVES(cons(cons(z0', z1'), z1), cons(cons(z01, z11), z3)) -> c4(LESSLEAVES(cons(z0', concat(z1', z1)), cons(z01, concat(z11, z3))), CONCAT(cons(z0', z1'), z1)) [1]
   LESSLEAVES(cons(cons(z0', z1'), z1), cons(z2, z3)) -> c4(LESSLEAVES(cons(z0', concat(z1', z1)), leaf), CONCAT(cons(z0', z1'), z1)) [1]
   LESSLEAVES(cons(z0, z1), cons(leaf, z3)) -> c4(LESSLEAVES(leaf, z3), CONCAT(z0, z1)) [1]
   LESSLEAVES(cons(z0, z1), cons(cons(z02, z12), z3)) -> c4(LESSLEAVES(leaf, cons(z02, concat(z12, z3))), CONCAT(z0, z1)) [1]
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(leaf, leaf), CONCAT(z0, z1)) [1]
   LESSLEAVES(cons(leaf, z1), cons(leaf, z3)) -> c5(LESSLEAVES(z1, z3), CONCAT(leaf, z3)) [1]
   LESSLEAVES(cons(leaf, z1), cons(cons(z04, z14), z3)) -> c5(LESSLEAVES(z1, cons(z04, concat(z14, z3))), CONCAT(cons(z04, z14), z3)) [1]
   LESSLEAVES(cons(leaf, z1), cons(z2, z3)) -> c5(LESSLEAVES(z1, leaf), CONCAT(z2, z3)) [1]
   LESSLEAVES(cons(cons(z03, z13), z1), cons(leaf, z3)) -> c5(LESSLEAVES(cons(z03, concat(z13, z1)), z3), CONCAT(leaf, z3)) [1]
   LESSLEAVES(cons(cons(z03, z13), z1), cons(cons(z05, z15), z3)) -> c5(LESSLEAVES(cons(z03, concat(z13, z1)), cons(z05, concat(z15, z3))), CONCAT(cons(z05, z15), z3)) [1]
   LESSLEAVES(cons(cons(z03, z13), z1), cons(z2, z3)) -> c5(LESSLEAVES(cons(z03, concat(z13, z1)), leaf), CONCAT(z2, z3)) [1]
   LESSLEAVES(cons(z0, z1), cons(leaf, z3)) -> c5(LESSLEAVES(leaf, z3), CONCAT(leaf, z3)) [1]
   LESSLEAVES(cons(z0, z1), cons(cons(z06, z16), z3)) -> c5(LESSLEAVES(leaf, cons(z06, concat(z16, z3))), CONCAT(cons(z06, z16), z3)) [1]
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(leaf, leaf), CONCAT(z2, z3)) [1]
   concat(leaf, z0) -> z0 [0]
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) [0]
   lessleaves(z0, leaf) -> false [0]
   lessleaves(leaf, cons(z0, z1)) -> true [0]
   lessleaves(cons(leaf, z1), cons(leaf, z3)) -> lessleaves(z1, z3) [0]
   lessleaves(cons(leaf, z1), cons(cons(z08, z18), z3)) -> lessleaves(z1, cons(z08, concat(z18, z3))) [0]
   lessleaves(cons(leaf, z1), cons(z2, z3)) -> lessleaves(z1, leaf) [0]
   lessleaves(cons(cons(z07, z17), z1), cons(leaf, z3)) -> lessleaves(cons(z07, concat(z17, z1)), z3) [0]
   lessleaves(cons(cons(z07, z17), z1), cons(cons(z09, z19), z3)) -> lessleaves(cons(z07, concat(z17, z1)), cons(z09, concat(z19, z3))) [0]
   lessleaves(cons(cons(z07, z17), z1), cons(z2, z3)) -> lessleaves(cons(z07, concat(z17, z1)), leaf) [0]
   lessleaves(cons(z0, z1), cons(leaf, z3)) -> lessleaves(leaf, z3) [0]
   lessleaves(cons(z0, z1), cons(cons(z010, z110), z3)) -> lessleaves(leaf, cons(z010, concat(z110, z3))) [0]
   lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(leaf, leaf) [0]
   concat(v0, v1) -> leaf [0]
   lessleaves(v0, v1) -> null_lessleaves [0]

The TRS has the following type information:
CONCAT :: leaf:cons -> leaf:cons -> c:c1
leaf :: leaf:cons
c :: c:c1
cons :: leaf:cons -> leaf:cons -> leaf:cons
c1 :: c:c1 -> c:c1
LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5
c2 :: c2:c3:c4:c5
c3 :: c2:c3:c4:c5
c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
concat :: leaf:cons -> leaf:cons -> leaf:cons
c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
lessleaves :: leaf:cons -> leaf:cons -> false:true:null_lessleaves
false :: false:true:null_lessleaves
true :: false:true:null_lessleaves
null_lessleaves :: false:true:null_lessleaves

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:

   leaf => 0
   c => 0
   c2 => 0
   c3 => 1
   false => 1
   true => 2
   null_lessleaves => 0

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   CONCAT(z, z') -{ 1 }-> 1 + CONCAT(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z1, z3) + CONCAT(0, z1) :|: z1 >= 0, z = 1 + 0 + z1, z' = 1 + 0 + z3, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z1, z3) + CONCAT(0, z3) :|: z1 >= 0, z = 1 + 0 + z1, z' = 1 + 0 + z3, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z1, 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z = 1 + 0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z1, 0) + CONCAT(0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z = 1 + 0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z1, 1 + z0'' + concat(z1'', z3)) + CONCAT(0, z1) :|: z1 >= 0, z = 1 + 0 + z1, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z1, 1 + z04 + concat(z14, z3)) + CONCAT(1 + z04 + z14, z3) :|: z04 >= 0, z1 >= 0, z = 1 + 0 + z1, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z3) + CONCAT(z0, z1) :|: z1 >= 0, z0 >= 0, z' = 1 + 0 + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z3) + CONCAT(0, z3) :|: z1 >= 0, z0 >= 0, z' = 1 + 0 + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z02 + concat(z12, z3)) + CONCAT(z0, z1) :|: z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z06 + concat(z16, z3)) + CONCAT(1 + z06 + z16, z3) :|: z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), z3) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z0' >= 0, z1' >= 0, z' = 1 + 0 + z3, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 0) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 1 + z01 + concat(z11, z3)) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), z3) + CONCAT(0, z3) :|: z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + 0 + z3, z03 >= 0, z13 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 1 + z05 + concat(z15, z3)) + CONCAT(1 + z05 + z15, z3) :|: z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z0 :|: z0 >= 0, z = 0, z' = z0
   concat(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   concat(z, z') -{ 0 }-> 1 + z0 + concat(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z1, z3) :|: z1 >= 0, z = 1 + 0 + z1, z' = 1 + 0 + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z1, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z = 1 + 0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z1, 1 + z08 + concat(z18, z3)) :|: z08 >= 0, z18 >= 0, z1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z = 1 + 0 + z1, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z3) :|: z1 >= 0, z0 >= 0, z' = 1 + 0 + z3, z = 1 + z0 + z1, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + concat(z110, z3)) :|: z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), z3) :|: z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' = 1 + 0 + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 0) :|: z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 1 + z09 + concat(z19, z3)) :|: z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z = z0, z0 >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1


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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 1 }-> 1 + CONCAT(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z02 + concat(z12, z3)) + CONCAT(z0, z1) :|: z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z06 + concat(z16, z3)) + CONCAT(1 + z06 + z16, z3) :|: z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(z2, z3) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + concat(z1'', z3)) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + concat(z14, z3)) + CONCAT(1 + z04 + z14, z3) :|: z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 0) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), z' - 1) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 1 + z01 + concat(z11, z3)) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 1 + z05 + concat(z15, z3)) + CONCAT(1 + z05 + z15, z3) :|: z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + concat(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + concat(z110, z3)) :|: z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + concat(z18, z3)) :|: z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 0) :|: z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), z' - 1) :|: z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 1 + z09 + concat(z19, z3)) :|: z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0


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

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

   { concat }
   { CONCAT }
   { lessleaves }
   { LESSLEAVES }

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 1 }-> 1 + CONCAT(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z02 + concat(z12, z3)) + CONCAT(z0, z1) :|: z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z06 + concat(z16, z3)) + CONCAT(1 + z06 + z16, z3) :|: z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(z2, z3) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + concat(z1'', z3)) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + concat(z14, z3)) + CONCAT(1 + z04 + z14, z3) :|: z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 0) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), z' - 1) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 1 + z01 + concat(z11, z3)) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 1 + z05 + concat(z15, z3)) + CONCAT(1 + z05 + z15, z3) :|: z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + concat(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + concat(z110, z3)) :|: z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + concat(z18, z3)) :|: z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 0) :|: z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), z' - 1) :|: z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 1 + z09 + concat(z19, z3)) :|: z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {concat}, {CONCAT}, {lessleaves}, {LESSLEAVES}

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 1 }-> 1 + CONCAT(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z02 + concat(z12, z3)) + CONCAT(z0, z1) :|: z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z06 + concat(z16, z3)) + CONCAT(1 + z06 + z16, z3) :|: z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(z2, z3) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + concat(z1'', z3)) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + concat(z14, z3)) + CONCAT(1 + z04 + z14, z3) :|: z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 0) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), z' - 1) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 1 + z01 + concat(z11, z3)) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 1 + z05 + concat(z15, z3)) + CONCAT(1 + z05 + z15, z3) :|: z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + concat(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + concat(z110, z3)) :|: z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + concat(z18, z3)) :|: z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 0) :|: z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), z' - 1) :|: z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 1 + z09 + concat(z19, z3)) :|: z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {concat}, {CONCAT}, {lessleaves}, {LESSLEAVES}

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

(19) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 1 }-> 1 + CONCAT(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z02 + concat(z12, z3)) + CONCAT(z0, z1) :|: z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z06 + concat(z16, z3)) + CONCAT(1 + z06 + z16, z3) :|: z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(z2, z3) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + concat(z1'', z3)) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + concat(z14, z3)) + CONCAT(1 + z04 + z14, z3) :|: z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 0) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), z' - 1) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 1 + z01 + concat(z11, z3)) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 1 + z05 + concat(z15, z3)) + CONCAT(1 + z05 + z15, z3) :|: z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + concat(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + concat(z110, z3)) :|: z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + concat(z18, z3)) :|: z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 0) :|: z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), z' - 1) :|: z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 1 + z09 + concat(z19, z3)) :|: z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {concat}, {CONCAT}, {lessleaves}, {LESSLEAVES}
Previous analysis results are:
  concat: runtime: ?, size: O(n^1) [z + z']

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

(21) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 1 }-> 1 + CONCAT(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z02 + concat(z12, z3)) + CONCAT(z0, z1) :|: z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z06 + concat(z16, z3)) + CONCAT(1 + z06 + z16, z3) :|: z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(z2, z3) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + concat(z1'', z3)) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + concat(z14, z3)) + CONCAT(1 + z04 + z14, z3) :|: z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 0) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), z' - 1) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + concat(z1', z1), 1 + z01 + concat(z11, z3)) + CONCAT(1 + z0' + z1', z1) :|: z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + concat(z13, z1), 1 + z05 + concat(z15, z3)) + CONCAT(1 + z05 + z15, z3) :|: z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + concat(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + concat(z110, z3)) :|: z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + concat(z18, z3)) :|: z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 0) :|: z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), z' - 1) :|: z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + concat(z17, z1), 1 + z09 + concat(z19, z3)) :|: z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {CONCAT}, {lessleaves}, {LESSLEAVES}
Previous analysis results are:
  concat: runtime: O(1) [0], size: O(n^1) [z + 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:

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 1 }-> 1 + CONCAT(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z02 + s3) + CONCAT(z0, z1) :|: s3 >= 0, s3 <= z12 + z3, z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z06 + s9) + CONCAT(1 + z06 + z16, z3) :|: s9 >= 0, s9 <= z16 + z3, z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(z2, z3) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + s) + CONCAT(0, z - 1) :|: s >= 0, s <= z1'' + z3, z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + s4) + CONCAT(1 + z04 + z14, z3) :|: s4 >= 0, s4 <= z14 + z3, z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + s', z' - 1) + CONCAT(1 + z0' + z1', z1) :|: s' >= 0, s' <= z1' + z1, z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + s'', 1 + z01 + s1) + CONCAT(1 + z0' + z1', z1) :|: s'' >= 0, s'' <= z1' + z1, s1 >= 0, s1 <= z11 + z3, z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + s2, 0) + CONCAT(1 + z0' + z1', z1) :|: s2 >= 0, s2 <= z1' + z1, z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + s5, z' - 1) + CONCAT(0, z' - 1) :|: s5 >= 0, s5 <= z13 + z1, z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + s6, 1 + z05 + s7) + CONCAT(1 + z05 + z15, z3) :|: s6 >= 0, s6 <= z13 + z1, s7 >= 0, s7 <= z15 + z3, z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + s8, 0) + CONCAT(z2, z3) :|: s8 >= 0, s8 <= z13 + z1, z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + s10 :|: s10 >= 0, s10 <= z1 + z', z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + s16) :|: s16 >= 0, s16 <= z110 + z3, z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + s11) :|: s11 >= 0, s11 <= z18 + z3, z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s12, z' - 1) :|: s12 >= 0, s12 <= z17 + z1, z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s13, 1 + z09 + s14) :|: s13 >= 0, s13 <= z17 + z1, s14 >= 0, s14 <= z19 + z3, z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s15, 0) :|: s15 >= 0, s15 <= z17 + z1, z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {CONCAT}, {lessleaves}, {LESSLEAVES}
Previous analysis results are:
  concat: runtime: O(1) [0], size: O(n^1) [z + z']

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

(25) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 1 }-> 1 + CONCAT(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z02 + s3) + CONCAT(z0, z1) :|: s3 >= 0, s3 <= z12 + z3, z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z06 + s9) + CONCAT(1 + z06 + z16, z3) :|: s9 >= 0, s9 <= z16 + z3, z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(z2, z3) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + s) + CONCAT(0, z - 1) :|: s >= 0, s <= z1'' + z3, z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + s4) + CONCAT(1 + z04 + z14, z3) :|: s4 >= 0, s4 <= z14 + z3, z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + s', z' - 1) + CONCAT(1 + z0' + z1', z1) :|: s' >= 0, s' <= z1' + z1, z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + s'', 1 + z01 + s1) + CONCAT(1 + z0' + z1', z1) :|: s'' >= 0, s'' <= z1' + z1, s1 >= 0, s1 <= z11 + z3, z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + s2, 0) + CONCAT(1 + z0' + z1', z1) :|: s2 >= 0, s2 <= z1' + z1, z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + s5, z' - 1) + CONCAT(0, z' - 1) :|: s5 >= 0, s5 <= z13 + z1, z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + s6, 1 + z05 + s7) + CONCAT(1 + z05 + z15, z3) :|: s6 >= 0, s6 <= z13 + z1, s7 >= 0, s7 <= z15 + z3, z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + s8, 0) + CONCAT(z2, z3) :|: s8 >= 0, s8 <= z13 + z1, z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + s10 :|: s10 >= 0, s10 <= z1 + z', z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + s16) :|: s16 >= 0, s16 <= z110 + z3, z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + s11) :|: s11 >= 0, s11 <= z18 + z3, z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s12, z' - 1) :|: s12 >= 0, s12 <= z17 + z1, z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s13, 1 + z09 + s14) :|: s13 >= 0, s13 <= z17 + z1, s14 >= 0, s14 <= z19 + z3, z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s15, 0) :|: s15 >= 0, s15 <= z17 + z1, z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {CONCAT}, {lessleaves}, {LESSLEAVES}
Previous analysis results are:
  concat: runtime: O(1) [0], size: O(n^1) [z + z']
  CONCAT: runtime: ?, size: O(n^1) [z]

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

(27) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 1 }-> 1 + CONCAT(z1, z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 0) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, z' - 1) + CONCAT(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z02 + s3) + CONCAT(z0, z1) :|: s3 >= 0, s3 <= z12 + z3, z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(0, 1 + z06 + s9) + CONCAT(1 + z06 + z16, z3) :|: s9 >= 0, s9 <= z16 + z3, z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(z2, z3) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 0) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, z' - 1) + CONCAT(0, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + s) + CONCAT(0, z - 1) :|: s >= 0, s <= z1'' + z3, z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + s4) + CONCAT(1 + z04 + z14, z3) :|: s4 >= 0, s4 <= z14 + z3, z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + s', z' - 1) + CONCAT(1 + z0' + z1', z1) :|: s' >= 0, s' <= z1' + z1, z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + s'', 1 + z01 + s1) + CONCAT(1 + z0' + z1', z1) :|: s'' >= 0, s'' <= z1' + z1, s1 >= 0, s1 <= z11 + z3, z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z0' + s2, 0) + CONCAT(1 + z0' + z1', z1) :|: s2 >= 0, s2 <= z1' + z1, z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + s5, z' - 1) + CONCAT(0, z' - 1) :|: s5 >= 0, s5 <= z13 + z1, z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + s6, 1 + z05 + s7) + CONCAT(1 + z05 + z15, z3) :|: s6 >= 0, s6 <= z13 + z1, s7 >= 0, s7 <= z15 + z3, z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 + LESSLEAVES(1 + z03 + s8, 0) + CONCAT(z2, z3) :|: s8 >= 0, s8 <= z13 + z1, z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + s10 :|: s10 >= 0, s10 <= z1 + z', z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + s16) :|: s16 >= 0, s16 <= z110 + z3, z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + s11) :|: s11 >= 0, s11 <= z18 + z3, z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s12, z' - 1) :|: s12 >= 0, s12 <= z17 + z1, z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s13, 1 + z09 + s14) :|: s13 >= 0, s13 <= z17 + z1, s14 >= 0, s14 <= z19 + z3, z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s15, 0) :|: s15 >= 0, s15 <= z17 + z1, z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {lessleaves}, {LESSLEAVES}
Previous analysis results are:
  concat: runtime: O(1) [0], size: O(n^1) [z + z']
  CONCAT: runtime: O(n^1) [1 + z], size: O(n^1) [z]

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 2 + z1 }-> 1 + s17 :|: s17 >= 0, s17 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 0) + s26 :|: s26 >= 0, s26 <= z0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(0, 0) + s35 :|: s35 >= 0, s35 <= z2, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, z' - 1) + s24 :|: s24 >= 0, s24 <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(0, z' - 1) + s33 :|: s33 >= 0, s33 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 1 + z02 + s3) + s25 :|: s25 >= 0, s25 <= z0, s3 >= 0, s3 <= z12 + z3, z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z06 + z16 }-> 1 + LESSLEAVES(0, 1 + z06 + s9) + s34 :|: s34 >= 0, s34 <= 1 + z06 + z16, s9 >= 0, s9 <= z16 + z3, z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 0) + s20 :|: s20 >= 0, s20 <= 0, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(z - 1, 0) + s29 :|: s29 >= 0, s29 <= z2, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s18 :|: s18 >= 0, s18 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s27 :|: s27 >= 0, s27 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + s) + s19 :|: s19 >= 0, s19 <= 0, s >= 0, s <= z1'' + z3, z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 3 + z04 + z14 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + s4) + s28 :|: s28 >= 0, s28 <= 1 + z04 + z14, s4 >= 0, s4 <= z14 + z3, z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s', z' - 1) + s21 :|: s21 >= 0, s21 <= 1 + z0' + z1', s' >= 0, s' <= z1' + z1, z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s'', 1 + z01 + s1) + s22 :|: s22 >= 0, s22 <= 1 + z0' + z1', s'' >= 0, s'' <= z1' + z1, s1 >= 0, s1 <= z11 + z3, z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s2, 0) + s23 :|: s23 >= 0, s23 <= 1 + z0' + z1', s2 >= 0, s2 <= z1' + z1, z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(1 + z03 + s5, z' - 1) + s30 :|: s30 >= 0, s30 <= 0, s5 >= 0, s5 <= z13 + z1, z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z05 + z15 }-> 1 + LESSLEAVES(1 + z03 + s6, 1 + z05 + s7) + s31 :|: s31 >= 0, s31 <= 1 + z05 + z15, s6 >= 0, s6 <= z13 + z1, s7 >= 0, s7 <= z15 + z3, z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(1 + z03 + s8, 0) + s32 :|: s32 >= 0, s32 <= z2, s8 >= 0, s8 <= z13 + z1, z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + s10 :|: s10 >= 0, s10 <= z1 + z', z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + s16) :|: s16 >= 0, s16 <= z110 + z3, z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + s11) :|: s11 >= 0, s11 <= z18 + z3, z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s12, z' - 1) :|: s12 >= 0, s12 <= z17 + z1, z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s13, 1 + z09 + s14) :|: s13 >= 0, s13 <= z17 + z1, s14 >= 0, s14 <= z19 + z3, z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s15, 0) :|: s15 >= 0, s15 <= z17 + z1, z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {lessleaves}, {LESSLEAVES}
Previous analysis results are:
  concat: runtime: O(1) [0], size: O(n^1) [z + z']
  CONCAT: runtime: O(n^1) [1 + z], size: O(n^1) [z]

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

(31) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 2 + z1 }-> 1 + s17 :|: s17 >= 0, s17 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 0) + s26 :|: s26 >= 0, s26 <= z0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(0, 0) + s35 :|: s35 >= 0, s35 <= z2, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, z' - 1) + s24 :|: s24 >= 0, s24 <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(0, z' - 1) + s33 :|: s33 >= 0, s33 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 1 + z02 + s3) + s25 :|: s25 >= 0, s25 <= z0, s3 >= 0, s3 <= z12 + z3, z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z06 + z16 }-> 1 + LESSLEAVES(0, 1 + z06 + s9) + s34 :|: s34 >= 0, s34 <= 1 + z06 + z16, s9 >= 0, s9 <= z16 + z3, z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 0) + s20 :|: s20 >= 0, s20 <= 0, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(z - 1, 0) + s29 :|: s29 >= 0, s29 <= z2, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s18 :|: s18 >= 0, s18 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s27 :|: s27 >= 0, s27 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + s) + s19 :|: s19 >= 0, s19 <= 0, s >= 0, s <= z1'' + z3, z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 3 + z04 + z14 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + s4) + s28 :|: s28 >= 0, s28 <= 1 + z04 + z14, s4 >= 0, s4 <= z14 + z3, z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s', z' - 1) + s21 :|: s21 >= 0, s21 <= 1 + z0' + z1', s' >= 0, s' <= z1' + z1, z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s'', 1 + z01 + s1) + s22 :|: s22 >= 0, s22 <= 1 + z0' + z1', s'' >= 0, s'' <= z1' + z1, s1 >= 0, s1 <= z11 + z3, z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s2, 0) + s23 :|: s23 >= 0, s23 <= 1 + z0' + z1', s2 >= 0, s2 <= z1' + z1, z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(1 + z03 + s5, z' - 1) + s30 :|: s30 >= 0, s30 <= 0, s5 >= 0, s5 <= z13 + z1, z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z05 + z15 }-> 1 + LESSLEAVES(1 + z03 + s6, 1 + z05 + s7) + s31 :|: s31 >= 0, s31 <= 1 + z05 + z15, s6 >= 0, s6 <= z13 + z1, s7 >= 0, s7 <= z15 + z3, z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(1 + z03 + s8, 0) + s32 :|: s32 >= 0, s32 <= z2, s8 >= 0, s8 <= z13 + z1, z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + s10 :|: s10 >= 0, s10 <= z1 + z', z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + s16) :|: s16 >= 0, s16 <= z110 + z3, z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + s11) :|: s11 >= 0, s11 <= z18 + z3, z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s12, z' - 1) :|: s12 >= 0, s12 <= z17 + z1, z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s13, 1 + z09 + s14) :|: s13 >= 0, s13 <= z17 + z1, s14 >= 0, s14 <= z19 + z3, z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s15, 0) :|: s15 >= 0, s15 <= z17 + z1, z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {lessleaves}, {LESSLEAVES}
Previous analysis results are:
  concat: runtime: O(1) [0], size: O(n^1) [z + z']
  CONCAT: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  lessleaves: runtime: ?, size: O(1) [2]

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

(33) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 2 + z1 }-> 1 + s17 :|: s17 >= 0, s17 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 0) + s26 :|: s26 >= 0, s26 <= z0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(0, 0) + s35 :|: s35 >= 0, s35 <= z2, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, z' - 1) + s24 :|: s24 >= 0, s24 <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(0, z' - 1) + s33 :|: s33 >= 0, s33 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 1 + z02 + s3) + s25 :|: s25 >= 0, s25 <= z0, s3 >= 0, s3 <= z12 + z3, z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z06 + z16 }-> 1 + LESSLEAVES(0, 1 + z06 + s9) + s34 :|: s34 >= 0, s34 <= 1 + z06 + z16, s9 >= 0, s9 <= z16 + z3, z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 0) + s20 :|: s20 >= 0, s20 <= 0, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(z - 1, 0) + s29 :|: s29 >= 0, s29 <= z2, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s18 :|: s18 >= 0, s18 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s27 :|: s27 >= 0, s27 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + s) + s19 :|: s19 >= 0, s19 <= 0, s >= 0, s <= z1'' + z3, z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 3 + z04 + z14 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + s4) + s28 :|: s28 >= 0, s28 <= 1 + z04 + z14, s4 >= 0, s4 <= z14 + z3, z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s', z' - 1) + s21 :|: s21 >= 0, s21 <= 1 + z0' + z1', s' >= 0, s' <= z1' + z1, z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s'', 1 + z01 + s1) + s22 :|: s22 >= 0, s22 <= 1 + z0' + z1', s'' >= 0, s'' <= z1' + z1, s1 >= 0, s1 <= z11 + z3, z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s2, 0) + s23 :|: s23 >= 0, s23 <= 1 + z0' + z1', s2 >= 0, s2 <= z1' + z1, z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(1 + z03 + s5, z' - 1) + s30 :|: s30 >= 0, s30 <= 0, s5 >= 0, s5 <= z13 + z1, z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z05 + z15 }-> 1 + LESSLEAVES(1 + z03 + s6, 1 + z05 + s7) + s31 :|: s31 >= 0, s31 <= 1 + z05 + z15, s6 >= 0, s6 <= z13 + z1, s7 >= 0, s7 <= z15 + z3, z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(1 + z03 + s8, 0) + s32 :|: s32 >= 0, s32 <= z2, s8 >= 0, s8 <= z13 + z1, z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + s10 :|: s10 >= 0, s10 <= z1 + z', z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 0) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, z' - 1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(0, 1 + z010 + s16) :|: s16 >= 0, s16 <= z110 + z3, z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 0) :|: z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(z - 1, 1 + z08 + s11) :|: s11 >= 0, s11 <= z18 + z3, z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s12, z' - 1) :|: s12 >= 0, s12 <= z17 + z1, z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s13, 1 + z09 + s14) :|: s13 >= 0, s13 <= z17 + z1, s14 >= 0, s14 <= z19 + z3, z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> lessleaves(1 + z07 + s15, 0) :|: s15 >= 0, s15 <= z17 + z1, z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {LESSLEAVES}
Previous analysis results are:
  concat: runtime: O(1) [0], size: O(n^1) [z + z']
  CONCAT: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  lessleaves: runtime: O(1) [0], size: O(1) [2]

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 2 + z1 }-> 1 + s17 :|: s17 >= 0, s17 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 0) + s26 :|: s26 >= 0, s26 <= z0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(0, 0) + s35 :|: s35 >= 0, s35 <= z2, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, z' - 1) + s24 :|: s24 >= 0, s24 <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(0, z' - 1) + s33 :|: s33 >= 0, s33 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 1 + z02 + s3) + s25 :|: s25 >= 0, s25 <= z0, s3 >= 0, s3 <= z12 + z3, z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z06 + z16 }-> 1 + LESSLEAVES(0, 1 + z06 + s9) + s34 :|: s34 >= 0, s34 <= 1 + z06 + z16, s9 >= 0, s9 <= z16 + z3, z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 0) + s20 :|: s20 >= 0, s20 <= 0, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(z - 1, 0) + s29 :|: s29 >= 0, s29 <= z2, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s18 :|: s18 >= 0, s18 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s27 :|: s27 >= 0, s27 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + s) + s19 :|: s19 >= 0, s19 <= 0, s >= 0, s <= z1'' + z3, z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 3 + z04 + z14 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + s4) + s28 :|: s28 >= 0, s28 <= 1 + z04 + z14, s4 >= 0, s4 <= z14 + z3, z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s', z' - 1) + s21 :|: s21 >= 0, s21 <= 1 + z0' + z1', s' >= 0, s' <= z1' + z1, z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s'', 1 + z01 + s1) + s22 :|: s22 >= 0, s22 <= 1 + z0' + z1', s'' >= 0, s'' <= z1' + z1, s1 >= 0, s1 <= z11 + z3, z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s2, 0) + s23 :|: s23 >= 0, s23 <= 1 + z0' + z1', s2 >= 0, s2 <= z1' + z1, z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(1 + z03 + s5, z' - 1) + s30 :|: s30 >= 0, s30 <= 0, s5 >= 0, s5 <= z13 + z1, z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z05 + z15 }-> 1 + LESSLEAVES(1 + z03 + s6, 1 + z05 + s7) + s31 :|: s31 >= 0, s31 <= 1 + z05 + z15, s6 >= 0, s6 <= z13 + z1, s7 >= 0, s7 <= z15 + z3, z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(1 + z03 + s8, 0) + s32 :|: s32 >= 0, s32 <= z2, s8 >= 0, s8 <= z13 + z1, z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + s10 :|: s10 >= 0, s10 <= z1 + z', z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> s36 :|: s36 >= 0, s36 <= 2, z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> s37 :|: s37 >= 0, s37 <= 2, s11 >= 0, s11 <= z18 + z3, z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s38 :|: s38 >= 0, s38 <= 2, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s39 :|: s39 >= 0, s39 <= 2, s12 >= 0, s12 <= z17 + z1, z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> s40 :|: s40 >= 0, s40 <= 2, s13 >= 0, s13 <= z17 + z1, s14 >= 0, s14 <= z19 + z3, z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s41 :|: s41 >= 0, s41 <= 2, s15 >= 0, s15 <= z17 + z1, z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s42 :|: s42 >= 0, s42 <= 2, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> s43 :|: s43 >= 0, s43 <= 2, s16 >= 0, s16 <= z110 + z3, z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s44 :|: s44 >= 0, s44 <= 2, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {LESSLEAVES}
Previous analysis results are:
  concat: runtime: O(1) [0], size: O(n^1) [z + z']
  CONCAT: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  lessleaves: runtime: O(1) [0], size: O(1) [2]

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

(37) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 2 + z1 }-> 1 + s17 :|: s17 >= 0, s17 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 0) + s26 :|: s26 >= 0, s26 <= z0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(0, 0) + s35 :|: s35 >= 0, s35 <= z2, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, z' - 1) + s24 :|: s24 >= 0, s24 <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(0, z' - 1) + s33 :|: s33 >= 0, s33 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 1 + z02 + s3) + s25 :|: s25 >= 0, s25 <= z0, s3 >= 0, s3 <= z12 + z3, z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z06 + z16 }-> 1 + LESSLEAVES(0, 1 + z06 + s9) + s34 :|: s34 >= 0, s34 <= 1 + z06 + z16, s9 >= 0, s9 <= z16 + z3, z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 0) + s20 :|: s20 >= 0, s20 <= 0, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(z - 1, 0) + s29 :|: s29 >= 0, s29 <= z2, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s18 :|: s18 >= 0, s18 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s27 :|: s27 >= 0, s27 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + s) + s19 :|: s19 >= 0, s19 <= 0, s >= 0, s <= z1'' + z3, z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 3 + z04 + z14 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + s4) + s28 :|: s28 >= 0, s28 <= 1 + z04 + z14, s4 >= 0, s4 <= z14 + z3, z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s', z' - 1) + s21 :|: s21 >= 0, s21 <= 1 + z0' + z1', s' >= 0, s' <= z1' + z1, z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s'', 1 + z01 + s1) + s22 :|: s22 >= 0, s22 <= 1 + z0' + z1', s'' >= 0, s'' <= z1' + z1, s1 >= 0, s1 <= z11 + z3, z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s2, 0) + s23 :|: s23 >= 0, s23 <= 1 + z0' + z1', s2 >= 0, s2 <= z1' + z1, z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(1 + z03 + s5, z' - 1) + s30 :|: s30 >= 0, s30 <= 0, s5 >= 0, s5 <= z13 + z1, z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z05 + z15 }-> 1 + LESSLEAVES(1 + z03 + s6, 1 + z05 + s7) + s31 :|: s31 >= 0, s31 <= 1 + z05 + z15, s6 >= 0, s6 <= z13 + z1, s7 >= 0, s7 <= z15 + z3, z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(1 + z03 + s8, 0) + s32 :|: s32 >= 0, s32 <= z2, s8 >= 0, s8 <= z13 + z1, z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + s10 :|: s10 >= 0, s10 <= z1 + z', z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> s36 :|: s36 >= 0, s36 <= 2, z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> s37 :|: s37 >= 0, s37 <= 2, s11 >= 0, s11 <= z18 + z3, z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s38 :|: s38 >= 0, s38 <= 2, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s39 :|: s39 >= 0, s39 <= 2, s12 >= 0, s12 <= z17 + z1, z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> s40 :|: s40 >= 0, s40 <= 2, s13 >= 0, s13 <= z17 + z1, s14 >= 0, s14 <= z19 + z3, z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s41 :|: s41 >= 0, s41 <= 2, s15 >= 0, s15 <= z17 + z1, z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s42 :|: s42 >= 0, s42 <= 2, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> s43 :|: s43 >= 0, s43 <= 2, s16 >= 0, s16 <= z110 + z3, z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s44 :|: s44 >= 0, s44 <= 2, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {LESSLEAVES}
Previous analysis results are:
  concat: runtime: O(1) [0], size: O(n^1) [z + z']
  CONCAT: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  lessleaves: runtime: O(1) [0], size: O(1) [2]
  LESSLEAVES: runtime: ?, size: O(n^2) [2 + 5*z + z*z' + z^2 + z']

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

(39) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: LESSLEAVES
after applying outer abstraction to obtain an ITS,
resulting in: O(n^2) with polynomial bound: 5 + 2*z + z*z' + z^2 + 2*z' + z'^2

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

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

   CONCAT(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   CONCAT(z, z') -{ 2 + z1 }-> 1 + s17 :|: s17 >= 0, s17 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   LESSLEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESSLEAVES(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 0) + s26 :|: s26 >= 0, s26 <= z0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(0, 0) + s35 :|: s35 >= 0, s35 <= z2, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, z' - 1) + s24 :|: s24 >= 0, s24 <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(0, z' - 1) + s33 :|: s33 >= 0, s33 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 + z0 }-> 1 + LESSLEAVES(0, 1 + z02 + s3) + s25 :|: s25 >= 0, s25 <= z0, s3 >= 0, s3 <= z12 + z3, z1 >= 0, z02 >= 0, z0 >= 0, z12 >= 0, z' = 1 + (1 + z02 + z12) + z3, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z06 + z16 }-> 1 + LESSLEAVES(0, 1 + z06 + s9) + s34 :|: s34 >= 0, s34 <= 1 + z06 + z16, s9 >= 0, s9 <= z16 + z3, z' = 1 + (1 + z06 + z16) + z3, z1 >= 0, z06 >= 0, z0 >= 0, z16 >= 0, z = 1 + z0 + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 0) + s20 :|: s20 >= 0, s20 <= 0, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(z - 1, 0) + s29 :|: s29 >= 0, s29 <= z2, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s18 :|: s18 >= 0, s18 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, z' - 1) + s27 :|: s27 >= 0, s27 <= 0, z - 1 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(z - 1, 1 + z0'' + s) + s19 :|: s19 >= 0, s19 <= 0, s >= 0, s <= z1'' + z3, z - 1 >= 0, z' = 1 + (1 + z0'' + z1'') + z3, z0'' >= 0, z3 >= 0, z1'' >= 0
   LESSLEAVES(z, z') -{ 3 + z04 + z14 }-> 1 + LESSLEAVES(z - 1, 1 + z04 + s4) + s28 :|: s28 >= 0, s28 <= 1 + z04 + z14, s4 >= 0, s4 <= z14 + z3, z04 >= 0, z - 1 >= 0, z' = 1 + (1 + z04 + z14) + z3, z14 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s', z' - 1) + s21 :|: s21 >= 0, s21 <= 1 + z0' + z1', s' >= 0, s' <= z1' + z1, z1 >= 0, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s'', 1 + z01 + s1) + s22 :|: s22 >= 0, s22 <= 1 + z0' + z1', s'' >= 0, s'' <= z1' + z1, s1 >= 0, s1 <= z11 + z3, z1 >= 0, z11 >= 0, z01 >= 0, z0' >= 0, z' = 1 + (1 + z01 + z11) + z3, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z3 >= 0
   LESSLEAVES(z, z') -{ 3 + z0' + z1' }-> 1 + LESSLEAVES(1 + z0' + s2, 0) + s23 :|: s23 >= 0, s23 <= 1 + z0' + z1', s2 >= 0, s2 <= z1' + z1, z1 >= 0, z' = 1 + z2 + z3, z0' >= 0, z1' >= 0, z = 1 + (1 + z0' + z1') + z1, z2 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 }-> 1 + LESSLEAVES(1 + z03 + s5, z' - 1) + s30 :|: s30 >= 0, s30 <= 0, s5 >= 0, s5 <= z13 + z1, z1 >= 0, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z' - 1 >= 0
   LESSLEAVES(z, z') -{ 3 + z05 + z15 }-> 1 + LESSLEAVES(1 + z03 + s6, 1 + z05 + s7) + s31 :|: s31 >= 0, s31 <= 1 + z05 + z15, s6 >= 0, s6 <= z13 + z1, s7 >= 0, s7 <= z15 + z3, z1 >= 0, z15 >= 0, z = 1 + (1 + z03 + z13) + z1, z' = 1 + (1 + z05 + z15) + z3, z03 >= 0, z05 >= 0, z13 >= 0, z3 >= 0
   LESSLEAVES(z, z') -{ 2 + z2 }-> 1 + LESSLEAVES(1 + z03 + s8, 0) + s32 :|: s32 >= 0, s32 <= z2, s8 >= 0, s8 <= z13 + z1, z1 >= 0, z' = 1 + z2 + z3, z = 1 + (1 + z03 + z13) + z1, z03 >= 0, z13 >= 0, z2 >= 0, z3 >= 0
   concat(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0
   concat(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   concat(z, z') -{ 0 }-> 1 + z0 + s10 :|: s10 >= 0, s10 <= z1 + z', z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0
   lessleaves(z, z') -{ 0 }-> s36 :|: s36 >= 0, s36 <= 2, z - 1 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> s37 :|: s37 >= 0, s37 <= 2, s11 >= 0, s11 <= z18 + z3, z08 >= 0, z18 >= 0, z - 1 >= 0, z' = 1 + (1 + z08 + z18) + z3, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s38 :|: s38 >= 0, s38 <= 2, z - 1 >= 0, z' = 1 + z2 + z3, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s39 :|: s39 >= 0, s39 <= 2, s12 >= 0, s12 <= z17 + z1, z1 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> s40 :|: s40 >= 0, s40 <= 2, s13 >= 0, s13 <= z17 + z1, s14 >= 0, s14 <= z19 + z3, z1 >= 0, z19 >= 0, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z' = 1 + (1 + z09 + z19) + z3, z17 >= 0, z09 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s41 :|: s41 >= 0, s41 <= 2, s15 >= 0, s15 <= z17 + z1, z1 >= 0, z' = 1 + z2 + z3, z07 >= 0, z = 1 + (1 + z07 + z17) + z1, z17 >= 0, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s42 :|: s42 >= 0, s42 <= 2, z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' - 1 >= 0
   lessleaves(z, z') -{ 0 }-> s43 :|: s43 >= 0, s43 <= 2, s16 >= 0, s16 <= z110 + z3, z1 >= 0, z110 >= 0, z' = 1 + (1 + z010 + z110) + z3, z0 >= 0, z = 1 + z0 + z1, z010 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> s44 :|: s44 >= 0, s44 <= 2, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lessleaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lessleaves(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0
   lessleaves(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: 
Previous analysis results are:
  concat: runtime: O(1) [0], size: O(n^1) [z + z']
  CONCAT: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  lessleaves: runtime: O(1) [0], size: O(1) [2]
  LESSLEAVES: runtime: O(n^2) [5 + 2*z + z*z' + z^2 + 2*z' + z'^2], size: O(n^2) [2 + 5*z + z*z' + z^2 + z']

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

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

(42)
BOUNDS(1, n^2)

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

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

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


The TRS R consists of the following rules:

   CONCAT(leaf, z0) -> c
   CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2))
   LESSLEAVES(z0, leaf) -> c2
   LESSLEAVES(leaf, cons(z0, z1)) -> c3
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1))
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3))

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

   concat(leaf, z0) -> z0
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
   lessleaves(z0, leaf) -> false
   lessleaves(leaf, cons(z0, z1)) -> true
   lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3))

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

(45) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
CONCAT/1

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

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


The TRS R consists of the following rules:

   CONCAT(leaf) -> c
   CONCAT(cons(z0, z1)) -> c1(CONCAT(z1))
   LESSLEAVES(z0, leaf) -> c2
   LESSLEAVES(leaf, cons(z0, z1)) -> c3
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
   LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))

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

   concat(leaf, z0) -> z0
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
   lessleaves(z0, leaf) -> false
   lessleaves(leaf, cons(z0, z1)) -> true
   lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3))

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

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

(48)
Obligation:
Innermost TRS:
Rules:
CONCAT(leaf) -> c
CONCAT(cons(z0, z1)) -> c1(CONCAT(z1))
LESSLEAVES(z0, leaf) -> c2
LESSLEAVES(leaf, cons(z0, z1)) -> c3
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
lessleaves(z0, leaf) -> false
lessleaves(leaf, cons(z0, z1)) -> true
lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3))

Types:
CONCAT :: leaf:cons -> c:c1
leaf :: leaf:cons
c :: c:c1
cons :: leaf:cons -> leaf:cons -> leaf:cons
c1 :: c:c1 -> c:c1
LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5
c2 :: c2:c3:c4:c5
c3 :: c2:c3:c4:c5
c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
concat :: leaf:cons -> leaf:cons -> leaf:cons
c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
lessleaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_6 :: c:c1
hole_leaf:cons2_6 :: leaf:cons
hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5
hole_false:true4_6 :: false:true
gen_c:c15_6 :: Nat -> c:c1
gen_leaf:cons6_6 :: Nat -> leaf:cons
gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5

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

(49) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
CONCAT, LESSLEAVES, concat, lessleaves

They will be analysed ascendingly in the following order:
CONCAT < LESSLEAVES
concat < LESSLEAVES
concat < lessleaves

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

(50)
Obligation:
Innermost TRS:
Rules:
CONCAT(leaf) -> c
CONCAT(cons(z0, z1)) -> c1(CONCAT(z1))
LESSLEAVES(z0, leaf) -> c2
LESSLEAVES(leaf, cons(z0, z1)) -> c3
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
lessleaves(z0, leaf) -> false
lessleaves(leaf, cons(z0, z1)) -> true
lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3))

Types:
CONCAT :: leaf:cons -> c:c1
leaf :: leaf:cons
c :: c:c1
cons :: leaf:cons -> leaf:cons -> leaf:cons
c1 :: c:c1 -> c:c1
LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5
c2 :: c2:c3:c4:c5
c3 :: c2:c3:c4:c5
c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
concat :: leaf:cons -> leaf:cons -> leaf:cons
c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
lessleaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_6 :: c:c1
hole_leaf:cons2_6 :: leaf:cons
hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5
hole_false:true4_6 :: false:true
gen_c:c15_6 :: Nat -> c:c1
gen_leaf:cons6_6 :: Nat -> leaf:cons
gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_leaf:cons6_6(0) <=> leaf
gen_leaf:cons6_6(+(x, 1)) <=> cons(leaf, gen_leaf:cons6_6(x))
gen_c2:c3:c4:c57_6(0) <=> c2
gen_c2:c3:c4:c57_6(+(x, 1)) <=> c4(gen_c2:c3:c4:c57_6(x), c)


The following defined symbols remain to be analysed:
CONCAT, LESSLEAVES, concat, lessleaves

They will be analysed ascendingly in the following order:
CONCAT < LESSLEAVES
concat < LESSLEAVES
concat < lessleaves

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

(51) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
CONCAT(gen_leaf:cons6_6(n9_6)) -> gen_c:c15_6(n9_6), rt in Omega(1 + n9_6)

Induction Base:
CONCAT(gen_leaf:cons6_6(0)) ->_R^Omega(1)
c

Induction Step:
CONCAT(gen_leaf:cons6_6(+(n9_6, 1))) ->_R^Omega(1)
c1(CONCAT(gen_leaf:cons6_6(n9_6))) ->_IH
c1(gen_c:c15_6(c10_6))

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

(52)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
CONCAT(leaf) -> c
CONCAT(cons(z0, z1)) -> c1(CONCAT(z1))
LESSLEAVES(z0, leaf) -> c2
LESSLEAVES(leaf, cons(z0, z1)) -> c3
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
lessleaves(z0, leaf) -> false
lessleaves(leaf, cons(z0, z1)) -> true
lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3))

Types:
CONCAT :: leaf:cons -> c:c1
leaf :: leaf:cons
c :: c:c1
cons :: leaf:cons -> leaf:cons -> leaf:cons
c1 :: c:c1 -> c:c1
LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5
c2 :: c2:c3:c4:c5
c3 :: c2:c3:c4:c5
c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
concat :: leaf:cons -> leaf:cons -> leaf:cons
c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
lessleaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_6 :: c:c1
hole_leaf:cons2_6 :: leaf:cons
hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5
hole_false:true4_6 :: false:true
gen_c:c15_6 :: Nat -> c:c1
gen_leaf:cons6_6 :: Nat -> leaf:cons
gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_leaf:cons6_6(0) <=> leaf
gen_leaf:cons6_6(+(x, 1)) <=> cons(leaf, gen_leaf:cons6_6(x))
gen_c2:c3:c4:c57_6(0) <=> c2
gen_c2:c3:c4:c57_6(+(x, 1)) <=> c4(gen_c2:c3:c4:c57_6(x), c)


The following defined symbols remain to be analysed:
CONCAT, LESSLEAVES, concat, lessleaves

They will be analysed ascendingly in the following order:
CONCAT < LESSLEAVES
concat < LESSLEAVES
concat < lessleaves

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

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

(55)
BOUNDS(n^1, INF)

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

(56)
Obligation:
Innermost TRS:
Rules:
CONCAT(leaf) -> c
CONCAT(cons(z0, z1)) -> c1(CONCAT(z1))
LESSLEAVES(z0, leaf) -> c2
LESSLEAVES(leaf, cons(z0, z1)) -> c3
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
lessleaves(z0, leaf) -> false
lessleaves(leaf, cons(z0, z1)) -> true
lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3))

Types:
CONCAT :: leaf:cons -> c:c1
leaf :: leaf:cons
c :: c:c1
cons :: leaf:cons -> leaf:cons -> leaf:cons
c1 :: c:c1 -> c:c1
LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5
c2 :: c2:c3:c4:c5
c3 :: c2:c3:c4:c5
c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
concat :: leaf:cons -> leaf:cons -> leaf:cons
c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
lessleaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_6 :: c:c1
hole_leaf:cons2_6 :: leaf:cons
hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5
hole_false:true4_6 :: false:true
gen_c:c15_6 :: Nat -> c:c1
gen_leaf:cons6_6 :: Nat -> leaf:cons
gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5


Lemmas:
CONCAT(gen_leaf:cons6_6(n9_6)) -> gen_c:c15_6(n9_6), rt in Omega(1 + n9_6)


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_leaf:cons6_6(0) <=> leaf
gen_leaf:cons6_6(+(x, 1)) <=> cons(leaf, gen_leaf:cons6_6(x))
gen_c2:c3:c4:c57_6(0) <=> c2
gen_c2:c3:c4:c57_6(+(x, 1)) <=> c4(gen_c2:c3:c4:c57_6(x), c)


The following defined symbols remain to be analysed:
concat, LESSLEAVES, lessleaves

They will be analysed ascendingly in the following order:
concat < LESSLEAVES
concat < lessleaves

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

(57) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
concat(gen_leaf:cons6_6(n241_6), gen_leaf:cons6_6(b)) -> gen_leaf:cons6_6(+(n241_6, b)), rt in Omega(0)

Induction Base:
concat(gen_leaf:cons6_6(0), gen_leaf:cons6_6(b)) ->_R^Omega(0)
gen_leaf:cons6_6(b)

Induction Step:
concat(gen_leaf:cons6_6(+(n241_6, 1)), gen_leaf:cons6_6(b)) ->_R^Omega(0)
cons(leaf, concat(gen_leaf:cons6_6(n241_6), gen_leaf:cons6_6(b))) ->_IH
cons(leaf, gen_leaf:cons6_6(+(b, c242_6)))

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

(58)
Obligation:
Innermost TRS:
Rules:
CONCAT(leaf) -> c
CONCAT(cons(z0, z1)) -> c1(CONCAT(z1))
LESSLEAVES(z0, leaf) -> c2
LESSLEAVES(leaf, cons(z0, z1)) -> c3
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
lessleaves(z0, leaf) -> false
lessleaves(leaf, cons(z0, z1)) -> true
lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3))

Types:
CONCAT :: leaf:cons -> c:c1
leaf :: leaf:cons
c :: c:c1
cons :: leaf:cons -> leaf:cons -> leaf:cons
c1 :: c:c1 -> c:c1
LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5
c2 :: c2:c3:c4:c5
c3 :: c2:c3:c4:c5
c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
concat :: leaf:cons -> leaf:cons -> leaf:cons
c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
lessleaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_6 :: c:c1
hole_leaf:cons2_6 :: leaf:cons
hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5
hole_false:true4_6 :: false:true
gen_c:c15_6 :: Nat -> c:c1
gen_leaf:cons6_6 :: Nat -> leaf:cons
gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5


Lemmas:
CONCAT(gen_leaf:cons6_6(n9_6)) -> gen_c:c15_6(n9_6), rt in Omega(1 + n9_6)
concat(gen_leaf:cons6_6(n241_6), gen_leaf:cons6_6(b)) -> gen_leaf:cons6_6(+(n241_6, b)), rt in Omega(0)


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_leaf:cons6_6(0) <=> leaf
gen_leaf:cons6_6(+(x, 1)) <=> cons(leaf, gen_leaf:cons6_6(x))
gen_c2:c3:c4:c57_6(0) <=> c2
gen_c2:c3:c4:c57_6(+(x, 1)) <=> c4(gen_c2:c3:c4:c57_6(x), c)


The following defined symbols remain to be analysed:
LESSLEAVES, lessleaves
----------------------------------------

(59) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LESSLEAVES(gen_leaf:cons6_6(n1122_6), gen_leaf:cons6_6(n1122_6)) -> gen_c2:c3:c4:c57_6(n1122_6), rt in Omega(1 + n1122_6)

Induction Base:
LESSLEAVES(gen_leaf:cons6_6(0), gen_leaf:cons6_6(0)) ->_R^Omega(1)
c2

Induction Step:
LESSLEAVES(gen_leaf:cons6_6(+(n1122_6, 1)), gen_leaf:cons6_6(+(n1122_6, 1))) ->_R^Omega(1)
c4(LESSLEAVES(concat(leaf, gen_leaf:cons6_6(n1122_6)), concat(leaf, gen_leaf:cons6_6(n1122_6))), CONCAT(leaf)) ->_L^Omega(0)
c4(LESSLEAVES(gen_leaf:cons6_6(+(0, n1122_6)), concat(leaf, gen_leaf:cons6_6(n1122_6))), CONCAT(leaf)) ->_L^Omega(0)
c4(LESSLEAVES(gen_leaf:cons6_6(n1122_6), gen_leaf:cons6_6(+(0, n1122_6))), CONCAT(leaf)) ->_IH
c4(gen_c2:c3:c4:c57_6(c1123_6), CONCAT(leaf)) ->_L^Omega(1)
c4(gen_c2:c3:c4:c57_6(n1122_6), gen_c:c15_6(0))

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

(60)
Obligation:
Innermost TRS:
Rules:
CONCAT(leaf) -> c
CONCAT(cons(z0, z1)) -> c1(CONCAT(z1))
LESSLEAVES(z0, leaf) -> c2
LESSLEAVES(leaf, cons(z0, z1)) -> c3
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
lessleaves(z0, leaf) -> false
lessleaves(leaf, cons(z0, z1)) -> true
lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3))

Types:
CONCAT :: leaf:cons -> c:c1
leaf :: leaf:cons
c :: c:c1
cons :: leaf:cons -> leaf:cons -> leaf:cons
c1 :: c:c1 -> c:c1
LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5
c2 :: c2:c3:c4:c5
c3 :: c2:c3:c4:c5
c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
concat :: leaf:cons -> leaf:cons -> leaf:cons
c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5
lessleaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_6 :: c:c1
hole_leaf:cons2_6 :: leaf:cons
hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5
hole_false:true4_6 :: false:true
gen_c:c15_6 :: Nat -> c:c1
gen_leaf:cons6_6 :: Nat -> leaf:cons
gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5


Lemmas:
CONCAT(gen_leaf:cons6_6(n9_6)) -> gen_c:c15_6(n9_6), rt in Omega(1 + n9_6)
concat(gen_leaf:cons6_6(n241_6), gen_leaf:cons6_6(b)) -> gen_leaf:cons6_6(+(n241_6, b)), rt in Omega(0)
LESSLEAVES(gen_leaf:cons6_6(n1122_6), gen_leaf:cons6_6(n1122_6)) -> gen_c2:c3:c4:c57_6(n1122_6), rt in Omega(1 + n1122_6)


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_leaf:cons6_6(0) <=> leaf
gen_leaf:cons6_6(+(x, 1)) <=> cons(leaf, gen_leaf:cons6_6(x))
gen_c2:c3:c4:c57_6(0) <=> c2
gen_c2:c3:c4:c57_6(+(x, 1)) <=> c4(gen_c2:c3:c4:c57_6(x), c)


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

(61) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
lessleaves(gen_leaf:cons6_6(n3420_6), gen_leaf:cons6_6(n3420_6)) -> false, rt in Omega(0)

Induction Base:
lessleaves(gen_leaf:cons6_6(0), gen_leaf:cons6_6(0)) ->_R^Omega(0)
false

Induction Step:
lessleaves(gen_leaf:cons6_6(+(n3420_6, 1)), gen_leaf:cons6_6(+(n3420_6, 1))) ->_R^Omega(0)
lessleaves(concat(leaf, gen_leaf:cons6_6(n3420_6)), concat(leaf, gen_leaf:cons6_6(n3420_6))) ->_L^Omega(0)
lessleaves(gen_leaf:cons6_6(+(0, n3420_6)), concat(leaf, gen_leaf:cons6_6(n3420_6))) ->_L^Omega(0)
lessleaves(gen_leaf:cons6_6(n3420_6), gen_leaf:cons6_6(+(0, n3420_6))) ->_IH
false

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

(62)
BOUNDS(1, INF)