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), 1363 ms]
(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), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 355 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), 45 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 48 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 80 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 46 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 39 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:

   GE(z0, 0) -> c
   GE(0, s(z0)) -> c1
   GE(s(z0), s(z1)) -> c2(GE(z0, z1))
   REV(z0) -> c3(IF(z0, eq(0, length(z0)), nil, 0, length(z0)), LENGTH(z0))
   REV(z0) -> c4(IF(z0, eq(0, length(z0)), nil, 0, length(z0)), LENGTH(z0))
   IF(z0, true, z1, z2, z3) -> c5
   IF(z0, false, z1, z2, z3) -> c6(HELP(s(z2), z3, z0, z1))
   HELP(z0, z1, cons(z2, z3), z4) -> c7(IF(append(z3, cons(z2, nil)), ge(z0, z1), cons(z2, z4), z0, z1), APPEND(z3, cons(z2, nil)))
   HELP(z0, z1, cons(z2, z3), z4) -> c8(IF(append(z3, cons(z2, nil)), ge(z0, z1), cons(z2, z4), z0, z1), GE(z0, z1))
   APPEND(nil, z0) -> c9
   APPEND(cons(z0, z1), z2) -> c10(APPEND(z1, z2))
   LENGTH(nil) -> c11
   LENGTH(cons(z0, z1)) -> c12(LENGTH(z1))

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

   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   rev(z0) -> if(z0, eq(0, length(z0)), nil, 0, length(z0))
   if(z0, true, z1, z2, z3) -> z1
   if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
   help(z0, z1, cons(z2, z3), z4) -> if(append(z3, cons(z2, nil)), ge(z0, z1), cons(z2, z4), z0, z1)
   append(nil, z0) -> z0
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))

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

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

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


The TRS R consists of the following rules:

   GE(z0, 0) -> c
   GE(0, s(z0)) -> c1
   GE(s(z0), s(z1)) -> c2(GE(z0, z1))
   REV(z0) -> c3(IF(z0, eq(0, length(z0)), nil, 0, length(z0)), LENGTH(z0))
   REV(z0) -> c4(IF(z0, eq(0, length(z0)), nil, 0, length(z0)), LENGTH(z0))
   IF(z0, true, z1, z2, z3) -> c5
   IF(z0, false, z1, z2, z3) -> c6(HELP(s(z2), z3, z0, z1))
   HELP(z0, z1, cons(z2, z3), z4) -> c7(IF(append(z3, cons(z2, nil)), ge(z0, z1), cons(z2, z4), z0, z1), APPEND(z3, cons(z2, nil)))
   HELP(z0, z1, cons(z2, z3), z4) -> c8(IF(append(z3, cons(z2, nil)), ge(z0, z1), cons(z2, z4), z0, z1), GE(z0, z1))
   APPEND(nil, z0) -> c9
   APPEND(cons(z0, z1), z2) -> c10(APPEND(z1, z2))
   LENGTH(nil) -> c11
   LENGTH(cons(z0, z1)) -> c12(LENGTH(z1))

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

   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   rev(z0) -> if(z0, eq(0, length(z0)), nil, 0, length(z0))
   if(z0, true, z1, z2, z3) -> z1
   if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
   help(z0, z1, cons(z2, z3), z4) -> if(append(z3, cons(z2, nil)), ge(z0, z1), cons(z2, z4), z0, z1)
   append(nil, z0) -> z0
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))

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:

   GE(z0, 0') -> c
   GE(0', s(z0)) -> c1
   GE(s(z0), s(z1)) -> c2(GE(z0, z1))
   REV(z0) -> c3(IF(z0, eq(0', length(z0)), nil, 0', length(z0)), LENGTH(z0))
   REV(z0) -> c4(IF(z0, eq(0', length(z0)), nil, 0', length(z0)), LENGTH(z0))
   IF(z0, true, z1, z2, z3) -> c5
   IF(z0, false, z1, z2, z3) -> c6(HELP(s(z2), z3, z0, z1))
   HELP(z0, z1, cons(z2, z3), z4) -> c7(IF(append(z3, cons(z2, nil)), ge(z0, z1), cons(z2, z4), z0, z1), APPEND(z3, cons(z2, nil)))
   HELP(z0, z1, cons(z2, z3), z4) -> c8(IF(append(z3, cons(z2, nil)), ge(z0, z1), cons(z2, z4), z0, z1), GE(z0, z1))
   APPEND(nil, z0) -> c9
   APPEND(cons(z0, z1), z2) -> c10(APPEND(z1, z2))
   LENGTH(nil) -> c11
   LENGTH(cons(z0, z1)) -> c12(LENGTH(z1))

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

   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   rev(z0) -> if(z0, eq(0', length(z0)), nil, 0', length(z0))
   if(z0, true, z1, z2, z3) -> z1
   if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
   help(z0, z1, cons(z2, z3), z4) -> if(append(z3, cons(z2, nil)), ge(z0, z1), cons(z2, z4), z0, z1)
   append(nil, z0) -> z0
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   length(nil) -> 0'
   length(cons(z0, z1)) -> s(length(z1))

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
IF/2
eq/0
HELP/3
cons/0
APPEND/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:

   GE(z0, 0') -> c
   GE(0', s(z0)) -> c1
   GE(s(z0), s(z1)) -> c2(GE(z0, z1))
   REV(z0) -> c3(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
   REV(z0) -> c4(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
   IF(z0, true, z2, z3) -> c5
   IF(z0, false, z2, z3) -> c6(HELP(s(z2), z3, z0))
   HELP(z0, z1, cons(z3)) -> c7(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), APPEND(z3, cons(nil)))
   HELP(z0, z1, cons(z3)) -> c8(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), GE(z0, z1))
   APPEND(nil) -> c9
   APPEND(cons(z1)) -> c10(APPEND(z1))
   LENGTH(nil) -> c11
   LENGTH(cons(z1)) -> c12(LENGTH(z1))

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

   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   rev(z0) -> if(z0, eq(length(z0)), nil, 0', length(z0))
   if(z0, true, z1, z2, z3) -> z1
   if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
   help(z0, z1, cons(z3), z4) -> if(append(z3, cons(nil)), ge(z0, z1), cons(z4), z0, z1)
   append(nil, z0) -> z0
   append(cons(z1), z2) -> cons(append(z1, z2))
   length(nil) -> 0'
   length(cons(z1)) -> s(length(z1))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
REV(z0) -> c3(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
REV(z0) -> c4(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
IF(z0, true, z2, z3) -> c5
IF(z0, false, z2, z3) -> c6(HELP(s(z2), z3, z0))
HELP(z0, z1, cons(z3)) -> c7(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), APPEND(z3, cons(nil)))
HELP(z0, z1, cons(z3)) -> c8(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), GE(z0, z1))
APPEND(nil) -> c9
APPEND(cons(z1)) -> c10(APPEND(z1))
LENGTH(nil) -> c11
LENGTH(cons(z1)) -> c12(LENGTH(z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
rev(z0) -> if(z0, eq(length(z0)), nil, 0', length(z0))
if(z0, true, z1, z2, z3) -> z1
if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
help(z0, z1, cons(z3), z4) -> if(append(z3, cons(nil)), ge(z0, z1), cons(z4), z0, z1)
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))

Types:
GE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
REV :: cons:nil -> c3:c4
c3 :: c5:c6 -> c11:c12 -> c3:c4
IF :: cons:nil -> eq:true:false -> 0':s -> 0':s -> c5:c6
eq :: 0':s -> eq:true:false
length :: cons:nil -> 0':s
LENGTH :: cons:nil -> c11:c12
c4 :: c5:c6 -> c11:c12 -> c3:c4
true :: eq:true:false
c5 :: c5:c6
false :: eq:true:false
c6 :: c7:c8 -> c5:c6
HELP :: 0':s -> 0':s -> cons:nil -> c7:c8
cons :: cons:nil -> cons:nil
c7 :: c5:c6 -> APPEND -> c7:c8
append :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil
ge :: 0':s -> 0':s -> eq:true:false
APPEND :: cons:nil -> cons:nil -> APPEND
c8 :: c5:c6 -> c:c1:c2 -> c7:c8
APPEND :: cons:nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
rev :: cons:nil -> cons:nil
if :: cons:nil -> eq:true:false -> cons:nil -> 0':s -> 0':s -> cons:nil
help :: 0':s -> 0':s -> cons:nil -> cons:nil -> cons:nil
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c43_13 :: c3:c4
hole_cons:nil4_13 :: cons:nil
hole_c5:c65_13 :: c5:c6
hole_c11:c126_13 :: c11:c12
hole_eq:true:false7_13 :: eq:true:false
hole_c7:c88_13 :: c7:c8
hole_APPEND9_13 :: APPEND
hole_c9:c1010_13 :: c9:c10
gen_c:c1:c211_13 :: Nat -> c:c1:c2
gen_0':s12_13 :: Nat -> 0':s
gen_cons:nil13_13 :: Nat -> cons:nil
gen_c11:c1214_13 :: Nat -> c11:c12
gen_c9:c1015_13 :: Nat -> c9:c10

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
GE, length, LENGTH, HELP, append, ge, APPEND, help

They will be analysed ascendingly in the following order:
GE < HELP
append < HELP
ge < HELP
append < help
ge < help

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

(10)
Obligation:
Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
REV(z0) -> c3(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
REV(z0) -> c4(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
IF(z0, true, z2, z3) -> c5
IF(z0, false, z2, z3) -> c6(HELP(s(z2), z3, z0))
HELP(z0, z1, cons(z3)) -> c7(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), APPEND(z3, cons(nil)))
HELP(z0, z1, cons(z3)) -> c8(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), GE(z0, z1))
APPEND(nil) -> c9
APPEND(cons(z1)) -> c10(APPEND(z1))
LENGTH(nil) -> c11
LENGTH(cons(z1)) -> c12(LENGTH(z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
rev(z0) -> if(z0, eq(length(z0)), nil, 0', length(z0))
if(z0, true, z1, z2, z3) -> z1
if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
help(z0, z1, cons(z3), z4) -> if(append(z3, cons(nil)), ge(z0, z1), cons(z4), z0, z1)
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))

Types:
GE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
REV :: cons:nil -> c3:c4
c3 :: c5:c6 -> c11:c12 -> c3:c4
IF :: cons:nil -> eq:true:false -> 0':s -> 0':s -> c5:c6
eq :: 0':s -> eq:true:false
length :: cons:nil -> 0':s
LENGTH :: cons:nil -> c11:c12
c4 :: c5:c6 -> c11:c12 -> c3:c4
true :: eq:true:false
c5 :: c5:c6
false :: eq:true:false
c6 :: c7:c8 -> c5:c6
HELP :: 0':s -> 0':s -> cons:nil -> c7:c8
cons :: cons:nil -> cons:nil
c7 :: c5:c6 -> APPEND -> c7:c8
append :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil
ge :: 0':s -> 0':s -> eq:true:false
APPEND :: cons:nil -> cons:nil -> APPEND
c8 :: c5:c6 -> c:c1:c2 -> c7:c8
APPEND :: cons:nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
rev :: cons:nil -> cons:nil
if :: cons:nil -> eq:true:false -> cons:nil -> 0':s -> 0':s -> cons:nil
help :: 0':s -> 0':s -> cons:nil -> cons:nil -> cons:nil
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c43_13 :: c3:c4
hole_cons:nil4_13 :: cons:nil
hole_c5:c65_13 :: c5:c6
hole_c11:c126_13 :: c11:c12
hole_eq:true:false7_13 :: eq:true:false
hole_c7:c88_13 :: c7:c8
hole_APPEND9_13 :: APPEND
hole_c9:c1010_13 :: c9:c10
gen_c:c1:c211_13 :: Nat -> c:c1:c2
gen_0':s12_13 :: Nat -> 0':s
gen_cons:nil13_13 :: Nat -> cons:nil
gen_c11:c1214_13 :: Nat -> c11:c12
gen_c9:c1015_13 :: Nat -> c9:c10


Generator Equations:
gen_c:c1:c211_13(0) <=> c
gen_c:c1:c211_13(+(x, 1)) <=> c2(gen_c:c1:c211_13(x))
gen_0':s12_13(0) <=> 0'
gen_0':s12_13(+(x, 1)) <=> s(gen_0':s12_13(x))
gen_cons:nil13_13(0) <=> nil
gen_cons:nil13_13(+(x, 1)) <=> cons(gen_cons:nil13_13(x))
gen_c11:c1214_13(0) <=> c11
gen_c11:c1214_13(+(x, 1)) <=> c12(gen_c11:c1214_13(x))
gen_c9:c1015_13(0) <=> c9
gen_c9:c1015_13(+(x, 1)) <=> c10(gen_c9:c1015_13(x))


The following defined symbols remain to be analysed:
GE, length, LENGTH, HELP, append, ge, APPEND, help

They will be analysed ascendingly in the following order:
GE < HELP
append < HELP
ge < HELP
append < help
ge < help

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s12_13(n17_13), gen_0':s12_13(n17_13)) -> gen_c:c1:c211_13(n17_13), rt in Omega(1 + n17_13)

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

Induction Step:
GE(gen_0':s12_13(+(n17_13, 1)), gen_0':s12_13(+(n17_13, 1))) ->_R^Omega(1)
c2(GE(gen_0':s12_13(n17_13), gen_0':s12_13(n17_13))) ->_IH
c2(gen_c:c1:c211_13(c18_13))

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:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
REV(z0) -> c3(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
REV(z0) -> c4(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
IF(z0, true, z2, z3) -> c5
IF(z0, false, z2, z3) -> c6(HELP(s(z2), z3, z0))
HELP(z0, z1, cons(z3)) -> c7(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), APPEND(z3, cons(nil)))
HELP(z0, z1, cons(z3)) -> c8(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), GE(z0, z1))
APPEND(nil) -> c9
APPEND(cons(z1)) -> c10(APPEND(z1))
LENGTH(nil) -> c11
LENGTH(cons(z1)) -> c12(LENGTH(z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
rev(z0) -> if(z0, eq(length(z0)), nil, 0', length(z0))
if(z0, true, z1, z2, z3) -> z1
if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
help(z0, z1, cons(z3), z4) -> if(append(z3, cons(nil)), ge(z0, z1), cons(z4), z0, z1)
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))

Types:
GE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
REV :: cons:nil -> c3:c4
c3 :: c5:c6 -> c11:c12 -> c3:c4
IF :: cons:nil -> eq:true:false -> 0':s -> 0':s -> c5:c6
eq :: 0':s -> eq:true:false
length :: cons:nil -> 0':s
LENGTH :: cons:nil -> c11:c12
c4 :: c5:c6 -> c11:c12 -> c3:c4
true :: eq:true:false
c5 :: c5:c6
false :: eq:true:false
c6 :: c7:c8 -> c5:c6
HELP :: 0':s -> 0':s -> cons:nil -> c7:c8
cons :: cons:nil -> cons:nil
c7 :: c5:c6 -> APPEND -> c7:c8
append :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil
ge :: 0':s -> 0':s -> eq:true:false
APPEND :: cons:nil -> cons:nil -> APPEND
c8 :: c5:c6 -> c:c1:c2 -> c7:c8
APPEND :: cons:nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
rev :: cons:nil -> cons:nil
if :: cons:nil -> eq:true:false -> cons:nil -> 0':s -> 0':s -> cons:nil
help :: 0':s -> 0':s -> cons:nil -> cons:nil -> cons:nil
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c43_13 :: c3:c4
hole_cons:nil4_13 :: cons:nil
hole_c5:c65_13 :: c5:c6
hole_c11:c126_13 :: c11:c12
hole_eq:true:false7_13 :: eq:true:false
hole_c7:c88_13 :: c7:c8
hole_APPEND9_13 :: APPEND
hole_c9:c1010_13 :: c9:c10
gen_c:c1:c211_13 :: Nat -> c:c1:c2
gen_0':s12_13 :: Nat -> 0':s
gen_cons:nil13_13 :: Nat -> cons:nil
gen_c11:c1214_13 :: Nat -> c11:c12
gen_c9:c1015_13 :: Nat -> c9:c10


Generator Equations:
gen_c:c1:c211_13(0) <=> c
gen_c:c1:c211_13(+(x, 1)) <=> c2(gen_c:c1:c211_13(x))
gen_0':s12_13(0) <=> 0'
gen_0':s12_13(+(x, 1)) <=> s(gen_0':s12_13(x))
gen_cons:nil13_13(0) <=> nil
gen_cons:nil13_13(+(x, 1)) <=> cons(gen_cons:nil13_13(x))
gen_c11:c1214_13(0) <=> c11
gen_c11:c1214_13(+(x, 1)) <=> c12(gen_c11:c1214_13(x))
gen_c9:c1015_13(0) <=> c9
gen_c9:c1015_13(+(x, 1)) <=> c10(gen_c9:c1015_13(x))


The following defined symbols remain to be analysed:
GE, length, LENGTH, HELP, append, ge, APPEND, help

They will be analysed ascendingly in the following order:
GE < HELP
append < HELP
ge < HELP
append < help
ge < help

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
REV(z0) -> c3(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
REV(z0) -> c4(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
IF(z0, true, z2, z3) -> c5
IF(z0, false, z2, z3) -> c6(HELP(s(z2), z3, z0))
HELP(z0, z1, cons(z3)) -> c7(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), APPEND(z3, cons(nil)))
HELP(z0, z1, cons(z3)) -> c8(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), GE(z0, z1))
APPEND(nil) -> c9
APPEND(cons(z1)) -> c10(APPEND(z1))
LENGTH(nil) -> c11
LENGTH(cons(z1)) -> c12(LENGTH(z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
rev(z0) -> if(z0, eq(length(z0)), nil, 0', length(z0))
if(z0, true, z1, z2, z3) -> z1
if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
help(z0, z1, cons(z3), z4) -> if(append(z3, cons(nil)), ge(z0, z1), cons(z4), z0, z1)
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))

Types:
GE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
REV :: cons:nil -> c3:c4
c3 :: c5:c6 -> c11:c12 -> c3:c4
IF :: cons:nil -> eq:true:false -> 0':s -> 0':s -> c5:c6
eq :: 0':s -> eq:true:false
length :: cons:nil -> 0':s
LENGTH :: cons:nil -> c11:c12
c4 :: c5:c6 -> c11:c12 -> c3:c4
true :: eq:true:false
c5 :: c5:c6
false :: eq:true:false
c6 :: c7:c8 -> c5:c6
HELP :: 0':s -> 0':s -> cons:nil -> c7:c8
cons :: cons:nil -> cons:nil
c7 :: c5:c6 -> APPEND -> c7:c8
append :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil
ge :: 0':s -> 0':s -> eq:true:false
APPEND :: cons:nil -> cons:nil -> APPEND
c8 :: c5:c6 -> c:c1:c2 -> c7:c8
APPEND :: cons:nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
rev :: cons:nil -> cons:nil
if :: cons:nil -> eq:true:false -> cons:nil -> 0':s -> 0':s -> cons:nil
help :: 0':s -> 0':s -> cons:nil -> cons:nil -> cons:nil
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c43_13 :: c3:c4
hole_cons:nil4_13 :: cons:nil
hole_c5:c65_13 :: c5:c6
hole_c11:c126_13 :: c11:c12
hole_eq:true:false7_13 :: eq:true:false
hole_c7:c88_13 :: c7:c8
hole_APPEND9_13 :: APPEND
hole_c9:c1010_13 :: c9:c10
gen_c:c1:c211_13 :: Nat -> c:c1:c2
gen_0':s12_13 :: Nat -> 0':s
gen_cons:nil13_13 :: Nat -> cons:nil
gen_c11:c1214_13 :: Nat -> c11:c12
gen_c9:c1015_13 :: Nat -> c9:c10


Lemmas:
GE(gen_0':s12_13(n17_13), gen_0':s12_13(n17_13)) -> gen_c:c1:c211_13(n17_13), rt in Omega(1 + n17_13)


Generator Equations:
gen_c:c1:c211_13(0) <=> c
gen_c:c1:c211_13(+(x, 1)) <=> c2(gen_c:c1:c211_13(x))
gen_0':s12_13(0) <=> 0'
gen_0':s12_13(+(x, 1)) <=> s(gen_0':s12_13(x))
gen_cons:nil13_13(0) <=> nil
gen_cons:nil13_13(+(x, 1)) <=> cons(gen_cons:nil13_13(x))
gen_c11:c1214_13(0) <=> c11
gen_c11:c1214_13(+(x, 1)) <=> c12(gen_c11:c1214_13(x))
gen_c9:c1015_13(0) <=> c9
gen_c9:c1015_13(+(x, 1)) <=> c10(gen_c9:c1015_13(x))


The following defined symbols remain to be analysed:
length, LENGTH, HELP, append, ge, APPEND, help

They will be analysed ascendingly in the following order:
append < HELP
ge < HELP
append < help
ge < help

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
length(gen_cons:nil13_13(n612_13)) -> gen_0':s12_13(n612_13), rt in Omega(0)

Induction Base:
length(gen_cons:nil13_13(0)) ->_R^Omega(0)
0'

Induction Step:
length(gen_cons:nil13_13(+(n612_13, 1))) ->_R^Omega(0)
s(length(gen_cons:nil13_13(n612_13))) ->_IH
s(gen_0':s12_13(c613_13))

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

(18)
Obligation:
Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
REV(z0) -> c3(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
REV(z0) -> c4(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
IF(z0, true, z2, z3) -> c5
IF(z0, false, z2, z3) -> c6(HELP(s(z2), z3, z0))
HELP(z0, z1, cons(z3)) -> c7(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), APPEND(z3, cons(nil)))
HELP(z0, z1, cons(z3)) -> c8(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), GE(z0, z1))
APPEND(nil) -> c9
APPEND(cons(z1)) -> c10(APPEND(z1))
LENGTH(nil) -> c11
LENGTH(cons(z1)) -> c12(LENGTH(z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
rev(z0) -> if(z0, eq(length(z0)), nil, 0', length(z0))
if(z0, true, z1, z2, z3) -> z1
if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
help(z0, z1, cons(z3), z4) -> if(append(z3, cons(nil)), ge(z0, z1), cons(z4), z0, z1)
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))

Types:
GE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
REV :: cons:nil -> c3:c4
c3 :: c5:c6 -> c11:c12 -> c3:c4
IF :: cons:nil -> eq:true:false -> 0':s -> 0':s -> c5:c6
eq :: 0':s -> eq:true:false
length :: cons:nil -> 0':s
LENGTH :: cons:nil -> c11:c12
c4 :: c5:c6 -> c11:c12 -> c3:c4
true :: eq:true:false
c5 :: c5:c6
false :: eq:true:false
c6 :: c7:c8 -> c5:c6
HELP :: 0':s -> 0':s -> cons:nil -> c7:c8
cons :: cons:nil -> cons:nil
c7 :: c5:c6 -> APPEND -> c7:c8
append :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil
ge :: 0':s -> 0':s -> eq:true:false
APPEND :: cons:nil -> cons:nil -> APPEND
c8 :: c5:c6 -> c:c1:c2 -> c7:c8
APPEND :: cons:nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
rev :: cons:nil -> cons:nil
if :: cons:nil -> eq:true:false -> cons:nil -> 0':s -> 0':s -> cons:nil
help :: 0':s -> 0':s -> cons:nil -> cons:nil -> cons:nil
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c43_13 :: c3:c4
hole_cons:nil4_13 :: cons:nil
hole_c5:c65_13 :: c5:c6
hole_c11:c126_13 :: c11:c12
hole_eq:true:false7_13 :: eq:true:false
hole_c7:c88_13 :: c7:c8
hole_APPEND9_13 :: APPEND
hole_c9:c1010_13 :: c9:c10
gen_c:c1:c211_13 :: Nat -> c:c1:c2
gen_0':s12_13 :: Nat -> 0':s
gen_cons:nil13_13 :: Nat -> cons:nil
gen_c11:c1214_13 :: Nat -> c11:c12
gen_c9:c1015_13 :: Nat -> c9:c10


Lemmas:
GE(gen_0':s12_13(n17_13), gen_0':s12_13(n17_13)) -> gen_c:c1:c211_13(n17_13), rt in Omega(1 + n17_13)
length(gen_cons:nil13_13(n612_13)) -> gen_0':s12_13(n612_13), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_13(0) <=> c
gen_c:c1:c211_13(+(x, 1)) <=> c2(gen_c:c1:c211_13(x))
gen_0':s12_13(0) <=> 0'
gen_0':s12_13(+(x, 1)) <=> s(gen_0':s12_13(x))
gen_cons:nil13_13(0) <=> nil
gen_cons:nil13_13(+(x, 1)) <=> cons(gen_cons:nil13_13(x))
gen_c11:c1214_13(0) <=> c11
gen_c11:c1214_13(+(x, 1)) <=> c12(gen_c11:c1214_13(x))
gen_c9:c1015_13(0) <=> c9
gen_c9:c1015_13(+(x, 1)) <=> c10(gen_c9:c1015_13(x))


The following defined symbols remain to be analysed:
LENGTH, HELP, append, ge, APPEND, help

They will be analysed ascendingly in the following order:
append < HELP
ge < HELP
append < help
ge < help

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LENGTH(gen_cons:nil13_13(n944_13)) -> gen_c11:c1214_13(n944_13), rt in Omega(1 + n944_13)

Induction Base:
LENGTH(gen_cons:nil13_13(0)) ->_R^Omega(1)
c11

Induction Step:
LENGTH(gen_cons:nil13_13(+(n944_13, 1))) ->_R^Omega(1)
c12(LENGTH(gen_cons:nil13_13(n944_13))) ->_IH
c12(gen_c11:c1214_13(c945_13))

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:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
REV(z0) -> c3(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
REV(z0) -> c4(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
IF(z0, true, z2, z3) -> c5
IF(z0, false, z2, z3) -> c6(HELP(s(z2), z3, z0))
HELP(z0, z1, cons(z3)) -> c7(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), APPEND(z3, cons(nil)))
HELP(z0, z1, cons(z3)) -> c8(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), GE(z0, z1))
APPEND(nil) -> c9
APPEND(cons(z1)) -> c10(APPEND(z1))
LENGTH(nil) -> c11
LENGTH(cons(z1)) -> c12(LENGTH(z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
rev(z0) -> if(z0, eq(length(z0)), nil, 0', length(z0))
if(z0, true, z1, z2, z3) -> z1
if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
help(z0, z1, cons(z3), z4) -> if(append(z3, cons(nil)), ge(z0, z1), cons(z4), z0, z1)
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))

Types:
GE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
REV :: cons:nil -> c3:c4
c3 :: c5:c6 -> c11:c12 -> c3:c4
IF :: cons:nil -> eq:true:false -> 0':s -> 0':s -> c5:c6
eq :: 0':s -> eq:true:false
length :: cons:nil -> 0':s
LENGTH :: cons:nil -> c11:c12
c4 :: c5:c6 -> c11:c12 -> c3:c4
true :: eq:true:false
c5 :: c5:c6
false :: eq:true:false
c6 :: c7:c8 -> c5:c6
HELP :: 0':s -> 0':s -> cons:nil -> c7:c8
cons :: cons:nil -> cons:nil
c7 :: c5:c6 -> APPEND -> c7:c8
append :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil
ge :: 0':s -> 0':s -> eq:true:false
APPEND :: cons:nil -> cons:nil -> APPEND
c8 :: c5:c6 -> c:c1:c2 -> c7:c8
APPEND :: cons:nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
rev :: cons:nil -> cons:nil
if :: cons:nil -> eq:true:false -> cons:nil -> 0':s -> 0':s -> cons:nil
help :: 0':s -> 0':s -> cons:nil -> cons:nil -> cons:nil
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c43_13 :: c3:c4
hole_cons:nil4_13 :: cons:nil
hole_c5:c65_13 :: c5:c6
hole_c11:c126_13 :: c11:c12
hole_eq:true:false7_13 :: eq:true:false
hole_c7:c88_13 :: c7:c8
hole_APPEND9_13 :: APPEND
hole_c9:c1010_13 :: c9:c10
gen_c:c1:c211_13 :: Nat -> c:c1:c2
gen_0':s12_13 :: Nat -> 0':s
gen_cons:nil13_13 :: Nat -> cons:nil
gen_c11:c1214_13 :: Nat -> c11:c12
gen_c9:c1015_13 :: Nat -> c9:c10


Lemmas:
GE(gen_0':s12_13(n17_13), gen_0':s12_13(n17_13)) -> gen_c:c1:c211_13(n17_13), rt in Omega(1 + n17_13)
length(gen_cons:nil13_13(n612_13)) -> gen_0':s12_13(n612_13), rt in Omega(0)
LENGTH(gen_cons:nil13_13(n944_13)) -> gen_c11:c1214_13(n944_13), rt in Omega(1 + n944_13)


Generator Equations:
gen_c:c1:c211_13(0) <=> c
gen_c:c1:c211_13(+(x, 1)) <=> c2(gen_c:c1:c211_13(x))
gen_0':s12_13(0) <=> 0'
gen_0':s12_13(+(x, 1)) <=> s(gen_0':s12_13(x))
gen_cons:nil13_13(0) <=> nil
gen_cons:nil13_13(+(x, 1)) <=> cons(gen_cons:nil13_13(x))
gen_c11:c1214_13(0) <=> c11
gen_c11:c1214_13(+(x, 1)) <=> c12(gen_c11:c1214_13(x))
gen_c9:c1015_13(0) <=> c9
gen_c9:c1015_13(+(x, 1)) <=> c10(gen_c9:c1015_13(x))


The following defined symbols remain to be analysed:
append, HELP, ge, APPEND, help

They will be analysed ascendingly in the following order:
append < HELP
ge < HELP
append < help
ge < help

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
append(gen_cons:nil13_13(n1348_13), gen_cons:nil13_13(b)) -> gen_cons:nil13_13(+(n1348_13, b)), rt in Omega(0)

Induction Base:
append(gen_cons:nil13_13(0), gen_cons:nil13_13(b)) ->_R^Omega(0)
gen_cons:nil13_13(b)

Induction Step:
append(gen_cons:nil13_13(+(n1348_13, 1)), gen_cons:nil13_13(b)) ->_R^Omega(0)
cons(append(gen_cons:nil13_13(n1348_13), gen_cons:nil13_13(b))) ->_IH
cons(gen_cons:nil13_13(+(b, c1349_13)))

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:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
REV(z0) -> c3(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
REV(z0) -> c4(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
IF(z0, true, z2, z3) -> c5
IF(z0, false, z2, z3) -> c6(HELP(s(z2), z3, z0))
HELP(z0, z1, cons(z3)) -> c7(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), APPEND(z3, cons(nil)))
HELP(z0, z1, cons(z3)) -> c8(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), GE(z0, z1))
APPEND(nil) -> c9
APPEND(cons(z1)) -> c10(APPEND(z1))
LENGTH(nil) -> c11
LENGTH(cons(z1)) -> c12(LENGTH(z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
rev(z0) -> if(z0, eq(length(z0)), nil, 0', length(z0))
if(z0, true, z1, z2, z3) -> z1
if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
help(z0, z1, cons(z3), z4) -> if(append(z3, cons(nil)), ge(z0, z1), cons(z4), z0, z1)
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))

Types:
GE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
REV :: cons:nil -> c3:c4
c3 :: c5:c6 -> c11:c12 -> c3:c4
IF :: cons:nil -> eq:true:false -> 0':s -> 0':s -> c5:c6
eq :: 0':s -> eq:true:false
length :: cons:nil -> 0':s
LENGTH :: cons:nil -> c11:c12
c4 :: c5:c6 -> c11:c12 -> c3:c4
true :: eq:true:false
c5 :: c5:c6
false :: eq:true:false
c6 :: c7:c8 -> c5:c6
HELP :: 0':s -> 0':s -> cons:nil -> c7:c8
cons :: cons:nil -> cons:nil
c7 :: c5:c6 -> APPEND -> c7:c8
append :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil
ge :: 0':s -> 0':s -> eq:true:false
APPEND :: cons:nil -> cons:nil -> APPEND
c8 :: c5:c6 -> c:c1:c2 -> c7:c8
APPEND :: cons:nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
rev :: cons:nil -> cons:nil
if :: cons:nil -> eq:true:false -> cons:nil -> 0':s -> 0':s -> cons:nil
help :: 0':s -> 0':s -> cons:nil -> cons:nil -> cons:nil
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c43_13 :: c3:c4
hole_cons:nil4_13 :: cons:nil
hole_c5:c65_13 :: c5:c6
hole_c11:c126_13 :: c11:c12
hole_eq:true:false7_13 :: eq:true:false
hole_c7:c88_13 :: c7:c8
hole_APPEND9_13 :: APPEND
hole_c9:c1010_13 :: c9:c10
gen_c:c1:c211_13 :: Nat -> c:c1:c2
gen_0':s12_13 :: Nat -> 0':s
gen_cons:nil13_13 :: Nat -> cons:nil
gen_c11:c1214_13 :: Nat -> c11:c12
gen_c9:c1015_13 :: Nat -> c9:c10


Lemmas:
GE(gen_0':s12_13(n17_13), gen_0':s12_13(n17_13)) -> gen_c:c1:c211_13(n17_13), rt in Omega(1 + n17_13)
length(gen_cons:nil13_13(n612_13)) -> gen_0':s12_13(n612_13), rt in Omega(0)
LENGTH(gen_cons:nil13_13(n944_13)) -> gen_c11:c1214_13(n944_13), rt in Omega(1 + n944_13)
append(gen_cons:nil13_13(n1348_13), gen_cons:nil13_13(b)) -> gen_cons:nil13_13(+(n1348_13, b)), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_13(0) <=> c
gen_c:c1:c211_13(+(x, 1)) <=> c2(gen_c:c1:c211_13(x))
gen_0':s12_13(0) <=> 0'
gen_0':s12_13(+(x, 1)) <=> s(gen_0':s12_13(x))
gen_cons:nil13_13(0) <=> nil
gen_cons:nil13_13(+(x, 1)) <=> cons(gen_cons:nil13_13(x))
gen_c11:c1214_13(0) <=> c11
gen_c11:c1214_13(+(x, 1)) <=> c12(gen_c11:c1214_13(x))
gen_c9:c1015_13(0) <=> c9
gen_c9:c1015_13(+(x, 1)) <=> c10(gen_c9:c1015_13(x))


The following defined symbols remain to be analysed:
ge, HELP, APPEND, help

They will be analysed ascendingly in the following order:
ge < HELP
ge < help

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s12_13(n2817_13), gen_0':s12_13(n2817_13)) -> true, rt in Omega(0)

Induction Base:
ge(gen_0':s12_13(0), gen_0':s12_13(0)) ->_R^Omega(0)
true

Induction Step:
ge(gen_0':s12_13(+(n2817_13, 1)), gen_0':s12_13(+(n2817_13, 1))) ->_R^Omega(0)
ge(gen_0':s12_13(n2817_13), gen_0':s12_13(n2817_13)) ->_IH
true

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:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
REV(z0) -> c3(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
REV(z0) -> c4(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
IF(z0, true, z2, z3) -> c5
IF(z0, false, z2, z3) -> c6(HELP(s(z2), z3, z0))
HELP(z0, z1, cons(z3)) -> c7(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), APPEND(z3, cons(nil)))
HELP(z0, z1, cons(z3)) -> c8(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), GE(z0, z1))
APPEND(nil) -> c9
APPEND(cons(z1)) -> c10(APPEND(z1))
LENGTH(nil) -> c11
LENGTH(cons(z1)) -> c12(LENGTH(z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
rev(z0) -> if(z0, eq(length(z0)), nil, 0', length(z0))
if(z0, true, z1, z2, z3) -> z1
if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
help(z0, z1, cons(z3), z4) -> if(append(z3, cons(nil)), ge(z0, z1), cons(z4), z0, z1)
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))

Types:
GE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
REV :: cons:nil -> c3:c4
c3 :: c5:c6 -> c11:c12 -> c3:c4
IF :: cons:nil -> eq:true:false -> 0':s -> 0':s -> c5:c6
eq :: 0':s -> eq:true:false
length :: cons:nil -> 0':s
LENGTH :: cons:nil -> c11:c12
c4 :: c5:c6 -> c11:c12 -> c3:c4
true :: eq:true:false
c5 :: c5:c6
false :: eq:true:false
c6 :: c7:c8 -> c5:c6
HELP :: 0':s -> 0':s -> cons:nil -> c7:c8
cons :: cons:nil -> cons:nil
c7 :: c5:c6 -> APPEND -> c7:c8
append :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil
ge :: 0':s -> 0':s -> eq:true:false
APPEND :: cons:nil -> cons:nil -> APPEND
c8 :: c5:c6 -> c:c1:c2 -> c7:c8
APPEND :: cons:nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
rev :: cons:nil -> cons:nil
if :: cons:nil -> eq:true:false -> cons:nil -> 0':s -> 0':s -> cons:nil
help :: 0':s -> 0':s -> cons:nil -> cons:nil -> cons:nil
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c43_13 :: c3:c4
hole_cons:nil4_13 :: cons:nil
hole_c5:c65_13 :: c5:c6
hole_c11:c126_13 :: c11:c12
hole_eq:true:false7_13 :: eq:true:false
hole_c7:c88_13 :: c7:c8
hole_APPEND9_13 :: APPEND
hole_c9:c1010_13 :: c9:c10
gen_c:c1:c211_13 :: Nat -> c:c1:c2
gen_0':s12_13 :: Nat -> 0':s
gen_cons:nil13_13 :: Nat -> cons:nil
gen_c11:c1214_13 :: Nat -> c11:c12
gen_c9:c1015_13 :: Nat -> c9:c10


Lemmas:
GE(gen_0':s12_13(n17_13), gen_0':s12_13(n17_13)) -> gen_c:c1:c211_13(n17_13), rt in Omega(1 + n17_13)
length(gen_cons:nil13_13(n612_13)) -> gen_0':s12_13(n612_13), rt in Omega(0)
LENGTH(gen_cons:nil13_13(n944_13)) -> gen_c11:c1214_13(n944_13), rt in Omega(1 + n944_13)
append(gen_cons:nil13_13(n1348_13), gen_cons:nil13_13(b)) -> gen_cons:nil13_13(+(n1348_13, b)), rt in Omega(0)
ge(gen_0':s12_13(n2817_13), gen_0':s12_13(n2817_13)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c211_13(0) <=> c
gen_c:c1:c211_13(+(x, 1)) <=> c2(gen_c:c1:c211_13(x))
gen_0':s12_13(0) <=> 0'
gen_0':s12_13(+(x, 1)) <=> s(gen_0':s12_13(x))
gen_cons:nil13_13(0) <=> nil
gen_cons:nil13_13(+(x, 1)) <=> cons(gen_cons:nil13_13(x))
gen_c11:c1214_13(0) <=> c11
gen_c11:c1214_13(+(x, 1)) <=> c12(gen_c11:c1214_13(x))
gen_c9:c1015_13(0) <=> c9
gen_c9:c1015_13(+(x, 1)) <=> c10(gen_c9:c1015_13(x))


The following defined symbols remain to be analysed:
HELP, APPEND, help
----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND(gen_cons:nil13_13(n3966_13)) -> gen_c9:c1015_13(n3966_13), rt in Omega(1 + n3966_13)

Induction Base:
APPEND(gen_cons:nil13_13(0)) ->_R^Omega(1)
c9

Induction Step:
APPEND(gen_cons:nil13_13(+(n3966_13, 1))) ->_R^Omega(1)
c10(APPEND(gen_cons:nil13_13(n3966_13))) ->_IH
c10(gen_c9:c1015_13(c3967_13))

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

(26)
Obligation:
Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
REV(z0) -> c3(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
REV(z0) -> c4(IF(z0, eq(length(z0)), 0', length(z0)), LENGTH(z0))
IF(z0, true, z2, z3) -> c5
IF(z0, false, z2, z3) -> c6(HELP(s(z2), z3, z0))
HELP(z0, z1, cons(z3)) -> c7(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), APPEND(z3, cons(nil)))
HELP(z0, z1, cons(z3)) -> c8(IF(append(z3, cons(nil)), ge(z0, z1), z0, z1), GE(z0, z1))
APPEND(nil) -> c9
APPEND(cons(z1)) -> c10(APPEND(z1))
LENGTH(nil) -> c11
LENGTH(cons(z1)) -> c12(LENGTH(z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
rev(z0) -> if(z0, eq(length(z0)), nil, 0', length(z0))
if(z0, true, z1, z2, z3) -> z1
if(z0, false, z1, z2, z3) -> help(s(z2), z3, z0, z1)
help(z0, z1, cons(z3), z4) -> if(append(z3, cons(nil)), ge(z0, z1), cons(z4), z0, z1)
append(nil, z0) -> z0
append(cons(z1), z2) -> cons(append(z1, z2))
length(nil) -> 0'
length(cons(z1)) -> s(length(z1))

Types:
GE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
REV :: cons:nil -> c3:c4
c3 :: c5:c6 -> c11:c12 -> c3:c4
IF :: cons:nil -> eq:true:false -> 0':s -> 0':s -> c5:c6
eq :: 0':s -> eq:true:false
length :: cons:nil -> 0':s
LENGTH :: cons:nil -> c11:c12
c4 :: c5:c6 -> c11:c12 -> c3:c4
true :: eq:true:false
c5 :: c5:c6
false :: eq:true:false
c6 :: c7:c8 -> c5:c6
HELP :: 0':s -> 0':s -> cons:nil -> c7:c8
cons :: cons:nil -> cons:nil
c7 :: c5:c6 -> APPEND -> c7:c8
append :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil
ge :: 0':s -> 0':s -> eq:true:false
APPEND :: cons:nil -> cons:nil -> APPEND
c8 :: c5:c6 -> c:c1:c2 -> c7:c8
APPEND :: cons:nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
rev :: cons:nil -> cons:nil
if :: cons:nil -> eq:true:false -> cons:nil -> 0':s -> 0':s -> cons:nil
help :: 0':s -> 0':s -> cons:nil -> cons:nil -> cons:nil
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c43_13 :: c3:c4
hole_cons:nil4_13 :: cons:nil
hole_c5:c65_13 :: c5:c6
hole_c11:c126_13 :: c11:c12
hole_eq:true:false7_13 :: eq:true:false
hole_c7:c88_13 :: c7:c8
hole_APPEND9_13 :: APPEND
hole_c9:c1010_13 :: c9:c10
gen_c:c1:c211_13 :: Nat -> c:c1:c2
gen_0':s12_13 :: Nat -> 0':s
gen_cons:nil13_13 :: Nat -> cons:nil
gen_c11:c1214_13 :: Nat -> c11:c12
gen_c9:c1015_13 :: Nat -> c9:c10


Lemmas:
GE(gen_0':s12_13(n17_13), gen_0':s12_13(n17_13)) -> gen_c:c1:c211_13(n17_13), rt in Omega(1 + n17_13)
length(gen_cons:nil13_13(n612_13)) -> gen_0':s12_13(n612_13), rt in Omega(0)
LENGTH(gen_cons:nil13_13(n944_13)) -> gen_c11:c1214_13(n944_13), rt in Omega(1 + n944_13)
append(gen_cons:nil13_13(n1348_13), gen_cons:nil13_13(b)) -> gen_cons:nil13_13(+(n1348_13, b)), rt in Omega(0)
ge(gen_0':s12_13(n2817_13), gen_0':s12_13(n2817_13)) -> true, rt in Omega(0)
APPEND(gen_cons:nil13_13(n3966_13)) -> gen_c9:c1015_13(n3966_13), rt in Omega(1 + n3966_13)


Generator Equations:
gen_c:c1:c211_13(0) <=> c
gen_c:c1:c211_13(+(x, 1)) <=> c2(gen_c:c1:c211_13(x))
gen_0':s12_13(0) <=> 0'
gen_0':s12_13(+(x, 1)) <=> s(gen_0':s12_13(x))
gen_cons:nil13_13(0) <=> nil
gen_cons:nil13_13(+(x, 1)) <=> cons(gen_cons:nil13_13(x))
gen_c11:c1214_13(0) <=> c11
gen_c11:c1214_13(+(x, 1)) <=> c12(gen_c11:c1214_13(x))
gen_c9:c1015_13(0) <=> c9
gen_c9:c1015_13(+(x, 1)) <=> c10(gen_c9:c1015_13(x))


The following defined symbols remain to be analysed:
help