WORST_CASE(Omega(n^2),?)
proof of input_fcK5LkWn84.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 5 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 293 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 93.9 s]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 56 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 19 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 1 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 9 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 445 ms]
        (28) BEST
            (29) proven lower bound
                (30) LowerBoundPropagationProof [FINISHED, 0 ms]
                (31) BOUNDS(n^2, INF)
            (32) typed CpxTrs
                (33) RewriteLemmaProof [LOWER BOUND(ID), 379 ms]
                (34) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   isEmpty(nil) -> true
   isEmpty(cons(x, xs)) -> false
   last(cons(x, nil)) -> x
   last(cons(x, cons(y, ys))) -> last(cons(y, ys))
   dropLast(nil) -> nil
   dropLast(cons(x, nil)) -> nil
   dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   reverse(xs) -> rev(xs, nil)
   rev(xs, ys) -> if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
   if(true, xs, ys, zs) -> zs
   if(false, xs, ys, zs) -> rev(xs, ys)

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

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   isEmpty(nil) -> true
   isEmpty(cons(z0, z1)) -> false
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
   dropLast(nil) -> nil
   dropLast(cons(z0, nil)) -> nil
   dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
   append(nil, z0) -> z0
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   reverse(z0) -> rev(z0, nil)
   rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> rev(z0, z1)
Tuples:
   ISEMPTY(nil) -> c
   ISEMPTY(cons(z0, z1)) -> c1
   LAST(cons(z0, nil)) -> c2
   LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
   DROPLAST(nil) -> c4
   DROPLAST(cons(z0, nil)) -> c5
   DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
   APPEND(nil, z0) -> c7
   APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
   REVERSE(z0) -> c9(REV(z0, nil))
   REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
   REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
   REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
   IF(true, z0, z1, z2) -> c13
   IF(false, z0, z1, z2) -> c14(REV(z0, z1))
S tuples:
   ISEMPTY(nil) -> c
   ISEMPTY(cons(z0, z1)) -> c1
   LAST(cons(z0, nil)) -> c2
   LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
   DROPLAST(nil) -> c4
   DROPLAST(cons(z0, nil)) -> c5
   DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
   APPEND(nil, z0) -> c7
   APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
   REVERSE(z0) -> c9(REV(z0, nil))
   REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
   REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
   REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
   IF(true, z0, z1, z2) -> c13
   IF(false, z0, z1, z2) -> c14(REV(z0, z1))
K tuples:none
Defined Rule Symbols:   isEmpty_1, last_1, dropLast_1, append_2, reverse_1, rev_2, if_4

Defined Pair Symbols:   ISEMPTY_1, LAST_1, DROPLAST_1, APPEND_2, REVERSE_1, REV_2, IF_4

Compound Symbols:   c, c1, c2, c3_1, c4, c5, c6_1, c7, c8_1, c9_1, c10_2, c11_2, c12_3, c13, c14_1


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

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

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


The TRS R consists of the following rules:

   ISEMPTY(nil) -> c
   ISEMPTY(cons(z0, z1)) -> c1
   LAST(cons(z0, nil)) -> c2
   LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
   DROPLAST(nil) -> c4
   DROPLAST(cons(z0, nil)) -> c5
   DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
   APPEND(nil, z0) -> c7
   APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
   REVERSE(z0) -> c9(REV(z0, nil))
   REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
   REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
   REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
   IF(true, z0, z1, z2) -> c13
   IF(false, z0, z1, z2) -> c14(REV(z0, z1))

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

   isEmpty(nil) -> true
   isEmpty(cons(z0, z1)) -> false
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
   dropLast(nil) -> nil
   dropLast(cons(z0, nil)) -> nil
   dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
   append(nil, z0) -> z0
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   reverse(z0) -> rev(z0, nil)
   rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> rev(z0, z1)

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

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

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


The TRS R consists of the following rules:

   ISEMPTY(nil) -> c
   ISEMPTY(cons(z0, z1)) -> c1
   LAST(cons(z0, nil)) -> c2
   LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
   DROPLAST(nil) -> c4
   DROPLAST(cons(z0, nil)) -> c5
   DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
   APPEND(nil, z0) -> c7
   APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
   REVERSE(z0) -> c9(REV(z0, nil))
   REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
   REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
   REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
   IF(true, z0, z1, z2) -> c13
   IF(false, z0, z1, z2) -> c14(REV(z0, z1))

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

   isEmpty(nil) -> true
   isEmpty(cons(z0, z1)) -> false
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
   dropLast(nil) -> nil
   dropLast(cons(z0, nil)) -> nil
   dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
   append(nil, z0) -> z0
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   reverse(z0) -> rev(z0, nil)
   rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> rev(z0, z1)

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

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

(8)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LAST, DROPLAST, APPEND, REV, dropLast, append, last, rev

They will be analysed ascendingly in the following order:
LAST < REV
DROPLAST < REV
APPEND < REV
dropLast < REV
append < REV
last < REV
dropLast < rev
append < rev
last < rev

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

(10)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8


Generator Equations:
gen_nil:cons10_15(0) <=> nil
gen_nil:cons10_15(+(x, 1)) <=> cons(nil, gen_nil:cons10_15(x))
gen_c2:c311_15(0) <=> c2
gen_c2:c311_15(+(x, 1)) <=> c3(gen_c2:c311_15(x))
gen_c4:c5:c612_15(0) <=> c4
gen_c4:c5:c612_15(+(x, 1)) <=> c6(gen_c4:c5:c612_15(x))
gen_c7:c813_15(0) <=> c7
gen_c7:c813_15(+(x, 1)) <=> c8(gen_c7:c813_15(x))


The following defined symbols remain to be analysed:
LAST, DROPLAST, APPEND, REV, dropLast, append, last, rev

They will be analysed ascendingly in the following order:
LAST < REV
DROPLAST < REV
APPEND < REV
dropLast < REV
append < REV
last < REV
dropLast < rev
append < rev
last < rev

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LAST(gen_nil:cons10_15(+(1, n15_15))) -> gen_c2:c311_15(n15_15), rt in Omega(1 + n15_15)

Induction Base:
LAST(gen_nil:cons10_15(+(1, 0))) ->_R^Omega(1)
c2

Induction Step:
LAST(gen_nil:cons10_15(+(1, +(n15_15, 1)))) ->_R^Omega(1)
c3(LAST(cons(nil, gen_nil:cons10_15(n15_15)))) ->_IH
c3(gen_c2:c311_15(c16_15))

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

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8


Generator Equations:
gen_nil:cons10_15(0) <=> nil
gen_nil:cons10_15(+(x, 1)) <=> cons(nil, gen_nil:cons10_15(x))
gen_c2:c311_15(0) <=> c2
gen_c2:c311_15(+(x, 1)) <=> c3(gen_c2:c311_15(x))
gen_c4:c5:c612_15(0) <=> c4
gen_c4:c5:c612_15(+(x, 1)) <=> c6(gen_c4:c5:c612_15(x))
gen_c7:c813_15(0) <=> c7
gen_c7:c813_15(+(x, 1)) <=> c8(gen_c7:c813_15(x))


The following defined symbols remain to be analysed:
LAST, DROPLAST, APPEND, REV, dropLast, append, last, rev

They will be analysed ascendingly in the following order:
LAST < REV
DROPLAST < REV
APPEND < REV
dropLast < REV
append < REV
last < REV
dropLast < rev
append < rev
last < rev

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8


Lemmas:
LAST(gen_nil:cons10_15(+(1, n15_15))) -> gen_c2:c311_15(n15_15), rt in Omega(1 + n15_15)


Generator Equations:
gen_nil:cons10_15(0) <=> nil
gen_nil:cons10_15(+(x, 1)) <=> cons(nil, gen_nil:cons10_15(x))
gen_c2:c311_15(0) <=> c2
gen_c2:c311_15(+(x, 1)) <=> c3(gen_c2:c311_15(x))
gen_c4:c5:c612_15(0) <=> c4
gen_c4:c5:c612_15(+(x, 1)) <=> c6(gen_c4:c5:c612_15(x))
gen_c7:c813_15(0) <=> c7
gen_c7:c813_15(+(x, 1)) <=> c8(gen_c7:c813_15(x))


The following defined symbols remain to be analysed:
DROPLAST, APPEND, REV, dropLast, append, last, rev

They will be analysed ascendingly in the following order:
DROPLAST < REV
APPEND < REV
dropLast < REV
append < REV
last < REV
dropLast < rev
append < rev
last < rev

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DROPLAST(gen_nil:cons10_15(+(2, n412_15))) -> *14_15, rt in Omega(n412_15)

Induction Base:
DROPLAST(gen_nil:cons10_15(+(2, 0)))

Induction Step:
DROPLAST(gen_nil:cons10_15(+(2, +(n412_15, 1)))) ->_R^Omega(1)
c6(DROPLAST(cons(nil, gen_nil:cons10_15(+(1, n412_15))))) ->_IH
c6(*14_15)

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

(18)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8


Lemmas:
LAST(gen_nil:cons10_15(+(1, n15_15))) -> gen_c2:c311_15(n15_15), rt in Omega(1 + n15_15)
DROPLAST(gen_nil:cons10_15(+(2, n412_15))) -> *14_15, rt in Omega(n412_15)


Generator Equations:
gen_nil:cons10_15(0) <=> nil
gen_nil:cons10_15(+(x, 1)) <=> cons(nil, gen_nil:cons10_15(x))
gen_c2:c311_15(0) <=> c2
gen_c2:c311_15(+(x, 1)) <=> c3(gen_c2:c311_15(x))
gen_c4:c5:c612_15(0) <=> c4
gen_c4:c5:c612_15(+(x, 1)) <=> c6(gen_c4:c5:c612_15(x))
gen_c7:c813_15(0) <=> c7
gen_c7:c813_15(+(x, 1)) <=> c8(gen_c7:c813_15(x))


The following defined symbols remain to be analysed:
APPEND, REV, dropLast, append, last, rev

They will be analysed ascendingly in the following order:
APPEND < REV
dropLast < REV
append < REV
last < REV
dropLast < rev
append < rev
last < rev

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND(gen_nil:cons10_15(n73855_15), gen_nil:cons10_15(b)) -> gen_c7:c813_15(n73855_15), rt in Omega(1 + n73855_15)

Induction Base:
APPEND(gen_nil:cons10_15(0), gen_nil:cons10_15(b)) ->_R^Omega(1)
c7

Induction Step:
APPEND(gen_nil:cons10_15(+(n73855_15, 1)), gen_nil:cons10_15(b)) ->_R^Omega(1)
c8(APPEND(gen_nil:cons10_15(n73855_15), gen_nil:cons10_15(b))) ->_IH
c8(gen_c7:c813_15(c73856_15))

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

(20)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8


Lemmas:
LAST(gen_nil:cons10_15(+(1, n15_15))) -> gen_c2:c311_15(n15_15), rt in Omega(1 + n15_15)
DROPLAST(gen_nil:cons10_15(+(2, n412_15))) -> *14_15, rt in Omega(n412_15)
APPEND(gen_nil:cons10_15(n73855_15), gen_nil:cons10_15(b)) -> gen_c7:c813_15(n73855_15), rt in Omega(1 + n73855_15)


Generator Equations:
gen_nil:cons10_15(0) <=> nil
gen_nil:cons10_15(+(x, 1)) <=> cons(nil, gen_nil:cons10_15(x))
gen_c2:c311_15(0) <=> c2
gen_c2:c311_15(+(x, 1)) <=> c3(gen_c2:c311_15(x))
gen_c4:c5:c612_15(0) <=> c4
gen_c4:c5:c612_15(+(x, 1)) <=> c6(gen_c4:c5:c612_15(x))
gen_c7:c813_15(0) <=> c7
gen_c7:c813_15(+(x, 1)) <=> c8(gen_c7:c813_15(x))


The following defined symbols remain to be analysed:
dropLast, REV, append, last, rev

They will be analysed ascendingly in the following order:
dropLast < REV
append < REV
last < REV
dropLast < rev
append < rev
last < rev

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
dropLast(gen_nil:cons10_15(+(1, n74737_15))) -> gen_nil:cons10_15(n74737_15), rt in Omega(0)

Induction Base:
dropLast(gen_nil:cons10_15(+(1, 0))) ->_R^Omega(0)
nil

Induction Step:
dropLast(gen_nil:cons10_15(+(1, +(n74737_15, 1)))) ->_R^Omega(0)
cons(nil, dropLast(cons(nil, gen_nil:cons10_15(n74737_15)))) ->_IH
cons(nil, gen_nil:cons10_15(c74738_15))

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

(22)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8


Lemmas:
LAST(gen_nil:cons10_15(+(1, n15_15))) -> gen_c2:c311_15(n15_15), rt in Omega(1 + n15_15)
DROPLAST(gen_nil:cons10_15(+(2, n412_15))) -> *14_15, rt in Omega(n412_15)
APPEND(gen_nil:cons10_15(n73855_15), gen_nil:cons10_15(b)) -> gen_c7:c813_15(n73855_15), rt in Omega(1 + n73855_15)
dropLast(gen_nil:cons10_15(+(1, n74737_15))) -> gen_nil:cons10_15(n74737_15), rt in Omega(0)


Generator Equations:
gen_nil:cons10_15(0) <=> nil
gen_nil:cons10_15(+(x, 1)) <=> cons(nil, gen_nil:cons10_15(x))
gen_c2:c311_15(0) <=> c2
gen_c2:c311_15(+(x, 1)) <=> c3(gen_c2:c311_15(x))
gen_c4:c5:c612_15(0) <=> c4
gen_c4:c5:c612_15(+(x, 1)) <=> c6(gen_c4:c5:c612_15(x))
gen_c7:c813_15(0) <=> c7
gen_c7:c813_15(+(x, 1)) <=> c8(gen_c7:c813_15(x))


The following defined symbols remain to be analysed:
append, REV, last, rev

They will be analysed ascendingly in the following order:
append < REV
last < REV
append < rev
last < rev

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
append(gen_nil:cons10_15(n75349_15), gen_nil:cons10_15(b)) -> gen_nil:cons10_15(+(n75349_15, b)), rt in Omega(0)

Induction Base:
append(gen_nil:cons10_15(0), gen_nil:cons10_15(b)) ->_R^Omega(0)
gen_nil:cons10_15(b)

Induction Step:
append(gen_nil:cons10_15(+(n75349_15, 1)), gen_nil:cons10_15(b)) ->_R^Omega(0)
cons(nil, append(gen_nil:cons10_15(n75349_15), gen_nil:cons10_15(b))) ->_IH
cons(nil, gen_nil:cons10_15(+(b, c75350_15)))

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

(24)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8


Lemmas:
LAST(gen_nil:cons10_15(+(1, n15_15))) -> gen_c2:c311_15(n15_15), rt in Omega(1 + n15_15)
DROPLAST(gen_nil:cons10_15(+(2, n412_15))) -> *14_15, rt in Omega(n412_15)
APPEND(gen_nil:cons10_15(n73855_15), gen_nil:cons10_15(b)) -> gen_c7:c813_15(n73855_15), rt in Omega(1 + n73855_15)
dropLast(gen_nil:cons10_15(+(1, n74737_15))) -> gen_nil:cons10_15(n74737_15), rt in Omega(0)
append(gen_nil:cons10_15(n75349_15), gen_nil:cons10_15(b)) -> gen_nil:cons10_15(+(n75349_15, b)), rt in Omega(0)


Generator Equations:
gen_nil:cons10_15(0) <=> nil
gen_nil:cons10_15(+(x, 1)) <=> cons(nil, gen_nil:cons10_15(x))
gen_c2:c311_15(0) <=> c2
gen_c2:c311_15(+(x, 1)) <=> c3(gen_c2:c311_15(x))
gen_c4:c5:c612_15(0) <=> c4
gen_c4:c5:c612_15(+(x, 1)) <=> c6(gen_c4:c5:c612_15(x))
gen_c7:c813_15(0) <=> c7
gen_c7:c813_15(+(x, 1)) <=> c8(gen_c7:c813_15(x))


The following defined symbols remain to be analysed:
last, REV, rev

They will be analysed ascendingly in the following order:
last < REV
last < rev

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
last(gen_nil:cons10_15(+(1, n76805_15))) -> gen_nil:cons10_15(0), rt in Omega(0)

Induction Base:
last(gen_nil:cons10_15(+(1, 0))) ->_R^Omega(0)
nil

Induction Step:
last(gen_nil:cons10_15(+(1, +(n76805_15, 1)))) ->_R^Omega(0)
last(cons(nil, gen_nil:cons10_15(n76805_15))) ->_IH
gen_nil:cons10_15(0)

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:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8


Lemmas:
LAST(gen_nil:cons10_15(+(1, n15_15))) -> gen_c2:c311_15(n15_15), rt in Omega(1 + n15_15)
DROPLAST(gen_nil:cons10_15(+(2, n412_15))) -> *14_15, rt in Omega(n412_15)
APPEND(gen_nil:cons10_15(n73855_15), gen_nil:cons10_15(b)) -> gen_c7:c813_15(n73855_15), rt in Omega(1 + n73855_15)
dropLast(gen_nil:cons10_15(+(1, n74737_15))) -> gen_nil:cons10_15(n74737_15), rt in Omega(0)
append(gen_nil:cons10_15(n75349_15), gen_nil:cons10_15(b)) -> gen_nil:cons10_15(+(n75349_15, b)), rt in Omega(0)
last(gen_nil:cons10_15(+(1, n76805_15))) -> gen_nil:cons10_15(0), rt in Omega(0)


Generator Equations:
gen_nil:cons10_15(0) <=> nil
gen_nil:cons10_15(+(x, 1)) <=> cons(nil, gen_nil:cons10_15(x))
gen_c2:c311_15(0) <=> c2
gen_c2:c311_15(+(x, 1)) <=> c3(gen_c2:c311_15(x))
gen_c4:c5:c612_15(0) <=> c4
gen_c4:c5:c612_15(+(x, 1)) <=> c6(gen_c4:c5:c612_15(x))
gen_c7:c813_15(0) <=> c7
gen_c7:c813_15(+(x, 1)) <=> c8(gen_c7:c813_15(x))


The following defined symbols remain to be analysed:
REV, rev
----------------------------------------

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REV(gen_nil:cons10_15(n77284_15), gen_nil:cons10_15(b)) -> *14_15, rt in Omega(n77284_15 + n77284_15^2)

Induction Base:
REV(gen_nil:cons10_15(0), gen_nil:cons10_15(b))

Induction Step:
REV(gen_nil:cons10_15(+(n77284_15, 1)), gen_nil:cons10_15(b)) ->_R^Omega(1)
c12(IF(isEmpty(gen_nil:cons10_15(+(n77284_15, 1))), dropLast(gen_nil:cons10_15(+(n77284_15, 1))), append(gen_nil:cons10_15(b), last(gen_nil:cons10_15(+(n77284_15, 1)))), gen_nil:cons10_15(b)), APPEND(gen_nil:cons10_15(b), last(gen_nil:cons10_15(+(n77284_15, 1)))), LAST(gen_nil:cons10_15(+(n77284_15, 1)))) ->_R^Omega(0)
c12(IF(false, dropLast(gen_nil:cons10_15(+(1, n77284_15))), append(gen_nil:cons10_15(b), last(gen_nil:cons10_15(+(1, n77284_15)))), gen_nil:cons10_15(b)), APPEND(gen_nil:cons10_15(b), last(gen_nil:cons10_15(+(1, n77284_15)))), LAST(gen_nil:cons10_15(+(1, n77284_15)))) ->_L^Omega(0)
c12(IF(false, gen_nil:cons10_15(n77284_15), append(gen_nil:cons10_15(b), last(gen_nil:cons10_15(+(1, n77284_15)))), gen_nil:cons10_15(b)), APPEND(gen_nil:cons10_15(b), last(gen_nil:cons10_15(+(1, n77284_15)))), LAST(gen_nil:cons10_15(+(1, n77284_15)))) ->_L^Omega(0)
c12(IF(false, gen_nil:cons10_15(n77284_15), append(gen_nil:cons10_15(b), gen_nil:cons10_15(0)), gen_nil:cons10_15(b)), APPEND(gen_nil:cons10_15(b), last(gen_nil:cons10_15(+(1, n77284_15)))), LAST(gen_nil:cons10_15(+(1, n77284_15)))) ->_L^Omega(0)
c12(IF(false, gen_nil:cons10_15(n77284_15), gen_nil:cons10_15(+(b, 0)), gen_nil:cons10_15(0)), APPEND(gen_nil:cons10_15(0), last(gen_nil:cons10_15(+(1, n77284_15)))), LAST(gen_nil:cons10_15(+(1, n77284_15)))) ->_R^Omega(1)
c12(c14(REV(gen_nil:cons10_15(n77284_15), gen_nil:cons10_15(b))), APPEND(gen_nil:cons10_15(0), last(gen_nil:cons10_15(+(1, n77284_15)))), LAST(gen_nil:cons10_15(+(1, n77284_15)))) ->_IH
c12(c14(*14_15), APPEND(gen_nil:cons10_15(0), last(gen_nil:cons10_15(+(1, n77284_15)))), LAST(gen_nil:cons10_15(+(1, n77284_15)))) ->_L^Omega(0)
c12(c14(*14_15), APPEND(gen_nil:cons10_15(0), gen_nil:cons10_15(0)), LAST(gen_nil:cons10_15(+(1, n77284_15)))) ->_L^Omega(1)
c12(c14(*14_15), gen_c7:c813_15(0), LAST(gen_nil:cons10_15(+(1, n77284_15)))) ->_L^Omega(1 + n77284_15)
c12(c14(*14_15), gen_c7:c813_15(0), gen_c2:c311_15(n77284_15))

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

(28)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8


Lemmas:
LAST(gen_nil:cons10_15(+(1, n15_15))) -> gen_c2:c311_15(n15_15), rt in Omega(1 + n15_15)
DROPLAST(gen_nil:cons10_15(+(2, n412_15))) -> *14_15, rt in Omega(n412_15)
APPEND(gen_nil:cons10_15(n73855_15), gen_nil:cons10_15(b)) -> gen_c7:c813_15(n73855_15), rt in Omega(1 + n73855_15)
dropLast(gen_nil:cons10_15(+(1, n74737_15))) -> gen_nil:cons10_15(n74737_15), rt in Omega(0)
append(gen_nil:cons10_15(n75349_15), gen_nil:cons10_15(b)) -> gen_nil:cons10_15(+(n75349_15, b)), rt in Omega(0)
last(gen_nil:cons10_15(+(1, n76805_15))) -> gen_nil:cons10_15(0), rt in Omega(0)


Generator Equations:
gen_nil:cons10_15(0) <=> nil
gen_nil:cons10_15(+(x, 1)) <=> cons(nil, gen_nil:cons10_15(x))
gen_c2:c311_15(0) <=> c2
gen_c2:c311_15(+(x, 1)) <=> c3(gen_c2:c311_15(x))
gen_c4:c5:c612_15(0) <=> c4
gen_c4:c5:c612_15(+(x, 1)) <=> c6(gen_c4:c5:c612_15(x))
gen_c7:c813_15(0) <=> c7
gen_c7:c813_15(+(x, 1)) <=> c8(gen_c7:c813_15(x))


The following defined symbols remain to be analysed:
REV, rev
----------------------------------------

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

(31)
BOUNDS(n^2, INF)

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

(32)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(nil) -> c
ISEMPTY(cons(z0, z1)) -> c1
LAST(cons(z0, nil)) -> c2
LAST(cons(z0, cons(z1, z2))) -> c3(LAST(cons(z1, z2)))
DROPLAST(nil) -> c4
DROPLAST(cons(z0, nil)) -> c5
DROPLAST(cons(z0, cons(z1, z2))) -> c6(DROPLAST(cons(z1, z2)))
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
REVERSE(z0) -> c9(REV(z0, nil))
REV(z0, z1) -> c10(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), ISEMPTY(z0))
REV(z0, z1) -> c11(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), DROPLAST(z0))
REV(z0, z1) -> c12(IF(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1), APPEND(z1, last(z0)), LAST(z0))
IF(true, z0, z1, z2) -> c13
IF(false, z0, z1, z2) -> c14(REV(z0, z1))
isEmpty(nil) -> true
isEmpty(cons(z0, z1)) -> false
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
dropLast(nil) -> nil
dropLast(cons(z0, nil)) -> nil
dropLast(cons(z0, cons(z1, z2))) -> cons(z0, dropLast(cons(z1, z2)))
append(nil, z0) -> z0
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
reverse(z0) -> rev(z0, nil)
rev(z0, z1) -> if(isEmpty(z0), dropLast(z0), append(z1, last(z0)), z1)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> rev(z0, z1)

Types:
ISEMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: nil:cons -> nil:cons -> nil:cons
c1 :: c:c1
LAST :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
DROPLAST :: nil:cons -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APPEND :: nil:cons -> nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10:c11:c12 -> c9
REV :: nil:cons -> nil:cons -> c10:c11:c12
c10 :: c13:c14 -> c:c1 -> c10:c11:c12
IF :: true:false -> nil:cons -> nil:cons -> nil:cons -> c13:c14
isEmpty :: nil:cons -> true:false
dropLast :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
last :: nil:cons -> nil:cons
c11 :: c13:c14 -> c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c7:c8 -> c2:c3 -> c10:c11:c12
true :: true:false
c13 :: c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
reverse :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons -> nil:cons
if :: true:false -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_nil:cons2_15 :: nil:cons
hole_c2:c33_15 :: c2:c3
hole_c4:c5:c64_15 :: c4:c5:c6
hole_c7:c85_15 :: c7:c8
hole_c96_15 :: c9
hole_c10:c11:c127_15 :: c10:c11:c12
hole_c13:c148_15 :: c13:c14
hole_true:false9_15 :: true:false
gen_nil:cons10_15 :: Nat -> nil:cons
gen_c2:c311_15 :: Nat -> c2:c3
gen_c4:c5:c612_15 :: Nat -> c4:c5:c6
gen_c7:c813_15 :: Nat -> c7:c8


Lemmas:
LAST(gen_nil:cons10_15(+(1, n15_15))) -> gen_c2:c311_15(n15_15), rt in Omega(1 + n15_15)
DROPLAST(gen_nil:cons10_15(+(2, n412_15))) -> *14_15, rt in Omega(n412_15)
APPEND(gen_nil:cons10_15(n73855_15), gen_nil:cons10_15(b)) -> gen_c7:c813_15(n73855_15), rt in Omega(1 + n73855_15)
dropLast(gen_nil:cons10_15(+(1, n74737_15))) -> gen_nil:cons10_15(n74737_15), rt in Omega(0)
append(gen_nil:cons10_15(n75349_15), gen_nil:cons10_15(b)) -> gen_nil:cons10_15(+(n75349_15, b)), rt in Omega(0)
last(gen_nil:cons10_15(+(1, n76805_15))) -> gen_nil:cons10_15(0), rt in Omega(0)
REV(gen_nil:cons10_15(n77284_15), gen_nil:cons10_15(b)) -> *14_15, rt in Omega(n77284_15 + n77284_15^2)


Generator Equations:
gen_nil:cons10_15(0) <=> nil
gen_nil:cons10_15(+(x, 1)) <=> cons(nil, gen_nil:cons10_15(x))
gen_c2:c311_15(0) <=> c2
gen_c2:c311_15(+(x, 1)) <=> c3(gen_c2:c311_15(x))
gen_c4:c5:c612_15(0) <=> c4
gen_c4:c5:c612_15(+(x, 1)) <=> c6(gen_c4:c5:c612_15(x))
gen_c7:c813_15(0) <=> c7
gen_c7:c813_15(+(x, 1)) <=> c8(gen_c7:c813_15(x))


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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
rev(gen_nil:cons10_15(n88633_15), gen_nil:cons10_15(0)) -> gen_nil:cons10_15(0), rt in Omega(0)

Induction Base:
rev(gen_nil:cons10_15(0), gen_nil:cons10_15(0)) ->_R^Omega(0)
if(isEmpty(gen_nil:cons10_15(0)), dropLast(gen_nil:cons10_15(0)), append(gen_nil:cons10_15(0), last(gen_nil:cons10_15(0))), gen_nil:cons10_15(0)) ->_R^Omega(0)
if(true, dropLast(gen_nil:cons10_15(0)), append(gen_nil:cons10_15(0), last(gen_nil:cons10_15(0))), gen_nil:cons10_15(0)) ->_R^Omega(0)
if(true, nil, append(gen_nil:cons10_15(0), last(gen_nil:cons10_15(0))), gen_nil:cons10_15(0)) ->_R^Omega(0)
if(true, nil, last(gen_nil:cons10_15(0)), gen_nil:cons10_15(0)) ->_R^Omega(0)
gen_nil:cons10_15(0)

Induction Step:
rev(gen_nil:cons10_15(+(n88633_15, 1)), gen_nil:cons10_15(0)) ->_R^Omega(0)
if(isEmpty(gen_nil:cons10_15(+(n88633_15, 1))), dropLast(gen_nil:cons10_15(+(n88633_15, 1))), append(gen_nil:cons10_15(0), last(gen_nil:cons10_15(+(n88633_15, 1)))), gen_nil:cons10_15(0)) ->_R^Omega(0)
if(false, dropLast(gen_nil:cons10_15(+(1, n88633_15))), append(gen_nil:cons10_15(0), last(gen_nil:cons10_15(+(1, n88633_15)))), gen_nil:cons10_15(0)) ->_L^Omega(0)
if(false, gen_nil:cons10_15(n88633_15), append(gen_nil:cons10_15(0), last(gen_nil:cons10_15(+(1, n88633_15)))), gen_nil:cons10_15(0)) ->_L^Omega(0)
if(false, gen_nil:cons10_15(n88633_15), append(gen_nil:cons10_15(0), gen_nil:cons10_15(0)), gen_nil:cons10_15(0)) ->_L^Omega(0)
if(false, gen_nil:cons10_15(n88633_15), gen_nil:cons10_15(+(0, 0)), gen_nil:cons10_15(0)) ->_R^Omega(0)
rev(gen_nil:cons10_15(n88633_15), gen_nil:cons10_15(0)) ->_IH
gen_nil:cons10_15(0)

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

(34)
BOUNDS(1, INF)