WORST_CASE(Omega(n^1),?)
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^1, INF).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 22.3 s]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 6 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 227 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 12 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 93 ms]
(16) BEST
    (17) proven lower bound
        (18) LowerBoundPropagationProof [FINISHED, 0 ms]
        (19) BOUNDS(n^1, INF)
    (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 11 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 17 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 48 ms]
        (26) typed CpxTrs


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

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


The TRS R consists of the following rules:

   LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0))
   LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
   LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
   IF(true, z0, z1, z2, z3) -> c4
   IF(false, true, z0, z1, z2) -> c5
   IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
   LENGTH(nil) -> c7
   LENGTH(cons(z0, z1)) -> c8(LENGTH(z1))
   TOLIST(leaf) -> c9
   TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0))
   TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2))
   APPEND(nil, z0) -> c12
   APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2))
   LE(s(z0), 0) -> c14
   LE(0, z0) -> c15
   LE(s(z0), s(z1)) -> c16(LE(z0, z1))
   A -> c17
   A -> c18

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

   lessElements(z0, z1) -> lessE(z0, z1, 0)
   lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
   if(true, z0, z1, z2, z3) -> z1
   if(false, true, z0, z1, z2) -> z1
   if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   toList(leaf) -> nil
   toList(node(z0, z1, z2)) -> append(toList(z0), cons(z1, toList(z2)))
   append(nil, z0) -> z0
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   le(s(z0), 0) -> false
   le(0, z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   a -> c
   a -> d

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

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

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


The TRS R consists of the following rules:

   LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0))
   LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
   LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
   IF(true, z0, z1, z2, z3) -> c4
   IF(false, true, z0, z1, z2) -> c5
   IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
   LENGTH(nil) -> c7
   LENGTH(cons(z0, z1)) -> c8(LENGTH(z1))
   TOLIST(leaf) -> c9
   TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0))
   TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2))
   APPEND(nil, z0) -> c12
   APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2))
   LE(s(z0), 0) -> c14
   LE(0, z0) -> c15
   LE(s(z0), s(z1)) -> c16(LE(z0, z1))
   A -> c17
   A -> c18

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

   lessElements(z0, z1) -> lessE(z0, z1, 0)
   lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
   if(true, z0, z1, z2, z3) -> z1
   if(false, true, z0, z1, z2) -> z1
   if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   toList(leaf) -> nil
   toList(node(z0, z1, z2)) -> append(toList(z0), cons(z1, toList(z2)))
   append(nil, z0) -> z0
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   le(s(z0), 0) -> false
   le(0, z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   a -> c
   a -> d

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

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

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


The TRS R consists of the following rules:

   LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
   LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
   LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
   IF(true, z0, z1, z2, z3) -> c4
   IF(false, true, z0, z1, z2) -> c5
   IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
   LENGTH(nil) -> c7
   LENGTH(cons(z0, z1)) -> c8(LENGTH(z1))
   TOLIST(leaf) -> c9
   TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0))
   TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2))
   APPEND(nil, z0) -> c12
   APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2))
   LE(s(z0), 0') -> c14
   LE(0', z0) -> c15
   LE(s(z0), s(z1)) -> c16(LE(z0, z1))
   A -> c17
   A -> c18

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

   lessElements(z0, z1) -> lessE(z0, z1, 0')
   lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
   if(true, z0, z1, z2, z3) -> z1
   if(false, true, z0, z1, z2) -> z1
   if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
   length(nil) -> 0'
   length(cons(z0, z1)) -> s(length(z1))
   toList(leaf) -> nil
   toList(node(z0, z1, z2)) -> append(toList(z0), cons(z1, toList(z2)))
   append(nil, z0) -> z0
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   le(s(z0), 0') -> false
   le(0', z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   a -> c
   a -> d

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
cons/0
node/1

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

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


The TRS R consists of the following rules:

   LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
   LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
   LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
   IF(true, z0, z1, z2, z3) -> c4
   IF(false, true, z0, z1, z2) -> c5
   IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
   LENGTH(nil) -> c7
   LENGTH(cons(z1)) -> c8(LENGTH(z1))
   TOLIST(leaf) -> c9
   TOLIST(node(z0, z2)) -> c10(APPEND(toList(z0), cons(toList(z2))), TOLIST(z0))
   TOLIST(node(z0, z2)) -> c11(APPEND(toList(z0), cons(toList(z2))), TOLIST(z2))
   APPEND(nil, z0) -> c12
   APPEND(cons(z1), z2) -> c13(APPEND(z1, z2))
   LE(s(z0), 0') -> c14
   LE(0', z0) -> c15
   LE(s(z0), s(z1)) -> c16(LE(z0, z1))
   A -> c17
   A -> c18

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

   lessElements(z0, z1) -> lessE(z0, z1, 0')
   lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
   if(true, z0, z1, z2, z3) -> z1
   if(false, true, z0, z1, z2) -> z1
   if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
   length(nil) -> 0'
   length(cons(z1)) -> s(length(z1))
   toList(leaf) -> nil
   toList(node(z0, z2)) -> append(toList(z0), cons(toList(z2)))
   append(nil, z0) -> z0
   append(cons(z1), z2) -> cons(append(z1, z2))
   le(s(z0), 0') -> false
   le(0', z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   a -> c
   a -> d

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

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

(8)
Obligation:
Innermost TRS:
Rules:
LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
IF(true, z0, z1, z2, z3) -> c4
IF(false, true, z0, z1, z2) -> c5
IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
LENGTH(nil) -> c7
LENGTH(cons(z1)) -> c8(LENGTH(z1))
TOLIST(leaf) -> c9
TOLIST(node(z0, z2)) -> c10(APPEND(toList(z0), cons(toList(z2))), TOLIST(z0))
TOLIST(node(z0, z2)) -> c11(APPEND(toList(z0), cons(toList(z2))), TOLIST(z2))
APPEND(nil, z0) -> c12
APPEND(cons(z1), z2) -> c13(APPEND(z1, z2))
LE(s(z0), 0') -> c14
LE(0', z0) -> c15
LE(s(z0), s(z1)) -> c16(LE(z0, z1))
A -> c17
A -> c18
lessElements(z0, z1) -> lessE(z0, z1, 0')
lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
if(true, z0, z1, z2, z3) -> z1
if(false, true, z0, z1, z2) -> z1
if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))
toList(leaf) -> nil
toList(node(z0, z2)) -> append(toList(z0), cons(toList(z2)))
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
a -> c
a -> d

Types:
LESSELEMENTS :: nil:cons:leaf:node -> nil:cons:leaf:node -> c1
c1 :: c2:c3 -> c1
LESSE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c2:c3
0' :: 0':s
c2 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c2:c3
IF :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c4:c5:c6
le :: 0':s -> 0':s -> true:false
length :: nil:cons:leaf:node -> 0':s
toList :: nil:cons:leaf:node -> nil:cons:leaf:node
LE :: 0':s -> 0':s -> c14:c15:c16
LENGTH :: nil:cons:leaf:node -> c7:c8
c3 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c9:c10:c11 -> c2:c3
TOLIST :: nil:cons:leaf:node -> c9:c10:c11
true :: true:false
c4 :: c4:c5:c6
false :: true:false
c5 :: c4:c5:c6
c6 :: c2:c3 -> c4:c5:c6
s :: 0':s -> 0':s
nil :: nil:cons:leaf:node
c7 :: c7:c8
cons :: nil:cons:leaf:node -> nil:cons:leaf:node
c8 :: c7:c8 -> c7:c8
leaf :: nil:cons:leaf:node
c9 :: c9:c10:c11
node :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
c10 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
APPEND :: nil:cons:leaf:node -> nil:cons:leaf:node -> c12:c13
c11 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
c14 :: c14:c15:c16
c15 :: c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
A :: c17:c18
c17 :: c17:c18
c18 :: c17:c18
lessElements :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
lessE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
if :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
append :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
a :: c:d
c :: c:d
d :: c:d
hole_c11_19 :: c1
hole_nil:cons:leaf:node2_19 :: nil:cons:leaf:node
hole_c2:c33_19 :: c2:c3
hole_0':s4_19 :: 0':s
hole_c4:c5:c65_19 :: c4:c5:c6
hole_c14:c15:c166_19 :: c14:c15:c16
hole_c7:c87_19 :: c7:c8
hole_true:false8_19 :: true:false
hole_c9:c10:c119_19 :: c9:c10:c11
hole_c12:c1310_19 :: c12:c13
hole_c17:c1811_19 :: c17:c18
hole_c:d12_19 :: c:d
gen_nil:cons:leaf:node13_19 :: Nat -> nil:cons:leaf:node
gen_0':s14_19 :: Nat -> 0':s
gen_c14:c15:c1615_19 :: Nat -> c14:c15:c16
gen_c7:c816_19 :: Nat -> c7:c8
gen_c9:c10:c1117_19 :: Nat -> c9:c10:c11
gen_c12:c1318_19 :: Nat -> c12:c13

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LESSE, le, length, toList, LE, LENGTH, TOLIST, APPEND, lessE, append

They will be analysed ascendingly in the following order:
le < LESSE
length < LESSE
toList < LESSE
LE < LESSE
LENGTH < LESSE
TOLIST < LESSE
le < lessE
length < lessE
toList < TOLIST
toList < lessE
append < toList
APPEND < TOLIST

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

(10)
Obligation:
Innermost TRS:
Rules:
LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
IF(true, z0, z1, z2, z3) -> c4
IF(false, true, z0, z1, z2) -> c5
IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
LENGTH(nil) -> c7
LENGTH(cons(z1)) -> c8(LENGTH(z1))
TOLIST(leaf) -> c9
TOLIST(node(z0, z2)) -> c10(APPEND(toList(z0), cons(toList(z2))), TOLIST(z0))
TOLIST(node(z0, z2)) -> c11(APPEND(toList(z0), cons(toList(z2))), TOLIST(z2))
APPEND(nil, z0) -> c12
APPEND(cons(z1), z2) -> c13(APPEND(z1, z2))
LE(s(z0), 0') -> c14
LE(0', z0) -> c15
LE(s(z0), s(z1)) -> c16(LE(z0, z1))
A -> c17
A -> c18
lessElements(z0, z1) -> lessE(z0, z1, 0')
lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
if(true, z0, z1, z2, z3) -> z1
if(false, true, z0, z1, z2) -> z1
if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))
toList(leaf) -> nil
toList(node(z0, z2)) -> append(toList(z0), cons(toList(z2)))
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
a -> c
a -> d

Types:
LESSELEMENTS :: nil:cons:leaf:node -> nil:cons:leaf:node -> c1
c1 :: c2:c3 -> c1
LESSE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c2:c3
0' :: 0':s
c2 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c2:c3
IF :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c4:c5:c6
le :: 0':s -> 0':s -> true:false
length :: nil:cons:leaf:node -> 0':s
toList :: nil:cons:leaf:node -> nil:cons:leaf:node
LE :: 0':s -> 0':s -> c14:c15:c16
LENGTH :: nil:cons:leaf:node -> c7:c8
c3 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c9:c10:c11 -> c2:c3
TOLIST :: nil:cons:leaf:node -> c9:c10:c11
true :: true:false
c4 :: c4:c5:c6
false :: true:false
c5 :: c4:c5:c6
c6 :: c2:c3 -> c4:c5:c6
s :: 0':s -> 0':s
nil :: nil:cons:leaf:node
c7 :: c7:c8
cons :: nil:cons:leaf:node -> nil:cons:leaf:node
c8 :: c7:c8 -> c7:c8
leaf :: nil:cons:leaf:node
c9 :: c9:c10:c11
node :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
c10 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
APPEND :: nil:cons:leaf:node -> nil:cons:leaf:node -> c12:c13
c11 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
c14 :: c14:c15:c16
c15 :: c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
A :: c17:c18
c17 :: c17:c18
c18 :: c17:c18
lessElements :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
lessE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
if :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
append :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
a :: c:d
c :: c:d
d :: c:d
hole_c11_19 :: c1
hole_nil:cons:leaf:node2_19 :: nil:cons:leaf:node
hole_c2:c33_19 :: c2:c3
hole_0':s4_19 :: 0':s
hole_c4:c5:c65_19 :: c4:c5:c6
hole_c14:c15:c166_19 :: c14:c15:c16
hole_c7:c87_19 :: c7:c8
hole_true:false8_19 :: true:false
hole_c9:c10:c119_19 :: c9:c10:c11
hole_c12:c1310_19 :: c12:c13
hole_c17:c1811_19 :: c17:c18
hole_c:d12_19 :: c:d
gen_nil:cons:leaf:node13_19 :: Nat -> nil:cons:leaf:node
gen_0':s14_19 :: Nat -> 0':s
gen_c14:c15:c1615_19 :: Nat -> c14:c15:c16
gen_c7:c816_19 :: Nat -> c7:c8
gen_c9:c10:c1117_19 :: Nat -> c9:c10:c11
gen_c12:c1318_19 :: Nat -> c12:c13


Generator Equations:
gen_nil:cons:leaf:node13_19(0) <=> nil
gen_nil:cons:leaf:node13_19(+(x, 1)) <=> cons(gen_nil:cons:leaf:node13_19(x))
gen_0':s14_19(0) <=> 0'
gen_0':s14_19(+(x, 1)) <=> s(gen_0':s14_19(x))
gen_c14:c15:c1615_19(0) <=> c14
gen_c14:c15:c1615_19(+(x, 1)) <=> c16(gen_c14:c15:c1615_19(x))
gen_c7:c816_19(0) <=> c7
gen_c7:c816_19(+(x, 1)) <=> c8(gen_c7:c816_19(x))
gen_c9:c10:c1117_19(0) <=> c9
gen_c9:c10:c1117_19(+(x, 1)) <=> c10(c12, gen_c9:c10:c1117_19(x))
gen_c12:c1318_19(0) <=> c12
gen_c12:c1318_19(+(x, 1)) <=> c13(gen_c12:c1318_19(x))


The following defined symbols remain to be analysed:
le, LESSE, length, toList, LE, LENGTH, TOLIST, APPEND, lessE, append

They will be analysed ascendingly in the following order:
le < LESSE
length < LESSE
toList < LESSE
LE < LESSE
LENGTH < LESSE
TOLIST < LESSE
le < lessE
length < lessE
toList < TOLIST
toList < lessE
append < toList
APPEND < TOLIST

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_0':s14_19(+(1, n20_19)), gen_0':s14_19(n20_19)) -> false, rt in Omega(0)

Induction Base:
le(gen_0':s14_19(+(1, 0)), gen_0':s14_19(0)) ->_R^Omega(0)
false

Induction Step:
le(gen_0':s14_19(+(1, +(n20_19, 1))), gen_0':s14_19(+(n20_19, 1))) ->_R^Omega(0)
le(gen_0':s14_19(+(1, n20_19)), gen_0':s14_19(n20_19)) ->_IH
false

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

(12)
Obligation:
Innermost TRS:
Rules:
LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
IF(true, z0, z1, z2, z3) -> c4
IF(false, true, z0, z1, z2) -> c5
IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
LENGTH(nil) -> c7
LENGTH(cons(z1)) -> c8(LENGTH(z1))
TOLIST(leaf) -> c9
TOLIST(node(z0, z2)) -> c10(APPEND(toList(z0), cons(toList(z2))), TOLIST(z0))
TOLIST(node(z0, z2)) -> c11(APPEND(toList(z0), cons(toList(z2))), TOLIST(z2))
APPEND(nil, z0) -> c12
APPEND(cons(z1), z2) -> c13(APPEND(z1, z2))
LE(s(z0), 0') -> c14
LE(0', z0) -> c15
LE(s(z0), s(z1)) -> c16(LE(z0, z1))
A -> c17
A -> c18
lessElements(z0, z1) -> lessE(z0, z1, 0')
lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
if(true, z0, z1, z2, z3) -> z1
if(false, true, z0, z1, z2) -> z1
if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))
toList(leaf) -> nil
toList(node(z0, z2)) -> append(toList(z0), cons(toList(z2)))
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
a -> c
a -> d

Types:
LESSELEMENTS :: nil:cons:leaf:node -> nil:cons:leaf:node -> c1
c1 :: c2:c3 -> c1
LESSE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c2:c3
0' :: 0':s
c2 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c2:c3
IF :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c4:c5:c6
le :: 0':s -> 0':s -> true:false
length :: nil:cons:leaf:node -> 0':s
toList :: nil:cons:leaf:node -> nil:cons:leaf:node
LE :: 0':s -> 0':s -> c14:c15:c16
LENGTH :: nil:cons:leaf:node -> c7:c8
c3 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c9:c10:c11 -> c2:c3
TOLIST :: nil:cons:leaf:node -> c9:c10:c11
true :: true:false
c4 :: c4:c5:c6
false :: true:false
c5 :: c4:c5:c6
c6 :: c2:c3 -> c4:c5:c6
s :: 0':s -> 0':s
nil :: nil:cons:leaf:node
c7 :: c7:c8
cons :: nil:cons:leaf:node -> nil:cons:leaf:node
c8 :: c7:c8 -> c7:c8
leaf :: nil:cons:leaf:node
c9 :: c9:c10:c11
node :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
c10 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
APPEND :: nil:cons:leaf:node -> nil:cons:leaf:node -> c12:c13
c11 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
c14 :: c14:c15:c16
c15 :: c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
A :: c17:c18
c17 :: c17:c18
c18 :: c17:c18
lessElements :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
lessE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
if :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
append :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
a :: c:d
c :: c:d
d :: c:d
hole_c11_19 :: c1
hole_nil:cons:leaf:node2_19 :: nil:cons:leaf:node
hole_c2:c33_19 :: c2:c3
hole_0':s4_19 :: 0':s
hole_c4:c5:c65_19 :: c4:c5:c6
hole_c14:c15:c166_19 :: c14:c15:c16
hole_c7:c87_19 :: c7:c8
hole_true:false8_19 :: true:false
hole_c9:c10:c119_19 :: c9:c10:c11
hole_c12:c1310_19 :: c12:c13
hole_c17:c1811_19 :: c17:c18
hole_c:d12_19 :: c:d
gen_nil:cons:leaf:node13_19 :: Nat -> nil:cons:leaf:node
gen_0':s14_19 :: Nat -> 0':s
gen_c14:c15:c1615_19 :: Nat -> c14:c15:c16
gen_c7:c816_19 :: Nat -> c7:c8
gen_c9:c10:c1117_19 :: Nat -> c9:c10:c11
gen_c12:c1318_19 :: Nat -> c12:c13


Lemmas:
le(gen_0':s14_19(+(1, n20_19)), gen_0':s14_19(n20_19)) -> false, rt in Omega(0)


Generator Equations:
gen_nil:cons:leaf:node13_19(0) <=> nil
gen_nil:cons:leaf:node13_19(+(x, 1)) <=> cons(gen_nil:cons:leaf:node13_19(x))
gen_0':s14_19(0) <=> 0'
gen_0':s14_19(+(x, 1)) <=> s(gen_0':s14_19(x))
gen_c14:c15:c1615_19(0) <=> c14
gen_c14:c15:c1615_19(+(x, 1)) <=> c16(gen_c14:c15:c1615_19(x))
gen_c7:c816_19(0) <=> c7
gen_c7:c816_19(+(x, 1)) <=> c8(gen_c7:c816_19(x))
gen_c9:c10:c1117_19(0) <=> c9
gen_c9:c10:c1117_19(+(x, 1)) <=> c10(c12, gen_c9:c10:c1117_19(x))
gen_c12:c1318_19(0) <=> c12
gen_c12:c1318_19(+(x, 1)) <=> c13(gen_c12:c1318_19(x))


The following defined symbols remain to be analysed:
length, LESSE, toList, LE, LENGTH, TOLIST, APPEND, lessE, append

They will be analysed ascendingly in the following order:
length < LESSE
toList < LESSE
LE < LESSE
LENGTH < LESSE
TOLIST < LESSE
length < lessE
toList < TOLIST
toList < lessE
append < toList
APPEND < TOLIST

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
length(gen_nil:cons:leaf:node13_19(n435_19)) -> gen_0':s14_19(n435_19), rt in Omega(0)

Induction Base:
length(gen_nil:cons:leaf:node13_19(0)) ->_R^Omega(0)
0'

Induction Step:
length(gen_nil:cons:leaf:node13_19(+(n435_19, 1))) ->_R^Omega(0)
s(length(gen_nil:cons:leaf:node13_19(n435_19))) ->_IH
s(gen_0':s14_19(c436_19))

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

(14)
Obligation:
Innermost TRS:
Rules:
LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
IF(true, z0, z1, z2, z3) -> c4
IF(false, true, z0, z1, z2) -> c5
IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
LENGTH(nil) -> c7
LENGTH(cons(z1)) -> c8(LENGTH(z1))
TOLIST(leaf) -> c9
TOLIST(node(z0, z2)) -> c10(APPEND(toList(z0), cons(toList(z2))), TOLIST(z0))
TOLIST(node(z0, z2)) -> c11(APPEND(toList(z0), cons(toList(z2))), TOLIST(z2))
APPEND(nil, z0) -> c12
APPEND(cons(z1), z2) -> c13(APPEND(z1, z2))
LE(s(z0), 0') -> c14
LE(0', z0) -> c15
LE(s(z0), s(z1)) -> c16(LE(z0, z1))
A -> c17
A -> c18
lessElements(z0, z1) -> lessE(z0, z1, 0')
lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
if(true, z0, z1, z2, z3) -> z1
if(false, true, z0, z1, z2) -> z1
if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))
toList(leaf) -> nil
toList(node(z0, z2)) -> append(toList(z0), cons(toList(z2)))
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
a -> c
a -> d

Types:
LESSELEMENTS :: nil:cons:leaf:node -> nil:cons:leaf:node -> c1
c1 :: c2:c3 -> c1
LESSE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c2:c3
0' :: 0':s
c2 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c2:c3
IF :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c4:c5:c6
le :: 0':s -> 0':s -> true:false
length :: nil:cons:leaf:node -> 0':s
toList :: nil:cons:leaf:node -> nil:cons:leaf:node
LE :: 0':s -> 0':s -> c14:c15:c16
LENGTH :: nil:cons:leaf:node -> c7:c8
c3 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c9:c10:c11 -> c2:c3
TOLIST :: nil:cons:leaf:node -> c9:c10:c11
true :: true:false
c4 :: c4:c5:c6
false :: true:false
c5 :: c4:c5:c6
c6 :: c2:c3 -> c4:c5:c6
s :: 0':s -> 0':s
nil :: nil:cons:leaf:node
c7 :: c7:c8
cons :: nil:cons:leaf:node -> nil:cons:leaf:node
c8 :: c7:c8 -> c7:c8
leaf :: nil:cons:leaf:node
c9 :: c9:c10:c11
node :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
c10 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
APPEND :: nil:cons:leaf:node -> nil:cons:leaf:node -> c12:c13
c11 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
c14 :: c14:c15:c16
c15 :: c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
A :: c17:c18
c17 :: c17:c18
c18 :: c17:c18
lessElements :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
lessE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
if :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
append :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
a :: c:d
c :: c:d
d :: c:d
hole_c11_19 :: c1
hole_nil:cons:leaf:node2_19 :: nil:cons:leaf:node
hole_c2:c33_19 :: c2:c3
hole_0':s4_19 :: 0':s
hole_c4:c5:c65_19 :: c4:c5:c6
hole_c14:c15:c166_19 :: c14:c15:c16
hole_c7:c87_19 :: c7:c8
hole_true:false8_19 :: true:false
hole_c9:c10:c119_19 :: c9:c10:c11
hole_c12:c1310_19 :: c12:c13
hole_c17:c1811_19 :: c17:c18
hole_c:d12_19 :: c:d
gen_nil:cons:leaf:node13_19 :: Nat -> nil:cons:leaf:node
gen_0':s14_19 :: Nat -> 0':s
gen_c14:c15:c1615_19 :: Nat -> c14:c15:c16
gen_c7:c816_19 :: Nat -> c7:c8
gen_c9:c10:c1117_19 :: Nat -> c9:c10:c11
gen_c12:c1318_19 :: Nat -> c12:c13


Lemmas:
le(gen_0':s14_19(+(1, n20_19)), gen_0':s14_19(n20_19)) -> false, rt in Omega(0)
length(gen_nil:cons:leaf:node13_19(n435_19)) -> gen_0':s14_19(n435_19), rt in Omega(0)


Generator Equations:
gen_nil:cons:leaf:node13_19(0) <=> nil
gen_nil:cons:leaf:node13_19(+(x, 1)) <=> cons(gen_nil:cons:leaf:node13_19(x))
gen_0':s14_19(0) <=> 0'
gen_0':s14_19(+(x, 1)) <=> s(gen_0':s14_19(x))
gen_c14:c15:c1615_19(0) <=> c14
gen_c14:c15:c1615_19(+(x, 1)) <=> c16(gen_c14:c15:c1615_19(x))
gen_c7:c816_19(0) <=> c7
gen_c7:c816_19(+(x, 1)) <=> c8(gen_c7:c816_19(x))
gen_c9:c10:c1117_19(0) <=> c9
gen_c9:c10:c1117_19(+(x, 1)) <=> c10(c12, gen_c9:c10:c1117_19(x))
gen_c12:c1318_19(0) <=> c12
gen_c12:c1318_19(+(x, 1)) <=> c13(gen_c12:c1318_19(x))


The following defined symbols remain to be analysed:
LE, LESSE, toList, LENGTH, TOLIST, APPEND, lessE, append

They will be analysed ascendingly in the following order:
toList < LESSE
LE < LESSE
LENGTH < LESSE
TOLIST < LESSE
toList < TOLIST
toList < lessE
append < toList
APPEND < TOLIST

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s14_19(+(1, n824_19)), gen_0':s14_19(n824_19)) -> gen_c14:c15:c1615_19(n824_19), rt in Omega(1 + n824_19)

Induction Base:
LE(gen_0':s14_19(+(1, 0)), gen_0':s14_19(0)) ->_R^Omega(1)
c14

Induction Step:
LE(gen_0':s14_19(+(1, +(n824_19, 1))), gen_0':s14_19(+(n824_19, 1))) ->_R^Omega(1)
c16(LE(gen_0':s14_19(+(1, n824_19)), gen_0':s14_19(n824_19))) ->_IH
c16(gen_c14:c15:c1615_19(c825_19))

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

(16)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
IF(true, z0, z1, z2, z3) -> c4
IF(false, true, z0, z1, z2) -> c5
IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
LENGTH(nil) -> c7
LENGTH(cons(z1)) -> c8(LENGTH(z1))
TOLIST(leaf) -> c9
TOLIST(node(z0, z2)) -> c10(APPEND(toList(z0), cons(toList(z2))), TOLIST(z0))
TOLIST(node(z0, z2)) -> c11(APPEND(toList(z0), cons(toList(z2))), TOLIST(z2))
APPEND(nil, z0) -> c12
APPEND(cons(z1), z2) -> c13(APPEND(z1, z2))
LE(s(z0), 0') -> c14
LE(0', z0) -> c15
LE(s(z0), s(z1)) -> c16(LE(z0, z1))
A -> c17
A -> c18
lessElements(z0, z1) -> lessE(z0, z1, 0')
lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
if(true, z0, z1, z2, z3) -> z1
if(false, true, z0, z1, z2) -> z1
if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))
toList(leaf) -> nil
toList(node(z0, z2)) -> append(toList(z0), cons(toList(z2)))
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
a -> c
a -> d

Types:
LESSELEMENTS :: nil:cons:leaf:node -> nil:cons:leaf:node -> c1
c1 :: c2:c3 -> c1
LESSE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c2:c3
0' :: 0':s
c2 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c2:c3
IF :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c4:c5:c6
le :: 0':s -> 0':s -> true:false
length :: nil:cons:leaf:node -> 0':s
toList :: nil:cons:leaf:node -> nil:cons:leaf:node
LE :: 0':s -> 0':s -> c14:c15:c16
LENGTH :: nil:cons:leaf:node -> c7:c8
c3 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c9:c10:c11 -> c2:c3
TOLIST :: nil:cons:leaf:node -> c9:c10:c11
true :: true:false
c4 :: c4:c5:c6
false :: true:false
c5 :: c4:c5:c6
c6 :: c2:c3 -> c4:c5:c6
s :: 0':s -> 0':s
nil :: nil:cons:leaf:node
c7 :: c7:c8
cons :: nil:cons:leaf:node -> nil:cons:leaf:node
c8 :: c7:c8 -> c7:c8
leaf :: nil:cons:leaf:node
c9 :: c9:c10:c11
node :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
c10 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
APPEND :: nil:cons:leaf:node -> nil:cons:leaf:node -> c12:c13
c11 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
c14 :: c14:c15:c16
c15 :: c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
A :: c17:c18
c17 :: c17:c18
c18 :: c17:c18
lessElements :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
lessE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
if :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
append :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
a :: c:d
c :: c:d
d :: c:d
hole_c11_19 :: c1
hole_nil:cons:leaf:node2_19 :: nil:cons:leaf:node
hole_c2:c33_19 :: c2:c3
hole_0':s4_19 :: 0':s
hole_c4:c5:c65_19 :: c4:c5:c6
hole_c14:c15:c166_19 :: c14:c15:c16
hole_c7:c87_19 :: c7:c8
hole_true:false8_19 :: true:false
hole_c9:c10:c119_19 :: c9:c10:c11
hole_c12:c1310_19 :: c12:c13
hole_c17:c1811_19 :: c17:c18
hole_c:d12_19 :: c:d
gen_nil:cons:leaf:node13_19 :: Nat -> nil:cons:leaf:node
gen_0':s14_19 :: Nat -> 0':s
gen_c14:c15:c1615_19 :: Nat -> c14:c15:c16
gen_c7:c816_19 :: Nat -> c7:c8
gen_c9:c10:c1117_19 :: Nat -> c9:c10:c11
gen_c12:c1318_19 :: Nat -> c12:c13


Lemmas:
le(gen_0':s14_19(+(1, n20_19)), gen_0':s14_19(n20_19)) -> false, rt in Omega(0)
length(gen_nil:cons:leaf:node13_19(n435_19)) -> gen_0':s14_19(n435_19), rt in Omega(0)


Generator Equations:
gen_nil:cons:leaf:node13_19(0) <=> nil
gen_nil:cons:leaf:node13_19(+(x, 1)) <=> cons(gen_nil:cons:leaf:node13_19(x))
gen_0':s14_19(0) <=> 0'
gen_0':s14_19(+(x, 1)) <=> s(gen_0':s14_19(x))
gen_c14:c15:c1615_19(0) <=> c14
gen_c14:c15:c1615_19(+(x, 1)) <=> c16(gen_c14:c15:c1615_19(x))
gen_c7:c816_19(0) <=> c7
gen_c7:c816_19(+(x, 1)) <=> c8(gen_c7:c816_19(x))
gen_c9:c10:c1117_19(0) <=> c9
gen_c9:c10:c1117_19(+(x, 1)) <=> c10(c12, gen_c9:c10:c1117_19(x))
gen_c12:c1318_19(0) <=> c12
gen_c12:c1318_19(+(x, 1)) <=> c13(gen_c12:c1318_19(x))


The following defined symbols remain to be analysed:
LE, LESSE, toList, LENGTH, TOLIST, APPEND, lessE, append

They will be analysed ascendingly in the following order:
toList < LESSE
LE < LESSE
LENGTH < LESSE
TOLIST < LESSE
toList < TOLIST
toList < lessE
append < toList
APPEND < TOLIST

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

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Innermost TRS:
Rules:
LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
IF(true, z0, z1, z2, z3) -> c4
IF(false, true, z0, z1, z2) -> c5
IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
LENGTH(nil) -> c7
LENGTH(cons(z1)) -> c8(LENGTH(z1))
TOLIST(leaf) -> c9
TOLIST(node(z0, z2)) -> c10(APPEND(toList(z0), cons(toList(z2))), TOLIST(z0))
TOLIST(node(z0, z2)) -> c11(APPEND(toList(z0), cons(toList(z2))), TOLIST(z2))
APPEND(nil, z0) -> c12
APPEND(cons(z1), z2) -> c13(APPEND(z1, z2))
LE(s(z0), 0') -> c14
LE(0', z0) -> c15
LE(s(z0), s(z1)) -> c16(LE(z0, z1))
A -> c17
A -> c18
lessElements(z0, z1) -> lessE(z0, z1, 0')
lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
if(true, z0, z1, z2, z3) -> z1
if(false, true, z0, z1, z2) -> z1
if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))
toList(leaf) -> nil
toList(node(z0, z2)) -> append(toList(z0), cons(toList(z2)))
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
a -> c
a -> d

Types:
LESSELEMENTS :: nil:cons:leaf:node -> nil:cons:leaf:node -> c1
c1 :: c2:c3 -> c1
LESSE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c2:c3
0' :: 0':s
c2 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c2:c3
IF :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c4:c5:c6
le :: 0':s -> 0':s -> true:false
length :: nil:cons:leaf:node -> 0':s
toList :: nil:cons:leaf:node -> nil:cons:leaf:node
LE :: 0':s -> 0':s -> c14:c15:c16
LENGTH :: nil:cons:leaf:node -> c7:c8
c3 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c9:c10:c11 -> c2:c3
TOLIST :: nil:cons:leaf:node -> c9:c10:c11
true :: true:false
c4 :: c4:c5:c6
false :: true:false
c5 :: c4:c5:c6
c6 :: c2:c3 -> c4:c5:c6
s :: 0':s -> 0':s
nil :: nil:cons:leaf:node
c7 :: c7:c8
cons :: nil:cons:leaf:node -> nil:cons:leaf:node
c8 :: c7:c8 -> c7:c8
leaf :: nil:cons:leaf:node
c9 :: c9:c10:c11
node :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
c10 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
APPEND :: nil:cons:leaf:node -> nil:cons:leaf:node -> c12:c13
c11 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
c14 :: c14:c15:c16
c15 :: c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
A :: c17:c18
c17 :: c17:c18
c18 :: c17:c18
lessElements :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
lessE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
if :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
append :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
a :: c:d
c :: c:d
d :: c:d
hole_c11_19 :: c1
hole_nil:cons:leaf:node2_19 :: nil:cons:leaf:node
hole_c2:c33_19 :: c2:c3
hole_0':s4_19 :: 0':s
hole_c4:c5:c65_19 :: c4:c5:c6
hole_c14:c15:c166_19 :: c14:c15:c16
hole_c7:c87_19 :: c7:c8
hole_true:false8_19 :: true:false
hole_c9:c10:c119_19 :: c9:c10:c11
hole_c12:c1310_19 :: c12:c13
hole_c17:c1811_19 :: c17:c18
hole_c:d12_19 :: c:d
gen_nil:cons:leaf:node13_19 :: Nat -> nil:cons:leaf:node
gen_0':s14_19 :: Nat -> 0':s
gen_c14:c15:c1615_19 :: Nat -> c14:c15:c16
gen_c7:c816_19 :: Nat -> c7:c8
gen_c9:c10:c1117_19 :: Nat -> c9:c10:c11
gen_c12:c1318_19 :: Nat -> c12:c13


Lemmas:
le(gen_0':s14_19(+(1, n20_19)), gen_0':s14_19(n20_19)) -> false, rt in Omega(0)
length(gen_nil:cons:leaf:node13_19(n435_19)) -> gen_0':s14_19(n435_19), rt in Omega(0)
LE(gen_0':s14_19(+(1, n824_19)), gen_0':s14_19(n824_19)) -> gen_c14:c15:c1615_19(n824_19), rt in Omega(1 + n824_19)


Generator Equations:
gen_nil:cons:leaf:node13_19(0) <=> nil
gen_nil:cons:leaf:node13_19(+(x, 1)) <=> cons(gen_nil:cons:leaf:node13_19(x))
gen_0':s14_19(0) <=> 0'
gen_0':s14_19(+(x, 1)) <=> s(gen_0':s14_19(x))
gen_c14:c15:c1615_19(0) <=> c14
gen_c14:c15:c1615_19(+(x, 1)) <=> c16(gen_c14:c15:c1615_19(x))
gen_c7:c816_19(0) <=> c7
gen_c7:c816_19(+(x, 1)) <=> c8(gen_c7:c816_19(x))
gen_c9:c10:c1117_19(0) <=> c9
gen_c9:c10:c1117_19(+(x, 1)) <=> c10(c12, gen_c9:c10:c1117_19(x))
gen_c12:c1318_19(0) <=> c12
gen_c12:c1318_19(+(x, 1)) <=> c13(gen_c12:c1318_19(x))


The following defined symbols remain to be analysed:
LENGTH, LESSE, toList, TOLIST, APPEND, lessE, append

They will be analysed ascendingly in the following order:
toList < LESSE
LENGTH < LESSE
TOLIST < LESSE
toList < TOLIST
toList < lessE
append < toList
APPEND < TOLIST

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LENGTH(gen_nil:cons:leaf:node13_19(n1574_19)) -> gen_c7:c816_19(n1574_19), rt in Omega(1 + n1574_19)

Induction Base:
LENGTH(gen_nil:cons:leaf:node13_19(0)) ->_R^Omega(1)
c7

Induction Step:
LENGTH(gen_nil:cons:leaf:node13_19(+(n1574_19, 1))) ->_R^Omega(1)
c8(LENGTH(gen_nil:cons:leaf:node13_19(n1574_19))) ->_IH
c8(gen_c7:c816_19(c1575_19))

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

(22)
Obligation:
Innermost TRS:
Rules:
LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
IF(true, z0, z1, z2, z3) -> c4
IF(false, true, z0, z1, z2) -> c5
IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
LENGTH(nil) -> c7
LENGTH(cons(z1)) -> c8(LENGTH(z1))
TOLIST(leaf) -> c9
TOLIST(node(z0, z2)) -> c10(APPEND(toList(z0), cons(toList(z2))), TOLIST(z0))
TOLIST(node(z0, z2)) -> c11(APPEND(toList(z0), cons(toList(z2))), TOLIST(z2))
APPEND(nil, z0) -> c12
APPEND(cons(z1), z2) -> c13(APPEND(z1, z2))
LE(s(z0), 0') -> c14
LE(0', z0) -> c15
LE(s(z0), s(z1)) -> c16(LE(z0, z1))
A -> c17
A -> c18
lessElements(z0, z1) -> lessE(z0, z1, 0')
lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
if(true, z0, z1, z2, z3) -> z1
if(false, true, z0, z1, z2) -> z1
if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))
toList(leaf) -> nil
toList(node(z0, z2)) -> append(toList(z0), cons(toList(z2)))
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
a -> c
a -> d

Types:
LESSELEMENTS :: nil:cons:leaf:node -> nil:cons:leaf:node -> c1
c1 :: c2:c3 -> c1
LESSE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c2:c3
0' :: 0':s
c2 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c2:c3
IF :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c4:c5:c6
le :: 0':s -> 0':s -> true:false
length :: nil:cons:leaf:node -> 0':s
toList :: nil:cons:leaf:node -> nil:cons:leaf:node
LE :: 0':s -> 0':s -> c14:c15:c16
LENGTH :: nil:cons:leaf:node -> c7:c8
c3 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c9:c10:c11 -> c2:c3
TOLIST :: nil:cons:leaf:node -> c9:c10:c11
true :: true:false
c4 :: c4:c5:c6
false :: true:false
c5 :: c4:c5:c6
c6 :: c2:c3 -> c4:c5:c6
s :: 0':s -> 0':s
nil :: nil:cons:leaf:node
c7 :: c7:c8
cons :: nil:cons:leaf:node -> nil:cons:leaf:node
c8 :: c7:c8 -> c7:c8
leaf :: nil:cons:leaf:node
c9 :: c9:c10:c11
node :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
c10 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
APPEND :: nil:cons:leaf:node -> nil:cons:leaf:node -> c12:c13
c11 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
c14 :: c14:c15:c16
c15 :: c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
A :: c17:c18
c17 :: c17:c18
c18 :: c17:c18
lessElements :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
lessE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
if :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
append :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
a :: c:d
c :: c:d
d :: c:d
hole_c11_19 :: c1
hole_nil:cons:leaf:node2_19 :: nil:cons:leaf:node
hole_c2:c33_19 :: c2:c3
hole_0':s4_19 :: 0':s
hole_c4:c5:c65_19 :: c4:c5:c6
hole_c14:c15:c166_19 :: c14:c15:c16
hole_c7:c87_19 :: c7:c8
hole_true:false8_19 :: true:false
hole_c9:c10:c119_19 :: c9:c10:c11
hole_c12:c1310_19 :: c12:c13
hole_c17:c1811_19 :: c17:c18
hole_c:d12_19 :: c:d
gen_nil:cons:leaf:node13_19 :: Nat -> nil:cons:leaf:node
gen_0':s14_19 :: Nat -> 0':s
gen_c14:c15:c1615_19 :: Nat -> c14:c15:c16
gen_c7:c816_19 :: Nat -> c7:c8
gen_c9:c10:c1117_19 :: Nat -> c9:c10:c11
gen_c12:c1318_19 :: Nat -> c12:c13


Lemmas:
le(gen_0':s14_19(+(1, n20_19)), gen_0':s14_19(n20_19)) -> false, rt in Omega(0)
length(gen_nil:cons:leaf:node13_19(n435_19)) -> gen_0':s14_19(n435_19), rt in Omega(0)
LE(gen_0':s14_19(+(1, n824_19)), gen_0':s14_19(n824_19)) -> gen_c14:c15:c1615_19(n824_19), rt in Omega(1 + n824_19)
LENGTH(gen_nil:cons:leaf:node13_19(n1574_19)) -> gen_c7:c816_19(n1574_19), rt in Omega(1 + n1574_19)


Generator Equations:
gen_nil:cons:leaf:node13_19(0) <=> nil
gen_nil:cons:leaf:node13_19(+(x, 1)) <=> cons(gen_nil:cons:leaf:node13_19(x))
gen_0':s14_19(0) <=> 0'
gen_0':s14_19(+(x, 1)) <=> s(gen_0':s14_19(x))
gen_c14:c15:c1615_19(0) <=> c14
gen_c14:c15:c1615_19(+(x, 1)) <=> c16(gen_c14:c15:c1615_19(x))
gen_c7:c816_19(0) <=> c7
gen_c7:c816_19(+(x, 1)) <=> c8(gen_c7:c816_19(x))
gen_c9:c10:c1117_19(0) <=> c9
gen_c9:c10:c1117_19(+(x, 1)) <=> c10(c12, gen_c9:c10:c1117_19(x))
gen_c12:c1318_19(0) <=> c12
gen_c12:c1318_19(+(x, 1)) <=> c13(gen_c12:c1318_19(x))


The following defined symbols remain to be analysed:
APPEND, LESSE, toList, TOLIST, lessE, append

They will be analysed ascendingly in the following order:
toList < LESSE
TOLIST < LESSE
toList < TOLIST
toList < lessE
append < toList
APPEND < TOLIST

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND(gen_nil:cons:leaf:node13_19(n2039_19), gen_nil:cons:leaf:node13_19(b)) -> gen_c12:c1318_19(n2039_19), rt in Omega(1 + n2039_19)

Induction Base:
APPEND(gen_nil:cons:leaf:node13_19(0), gen_nil:cons:leaf:node13_19(b)) ->_R^Omega(1)
c12

Induction Step:
APPEND(gen_nil:cons:leaf:node13_19(+(n2039_19, 1)), gen_nil:cons:leaf:node13_19(b)) ->_R^Omega(1)
c13(APPEND(gen_nil:cons:leaf:node13_19(n2039_19), gen_nil:cons:leaf:node13_19(b))) ->_IH
c13(gen_c12:c1318_19(c2040_19))

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

(24)
Obligation:
Innermost TRS:
Rules:
LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
IF(true, z0, z1, z2, z3) -> c4
IF(false, true, z0, z1, z2) -> c5
IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
LENGTH(nil) -> c7
LENGTH(cons(z1)) -> c8(LENGTH(z1))
TOLIST(leaf) -> c9
TOLIST(node(z0, z2)) -> c10(APPEND(toList(z0), cons(toList(z2))), TOLIST(z0))
TOLIST(node(z0, z2)) -> c11(APPEND(toList(z0), cons(toList(z2))), TOLIST(z2))
APPEND(nil, z0) -> c12
APPEND(cons(z1), z2) -> c13(APPEND(z1, z2))
LE(s(z0), 0') -> c14
LE(0', z0) -> c15
LE(s(z0), s(z1)) -> c16(LE(z0, z1))
A -> c17
A -> c18
lessElements(z0, z1) -> lessE(z0, z1, 0')
lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
if(true, z0, z1, z2, z3) -> z1
if(false, true, z0, z1, z2) -> z1
if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))
toList(leaf) -> nil
toList(node(z0, z2)) -> append(toList(z0), cons(toList(z2)))
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
a -> c
a -> d

Types:
LESSELEMENTS :: nil:cons:leaf:node -> nil:cons:leaf:node -> c1
c1 :: c2:c3 -> c1
LESSE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c2:c3
0' :: 0':s
c2 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c2:c3
IF :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c4:c5:c6
le :: 0':s -> 0':s -> true:false
length :: nil:cons:leaf:node -> 0':s
toList :: nil:cons:leaf:node -> nil:cons:leaf:node
LE :: 0':s -> 0':s -> c14:c15:c16
LENGTH :: nil:cons:leaf:node -> c7:c8
c3 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c9:c10:c11 -> c2:c3
TOLIST :: nil:cons:leaf:node -> c9:c10:c11
true :: true:false
c4 :: c4:c5:c6
false :: true:false
c5 :: c4:c5:c6
c6 :: c2:c3 -> c4:c5:c6
s :: 0':s -> 0':s
nil :: nil:cons:leaf:node
c7 :: c7:c8
cons :: nil:cons:leaf:node -> nil:cons:leaf:node
c8 :: c7:c8 -> c7:c8
leaf :: nil:cons:leaf:node
c9 :: c9:c10:c11
node :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
c10 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
APPEND :: nil:cons:leaf:node -> nil:cons:leaf:node -> c12:c13
c11 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
c14 :: c14:c15:c16
c15 :: c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
A :: c17:c18
c17 :: c17:c18
c18 :: c17:c18
lessElements :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
lessE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
if :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
append :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
a :: c:d
c :: c:d
d :: c:d
hole_c11_19 :: c1
hole_nil:cons:leaf:node2_19 :: nil:cons:leaf:node
hole_c2:c33_19 :: c2:c3
hole_0':s4_19 :: 0':s
hole_c4:c5:c65_19 :: c4:c5:c6
hole_c14:c15:c166_19 :: c14:c15:c16
hole_c7:c87_19 :: c7:c8
hole_true:false8_19 :: true:false
hole_c9:c10:c119_19 :: c9:c10:c11
hole_c12:c1310_19 :: c12:c13
hole_c17:c1811_19 :: c17:c18
hole_c:d12_19 :: c:d
gen_nil:cons:leaf:node13_19 :: Nat -> nil:cons:leaf:node
gen_0':s14_19 :: Nat -> 0':s
gen_c14:c15:c1615_19 :: Nat -> c14:c15:c16
gen_c7:c816_19 :: Nat -> c7:c8
gen_c9:c10:c1117_19 :: Nat -> c9:c10:c11
gen_c12:c1318_19 :: Nat -> c12:c13


Lemmas:
le(gen_0':s14_19(+(1, n20_19)), gen_0':s14_19(n20_19)) -> false, rt in Omega(0)
length(gen_nil:cons:leaf:node13_19(n435_19)) -> gen_0':s14_19(n435_19), rt in Omega(0)
LE(gen_0':s14_19(+(1, n824_19)), gen_0':s14_19(n824_19)) -> gen_c14:c15:c1615_19(n824_19), rt in Omega(1 + n824_19)
LENGTH(gen_nil:cons:leaf:node13_19(n1574_19)) -> gen_c7:c816_19(n1574_19), rt in Omega(1 + n1574_19)
APPEND(gen_nil:cons:leaf:node13_19(n2039_19), gen_nil:cons:leaf:node13_19(b)) -> gen_c12:c1318_19(n2039_19), rt in Omega(1 + n2039_19)


Generator Equations:
gen_nil:cons:leaf:node13_19(0) <=> nil
gen_nil:cons:leaf:node13_19(+(x, 1)) <=> cons(gen_nil:cons:leaf:node13_19(x))
gen_0':s14_19(0) <=> 0'
gen_0':s14_19(+(x, 1)) <=> s(gen_0':s14_19(x))
gen_c14:c15:c1615_19(0) <=> c14
gen_c14:c15:c1615_19(+(x, 1)) <=> c16(gen_c14:c15:c1615_19(x))
gen_c7:c816_19(0) <=> c7
gen_c7:c816_19(+(x, 1)) <=> c8(gen_c7:c816_19(x))
gen_c9:c10:c1117_19(0) <=> c9
gen_c9:c10:c1117_19(+(x, 1)) <=> c10(c12, gen_c9:c10:c1117_19(x))
gen_c12:c1318_19(0) <=> c12
gen_c12:c1318_19(+(x, 1)) <=> c13(gen_c12:c1318_19(x))


The following defined symbols remain to be analysed:
append, LESSE, toList, TOLIST, lessE

They will be analysed ascendingly in the following order:
toList < LESSE
TOLIST < LESSE
toList < TOLIST
toList < lessE
append < toList

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
append(gen_nil:cons:leaf:node13_19(n3026_19), gen_nil:cons:leaf:node13_19(b)) -> gen_nil:cons:leaf:node13_19(+(n3026_19, b)), rt in Omega(0)

Induction Base:
append(gen_nil:cons:leaf:node13_19(0), gen_nil:cons:leaf:node13_19(b)) ->_R^Omega(0)
gen_nil:cons:leaf:node13_19(b)

Induction Step:
append(gen_nil:cons:leaf:node13_19(+(n3026_19, 1)), gen_nil:cons:leaf:node13_19(b)) ->_R^Omega(0)
cons(append(gen_nil:cons:leaf:node13_19(n3026_19), gen_nil:cons:leaf:node13_19(b))) ->_IH
cons(gen_nil:cons:leaf:node13_19(+(b, c3027_19)))

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

(26)
Obligation:
Innermost TRS:
Rules:
LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0'))
LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0))
LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1))
IF(true, z0, z1, z2, z3) -> c4
IF(false, true, z0, z1, z2) -> c5
IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2)))
LENGTH(nil) -> c7
LENGTH(cons(z1)) -> c8(LENGTH(z1))
TOLIST(leaf) -> c9
TOLIST(node(z0, z2)) -> c10(APPEND(toList(z0), cons(toList(z2))), TOLIST(z0))
TOLIST(node(z0, z2)) -> c11(APPEND(toList(z0), cons(toList(z2))), TOLIST(z2))
APPEND(nil, z0) -> c12
APPEND(cons(z1), z2) -> c13(APPEND(z1, z2))
LE(s(z0), 0') -> c14
LE(0', z0) -> c15
LE(s(z0), s(z1)) -> c16(LE(z0, z1))
A -> c17
A -> c18
lessElements(z0, z1) -> lessE(z0, z1, 0')
lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2)
if(true, z0, z1, z2, z3) -> z1
if(false, true, z0, z1, z2) -> z1
if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))
toList(leaf) -> nil
toList(node(z0, z2)) -> append(toList(z0), cons(toList(z2)))
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
a -> c
a -> d

Types:
LESSELEMENTS :: nil:cons:leaf:node -> nil:cons:leaf:node -> c1
c1 :: c2:c3 -> c1
LESSE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c2:c3
0' :: 0':s
c2 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c2:c3
IF :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> c4:c5:c6
le :: 0':s -> 0':s -> true:false
length :: nil:cons:leaf:node -> 0':s
toList :: nil:cons:leaf:node -> nil:cons:leaf:node
LE :: 0':s -> 0':s -> c14:c15:c16
LENGTH :: nil:cons:leaf:node -> c7:c8
c3 :: c4:c5:c6 -> c14:c15:c16 -> c7:c8 -> c9:c10:c11 -> c2:c3
TOLIST :: nil:cons:leaf:node -> c9:c10:c11
true :: true:false
c4 :: c4:c5:c6
false :: true:false
c5 :: c4:c5:c6
c6 :: c2:c3 -> c4:c5:c6
s :: 0':s -> 0':s
nil :: nil:cons:leaf:node
c7 :: c7:c8
cons :: nil:cons:leaf:node -> nil:cons:leaf:node
c8 :: c7:c8 -> c7:c8
leaf :: nil:cons:leaf:node
c9 :: c9:c10:c11
node :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
c10 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
APPEND :: nil:cons:leaf:node -> nil:cons:leaf:node -> c12:c13
c11 :: c12:c13 -> c9:c10:c11 -> c9:c10:c11
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
c14 :: c14:c15:c16
c15 :: c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
A :: c17:c18
c17 :: c17:c18
c18 :: c17:c18
lessElements :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
lessE :: nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
if :: true:false -> true:false -> nil:cons:leaf:node -> nil:cons:leaf:node -> 0':s -> nil:cons:leaf:node
append :: nil:cons:leaf:node -> nil:cons:leaf:node -> nil:cons:leaf:node
a :: c:d
c :: c:d
d :: c:d
hole_c11_19 :: c1
hole_nil:cons:leaf:node2_19 :: nil:cons:leaf:node
hole_c2:c33_19 :: c2:c3
hole_0':s4_19 :: 0':s
hole_c4:c5:c65_19 :: c4:c5:c6
hole_c14:c15:c166_19 :: c14:c15:c16
hole_c7:c87_19 :: c7:c8
hole_true:false8_19 :: true:false
hole_c9:c10:c119_19 :: c9:c10:c11
hole_c12:c1310_19 :: c12:c13
hole_c17:c1811_19 :: c17:c18
hole_c:d12_19 :: c:d
gen_nil:cons:leaf:node13_19 :: Nat -> nil:cons:leaf:node
gen_0':s14_19 :: Nat -> 0':s
gen_c14:c15:c1615_19 :: Nat -> c14:c15:c16
gen_c7:c816_19 :: Nat -> c7:c8
gen_c9:c10:c1117_19 :: Nat -> c9:c10:c11
gen_c12:c1318_19 :: Nat -> c12:c13


Lemmas:
le(gen_0':s14_19(+(1, n20_19)), gen_0':s14_19(n20_19)) -> false, rt in Omega(0)
length(gen_nil:cons:leaf:node13_19(n435_19)) -> gen_0':s14_19(n435_19), rt in Omega(0)
LE(gen_0':s14_19(+(1, n824_19)), gen_0':s14_19(n824_19)) -> gen_c14:c15:c1615_19(n824_19), rt in Omega(1 + n824_19)
LENGTH(gen_nil:cons:leaf:node13_19(n1574_19)) -> gen_c7:c816_19(n1574_19), rt in Omega(1 + n1574_19)
APPEND(gen_nil:cons:leaf:node13_19(n2039_19), gen_nil:cons:leaf:node13_19(b)) -> gen_c12:c1318_19(n2039_19), rt in Omega(1 + n2039_19)
append(gen_nil:cons:leaf:node13_19(n3026_19), gen_nil:cons:leaf:node13_19(b)) -> gen_nil:cons:leaf:node13_19(+(n3026_19, b)), rt in Omega(0)


Generator Equations:
gen_nil:cons:leaf:node13_19(0) <=> nil
gen_nil:cons:leaf:node13_19(+(x, 1)) <=> cons(gen_nil:cons:leaf:node13_19(x))
gen_0':s14_19(0) <=> 0'
gen_0':s14_19(+(x, 1)) <=> s(gen_0':s14_19(x))
gen_c14:c15:c1615_19(0) <=> c14
gen_c14:c15:c1615_19(+(x, 1)) <=> c16(gen_c14:c15:c1615_19(x))
gen_c7:c816_19(0) <=> c7
gen_c7:c816_19(+(x, 1)) <=> c8(gen_c7:c816_19(x))
gen_c9:c10:c1117_19(0) <=> c9
gen_c9:c10:c1117_19(+(x, 1)) <=> c10(c12, gen_c9:c10:c1117_19(x))
gen_c12:c1318_19(0) <=> c12
gen_c12:c1318_19(+(x, 1)) <=> c13(gen_c12:c1318_19(x))


The following defined symbols remain to be analysed:
toList, LESSE, TOLIST, lessE

They will be analysed ascendingly in the following order:
toList < LESSE
TOLIST < LESSE
toList < TOLIST
toList < lessE