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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 518 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) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 2 ms]
    (10) CpxRNTS
    (11) CompleteCoflocoProof [FINISHED, 2881 ms]
    (12) BOUNDS(1, n^3)
(13) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxRelTRS
    (15) SlicingProof [LOWER BOUND(ID), 0 ms]
    (16) CpxRelTRS
    (17) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) typed CpxTrs
    (19) OrderProof [LOWER BOUND(ID), 20 ms]
    (20) typed CpxTrs
    (21) RewriteLemmaProof [LOWER BOUND(ID), 331 ms]
    (22) BEST
        (23) proven lower bound
            (24) LowerBoundPropagationProof [FINISHED, 0 ms]
            (25) BOUNDS(n^1, INF)
        (26) typed CpxTrs
            (27) RewriteLemmaProof [LOWER BOUND(ID), 99 ms]
            (28) typed CpxTrs
            (29) RewriteLemmaProof [LOWER BOUND(ID), 106 ms]
            (30) typed CpxTrs
            (31) RewriteLemmaProof [LOWER BOUND(ID), 46 ms]
            (32) typed CpxTrs
            (33) RewriteLemmaProof [LOWER BOUND(ID), 54 ms]
            (34) typed CpxTrs
            (35) RewriteLemmaProof [LOWER BOUND(ID), 254 ms]
            (36) typed CpxTrs
            (37) RewriteLemmaProof [LOWER BOUND(ID), 66 ms]
            (38) typed CpxTrs
            (39) RewriteLemmaProof [LOWER BOUND(ID), 12 ms]
            (40) typed CpxTrs
            (41) RewriteLemmaProof [LOWER BOUND(ID), 856 ms]
            (42) BEST
                (43) proven lower bound
                    (44) LowerBoundPropagationProof [FINISHED, 0 ms]
                    (45) BOUNDS(n^2, INF)
                (46) typed CpxTrs
                    (47) RewriteLemmaProof [LOWER BOUND(ID), 1008 ms]
                    (48) BEST
                        (49) proven lower bound
                            (50) LowerBoundPropagationProof [FINISHED, 0 ms]
                            (51) BOUNDS(n^3, INF)
                        (52) typed CpxTrs
                            (53) RewriteLemmaProof [LOWER BOUND(ID), 21 ms]
                            (54) typed CpxTrs
                            (55) RewriteLemmaProof [LOWER BOUND(ID), 67 ms]
                            (56) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c2
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   APP(nil, z0) -> c4
   APP(add(z0, z1), z2) -> c5(APP(z1, z2))
   REVERSE(nil) -> c6
   REVERSE(add(z0, z1)) -> c7(APP(reverse(z1), add(z0, nil)), REVERSE(z1))
   SHUFFLE(nil) -> c8
   SHUFFLE(add(z0, z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
   CONCAT(leaf, z0) -> c10
   CONCAT(cons(z0, z1), z2) -> c11(CONCAT(z1, z2))
   LESS_LEAVES(z0, leaf) -> c12
   LESS_LEAVES(leaf, cons(z0, z1)) -> c13
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1))
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3))

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

   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   app(nil, z0) -> z0
   app(add(z0, z1), z2) -> add(z0, app(z1, z2))
   reverse(nil) -> nil
   reverse(add(z0, z1)) -> app(reverse(z1), add(z0, nil))
   shuffle(nil) -> nil
   shuffle(add(z0, z1)) -> add(z0, shuffle(reverse(z1)))
   concat(leaf, z0) -> z0
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
   less_leaves(z0, leaf) -> false
   less_leaves(leaf, cons(z0, z1)) -> true
   less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(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^3, n^3).


The TRS R consists of the following rules:

   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c2
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   APP(nil, z0) -> c4
   APP(add(z0, z1), z2) -> c5(APP(z1, z2))
   REVERSE(nil) -> c6
   REVERSE(add(z0, z1)) -> c7(APP(reverse(z1), add(z0, nil)), REVERSE(z1))
   SHUFFLE(nil) -> c8
   SHUFFLE(add(z0, z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
   CONCAT(leaf, z0) -> c10
   CONCAT(cons(z0, z1), z2) -> c11(CONCAT(z1, z2))
   LESS_LEAVES(z0, leaf) -> c12
   LESS_LEAVES(leaf, cons(z0, z1)) -> c13
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1))
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3))

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

   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   app(nil, z0) -> z0
   app(add(z0, z1), z2) -> add(z0, app(z1, z2))
   reverse(nil) -> nil
   reverse(add(z0, z1)) -> app(reverse(z1), add(z0, nil))
   shuffle(nil) -> nil
   shuffle(add(z0, z1)) -> add(z0, shuffle(reverse(z1)))
   concat(leaf, z0) -> z0
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
   less_leaves(z0, leaf) -> false
   less_leaves(leaf, cons(z0, z1)) -> true
   less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(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^3).


The TRS R consists of the following rules:

   MINUS(z0, 0) -> c [1]
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1)) [1]
   QUOT(0, s(z0)) -> c2 [1]
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   APP(nil, z0) -> c4 [1]
   APP(add(z0, z1), z2) -> c5(APP(z1, z2)) [1]
   REVERSE(nil) -> c6 [1]
   REVERSE(add(z0, z1)) -> c7(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) [1]
   SHUFFLE(nil) -> c8 [1]
   SHUFFLE(add(z0, z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1)) [1]
   CONCAT(leaf, z0) -> c10 [1]
   CONCAT(cons(z0, z1), z2) -> c11(CONCAT(z1, z2)) [1]
   LESS_LEAVES(z0, leaf) -> c12 [1]
   LESS_LEAVES(leaf, cons(z0, z1)) -> c13 [1]
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) [1]
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) [1]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   quot(0, s(z0)) -> 0 [0]
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) [0]
   app(nil, z0) -> z0 [0]
   app(add(z0, z1), z2) -> add(z0, app(z1, z2)) [0]
   reverse(nil) -> nil [0]
   reverse(add(z0, z1)) -> app(reverse(z1), add(z0, nil)) [0]
   shuffle(nil) -> nil [0]
   shuffle(add(z0, z1)) -> add(z0, shuffle(reverse(z1))) [0]
   concat(leaf, z0) -> z0 [0]
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) [0]
   less_leaves(z0, leaf) -> false [0]
   less_leaves(leaf, cons(z0, z1)) -> true [0]
   less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(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:

   MINUS(z0, 0) -> c [1]
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1)) [1]
   QUOT(0, s(z0)) -> c2 [1]
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   APP(nil, z0) -> c4 [1]
   APP(add(z0, z1), z2) -> c5(APP(z1, z2)) [1]
   REVERSE(nil) -> c6 [1]
   REVERSE(add(z0, z1)) -> c7(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) [1]
   SHUFFLE(nil) -> c8 [1]
   SHUFFLE(add(z0, z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1)) [1]
   CONCAT(leaf, z0) -> c10 [1]
   CONCAT(cons(z0, z1), z2) -> c11(CONCAT(z1, z2)) [1]
   LESS_LEAVES(z0, leaf) -> c12 [1]
   LESS_LEAVES(leaf, cons(z0, z1)) -> c13 [1]
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) [1]
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) [1]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   quot(0, s(z0)) -> 0 [0]
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) [0]
   app(nil, z0) -> z0 [0]
   app(add(z0, z1), z2) -> add(z0, app(z1, z2)) [0]
   reverse(nil) -> nil [0]
   reverse(add(z0, z1)) -> app(reverse(z1), add(z0, nil)) [0]
   shuffle(nil) -> nil [0]
   shuffle(add(z0, z1)) -> add(z0, shuffle(reverse(z1))) [0]
   concat(leaf, z0) -> z0 [0]
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) [0]
   less_leaves(z0, leaf) -> false [0]
   less_leaves(leaf, cons(z0, z1)) -> true [0]
   less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3)) [0]

The TRS has the following type information:
MINUS :: 0:s -> 0:s -> c:c1
0 :: 0:s
c :: c:c1
s :: 0:s -> 0:s
c1 :: c:c1 -> c:c1
QUOT :: 0:s -> 0:s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0:s -> 0:s -> 0:s
APP :: nil:add -> nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: a -> nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0:s -> 0:s -> 0:s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true

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

(7) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   minus(v0, v1) -> null_minus [0]
   quot(v0, v1) -> null_quot [0]
   app(v0, v1) -> null_app [0]
   reverse(v0) -> null_reverse [0]
   shuffle(v0) -> null_shuffle [0]
   concat(v0, v1) -> null_concat [0]
   less_leaves(v0, v1) -> null_less_leaves [0]
   MINUS(v0, v1) -> null_MINUS [0]
   QUOT(v0, v1) -> null_QUOT [0]
   APP(v0, v1) -> null_APP [0]
   REVERSE(v0) -> null_REVERSE [0]
   SHUFFLE(v0) -> null_SHUFFLE [0]
   CONCAT(v0, v1) -> null_CONCAT [0]
   LESS_LEAVES(v0, v1) -> null_LESS_LEAVES [0]

And the following fresh constants:    null_minus, null_quot, null_app, null_reverse, null_shuffle, null_concat, null_less_leaves, null_MINUS, null_QUOT, null_APP, null_REVERSE, null_SHUFFLE, null_CONCAT, null_LESS_LEAVES, const

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

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

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

   MINUS(z0, 0) -> c [1]
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1)) [1]
   QUOT(0, s(z0)) -> c2 [1]
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   APP(nil, z0) -> c4 [1]
   APP(add(z0, z1), z2) -> c5(APP(z1, z2)) [1]
   REVERSE(nil) -> c6 [1]
   REVERSE(add(z0, z1)) -> c7(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) [1]
   SHUFFLE(nil) -> c8 [1]
   SHUFFLE(add(z0, z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1)) [1]
   CONCAT(leaf, z0) -> c10 [1]
   CONCAT(cons(z0, z1), z2) -> c11(CONCAT(z1, z2)) [1]
   LESS_LEAVES(z0, leaf) -> c12 [1]
   LESS_LEAVES(leaf, cons(z0, z1)) -> c13 [1]
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) [1]
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) [1]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   quot(0, s(z0)) -> 0 [0]
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) [0]
   app(nil, z0) -> z0 [0]
   app(add(z0, z1), z2) -> add(z0, app(z1, z2)) [0]
   reverse(nil) -> nil [0]
   reverse(add(z0, z1)) -> app(reverse(z1), add(z0, nil)) [0]
   shuffle(nil) -> nil [0]
   shuffle(add(z0, z1)) -> add(z0, shuffle(reverse(z1))) [0]
   concat(leaf, z0) -> z0 [0]
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) [0]
   less_leaves(z0, leaf) -> false [0]
   less_leaves(leaf, cons(z0, z1)) -> true [0]
   less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3)) [0]
   minus(v0, v1) -> null_minus [0]
   quot(v0, v1) -> null_quot [0]
   app(v0, v1) -> null_app [0]
   reverse(v0) -> null_reverse [0]
   shuffle(v0) -> null_shuffle [0]
   concat(v0, v1) -> null_concat [0]
   less_leaves(v0, v1) -> null_less_leaves [0]
   MINUS(v0, v1) -> null_MINUS [0]
   QUOT(v0, v1) -> null_QUOT [0]
   APP(v0, v1) -> null_APP [0]
   REVERSE(v0) -> null_REVERSE [0]
   SHUFFLE(v0) -> null_SHUFFLE [0]
   CONCAT(v0, v1) -> null_CONCAT [0]
   LESS_LEAVES(v0, v1) -> null_LESS_LEAVES [0]

The TRS has the following type information:
MINUS :: 0:s:null_minus:null_quot -> 0:s:null_minus:null_quot -> c:c1:null_MINUS
0 :: 0:s:null_minus:null_quot
c :: c:c1:null_MINUS
s :: 0:s:null_minus:null_quot -> 0:s:null_minus:null_quot
c1 :: c:c1:null_MINUS -> c:c1:null_MINUS
QUOT :: 0:s:null_minus:null_quot -> 0:s:null_minus:null_quot -> c2:c3:null_QUOT
c2 :: c2:c3:null_QUOT
c3 :: c2:c3:null_QUOT -> c:c1:null_MINUS -> c2:c3:null_QUOT
minus :: 0:s:null_minus:null_quot -> 0:s:null_minus:null_quot -> 0:s:null_minus:null_quot
APP :: nil:add:null_app:null_reverse:null_shuffle -> nil:add:null_app:null_reverse:null_shuffle -> c4:c5:null_APP
nil :: nil:add:null_app:null_reverse:null_shuffle
c4 :: c4:c5:null_APP
add :: a -> nil:add:null_app:null_reverse:null_shuffle -> nil:add:null_app:null_reverse:null_shuffle
c5 :: c4:c5:null_APP -> c4:c5:null_APP
REVERSE :: nil:add:null_app:null_reverse:null_shuffle -> c6:c7:null_REVERSE
c6 :: c6:c7:null_REVERSE
c7 :: c4:c5:null_APP -> c6:c7:null_REVERSE -> c6:c7:null_REVERSE
reverse :: nil:add:null_app:null_reverse:null_shuffle -> nil:add:null_app:null_reverse:null_shuffle
SHUFFLE :: nil:add:null_app:null_reverse:null_shuffle -> c8:c9:null_SHUFFLE
c8 :: c8:c9:null_SHUFFLE
c9 :: c8:c9:null_SHUFFLE -> c6:c7:null_REVERSE -> c8:c9:null_SHUFFLE
CONCAT :: leaf:cons:null_concat -> leaf:cons:null_concat -> c10:c11:null_CONCAT
leaf :: leaf:cons:null_concat
c10 :: c10:c11:null_CONCAT
cons :: leaf:cons:null_concat -> leaf:cons:null_concat -> leaf:cons:null_concat
c11 :: c10:c11:null_CONCAT -> c10:c11:null_CONCAT
LESS_LEAVES :: leaf:cons:null_concat -> leaf:cons:null_concat -> c12:c13:c14:c15:null_LESS_LEAVES
c12 :: c12:c13:c14:c15:null_LESS_LEAVES
c13 :: c12:c13:c14:c15:null_LESS_LEAVES
c14 :: c12:c13:c14:c15:null_LESS_LEAVES -> c10:c11:null_CONCAT -> c12:c13:c14:c15:null_LESS_LEAVES
concat :: leaf:cons:null_concat -> leaf:cons:null_concat -> leaf:cons:null_concat
c15 :: c12:c13:c14:c15:null_LESS_LEAVES -> c10:c11:null_CONCAT -> c12:c13:c14:c15:null_LESS_LEAVES
quot :: 0:s:null_minus:null_quot -> 0:s:null_minus:null_quot -> 0:s:null_minus:null_quot
app :: nil:add:null_app:null_reverse:null_shuffle -> nil:add:null_app:null_reverse:null_shuffle -> nil:add:null_app:null_reverse:null_shuffle
shuffle :: nil:add:null_app:null_reverse:null_shuffle -> nil:add:null_app:null_reverse:null_shuffle
less_leaves :: leaf:cons:null_concat -> leaf:cons:null_concat -> false:true:null_less_leaves
false :: false:true:null_less_leaves
true :: false:true:null_less_leaves
null_minus :: 0:s:null_minus:null_quot
null_quot :: 0:s:null_minus:null_quot
null_app :: nil:add:null_app:null_reverse:null_shuffle
null_reverse :: nil:add:null_app:null_reverse:null_shuffle
null_shuffle :: nil:add:null_app:null_reverse:null_shuffle
null_concat :: leaf:cons:null_concat
null_less_leaves :: false:true:null_less_leaves
null_MINUS :: c:c1:null_MINUS
null_QUOT :: c2:c3:null_QUOT
null_APP :: c4:c5:null_APP
null_REVERSE :: c6:c7:null_REVERSE
null_SHUFFLE :: c8:c9:null_SHUFFLE
null_CONCAT :: c10:c11:null_CONCAT
null_LESS_LEAVES :: c12:c13:c14:c15:null_LESS_LEAVES
const :: a

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

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

   0 => 0
   c => 0
   c2 => 0
   nil => 0
   c4 => 0
   c6 => 0
   c8 => 0
   leaf => 0
   c10 => 0
   c12 => 0
   c13 => 1
   false => 1
   true => 2
   null_minus => 0
   null_quot => 0
   null_app => 0
   null_reverse => 0
   null_shuffle => 0
   null_concat => 0
   null_less_leaves => 0
   null_MINUS => 0
   null_QUOT => 0
   null_APP => 0
   null_REVERSE => 0
   null_SHUFFLE => 0
   null_CONCAT => 0
   null_LESS_LEAVES => 0
   const => 0

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

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

   APP(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   APP(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   APP(z, z') -{ 1 }-> 1 + APP(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0
   CONCAT(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   CONCAT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   CONCAT(z, z') -{ 1 }-> 1 + CONCAT(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0
   LESS_LEAVES(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LESS_LEAVES(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   LESS_LEAVES(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   LESS_LEAVES(z, z') -{ 1 }-> 1 + LESS_LEAVES(concat(z0, z1), concat(z2, z3)) + CONCAT(z0, z1) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   LESS_LEAVES(z, z') -{ 1 }-> 1 + LESS_LEAVES(concat(z0, z1), concat(z2, z3)) + CONCAT(z2, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   MINUS(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   MINUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   QUOT(z, z') -{ 1 }-> 0 :|: z0 >= 0, z' = 1 + z0, z = 0
   QUOT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   QUOT(z, z') -{ 1 }-> 1 + QUOT(minus(z0, z1), 1 + z1) + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   REVERSE(z) -{ 1 }-> 0 :|: z = 0
   REVERSE(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   REVERSE(z) -{ 1 }-> 1 + APP(reverse(z1), 1 + z0 + 0) + REVERSE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   SHUFFLE(z) -{ 1 }-> 0 :|: z = 0
   SHUFFLE(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   SHUFFLE(z) -{ 1 }-> 1 + SHUFFLE(reverse(z1)) + REVERSE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   app(z, z') -{ 0 }-> z0 :|: z0 >= 0, z = 0, z' = z0
   app(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   app(z, z') -{ 0 }-> 1 + z0 + app(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 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
   less_leaves(z, z') -{ 0 }-> less_leaves(concat(z0, z1), concat(z2, z3)) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   less_leaves(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   less_leaves(z, z') -{ 0 }-> 1 :|: z = z0, z0 >= 0, z' = 0
   less_leaves(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   minus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   quot(z, z') -{ 0 }-> 0 :|: z0 >= 0, z' = 1 + z0, z = 0
   quot(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   quot(z, z') -{ 0 }-> 1 + quot(minus(z0, z1), 1 + z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   reverse(z) -{ 0 }-> app(reverse(z1), 1 + z0 + 0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   reverse(z) -{ 0 }-> 0 :|: z = 0
   reverse(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   shuffle(z) -{ 0 }-> 0 :|: z = 0
   shuffle(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   shuffle(z) -{ 0 }-> 1 + z0 + shuffle(reverse(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Only complete derivations are relevant for the runtime complexity.

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

(11) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V1, V),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun2(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun3(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun4(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun5(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun6(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[minus(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[quot(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[app(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[reverse(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[shuffle(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[concat(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun7(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(fun(V1, V, Out),1,[],[Out = 0,V1 = V2,V2 >= 0,V = 0]).
eq(fun(V1, V, Out),1,[fun(V4, V3, Ret1)],[Out = 1 + Ret1,V3 >= 0,V1 = 1 + V4,V4 >= 0,V = 1 + V3]).
eq(fun1(V1, V, Out),1,[],[Out = 0,V5 >= 0,V = 1 + V5,V1 = 0]).
eq(fun1(V1, V, Out),1,[minus(V6, V7, Ret010),fun1(Ret010, 1 + V7, Ret01),fun(V6, V7, Ret11)],[Out = 1 + Ret01 + Ret11,V7 >= 0,V1 = 1 + V6,V6 >= 0,V = 1 + V7]).
eq(fun2(V1, V, Out),1,[],[Out = 0,V8 >= 0,V1 = 0,V = V8]).
eq(fun2(V1, V, Out),1,[fun2(V10, V11, Ret12)],[Out = 1 + Ret12,V10 >= 0,V = V11,V9 >= 0,V1 = 1 + V10 + V9,V11 >= 0]).
eq(fun3(V1, Out),1,[],[Out = 0,V1 = 0]).
eq(fun3(V1, Out),1,[reverse(V13, Ret0101),fun2(Ret0101, 1 + V12 + 0, Ret011),fun3(V13, Ret13)],[Out = 1 + Ret011 + Ret13,V13 >= 0,V12 >= 0,V1 = 1 + V12 + V13]).
eq(fun4(V1, Out),1,[],[Out = 0,V1 = 0]).
eq(fun4(V1, Out),1,[reverse(V14, Ret0102),fun4(Ret0102, Ret012),fun3(V14, Ret14)],[Out = 1 + Ret012 + Ret14,V14 >= 0,V15 >= 0,V1 = 1 + V14 + V15]).
eq(fun5(V1, V, Out),1,[],[Out = 0,V16 >= 0,V1 = 0,V = V16]).
eq(fun5(V1, V, Out),1,[fun5(V17, V19, Ret15)],[Out = 1 + Ret15,V17 >= 0,V = V19,V18 >= 0,V1 = 1 + V17 + V18,V19 >= 0]).
eq(fun6(V1, V, Out),1,[],[Out = 0,V1 = V20,V20 >= 0,V = 0]).
eq(fun6(V1, V, Out),1,[],[Out = 1,V = 1 + V21 + V22,V21 >= 0,V22 >= 0,V1 = 0]).
eq(fun6(V1, V, Out),1,[concat(V24, V23, Ret0103),concat(V25, V26, Ret0111),fun6(Ret0103, Ret0111, Ret013),fun5(V24, V23, Ret16)],[Out = 1 + Ret013 + Ret16,V23 >= 0,V = 1 + V25 + V26,V24 >= 0,V1 = 1 + V23 + V24,V25 >= 0,V26 >= 0]).
eq(fun6(V1, V, Out),1,[concat(V27, V30, Ret0104),concat(V28, V29, Ret0112),fun6(Ret0104, Ret0112, Ret014),fun5(V28, V29, Ret17)],[Out = 1 + Ret014 + Ret17,V30 >= 0,V = 1 + V28 + V29,V27 >= 0,V1 = 1 + V27 + V30,V28 >= 0,V29 >= 0]).
eq(minus(V1, V, Out),0,[],[Out = V31,V1 = V31,V31 >= 0,V = 0]).
eq(minus(V1, V, Out),0,[minus(V33, V32, Ret)],[Out = Ret,V32 >= 0,V1 = 1 + V33,V33 >= 0,V = 1 + V32]).
eq(quot(V1, V, Out),0,[],[Out = 0,V34 >= 0,V = 1 + V34,V1 = 0]).
eq(quot(V1, V, Out),0,[minus(V36, V35, Ret10),quot(Ret10, 1 + V35, Ret18)],[Out = 1 + Ret18,V35 >= 0,V1 = 1 + V36,V36 >= 0,V = 1 + V35]).
eq(app(V1, V, Out),0,[],[Out = V37,V37 >= 0,V1 = 0,V = V37]).
eq(app(V1, V, Out),0,[app(V39, V40, Ret19)],[Out = 1 + Ret19 + V38,V39 >= 0,V = V40,V38 >= 0,V1 = 1 + V38 + V39,V40 >= 0]).
eq(reverse(V1, Out),0,[],[Out = 0,V1 = 0]).
eq(reverse(V1, Out),0,[reverse(V42, Ret0),app(Ret0, 1 + V41 + 0, Ret2)],[Out = Ret2,V42 >= 0,V41 >= 0,V1 = 1 + V41 + V42]).
eq(shuffle(V1, Out),0,[],[Out = 0,V1 = 0]).
eq(shuffle(V1, Out),0,[reverse(V44, Ret101),shuffle(Ret101, Ret110)],[Out = 1 + Ret110 + V43,V44 >= 0,V43 >= 0,V1 = 1 + V43 + V44]).
eq(concat(V1, V, Out),0,[],[Out = V45,V45 >= 0,V1 = 0,V = V45]).
eq(concat(V1, V, Out),0,[concat(V48, V46, Ret111)],[Out = 1 + Ret111 + V47,V48 >= 0,V = V46,V47 >= 0,V1 = 1 + V47 + V48,V46 >= 0]).
eq(fun7(V1, V, Out),0,[],[Out = 1,V1 = V49,V49 >= 0,V = 0]).
eq(fun7(V1, V, Out),0,[],[Out = 2,V = 1 + V50 + V51,V50 >= 0,V51 >= 0,V1 = 0]).
eq(fun7(V1, V, Out),0,[concat(V55, V54, Ret02),concat(V52, V53, Ret112),fun7(Ret02, Ret112, Ret3)],[Out = Ret3,V54 >= 0,V = 1 + V52 + V53,V55 >= 0,V1 = 1 + V54 + V55,V52 >= 0,V53 >= 0]).
eq(minus(V1, V, Out),0,[],[Out = 0,V57 >= 0,V56 >= 0,V1 = V57,V = V56]).
eq(quot(V1, V, Out),0,[],[Out = 0,V59 >= 0,V58 >= 0,V1 = V59,V = V58]).
eq(app(V1, V, Out),0,[],[Out = 0,V61 >= 0,V60 >= 0,V1 = V61,V = V60]).
eq(reverse(V1, Out),0,[],[Out = 0,V62 >= 0,V1 = V62]).
eq(shuffle(V1, Out),0,[],[Out = 0,V63 >= 0,V1 = V63]).
eq(concat(V1, V, Out),0,[],[Out = 0,V64 >= 0,V65 >= 0,V1 = V64,V = V65]).
eq(fun7(V1, V, Out),0,[],[Out = 0,V67 >= 0,V66 >= 0,V1 = V67,V = V66]).
eq(fun(V1, V, Out),0,[],[Out = 0,V68 >= 0,V69 >= 0,V1 = V68,V = V69]).
eq(fun1(V1, V, Out),0,[],[Out = 0,V70 >= 0,V71 >= 0,V1 = V70,V = V71]).
eq(fun2(V1, V, Out),0,[],[Out = 0,V72 >= 0,V73 >= 0,V1 = V72,V = V73]).
eq(fun3(V1, Out),0,[],[Out = 0,V74 >= 0,V1 = V74]).
eq(fun4(V1, Out),0,[],[Out = 0,V75 >= 0,V1 = V75]).
eq(fun5(V1, V, Out),0,[],[Out = 0,V77 >= 0,V76 >= 0,V1 = V77,V = V76]).
eq(fun6(V1, V, Out),0,[],[Out = 0,V79 >= 0,V78 >= 0,V1 = V79,V = V78]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun3(V1,Out),[V1],[Out]).
input_output_vars(fun4(V1,Out),[V1],[Out]).
input_output_vars(fun5(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun6(V1,V,Out),[V1,V],[Out]).
input_output_vars(minus(V1,V,Out),[V1,V],[Out]).
input_output_vars(quot(V1,V,Out),[V1,V],[Out]).
input_output_vars(app(V1,V,Out),[V1,V],[Out]).
input_output_vars(reverse(V1,Out),[V1],[Out]).
input_output_vars(shuffle(V1,Out),[V1],[Out]).
input_output_vars(concat(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun7(V1,V,Out),[V1,V],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive  : [app/3]
1. recursive  : [concat/3]
2. recursive  : [fun/3]
3. recursive  : [minus/3]
4. recursive [non_tail] : [fun1/3]
5. recursive  : [fun2/3]
6. recursive [non_tail] : [reverse/2]
7. recursive  : [fun3/2]
8. recursive [non_tail] : [fun4/2]
9. recursive  : [fun5/3]
10. recursive [non_tail] : [fun6/3]
11. recursive  : [fun7/3]
12. recursive  : [quot/3]
13. recursive  : [shuffle/2]
14. non_recursive  : [start/2]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into app/3
1. SCC is partially evaluated into concat/3
2. SCC is partially evaluated into fun/3
3. SCC is partially evaluated into minus/3
4. SCC is partially evaluated into fun1/3
5. SCC is partially evaluated into fun2/3
6. SCC is partially evaluated into reverse/2
7. SCC is partially evaluated into fun3/2
8. SCC is partially evaluated into fun4/2
9. SCC is partially evaluated into fun5/3
10. SCC is partially evaluated into fun6/3
11. SCC is partially evaluated into fun7/3
12. SCC is partially evaluated into quot/3
13. SCC is partially evaluated into shuffle/2
14. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations app/3 
* CE 45 is refined into CE [57] 
* CE 43 is refined into CE [58] 
* CE 44 is refined into CE [59] 


### Cost equations --> "Loop" of app/3 
* CEs [59] --> Loop 36 
* CEs [57] --> Loop 37 
* CEs [58] --> Loop 38 

### Ranking functions of CR app(V1,V,Out) 
* RF of phase [36]: [V1]

#### Partial ranking functions of CR app(V1,V,Out) 
* Partial RF of phase [36]:
  - RF of loop [36:1]:
    V1


### Specialization of cost equations concat/3 
* CE 52 is refined into CE [60] 
* CE 50 is refined into CE [61] 
* CE 51 is refined into CE [62] 


### Cost equations --> "Loop" of concat/3 
* CEs [62] --> Loop 39 
* CEs [60] --> Loop 40 
* CEs [61] --> Loop 41 

### Ranking functions of CR concat(V1,V,Out) 
* RF of phase [39]: [V1]

#### Partial ranking functions of CR concat(V1,V,Out) 
* Partial RF of phase [39]:
  - RF of loop [39:1]:
    V1


### Specialization of cost equations fun/3 
* CE 15 is refined into CE [63] 
* CE 17 is refined into CE [64] 
* CE 16 is refined into CE [65] 


### Cost equations --> "Loop" of fun/3 
* CEs [65] --> Loop 42 
* CEs [63,64] --> Loop 43 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [42]: [V,V1]

#### Partial ranking functions of CR fun(V1,V,Out) 
* Partial RF of phase [42]:
  - RF of loop [42:1]:
    V
    V1


### Specialization of cost equations minus/3 
* CE 40 is refined into CE [66] 
* CE 38 is refined into CE [67] 
* CE 39 is refined into CE [68] 


### Cost equations --> "Loop" of minus/3 
* CEs [68] --> Loop 44 
* CEs [66] --> Loop 45 
* CEs [67] --> Loop 46 

### Ranking functions of CR minus(V1,V,Out) 
* RF of phase [44]: [V,V1]

#### Partial ranking functions of CR minus(V1,V,Out) 
* Partial RF of phase [44]:
  - RF of loop [44:1]:
    V
    V1


### Specialization of cost equations fun1/3 
* CE 18 is refined into CE [69] 
* CE 20 is refined into CE [70] 
* CE 19 is refined into CE [71,72,73,74,75] 


### Cost equations --> "Loop" of fun1/3 
* CEs [75] --> Loop 47 
* CEs [74] --> Loop 48 
* CEs [73] --> Loop 49 
* CEs [72] --> Loop 50 
* CEs [71] --> Loop 51 
* CEs [69,70] --> Loop 52 

### Ranking functions of CR fun1(V1,V,Out) 
* RF of phase [47,48]: [V1-1,V1-V+1]
* RF of phase [51]: [V1]

#### Partial ranking functions of CR fun1(V1,V,Out) 
* Partial RF of phase [47,48]:
  - RF of loop [47:1,48:1]:
    V1-1
    V1-V+1
* Partial RF of phase [51]:
  - RF of loop [51:1]:
    V1


### Specialization of cost equations fun2/3 
* CE 21 is refined into CE [76] 
* CE 23 is refined into CE [77] 
* CE 22 is refined into CE [78] 


### Cost equations --> "Loop" of fun2/3 
* CEs [78] --> Loop 53 
* CEs [76,77] --> Loop 54 

### Ranking functions of CR fun2(V1,V,Out) 
* RF of phase [53]: [V1]

#### Partial ranking functions of CR fun2(V1,V,Out) 
* Partial RF of phase [53]:
  - RF of loop [53:1]:
    V1


### Specialization of cost equations reverse/2 
* CE 46 is refined into CE [79] 
* CE 47 is refined into CE [80,81,82,83] 


### Cost equations --> "Loop" of reverse/2 
* CEs [83] --> Loop 55 
* CEs [82] --> Loop 56 
* CEs [80] --> Loop 57 
* CEs [81] --> Loop 58 
* CEs [79] --> Loop 59 

### Ranking functions of CR reverse(V1,Out) 
* RF of phase [55,56,57,58]: [V1]

#### Partial ranking functions of CR reverse(V1,Out) 
* Partial RF of phase [55,56,57,58]:
  - RF of loop [55:1,56:1,57:1,58:1]:
    V1


### Specialization of cost equations fun3/2 
* CE 24 is refined into CE [84] 
* CE 26 is refined into CE [85] 
* CE 25 is refined into CE [86,87,88] 


### Cost equations --> "Loop" of fun3/2 
* CEs [88] --> Loop 60 
* CEs [86,87] --> Loop 61 
* CEs [84,85] --> Loop 62 

### Ranking functions of CR fun3(V1,Out) 
* RF of phase [60,61]: [V1]

#### Partial ranking functions of CR fun3(V1,Out) 
* Partial RF of phase [60,61]:
  - RF of loop [60:1]:
    V1-1
  - RF of loop [61:1]:
    V1


### Specialization of cost equations fun4/2 
* CE 27 is refined into CE [89] 
* CE 29 is refined into CE [90] 
* CE 28 is refined into CE [91,92,93,94] 


### Cost equations --> "Loop" of fun4/2 
* CEs [93] --> Loop 63 
* CEs [92,94] --> Loop 64 
* CEs [91] --> Loop 65 
* CEs [89,90] --> Loop 66 

### Ranking functions of CR fun4(V1,Out) 
* RF of phase [63,64]: [V1-1]

#### Partial ranking functions of CR fun4(V1,Out) 
* Partial RF of phase [63,64]:
  - RF of loop [63:1,64:1]:
    V1-1


### Specialization of cost equations fun5/3 
* CE 30 is refined into CE [95] 
* CE 32 is refined into CE [96] 
* CE 31 is refined into CE [97] 


### Cost equations --> "Loop" of fun5/3 
* CEs [97] --> Loop 67 
* CEs [95,96] --> Loop 68 

### Ranking functions of CR fun5(V1,V,Out) 
* RF of phase [67]: [V1]

#### Partial ranking functions of CR fun5(V1,V,Out) 
* Partial RF of phase [67]:
  - RF of loop [67:1]:
    V1


### Specialization of cost equations fun6/3 
* CE 33 is refined into CE [98] 
* CE 37 is refined into CE [99] 
* CE 34 is refined into CE [100] 
* CE 35 is refined into CE [101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128] 
* CE 36 is refined into CE [129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156] 


### Cost equations --> "Loop" of fun6/3 
* CEs [127,155] --> Loop 69 
* CEs [154,156] --> Loop 70 
* CEs [120,128] --> Loop 71 
* CEs [121,125,150,153] --> Loop 72 
* CEs [114,118,122,126] --> Loop 73 
* CEs [104,119,134,148] --> Loop 74 
* CEs [133,135,147,149] --> Loop 75 
* CEs [101,103,113,117,129,132,143,146] --> Loop 76 
* CEs [152] --> Loop 77 
* CEs [123,151] --> Loop 78 
* CEs [116,124] --> Loop 79 
* CEs [131,145] --> Loop 80 
* CEs [102,115,130,144] --> Loop 81 
* CEs [112] --> Loop 82 
* CEs [111,141] --> Loop 83 
* CEs [140,142] --> Loop 84 
* CEs [106,110] --> Loop 85 
* CEs [105,109,136,139] --> Loop 86 
* CEs [108] --> Loop 87 
* CEs [138] --> Loop 88 
* CEs [107,137] --> Loop 89 
* CEs [98,99] --> Loop 90 
* CEs [100] --> Loop 91 

### Ranking functions of CR fun6(V1,V,Out) 
* RF of phase [69,70,71,72,73,74,75,76]: [V,V1]

#### Partial ranking functions of CR fun6(V1,V,Out) 
* Partial RF of phase [69,70,71,72,73,74,75,76]:
  - RF of loop [69:1,70:1,71:1,72:1,73:1]:
    V1-1
  - RF of loop [69:1,70:1,71:1,74:1,75:1]:
    V-1
  - RF of loop [72:1,73:1,76:1]:
    V
  - RF of loop [74:1,75:1,76:1]:
    V1


### Specialization of cost equations fun7/3 
* CE 56 is refined into CE [157] 
* CE 53 is refined into CE [158] 
* CE 54 is refined into CE [159] 
* CE 55 is refined into CE [160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175] 


### Cost equations --> "Loop" of fun7/3 
* CEs [175] --> Loop 92 
* CEs [172,174] --> Loop 93 
* CEs [163,171] --> Loop 94 
* CEs [160,162,168,170] --> Loop 95 
* CEs [173] --> Loop 96 
* CEs [161,169] --> Loop 97 
* CEs [167] --> Loop 98 
* CEs [164,166] --> Loop 99 
* CEs [165] --> Loop 100 
* CEs [157] --> Loop 101 
* CEs [158] --> Loop 102 
* CEs [159] --> Loop 103 

### Ranking functions of CR fun7(V1,V,Out) 
* RF of phase [92,93,94,95]: [V,V1]

#### Partial ranking functions of CR fun7(V1,V,Out) 
* Partial RF of phase [92,93,94,95]:
  - RF of loop [92:1,93:1]:
    V1-1
  - RF of loop [92:1,94:1]:
    V-1
  - RF of loop [93:1,95:1]:
    V
  - RF of loop [94:1,95:1]:
    V1


### Specialization of cost equations quot/3 
* CE 41 is refined into CE [176] 
* CE 42 is refined into CE [177,178,179] 


### Cost equations --> "Loop" of quot/3 
* CEs [179] --> Loop 104 
* CEs [178] --> Loop 105 
* CEs [177] --> Loop 106 
* CEs [176] --> Loop 107 

### Ranking functions of CR quot(V1,V,Out) 
* RF of phase [104]: [V1-1,V1-V+1]
* RF of phase [106]: [V1]

#### Partial ranking functions of CR quot(V1,V,Out) 
* Partial RF of phase [104]:
  - RF of loop [104:1]:
    V1-1
    V1-V+1
* Partial RF of phase [106]:
  - RF of loop [106:1]:
    V1


### Specialization of cost equations shuffle/2 
* CE 48 is refined into CE [180] 
* CE 49 is refined into CE [181,182] 


### Cost equations --> "Loop" of shuffle/2 
* CEs [182] --> Loop 108 
* CEs [181] --> Loop 109 
* CEs [180] --> Loop 110 

### Ranking functions of CR shuffle(V1,Out) 
* RF of phase [108]: [V1-1]

#### Partial ranking functions of CR shuffle(V1,Out) 
* Partial RF of phase [108]:
  - RF of loop [108:1]:
    V1-1


### Specialization of cost equations start/2 
* CE 1 is refined into CE [183,184] 
* CE 2 is refined into CE [185,186,187,188,189] 
* CE 3 is refined into CE [190,191] 
* CE 4 is refined into CE [192,193] 
* CE 5 is refined into CE [194,195,196] 
* CE 6 is refined into CE [197,198] 
* CE 7 is refined into CE [199,200,201,202] 
* CE 8 is refined into CE [203,204,205] 
* CE 9 is refined into CE [206,207,208,209,210] 
* CE 10 is refined into CE [211,212,213,214] 
* CE 11 is refined into CE [215,216] 
* CE 12 is refined into CE [217,218] 
* CE 13 is refined into CE [219,220,221,222] 
* CE 14 is refined into CE [223,224,225,226,227] 


### Cost equations --> "Loop" of start/2 
* CEs [185,206] --> Loop 111 
* CEs [203,224] --> Loop 112 
* CEs [183,184,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,204,205,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,225,226,227] --> Loop 113 

### Ranking functions of CR start(V1,V) 

#### Partial ranking functions of CR start(V1,V) 


Computing Bounds
=====================================

#### Cost of chains of app(V1,V,Out):
* Chain [[36],38]: 0
  with precondition: [V+V1=Out,V1>=1,V>=0] 

* Chain [[36],37]: 0
  with precondition: [V>=0,Out>=1,V1>=Out] 

* Chain [38]: 0
  with precondition: [V1=0,V=Out,V>=0] 

* Chain [37]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of concat(V1,V,Out):
* Chain [[39],41]: 0
  with precondition: [V+V1=Out,V1>=1,V>=0] 

* Chain [[39],40]: 0
  with precondition: [V>=0,Out>=1,V1>=Out] 

* Chain [41]: 0
  with precondition: [V1=0,V=Out,V>=0] 

* Chain [40]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun(V1,V,Out):
* Chain [[42],43]: 1*it(42)+1
  Such that:it(42) =< Out

  with precondition: [Out>=1,V1>=Out,V>=Out] 

* Chain [43]: 1
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of minus(V1,V,Out):
* Chain [[44],46]: 0
  with precondition: [V1=Out+V,V>=1,V1>=V] 

* Chain [[44],45]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [46]: 0
  with precondition: [V=0,V1=Out,V1>=0] 

* Chain [45]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun1(V1,V,Out):
* Chain [[51],52]: 2*it(51)+1
  Such that:it(51) =< Out

  with precondition: [V=1,Out>=1,V1>=Out] 

* Chain [[51],50,52]: 2*it(51)+3
  Such that:it(51) =< Out

  with precondition: [V=1,Out>=2,V1>=Out] 

* Chain [[47,48],52]: 4*it(47)+1*s(3)+1
  Such that:aux(2) =< V1-V+1
aux(5) =< V1
it(47) =< aux(5)
s(3) =< aux(5)
it(47) =< aux(2)

  with precondition: [V>=2,Out>=1,V1>=V,V1>=Out] 

* Chain [[47,48],50,52]: 4*it(47)+1*s(3)+3
  Such that:aux(2) =< V1-V+1
aux(6) =< V1
it(47) =< aux(6)
s(3) =< aux(6)
it(47) =< aux(2)

  with precondition: [V>=2,Out>=2,V1>=V+1,V1>=Out] 

* Chain [[47,48],49,52]: 4*it(47)+2*s(3)+3
  Such that:aux(2) =< V1-V+1
aux(7) =< V1
s(3) =< aux(7)
it(47) =< aux(7)
it(47) =< aux(2)

  with precondition: [V>=2,Out>=3,V1>=V+2,V1>=Out] 

* Chain [52]: 1
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [50,52]: 3
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [49,52]: 1*s(4)+3
  Such that:s(4) =< V1

  with precondition: [Out>=2,V1>=Out,V>=Out] 


#### Cost of chains of fun2(V1,V,Out):
* Chain [[53],54]: 1*it(53)+1
  Such that:it(53) =< V1

  with precondition: [V>=0,Out>=1,V1>=Out] 

* Chain [54]: 1
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of reverse(V1,Out):
* Chain [[55,56,57,58],59]: 0
  with precondition: [V1>=1,Out>=0,V1>=Out] 

* Chain [59]: 0
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of fun3(V1,Out):
* Chain [[60,61],62]: 4*it(60)+1*s(21)+1
  Such that:aux(16) =< V1
it(60) =< aux(16)
s(21) =< it(60)*aux(16)

  with precondition: [V1>=1,Out>=1] 

* Chain [62]: 1
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of fun4(V1,Out):
* Chain [[63,64],66]: 4*it(63)+8*s(31)+2*s(32)+1
  Such that:aux(21) =< V1
it(63) =< aux(21)
aux(18) =< aux(21)
s(33) =< it(63)*aux(18)
s(31) =< s(33)
s(32) =< s(31)*aux(21)

  with precondition: [V1>=2,Out>=1] 

* Chain [[63,64],65,66]: 4*it(63)+8*s(31)+2*s(32)+3
  Such that:aux(22) =< V1
it(63) =< aux(22)
aux(18) =< aux(22)
s(33) =< it(63)*aux(18)
s(31) =< s(33)
s(32) =< s(31)*aux(22)

  with precondition: [V1>=2,Out>=2] 

* Chain [66]: 1
  with precondition: [Out=0,V1>=0] 

* Chain [65,66]: 3
  with precondition: [Out=1,V1>=1] 


#### Cost of chains of fun5(V1,V,Out):
* Chain [[67],68]: 1*it(67)+1
  Such that:it(67) =< V1

  with precondition: [V>=0,Out>=1,V1>=Out] 

* Chain [68]: 1
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun6(V1,V,Out):
* Chain [[69,70,71,72,73,74,75,76],91]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+1
  Such that:aux(40) =< V1
aux(41) =< V
it(69) =< aux(40)
it(69) =< aux(41)
aux(29) =< aux(41)-1
aux(34) =< aux(41)
aux(31) =< aux(40)-1
aux(32) =< aux(40)
s(73) =< it(69)*aux(40)
s(71) =< it(69)*aux(41)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=1,V>=2,Out>=2] 

* Chain [[69,70,71,72,73,74,75,76],90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+1
  Such that:aux(42) =< V1
aux(43) =< V
it(69) =< aux(42)
it(69) =< aux(43)
aux(29) =< aux(43)-1
aux(34) =< aux(43)
aux(31) =< aux(42)-1
aux(32) =< aux(42)
s(73) =< it(69)*aux(42)
s(71) =< it(69)*aux(43)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=1,V>=1,Out>=1] 

* Chain [[69,70,71,72,73,74,75,76],89,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+3
  Such that:aux(44) =< V1
aux(45) =< V
it(69) =< aux(44)
it(69) =< aux(45)
aux(29) =< aux(45)-1
aux(34) =< aux(45)
aux(31) =< aux(44)-1
aux(32) =< aux(44)
s(73) =< it(69)*aux(44)
s(71) =< it(69)*aux(45)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=2,V>=2,Out>=2] 

* Chain [[69,70,71,72,73,74,75,76],88,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+1*s(82)+3
  Such that:aux(46) =< V1
aux(47) =< V
s(82) =< aux(47)
it(69) =< aux(46)
it(69) =< aux(47)
aux(29) =< aux(47)-1
aux(34) =< aux(47)
aux(31) =< aux(46)-1
aux(32) =< aux(46)
s(73) =< it(69)*aux(46)
s(71) =< it(69)*aux(47)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=2,V>=3,Out>=3] 

* Chain [[69,70,71,72,73,74,75,76],87,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+1*s(83)+3
  Such that:aux(48) =< V1
aux(49) =< V
s(83) =< aux(48)
it(69) =< aux(48)
it(69) =< aux(49)
aux(29) =< aux(49)-1
aux(34) =< aux(49)
aux(31) =< aux(48)-1
aux(32) =< aux(48)
s(73) =< it(69)*aux(48)
s(71) =< it(69)*aux(49)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=3,V>=2,Out>=3] 

* Chain [[69,70,71,72,73,74,75,76],86,91]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+3
  Such that:aux(50) =< V1
aux(51) =< V
it(69) =< aux(50)
it(69) =< aux(51)
aux(29) =< aux(51)-1
aux(34) =< aux(51)
aux(31) =< aux(50)-1
aux(32) =< aux(50)
s(73) =< it(69)*aux(50)
s(71) =< it(69)*aux(51)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=2,V>=3,Out>=3] 

* Chain [[69,70,71,72,73,74,75,76],86,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+3
  Such that:aux(52) =< V1
aux(53) =< V
it(69) =< aux(52)
it(69) =< aux(53)
aux(29) =< aux(53)-1
aux(34) =< aux(53)
aux(31) =< aux(52)-1
aux(32) =< aux(52)
s(73) =< it(69)*aux(52)
s(71) =< it(69)*aux(53)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=2,V>=2,Out>=2] 

* Chain [[69,70,71,72,73,74,75,76],85,91]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+2*s(84)+3
  Such that:aux(55) =< V1
aux(56) =< V
s(84) =< aux(55)
it(69) =< aux(55)
it(69) =< aux(56)
aux(29) =< aux(56)-1
aux(34) =< aux(56)
aux(31) =< aux(55)-1
aux(32) =< aux(55)
s(73) =< it(69)*aux(55)
s(71) =< it(69)*aux(56)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=3,V>=3,Out>=4] 

* Chain [[69,70,71,72,73,74,75,76],85,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+2*s(84)+3
  Such that:aux(57) =< V1
aux(58) =< V
s(84) =< aux(57)
it(69) =< aux(57)
it(69) =< aux(58)
aux(29) =< aux(58)-1
aux(34) =< aux(58)
aux(31) =< aux(57)-1
aux(32) =< aux(57)
s(73) =< it(69)*aux(57)
s(71) =< it(69)*aux(58)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=3,V>=2,Out>=3] 

* Chain [[69,70,71,72,73,74,75,76],84,91]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+2*s(86)+3
  Such that:aux(60) =< V1
aux(61) =< V
s(86) =< aux(61)
it(69) =< aux(60)
it(69) =< aux(61)
aux(29) =< aux(61)-1
aux(34) =< aux(61)
aux(31) =< aux(60)-1
aux(32) =< aux(60)
s(73) =< it(69)*aux(60)
s(71) =< it(69)*aux(61)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=2,V>=3,Out>=4] 

* Chain [[69,70,71,72,73,74,75,76],84,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+2*s(86)+3
  Such that:aux(63) =< V1
aux(64) =< V
s(86) =< aux(64)
it(69) =< aux(63)
it(69) =< aux(64)
aux(29) =< aux(64)-1
aux(34) =< aux(64)
aux(31) =< aux(63)-1
aux(32) =< aux(63)
s(73) =< it(69)*aux(63)
s(71) =< it(69)*aux(64)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=2,V>=3,Out>=3] 

* Chain [[69,70,71,72,73,74,75,76],83,91]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+3
  Such that:aux(65) =< V1
aux(66) =< V
it(69) =< aux(65)
it(69) =< aux(66)
aux(29) =< aux(66)-1
aux(34) =< aux(66)
aux(31) =< aux(65)-1
aux(32) =< aux(65)
s(73) =< it(69)*aux(65)
s(71) =< it(69)*aux(66)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=2,V>=3,Out>=3] 

* Chain [[69,70,71,72,73,74,75,76],83,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+3
  Such that:aux(67) =< V1
aux(68) =< V
it(69) =< aux(67)
it(69) =< aux(68)
aux(29) =< aux(68)-1
aux(34) =< aux(68)
aux(31) =< aux(67)-1
aux(32) =< aux(67)
s(73) =< it(69)*aux(67)
s(71) =< it(69)*aux(68)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=2,V>=3,Out>=2] 

* Chain [[69,70,71,72,73,74,75,76],82,91]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+1*s(88)+3
  Such that:aux(69) =< V1
aux(70) =< V
s(88) =< aux(69)
it(69) =< aux(69)
it(69) =< aux(70)
aux(29) =< aux(70)-1
aux(34) =< aux(70)
aux(31) =< aux(69)-1
aux(32) =< aux(69)
s(73) =< it(69)*aux(69)
s(71) =< it(69)*aux(70)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=3,V>=3,Out>=4] 

* Chain [[69,70,71,72,73,74,75,76],82,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+1*s(88)+3
  Such that:aux(71) =< V1
aux(72) =< V
s(88) =< aux(71)
it(69) =< aux(71)
it(69) =< aux(72)
aux(29) =< aux(72)-1
aux(34) =< aux(72)
aux(31) =< aux(71)-1
aux(32) =< aux(71)
s(73) =< it(69)*aux(71)
s(71) =< it(69)*aux(72)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=3,V>=3,Out>=3] 

* Chain [[69,70,71,72,73,74,75,76],81,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+3
  Such that:aux(73) =< V1
aux(74) =< V
it(69) =< aux(73)
it(69) =< aux(74)
aux(29) =< aux(74)-1
aux(34) =< aux(74)
aux(31) =< aux(73)-1
aux(32) =< aux(73)
s(73) =< it(69)*aux(73)
s(71) =< it(69)*aux(74)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=2,V>=2,Out>=2] 

* Chain [[69,70,71,72,73,74,75,76],80,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+2*s(89)+3
  Such that:aux(76) =< V1
aux(77) =< V
s(89) =< aux(77)
it(69) =< aux(76)
it(69) =< aux(77)
aux(29) =< aux(77)-1
aux(34) =< aux(77)
aux(31) =< aux(76)-1
aux(32) =< aux(76)
s(73) =< it(69)*aux(76)
s(71) =< it(69)*aux(77)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=2,V>=3,Out>=3] 

* Chain [[69,70,71,72,73,74,75,76],79,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+2*s(91)+3
  Such that:aux(79) =< V1
aux(80) =< V
s(91) =< aux(79)
it(69) =< aux(79)
it(69) =< aux(80)
aux(29) =< aux(80)-1
aux(34) =< aux(80)
aux(31) =< aux(79)-1
aux(32) =< aux(79)
s(73) =< it(69)*aux(79)
s(71) =< it(69)*aux(80)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=3,V>=2,Out>=3] 

* Chain [[69,70,71,72,73,74,75,76],78,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+3
  Such that:aux(81) =< V1
aux(82) =< V
it(69) =< aux(81)
it(69) =< aux(82)
aux(29) =< aux(82)-1
aux(34) =< aux(82)
aux(31) =< aux(81)-1
aux(32) =< aux(81)
s(73) =< it(69)*aux(81)
s(71) =< it(69)*aux(82)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=3,V>=2,Out>=2] 

* Chain [[69,70,71,72,73,74,75,76],77,90]: 16*it(69)+1*s(70)+1*s(71)+1*s(72)+1*s(73)+2*s(74)+2*s(75)+2*s(78)+2*s(79)+1*s(93)+3
  Such that:aux(83) =< V1
aux(84) =< V
s(93) =< aux(84)
it(69) =< aux(83)
it(69) =< aux(84)
aux(29) =< aux(84)-1
aux(34) =< aux(84)
aux(31) =< aux(83)-1
aux(32) =< aux(83)
s(73) =< it(69)*aux(83)
s(71) =< it(69)*aux(84)
s(80) =< it(69)*aux(29)
s(81) =< it(69)*aux(34)
s(76) =< it(69)*aux(31)
s(77) =< it(69)*aux(32)
s(72) =< it(69)*aux(31)
s(70) =< it(69)*aux(29)
s(79) =< s(81)
s(78) =< s(80)
s(75) =< s(77)
s(74) =< s(76)

  with precondition: [V1>=3,V>=3,Out>=3] 

* Chain [91]: 1
  with precondition: [V1=0,Out=1,V>=1] 

* Chain [90]: 1
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [89,90]: 3
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [88,90]: 1*s(82)+3
  Such that:s(82) =< V

  with precondition: [V1>=1,Out>=2,V>=Out] 

* Chain [87,90]: 1*s(83)+3
  Such that:s(83) =< V1

  with precondition: [V>=1,Out>=2,V1>=Out] 

* Chain [86,91]: 3
  with precondition: [Out=2,V1>=1,V>=2] 

* Chain [86,90]: 3
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [85,91]: 2*s(84)+3
  Such that:aux(54) =< V1
s(84) =< aux(54)

  with precondition: [V>=2,Out>=3,V1+1>=Out] 

* Chain [85,90]: 2*s(84)+3
  Such that:aux(54) =< V1
s(84) =< aux(54)

  with precondition: [V>=1,Out>=2,V1>=Out] 

* Chain [84,91]: 2*s(86)+3
  Such that:aux(59) =< V
s(86) =< aux(59)

  with precondition: [V1>=1,Out>=3,V+1>=Out] 

* Chain [84,90]: 2*s(86)+3
  Such that:aux(62) =< V
s(86) =< aux(62)

  with precondition: [V1>=1,Out>=2,V>=Out] 

* Chain [83,91]: 3
  with precondition: [Out=2,V1>=1,V>=2] 

* Chain [83,90]: 3
  with precondition: [Out=1,V1>=1,V>=2] 

* Chain [82,91]: 1*s(88)+3
  Such that:s(88) =< V1

  with precondition: [V>=2,Out>=3,V1+1>=Out] 

* Chain [82,90]: 1*s(88)+3
  Such that:s(88) =< V1

  with precondition: [V>=2,Out>=2,V1>=Out] 

* Chain [81,90]: 3
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [80,90]: 2*s(89)+3
  Such that:aux(75) =< V
s(89) =< aux(75)

  with precondition: [V1>=1,Out>=2,V>=Out] 

* Chain [79,90]: 2*s(91)+3
  Such that:aux(78) =< V1
s(91) =< aux(78)

  with precondition: [V>=1,Out>=2,V1>=Out] 

* Chain [78,90]: 3
  with precondition: [Out=1,V1>=2,V>=1] 

* Chain [77,90]: 1*s(93)+3
  Such that:s(93) =< V

  with precondition: [V1>=2,Out>=2,V>=Out] 


#### Cost of chains of fun7(V1,V,Out):
* Chain [[92,93,94,95],103]: 0
  with precondition: [Out=2,V1>=1,V>=2] 

* Chain [[92,93,94,95],102]: 0
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [[92,93,94,95],101]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [[92,93,94,95],100,102]: 0
  with precondition: [Out=1,V1>=2,V>=2] 

* Chain [[92,93,94,95],100,101]: 0
  with precondition: [Out=0,V1>=2,V>=2] 

* Chain [[92,93,94,95],99,103]: 0
  with precondition: [Out=2,V1>=2,V>=3] 

* Chain [[92,93,94,95],99,102]: 0
  with precondition: [Out=1,V1>=2,V>=2] 

* Chain [[92,93,94,95],99,101]: 0
  with precondition: [Out=0,V1>=2,V>=2] 

* Chain [[92,93,94,95],98,103]: 0
  with precondition: [Out=2,V1>=2,V>=3] 

* Chain [[92,93,94,95],98,101]: 0
  with precondition: [Out=0,V1>=2,V>=3] 

* Chain [[92,93,94,95],97,102]: 0
  with precondition: [Out=1,V1>=2,V>=2] 

* Chain [[92,93,94,95],97,101]: 0
  with precondition: [Out=0,V1>=2,V>=2] 

* Chain [[92,93,94,95],96,102]: 0
  with precondition: [Out=1,V1>=3,V>=2] 

* Chain [[92,93,94,95],96,101]: 0
  with precondition: [Out=0,V1>=3,V>=2] 

* Chain [103]: 0
  with precondition: [V1=0,Out=2,V>=1] 

* Chain [102]: 0
  with precondition: [V=0,Out=1,V1>=0] 

* Chain [101]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [100,102]: 0
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [100,101]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [99,103]: 0
  with precondition: [Out=2,V1>=1,V>=2] 

* Chain [99,102]: 0
  with precondition: [V=1,Out=1,V1>=1] 

* Chain [99,101]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [98,103]: 0
  with precondition: [Out=2,V1>=1,V>=2] 

* Chain [98,101]: 0
  with precondition: [Out=0,V1>=1,V>=2] 

* Chain [97,102]: 0
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [97,101]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [96,102]: 0
  with precondition: [Out=1,V1>=2,V>=1] 

* Chain [96,101]: 0
  with precondition: [Out=0,V1>=2,V>=1] 


#### Cost of chains of quot(V1,V,Out):
* Chain [[106],107]: 0
  with precondition: [V=1,Out>=1,V1>=Out] 

* Chain [[106],105,107]: 0
  with precondition: [V=1,Out>=2,V1>=Out] 

* Chain [[104],107]: 0
  with precondition: [V>=2,Out>=1,V1+2>=2*Out+V] 

* Chain [[104],105,107]: 0
  with precondition: [V>=2,Out>=2,V1+3>=2*Out+V] 

* Chain [107]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [105,107]: 0
  with precondition: [Out=1,V1>=1,V>=1] 


#### Cost of chains of shuffle(V1,Out):
* Chain [[108],110]: 0
  with precondition: [Out>=1,V1>=Out+1] 

* Chain [[108],109,110]: 0
  with precondition: [Out>=2,V1>=Out] 

* Chain [110]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [109,110]: 0
  with precondition: [Out>=1,V1>=Out] 


#### Cost of chains of start(V1,V):
* Chain [113]: 17*s(502)+37*s(505)+12*s(506)+1*s(511)+16*s(516)+4*s(517)+320*s(523)+20*s(528)+20*s(529)+20*s(534)+20*s(535)+40*s(536)+40*s(537)+40*s(538)+40*s(539)+3
  Such that:s(504) =< V1-V+1
aux(91) =< V1
aux(92) =< V
s(505) =< aux(91)
s(502) =< aux(92)
s(506) =< aux(91)
s(506) =< s(504)
s(511) =< s(505)*aux(91)
s(514) =< aux(91)
s(515) =< s(505)*s(514)
s(516) =< s(515)
s(517) =< s(516)*aux(91)
s(523) =< aux(91)
s(523) =< aux(92)
s(524) =< aux(92)-1
s(525) =< aux(92)
s(526) =< aux(91)-1
s(528) =< s(523)*aux(91)
s(529) =< s(523)*aux(92)
s(530) =< s(523)*s(524)
s(531) =< s(523)*s(525)
s(532) =< s(523)*s(526)
s(533) =< s(523)*s(514)
s(534) =< s(523)*s(526)
s(535) =< s(523)*s(524)
s(536) =< s(531)
s(537) =< s(530)
s(538) =< s(533)
s(539) =< s(532)

  with precondition: [V1>=0] 

* Chain [112]: 0
  with precondition: [V=0,V1>=0] 

* Chain [111]: 4*s(541)+3
  Such that:s(540) =< V1
s(541) =< s(540)

  with precondition: [V=1,V1>=1] 


Closed-form bounds of start(V1,V): 
-------------------------------------
* Chain [113] with precondition: [V1>=0] 
    - Upper bound: 369*V1+3+77*V1*V1+4*V1*V1*V1+60*V1*nat(V)+60*V1*nat(V1-1)+60*V1*nat(nat(V)+ -1)+nat(V)*17 
    - Complexity: n^3 
* Chain [112] with precondition: [V=0,V1>=0] 
    - Upper bound: 0 
    - Complexity: constant 
* Chain [111] with precondition: [V=1,V1>=1] 
    - Upper bound: 4*V1+3 
    - Complexity: n 

### Maximum cost of start(V1,V): 77*V1*V1+365*V1+4*V1*V1*V1+60*V1*nat(V)+60*V1*nat(V1-1)+60*V1*nat(nat(V)+ -1)+nat(V)*17+(4*V1+3) 
Asymptotic class: n^3 
* Total analysis performed in 2634 ms.


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

(12)
BOUNDS(1, n^3)

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

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

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


The TRS R consists of the following rules:

   MINUS(z0, 0') -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   QUOT(0', s(z0)) -> c2
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   APP(nil, z0) -> c4
   APP(add(z0, z1), z2) -> c5(APP(z1, z2))
   REVERSE(nil) -> c6
   REVERSE(add(z0, z1)) -> c7(APP(reverse(z1), add(z0, nil)), REVERSE(z1))
   SHUFFLE(nil) -> c8
   SHUFFLE(add(z0, z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
   CONCAT(leaf, z0) -> c10
   CONCAT(cons(z0, z1), z2) -> c11(CONCAT(z1, z2))
   LESS_LEAVES(z0, leaf) -> c12
   LESS_LEAVES(leaf, cons(z0, z1)) -> c13
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1))
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3))

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

   minus(z0, 0') -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0', s(z0)) -> 0'
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   app(nil, z0) -> z0
   app(add(z0, z1), z2) -> add(z0, app(z1, z2))
   reverse(nil) -> nil
   reverse(add(z0, z1)) -> app(reverse(z1), add(z0, nil))
   shuffle(nil) -> nil
   shuffle(add(z0, z1)) -> add(z0, shuffle(reverse(z1)))
   concat(leaf, z0) -> z0
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
   less_leaves(z0, leaf) -> false
   less_leaves(leaf, cons(z0, z1)) -> true
   less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

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

(15) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
APP/1
add/0
CONCAT/1

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

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


The TRS R consists of the following rules:

   MINUS(z0, 0') -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   QUOT(0', s(z0)) -> c2
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   APP(nil) -> c4
   APP(add(z1)) -> c5(APP(z1))
   REVERSE(nil) -> c6
   REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
   SHUFFLE(nil) -> c8
   SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
   CONCAT(leaf) -> c10
   CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
   LESS_LEAVES(z0, leaf) -> c12
   LESS_LEAVES(leaf, cons(z0, z1)) -> c13
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
   LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))

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

   minus(z0, 0') -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0', s(z0)) -> 0'
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   app(nil, z0) -> z0
   app(add(z1), z2) -> add(app(z1, z2))
   reverse(nil) -> nil
   reverse(add(z1)) -> app(reverse(z1), add(nil))
   shuffle(nil) -> nil
   shuffle(add(z1)) -> add(shuffle(reverse(z1)))
   concat(leaf, z0) -> z0
   concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
   less_leaves(z0, leaf) -> false
   less_leaves(leaf, cons(z0, z1)) -> true
   less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

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

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

(18)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15

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

(19) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MINUS, QUOT, minus, APP, REVERSE, reverse, SHUFFLE, CONCAT, LESS_LEAVES, concat, quot, app, shuffle, less_leaves

They will be analysed ascendingly in the following order:
MINUS < QUOT
minus < QUOT
minus < quot
APP < REVERSE
reverse < REVERSE
REVERSE < SHUFFLE
reverse < SHUFFLE
app < reverse
reverse < shuffle
CONCAT < LESS_LEAVES
concat < LESS_LEAVES
concat < less_leaves

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

(20)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
MINUS, QUOT, minus, APP, REVERSE, reverse, SHUFFLE, CONCAT, LESS_LEAVES, concat, quot, app, shuffle, less_leaves

They will be analysed ascendingly in the following order:
MINUS < QUOT
minus < QUOT
minus < quot
APP < REVERSE
reverse < REVERSE
REVERSE < SHUFFLE
reverse < SHUFFLE
app < reverse
reverse < shuffle
CONCAT < LESS_LEAVES
concat < LESS_LEAVES
concat < less_leaves

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)

Induction Base:
MINUS(gen_0':s13_16(0), gen_0':s13_16(0)) ->_R^Omega(1)
c

Induction Step:
MINUS(gen_0':s13_16(+(n23_16, 1)), gen_0':s13_16(+(n23_16, 1))) ->_R^Omega(1)
c1(MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16))) ->_IH
c1(gen_c:c112_16(c24_16))

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

(22)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
MINUS, QUOT, minus, APP, REVERSE, reverse, SHUFFLE, CONCAT, LESS_LEAVES, concat, quot, app, shuffle, less_leaves

They will be analysed ascendingly in the following order:
MINUS < QUOT
minus < QUOT
minus < quot
APP < REVERSE
reverse < REVERSE
REVERSE < SHUFFLE
reverse < SHUFFLE
app < reverse
reverse < shuffle
CONCAT < LESS_LEAVES
concat < LESS_LEAVES
concat < less_leaves

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

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

(25)
BOUNDS(n^1, INF)

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

(26)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
minus, QUOT, APP, REVERSE, reverse, SHUFFLE, CONCAT, LESS_LEAVES, concat, quot, app, shuffle, less_leaves

They will be analysed ascendingly in the following order:
minus < QUOT
minus < quot
APP < REVERSE
reverse < REVERSE
REVERSE < SHUFFLE
reverse < SHUFFLE
app < reverse
reverse < shuffle
CONCAT < LESS_LEAVES
concat < LESS_LEAVES
concat < less_leaves

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)

Induction Base:
minus(gen_0':s13_16(0), gen_0':s13_16(0)) ->_R^Omega(0)
gen_0':s13_16(0)

Induction Step:
minus(gen_0':s13_16(+(n545_16, 1)), gen_0':s13_16(+(n545_16, 1))) ->_R^Omega(0)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) ->_IH
gen_0':s13_16(0)

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

(28)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
QUOT, APP, REVERSE, reverse, SHUFFLE, CONCAT, LESS_LEAVES, concat, quot, app, shuffle, less_leaves

They will be analysed ascendingly in the following order:
APP < REVERSE
reverse < REVERSE
REVERSE < SHUFFLE
reverse < SHUFFLE
app < reverse
reverse < shuffle
CONCAT < LESS_LEAVES
concat < LESS_LEAVES
concat < less_leaves

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)

Induction Base:
APP(gen_nil:add16_16(0)) ->_R^Omega(1)
c4

Induction Step:
APP(gen_nil:add16_16(+(n3099_16, 1))) ->_R^Omega(1)
c5(APP(gen_nil:add16_16(n3099_16))) ->_IH
c5(gen_c4:c515_16(c3100_16))

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

(30)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
CONCAT, REVERSE, reverse, SHUFFLE, LESS_LEAVES, concat, quot, app, shuffle, less_leaves

They will be analysed ascendingly in the following order:
reverse < REVERSE
REVERSE < SHUFFLE
reverse < SHUFFLE
app < reverse
reverse < shuffle
CONCAT < LESS_LEAVES
concat < LESS_LEAVES
concat < less_leaves

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)

Induction Base:
CONCAT(gen_leaf:cons20_16(0)) ->_R^Omega(1)
c10

Induction Step:
CONCAT(gen_leaf:cons20_16(+(n3571_16, 1))) ->_R^Omega(1)
c11(CONCAT(gen_leaf:cons20_16(n3571_16))) ->_IH
c11(gen_c10:c1119_16(c3572_16))

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

(32)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
concat, REVERSE, reverse, SHUFFLE, LESS_LEAVES, quot, app, shuffle, less_leaves

They will be analysed ascendingly in the following order:
reverse < REVERSE
REVERSE < SHUFFLE
reverse < SHUFFLE
app < reverse
reverse < shuffle
concat < LESS_LEAVES
concat < less_leaves

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b)) -> gen_leaf:cons20_16(+(n4189_16, b)), rt in Omega(0)

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

Induction Step:
concat(gen_leaf:cons20_16(+(n4189_16, 1)), gen_leaf:cons20_16(b)) ->_R^Omega(0)
cons(leaf, concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b))) ->_IH
cons(leaf, gen_leaf:cons20_16(+(b, c4190_16)))

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

(34)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)
concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b)) -> gen_leaf:cons20_16(+(n4189_16, b)), rt in Omega(0)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
LESS_LEAVES, REVERSE, reverse, SHUFFLE, quot, app, shuffle, less_leaves

They will be analysed ascendingly in the following order:
reverse < REVERSE
REVERSE < SHUFFLE
reverse < SHUFFLE
app < reverse
reverse < shuffle

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LESS_LEAVES(gen_leaf:cons20_16(n6898_16), gen_leaf:cons20_16(n6898_16)) -> gen_c12:c13:c14:c1521_16(n6898_16), rt in Omega(1 + n6898_16)

Induction Base:
LESS_LEAVES(gen_leaf:cons20_16(0), gen_leaf:cons20_16(0)) ->_R^Omega(1)
c12

Induction Step:
LESS_LEAVES(gen_leaf:cons20_16(+(n6898_16, 1)), gen_leaf:cons20_16(+(n6898_16, 1))) ->_R^Omega(1)
c14(LESS_LEAVES(concat(leaf, gen_leaf:cons20_16(n6898_16)), concat(leaf, gen_leaf:cons20_16(n6898_16))), CONCAT(leaf)) ->_L^Omega(0)
c14(LESS_LEAVES(gen_leaf:cons20_16(+(0, n6898_16)), concat(leaf, gen_leaf:cons20_16(n6898_16))), CONCAT(leaf)) ->_L^Omega(0)
c14(LESS_LEAVES(gen_leaf:cons20_16(n6898_16), gen_leaf:cons20_16(+(0, n6898_16))), CONCAT(leaf)) ->_IH
c14(gen_c12:c13:c14:c1521_16(c6899_16), CONCAT(leaf)) ->_L^Omega(1)
c14(gen_c12:c13:c14:c1521_16(n6898_16), gen_c10:c1119_16(0))

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

(36)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)
concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b)) -> gen_leaf:cons20_16(+(n4189_16, b)), rt in Omega(0)
LESS_LEAVES(gen_leaf:cons20_16(n6898_16), gen_leaf:cons20_16(n6898_16)) -> gen_c12:c13:c14:c1521_16(n6898_16), rt in Omega(1 + n6898_16)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
quot, REVERSE, reverse, SHUFFLE, app, shuffle, less_leaves

They will be analysed ascendingly in the following order:
reverse < REVERSE
REVERSE < SHUFFLE
reverse < SHUFFLE
app < reverse
reverse < shuffle

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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
app(gen_nil:add16_16(n12374_16), gen_nil:add16_16(b)) -> gen_nil:add16_16(+(n12374_16, b)), rt in Omega(0)

Induction Base:
app(gen_nil:add16_16(0), gen_nil:add16_16(b)) ->_R^Omega(0)
gen_nil:add16_16(b)

Induction Step:
app(gen_nil:add16_16(+(n12374_16, 1)), gen_nil:add16_16(b)) ->_R^Omega(0)
add(app(gen_nil:add16_16(n12374_16), gen_nil:add16_16(b))) ->_IH
add(gen_nil:add16_16(+(b, c12375_16)))

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

(38)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)
concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b)) -> gen_leaf:cons20_16(+(n4189_16, b)), rt in Omega(0)
LESS_LEAVES(gen_leaf:cons20_16(n6898_16), gen_leaf:cons20_16(n6898_16)) -> gen_c12:c13:c14:c1521_16(n6898_16), rt in Omega(1 + n6898_16)
app(gen_nil:add16_16(n12374_16), gen_nil:add16_16(b)) -> gen_nil:add16_16(+(n12374_16, b)), rt in Omega(0)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
reverse, REVERSE, SHUFFLE, shuffle, less_leaves

They will be analysed ascendingly in the following order:
reverse < REVERSE
REVERSE < SHUFFLE
reverse < SHUFFLE
reverse < shuffle

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

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
reverse(gen_nil:add16_16(n14733_16)) -> gen_nil:add16_16(n14733_16), rt in Omega(0)

Induction Base:
reverse(gen_nil:add16_16(0)) ->_R^Omega(0)
nil

Induction Step:
reverse(gen_nil:add16_16(+(n14733_16, 1))) ->_R^Omega(0)
app(reverse(gen_nil:add16_16(n14733_16)), add(nil)) ->_IH
app(gen_nil:add16_16(c14734_16), add(nil)) ->_L^Omega(0)
gen_nil:add16_16(+(n14733_16, +(0, 1)))

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

(40)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)
concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b)) -> gen_leaf:cons20_16(+(n4189_16, b)), rt in Omega(0)
LESS_LEAVES(gen_leaf:cons20_16(n6898_16), gen_leaf:cons20_16(n6898_16)) -> gen_c12:c13:c14:c1521_16(n6898_16), rt in Omega(1 + n6898_16)
app(gen_nil:add16_16(n12374_16), gen_nil:add16_16(b)) -> gen_nil:add16_16(+(n12374_16, b)), rt in Omega(0)
reverse(gen_nil:add16_16(n14733_16)) -> gen_nil:add16_16(n14733_16), rt in Omega(0)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
REVERSE, SHUFFLE, shuffle, less_leaves

They will be analysed ascendingly in the following order:
REVERSE < SHUFFLE

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

(41) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REVERSE(gen_nil:add16_16(n15246_16)) -> *22_16, rt in Omega(n15246_16 + n15246_16^2)

Induction Base:
REVERSE(gen_nil:add16_16(0))

Induction Step:
REVERSE(gen_nil:add16_16(+(n15246_16, 1))) ->_R^Omega(1)
c7(APP(reverse(gen_nil:add16_16(n15246_16))), REVERSE(gen_nil:add16_16(n15246_16))) ->_L^Omega(0)
c7(APP(gen_nil:add16_16(n15246_16)), REVERSE(gen_nil:add16_16(n15246_16))) ->_L^Omega(1 + n15246_16)
c7(gen_c4:c515_16(n15246_16), REVERSE(gen_nil:add16_16(n15246_16))) ->_IH
c7(gen_c4:c515_16(n15246_16), *22_16)

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

(42)
Complex Obligation (BEST)

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

(43)
Obligation:
Proved the lower bound n^2 for the following obligation:

Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)
concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b)) -> gen_leaf:cons20_16(+(n4189_16, b)), rt in Omega(0)
LESS_LEAVES(gen_leaf:cons20_16(n6898_16), gen_leaf:cons20_16(n6898_16)) -> gen_c12:c13:c14:c1521_16(n6898_16), rt in Omega(1 + n6898_16)
app(gen_nil:add16_16(n12374_16), gen_nil:add16_16(b)) -> gen_nil:add16_16(+(n12374_16, b)), rt in Omega(0)
reverse(gen_nil:add16_16(n14733_16)) -> gen_nil:add16_16(n14733_16), rt in Omega(0)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
REVERSE, SHUFFLE, shuffle, less_leaves

They will be analysed ascendingly in the following order:
REVERSE < SHUFFLE

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

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

(45)
BOUNDS(n^2, INF)

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

(46)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)
concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b)) -> gen_leaf:cons20_16(+(n4189_16, b)), rt in Omega(0)
LESS_LEAVES(gen_leaf:cons20_16(n6898_16), gen_leaf:cons20_16(n6898_16)) -> gen_c12:c13:c14:c1521_16(n6898_16), rt in Omega(1 + n6898_16)
app(gen_nil:add16_16(n12374_16), gen_nil:add16_16(b)) -> gen_nil:add16_16(+(n12374_16, b)), rt in Omega(0)
reverse(gen_nil:add16_16(n14733_16)) -> gen_nil:add16_16(n14733_16), rt in Omega(0)
REVERSE(gen_nil:add16_16(n15246_16)) -> *22_16, rt in Omega(n15246_16 + n15246_16^2)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
SHUFFLE, shuffle, less_leaves
----------------------------------------

(47) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SHUFFLE(gen_nil:add16_16(n22278_16)) -> *22_16, rt in Omega(n22278_16 + n22278_16^2 + n22278_16^3)

Induction Base:
SHUFFLE(gen_nil:add16_16(0))

Induction Step:
SHUFFLE(gen_nil:add16_16(+(n22278_16, 1))) ->_R^Omega(1)
c9(SHUFFLE(reverse(gen_nil:add16_16(n22278_16))), REVERSE(gen_nil:add16_16(n22278_16))) ->_L^Omega(0)
c9(SHUFFLE(gen_nil:add16_16(n22278_16)), REVERSE(gen_nil:add16_16(n22278_16))) ->_IH
c9(*22_16, REVERSE(gen_nil:add16_16(n22278_16))) ->_L^Omega(n22278_16 + n22278_16^2)
c9(*22_16, *22_16)

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

(48)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)
concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b)) -> gen_leaf:cons20_16(+(n4189_16, b)), rt in Omega(0)
LESS_LEAVES(gen_leaf:cons20_16(n6898_16), gen_leaf:cons20_16(n6898_16)) -> gen_c12:c13:c14:c1521_16(n6898_16), rt in Omega(1 + n6898_16)
app(gen_nil:add16_16(n12374_16), gen_nil:add16_16(b)) -> gen_nil:add16_16(+(n12374_16, b)), rt in Omega(0)
reverse(gen_nil:add16_16(n14733_16)) -> gen_nil:add16_16(n14733_16), rt in Omega(0)
REVERSE(gen_nil:add16_16(n15246_16)) -> *22_16, rt in Omega(n15246_16 + n15246_16^2)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
SHUFFLE, shuffle, less_leaves
----------------------------------------

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

(51)
BOUNDS(n^3, INF)

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

(52)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)
concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b)) -> gen_leaf:cons20_16(+(n4189_16, b)), rt in Omega(0)
LESS_LEAVES(gen_leaf:cons20_16(n6898_16), gen_leaf:cons20_16(n6898_16)) -> gen_c12:c13:c14:c1521_16(n6898_16), rt in Omega(1 + n6898_16)
app(gen_nil:add16_16(n12374_16), gen_nil:add16_16(b)) -> gen_nil:add16_16(+(n12374_16, b)), rt in Omega(0)
reverse(gen_nil:add16_16(n14733_16)) -> gen_nil:add16_16(n14733_16), rt in Omega(0)
REVERSE(gen_nil:add16_16(n15246_16)) -> *22_16, rt in Omega(n15246_16 + n15246_16^2)
SHUFFLE(gen_nil:add16_16(n22278_16)) -> *22_16, rt in Omega(n22278_16 + n22278_16^2 + n22278_16^3)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


The following defined symbols remain to be analysed:
shuffle, less_leaves
----------------------------------------

(53) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
shuffle(gen_nil:add16_16(n35865_16)) -> gen_nil:add16_16(n35865_16), rt in Omega(0)

Induction Base:
shuffle(gen_nil:add16_16(0)) ->_R^Omega(0)
nil

Induction Step:
shuffle(gen_nil:add16_16(+(n35865_16, 1))) ->_R^Omega(0)
add(shuffle(reverse(gen_nil:add16_16(n35865_16)))) ->_L^Omega(0)
add(shuffle(gen_nil:add16_16(n35865_16))) ->_IH
add(gen_nil:add16_16(c35866_16))

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

(54)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
APP(nil) -> c4
APP(add(z1)) -> c5(APP(z1))
REVERSE(nil) -> c6
REVERSE(add(z1)) -> c7(APP(reverse(z1)), REVERSE(z1))
SHUFFLE(nil) -> c8
SHUFFLE(add(z1)) -> c9(SHUFFLE(reverse(z1)), REVERSE(z1))
CONCAT(leaf) -> c10
CONCAT(cons(z0, z1)) -> c11(CONCAT(z1))
LESS_LEAVES(z0, leaf) -> c12
LESS_LEAVES(leaf, cons(z0, z1)) -> c13
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c14(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0))
LESS_LEAVES(cons(z0, z1), cons(z2, z3)) -> c15(LESS_LEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
app(nil, z0) -> z0
app(add(z1), z2) -> add(app(z1, z2))
reverse(nil) -> nil
reverse(add(z1)) -> app(reverse(z1), add(nil))
shuffle(nil) -> nil
shuffle(add(z1)) -> add(shuffle(reverse(z1)))
concat(leaf, z0) -> z0
concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2))
less_leaves(z0, leaf) -> false
less_leaves(leaf, cons(z0, z1)) -> true
less_leaves(cons(z0, z1), cons(z2, z3)) -> less_leaves(concat(z0, z1), concat(z2, z3))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
APP :: nil:add -> c4:c5
nil :: nil:add
c4 :: c4:c5
add :: nil:add -> nil:add
c5 :: c4:c5 -> c4:c5
REVERSE :: nil:add -> c6:c7
c6 :: c6:c7
c7 :: c4:c5 -> c6:c7 -> c6:c7
reverse :: nil:add -> nil:add
SHUFFLE :: nil:add -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c6:c7 -> c8:c9
CONCAT :: leaf:cons -> c10:c11
leaf :: leaf:cons
c10 :: c10:c11
cons :: leaf:cons -> leaf:cons -> leaf:cons
c11 :: c10:c11 -> c10:c11
LESS_LEAVES :: leaf:cons -> leaf:cons -> c12:c13:c14:c15
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
concat :: leaf:cons -> leaf:cons -> leaf:cons
c15 :: c12:c13:c14:c15 -> c10:c11 -> c12:c13:c14:c15
quot :: 0':s -> 0':s -> 0':s
app :: nil:add -> nil:add -> nil:add
shuffle :: nil:add -> nil:add
less_leaves :: leaf:cons -> leaf:cons -> false:true
false :: false:true
true :: false:true
hole_c:c11_16 :: c:c1
hole_0':s2_16 :: 0':s
hole_c2:c33_16 :: c2:c3
hole_c4:c54_16 :: c4:c5
hole_nil:add5_16 :: nil:add
hole_c6:c76_16 :: c6:c7
hole_c8:c97_16 :: c8:c9
hole_c10:c118_16 :: c10:c11
hole_leaf:cons9_16 :: leaf:cons
hole_c12:c13:c14:c1510_16 :: c12:c13:c14:c15
hole_false:true11_16 :: false:true
gen_c:c112_16 :: Nat -> c:c1
gen_0':s13_16 :: Nat -> 0':s
gen_c2:c314_16 :: Nat -> c2:c3
gen_c4:c515_16 :: Nat -> c4:c5
gen_nil:add16_16 :: Nat -> nil:add
gen_c6:c717_16 :: Nat -> c6:c7
gen_c8:c918_16 :: Nat -> c8:c9
gen_c10:c1119_16 :: Nat -> c10:c11
gen_leaf:cons20_16 :: Nat -> leaf:cons
gen_c12:c13:c14:c1521_16 :: Nat -> c12:c13:c14:c15


Lemmas:
MINUS(gen_0':s13_16(n23_16), gen_0':s13_16(n23_16)) -> gen_c:c112_16(n23_16), rt in Omega(1 + n23_16)
minus(gen_0':s13_16(n545_16), gen_0':s13_16(n545_16)) -> gen_0':s13_16(0), rt in Omega(0)
APP(gen_nil:add16_16(n3099_16)) -> gen_c4:c515_16(n3099_16), rt in Omega(1 + n3099_16)
CONCAT(gen_leaf:cons20_16(n3571_16)) -> gen_c10:c1119_16(n3571_16), rt in Omega(1 + n3571_16)
concat(gen_leaf:cons20_16(n4189_16), gen_leaf:cons20_16(b)) -> gen_leaf:cons20_16(+(n4189_16, b)), rt in Omega(0)
LESS_LEAVES(gen_leaf:cons20_16(n6898_16), gen_leaf:cons20_16(n6898_16)) -> gen_c12:c13:c14:c1521_16(n6898_16), rt in Omega(1 + n6898_16)
app(gen_nil:add16_16(n12374_16), gen_nil:add16_16(b)) -> gen_nil:add16_16(+(n12374_16, b)), rt in Omega(0)
reverse(gen_nil:add16_16(n14733_16)) -> gen_nil:add16_16(n14733_16), rt in Omega(0)
REVERSE(gen_nil:add16_16(n15246_16)) -> *22_16, rt in Omega(n15246_16 + n15246_16^2)
SHUFFLE(gen_nil:add16_16(n22278_16)) -> *22_16, rt in Omega(n22278_16 + n22278_16^2 + n22278_16^3)
shuffle(gen_nil:add16_16(n35865_16)) -> gen_nil:add16_16(n35865_16), rt in Omega(0)


Generator Equations:
gen_c:c112_16(0) <=> c
gen_c:c112_16(+(x, 1)) <=> c1(gen_c:c112_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c2:c314_16(0) <=> c2
gen_c2:c314_16(+(x, 1)) <=> c3(gen_c2:c314_16(x), c)
gen_c4:c515_16(0) <=> c4
gen_c4:c515_16(+(x, 1)) <=> c5(gen_c4:c515_16(x))
gen_nil:add16_16(0) <=> nil
gen_nil:add16_16(+(x, 1)) <=> add(gen_nil:add16_16(x))
gen_c6:c717_16(0) <=> c6
gen_c6:c717_16(+(x, 1)) <=> c7(c4, gen_c6:c717_16(x))
gen_c8:c918_16(0) <=> c8
gen_c8:c918_16(+(x, 1)) <=> c9(gen_c8:c918_16(x), c6)
gen_c10:c1119_16(0) <=> c10
gen_c10:c1119_16(+(x, 1)) <=> c11(gen_c10:c1119_16(x))
gen_leaf:cons20_16(0) <=> leaf
gen_leaf:cons20_16(+(x, 1)) <=> cons(leaf, gen_leaf:cons20_16(x))
gen_c12:c13:c14:c1521_16(0) <=> c12
gen_c12:c13:c14:c1521_16(+(x, 1)) <=> c14(gen_c12:c13:c14:c1521_16(x), c10)


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

(55) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
less_leaves(gen_leaf:cons20_16(n36377_16), gen_leaf:cons20_16(n36377_16)) -> false, rt in Omega(0)

Induction Base:
less_leaves(gen_leaf:cons20_16(0), gen_leaf:cons20_16(0)) ->_R^Omega(0)
false

Induction Step:
less_leaves(gen_leaf:cons20_16(+(n36377_16, 1)), gen_leaf:cons20_16(+(n36377_16, 1))) ->_R^Omega(0)
less_leaves(concat(leaf, gen_leaf:cons20_16(n36377_16)), concat(leaf, gen_leaf:cons20_16(n36377_16))) ->_L^Omega(0)
less_leaves(gen_leaf:cons20_16(+(0, n36377_16)), concat(leaf, gen_leaf:cons20_16(n36377_16))) ->_L^Omega(0)
less_leaves(gen_leaf:cons20_16(n36377_16), gen_leaf:cons20_16(+(0, n36377_16))) ->_IH
false

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

(56)
BOUNDS(1, INF)