WORST_CASE(Omega(n^1),?)
proof of input_AwErOl4jS8.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, 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), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 10 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 98.8 s]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 69 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 61 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 55 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 858 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 54 ms]
        (26) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   last(nil) -> 0
   last(cons(x, nil)) -> x
   last(cons(x, cons(y, xs))) -> last(cons(y, xs))
   del(x, nil) -> nil
   del(x, cons(y, xs)) -> if(eq(x, y), x, y, xs)
   if(true, x, y, xs) -> xs
   if(false, x, y, xs) -> cons(y, del(x, xs))
   eq(0, 0) -> true
   eq(0, s(y)) -> false
   eq(s(x), 0) -> false
   eq(s(x), s(y)) -> eq(x, y)
   reverse(nil) -> nil
   reverse(cons(x, xs)) -> cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))

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:
   last(nil) -> 0
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   reverse(nil) -> nil
   reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(z0, z1))))
Tuples:
   LAST(nil) -> c
   LAST(cons(z0, nil)) -> c1
   LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
   DEL(z0, nil) -> c3
   DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF(true, z0, z1, z2) -> c5
   IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
   EQ(0, 0) -> c7
   EQ(0, s(z0)) -> c8
   EQ(s(z0), 0) -> c9
   EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
   REVERSE(nil) -> c11
   REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
   REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
S tuples:
   LAST(nil) -> c
   LAST(cons(z0, nil)) -> c1
   LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
   DEL(z0, nil) -> c3
   DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF(true, z0, z1, z2) -> c5
   IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
   EQ(0, 0) -> c7
   EQ(0, s(z0)) -> c8
   EQ(s(z0), 0) -> c9
   EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
   REVERSE(nil) -> c11
   REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
   REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
K tuples:none
Defined Rule Symbols:   last_1, del_2, if_4, eq_2, reverse_1

Defined Pair Symbols:   LAST_1, DEL_2, IF_4, EQ_2, REVERSE_1

Compound Symbols:   c, c1, c2_1, c3, c4_2, c5, c6_1, c7, c8, c9, c10_1, c11, c12_1, c13_3


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

(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^1, INF).


The TRS R consists of the following rules:

   LAST(nil) -> c
   LAST(cons(z0, nil)) -> c1
   LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
   DEL(z0, nil) -> c3
   DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF(true, z0, z1, z2) -> c5
   IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
   EQ(0, 0) -> c7
   EQ(0, s(z0)) -> c8
   EQ(s(z0), 0) -> c9
   EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
   REVERSE(nil) -> c11
   REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
   REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))

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

   last(nil) -> 0
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   reverse(nil) -> nil
   reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(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^1, INF).


The TRS R consists of the following rules:

   LAST(nil) -> c
   LAST(cons(z0, nil)) -> c1
   LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
   DEL(z0, nil) -> c3
   DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF(true, z0, z1, z2) -> c5
   IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
   EQ(0', 0') -> c7
   EQ(0', s(z0)) -> c8
   EQ(s(z0), 0') -> c9
   EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
   REVERSE(nil) -> c11
   REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
   REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))

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

   last(nil) -> 0'
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   reverse(nil) -> nil
   reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(z0, z1))))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
LAST(nil) -> c
LAST(cons(z0, nil)) -> c1
LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
DEL(z0, nil) -> c3
DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF(true, z0, z1, z2) -> c5
IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
EQ(0', 0') -> c7
EQ(0', s(z0)) -> c8
EQ(s(z0), 0') -> c9
EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
REVERSE(nil) -> c11
REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
reverse(nil) -> nil
reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(z0, z1))))

Types:
LAST :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DEL :: 0':s -> nil:cons -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c7:c8:c9:c10 -> c3:c4
IF :: true:false -> 0':s -> 0':s -> nil:cons -> c5:c6
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c7:c8:c9:c10
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
0' :: 0':s
c7 :: c7:c8:c9:c10
s :: 0':s -> 0':s
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
REVERSE :: nil:cons -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c3:c4 -> c:c1:c2 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
last :: nil:cons -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
reverse :: nil:cons -> nil:cons
hole_c:c1:c21_14 :: c:c1:c2
hole_nil:cons2_14 :: nil:cons
hole_0':s3_14 :: 0':s
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c7:c8:c9:c106_14 :: c7:c8:c9:c10
hole_true:false7_14 :: true:false
hole_c11:c12:c138_14 :: c11:c12:c13
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_nil:cons10_14 :: Nat -> nil:cons
gen_0':s11_14 :: Nat -> 0':s
gen_c7:c8:c9:c1012_14 :: Nat -> c7:c8:c9:c10
gen_c11:c12:c1313_14 :: Nat -> c11:c12:c13

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LAST, DEL, eq, EQ, REVERSE, del, last, reverse

They will be analysed ascendingly in the following order:
LAST < REVERSE
eq < DEL
EQ < DEL
DEL < REVERSE
eq < del
del < REVERSE
last < REVERSE
del < reverse
last < reverse

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

(10)
Obligation:
Innermost TRS:
Rules:
LAST(nil) -> c
LAST(cons(z0, nil)) -> c1
LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
DEL(z0, nil) -> c3
DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF(true, z0, z1, z2) -> c5
IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
EQ(0', 0') -> c7
EQ(0', s(z0)) -> c8
EQ(s(z0), 0') -> c9
EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
REVERSE(nil) -> c11
REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
reverse(nil) -> nil
reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(z0, z1))))

Types:
LAST :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DEL :: 0':s -> nil:cons -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c7:c8:c9:c10 -> c3:c4
IF :: true:false -> 0':s -> 0':s -> nil:cons -> c5:c6
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c7:c8:c9:c10
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
0' :: 0':s
c7 :: c7:c8:c9:c10
s :: 0':s -> 0':s
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
REVERSE :: nil:cons -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c3:c4 -> c:c1:c2 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
last :: nil:cons -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
reverse :: nil:cons -> nil:cons
hole_c:c1:c21_14 :: c:c1:c2
hole_nil:cons2_14 :: nil:cons
hole_0':s3_14 :: 0':s
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c7:c8:c9:c106_14 :: c7:c8:c9:c10
hole_true:false7_14 :: true:false
hole_c11:c12:c138_14 :: c11:c12:c13
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_nil:cons10_14 :: Nat -> nil:cons
gen_0':s11_14 :: Nat -> 0':s
gen_c7:c8:c9:c1012_14 :: Nat -> c7:c8:c9:c10
gen_c11:c12:c1313_14 :: Nat -> c11:c12:c13


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_nil:cons10_14(0) <=> nil
gen_nil:cons10_14(+(x, 1)) <=> cons(0', gen_nil:cons10_14(x))
gen_0':s11_14(0) <=> 0'
gen_0':s11_14(+(x, 1)) <=> s(gen_0':s11_14(x))
gen_c7:c8:c9:c1012_14(0) <=> c7
gen_c7:c8:c9:c1012_14(+(x, 1)) <=> c10(gen_c7:c8:c9:c1012_14(x))
gen_c11:c12:c1313_14(0) <=> c11
gen_c11:c12:c1313_14(+(x, 1)) <=> c13(gen_c11:c12:c1313_14(x), c3, c)


The following defined symbols remain to be analysed:
LAST, DEL, eq, EQ, REVERSE, del, last, reverse

They will be analysed ascendingly in the following order:
LAST < REVERSE
eq < DEL
EQ < DEL
DEL < REVERSE
eq < del
del < REVERSE
last < REVERSE
del < reverse
last < reverse

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LAST(gen_nil:cons10_14(+(2, n15_14))) -> *14_14, rt in Omega(n15_14)

Induction Base:
LAST(gen_nil:cons10_14(+(2, 0)))

Induction Step:
LAST(gen_nil:cons10_14(+(2, +(n15_14, 1)))) ->_R^Omega(1)
c2(LAST(cons(0', gen_nil:cons10_14(+(1, n15_14))))) ->_IH
c2(*14_14)

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:
LAST(nil) -> c
LAST(cons(z0, nil)) -> c1
LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
DEL(z0, nil) -> c3
DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF(true, z0, z1, z2) -> c5
IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
EQ(0', 0') -> c7
EQ(0', s(z0)) -> c8
EQ(s(z0), 0') -> c9
EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
REVERSE(nil) -> c11
REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
reverse(nil) -> nil
reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(z0, z1))))

Types:
LAST :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DEL :: 0':s -> nil:cons -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c7:c8:c9:c10 -> c3:c4
IF :: true:false -> 0':s -> 0':s -> nil:cons -> c5:c6
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c7:c8:c9:c10
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
0' :: 0':s
c7 :: c7:c8:c9:c10
s :: 0':s -> 0':s
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
REVERSE :: nil:cons -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c3:c4 -> c:c1:c2 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
last :: nil:cons -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
reverse :: nil:cons -> nil:cons
hole_c:c1:c21_14 :: c:c1:c2
hole_nil:cons2_14 :: nil:cons
hole_0':s3_14 :: 0':s
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c7:c8:c9:c106_14 :: c7:c8:c9:c10
hole_true:false7_14 :: true:false
hole_c11:c12:c138_14 :: c11:c12:c13
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_nil:cons10_14 :: Nat -> nil:cons
gen_0':s11_14 :: Nat -> 0':s
gen_c7:c8:c9:c1012_14 :: Nat -> c7:c8:c9:c10
gen_c11:c12:c1313_14 :: Nat -> c11:c12:c13


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_nil:cons10_14(0) <=> nil
gen_nil:cons10_14(+(x, 1)) <=> cons(0', gen_nil:cons10_14(x))
gen_0':s11_14(0) <=> 0'
gen_0':s11_14(+(x, 1)) <=> s(gen_0':s11_14(x))
gen_c7:c8:c9:c1012_14(0) <=> c7
gen_c7:c8:c9:c1012_14(+(x, 1)) <=> c10(gen_c7:c8:c9:c1012_14(x))
gen_c11:c12:c1313_14(0) <=> c11
gen_c11:c12:c1313_14(+(x, 1)) <=> c13(gen_c11:c12:c1313_14(x), c3, c)


The following defined symbols remain to be analysed:
LAST, DEL, eq, EQ, REVERSE, del, last, reverse

They will be analysed ascendingly in the following order:
LAST < REVERSE
eq < DEL
EQ < DEL
DEL < REVERSE
eq < del
del < REVERSE
last < REVERSE
del < reverse
last < reverse

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
LAST(nil) -> c
LAST(cons(z0, nil)) -> c1
LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
DEL(z0, nil) -> c3
DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF(true, z0, z1, z2) -> c5
IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
EQ(0', 0') -> c7
EQ(0', s(z0)) -> c8
EQ(s(z0), 0') -> c9
EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
REVERSE(nil) -> c11
REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
reverse(nil) -> nil
reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(z0, z1))))

Types:
LAST :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DEL :: 0':s -> nil:cons -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c7:c8:c9:c10 -> c3:c4
IF :: true:false -> 0':s -> 0':s -> nil:cons -> c5:c6
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c7:c8:c9:c10
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
0' :: 0':s
c7 :: c7:c8:c9:c10
s :: 0':s -> 0':s
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
REVERSE :: nil:cons -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c3:c4 -> c:c1:c2 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
last :: nil:cons -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
reverse :: nil:cons -> nil:cons
hole_c:c1:c21_14 :: c:c1:c2
hole_nil:cons2_14 :: nil:cons
hole_0':s3_14 :: 0':s
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c7:c8:c9:c106_14 :: c7:c8:c9:c10
hole_true:false7_14 :: true:false
hole_c11:c12:c138_14 :: c11:c12:c13
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_nil:cons10_14 :: Nat -> nil:cons
gen_0':s11_14 :: Nat -> 0':s
gen_c7:c8:c9:c1012_14 :: Nat -> c7:c8:c9:c10
gen_c11:c12:c1313_14 :: Nat -> c11:c12:c13


Lemmas:
LAST(gen_nil:cons10_14(+(2, n15_14))) -> *14_14, rt in Omega(n15_14)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_nil:cons10_14(0) <=> nil
gen_nil:cons10_14(+(x, 1)) <=> cons(0', gen_nil:cons10_14(x))
gen_0':s11_14(0) <=> 0'
gen_0':s11_14(+(x, 1)) <=> s(gen_0':s11_14(x))
gen_c7:c8:c9:c1012_14(0) <=> c7
gen_c7:c8:c9:c1012_14(+(x, 1)) <=> c10(gen_c7:c8:c9:c1012_14(x))
gen_c11:c12:c1313_14(0) <=> c11
gen_c11:c12:c1313_14(+(x, 1)) <=> c13(gen_c11:c12:c1313_14(x), c3, c)


The following defined symbols remain to be analysed:
eq, DEL, EQ, REVERSE, del, last, reverse

They will be analysed ascendingly in the following order:
eq < DEL
EQ < DEL
DEL < REVERSE
eq < del
del < REVERSE
last < REVERSE
del < reverse
last < reverse

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eq(gen_0':s11_14(n73455_14), gen_0':s11_14(n73455_14)) -> true, rt in Omega(0)

Induction Base:
eq(gen_0':s11_14(0), gen_0':s11_14(0)) ->_R^Omega(0)
true

Induction Step:
eq(gen_0':s11_14(+(n73455_14, 1)), gen_0':s11_14(+(n73455_14, 1))) ->_R^Omega(0)
eq(gen_0':s11_14(n73455_14), gen_0':s11_14(n73455_14)) ->_IH
true

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:
LAST(nil) -> c
LAST(cons(z0, nil)) -> c1
LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
DEL(z0, nil) -> c3
DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF(true, z0, z1, z2) -> c5
IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
EQ(0', 0') -> c7
EQ(0', s(z0)) -> c8
EQ(s(z0), 0') -> c9
EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
REVERSE(nil) -> c11
REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
reverse(nil) -> nil
reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(z0, z1))))

Types:
LAST :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DEL :: 0':s -> nil:cons -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c7:c8:c9:c10 -> c3:c4
IF :: true:false -> 0':s -> 0':s -> nil:cons -> c5:c6
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c7:c8:c9:c10
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
0' :: 0':s
c7 :: c7:c8:c9:c10
s :: 0':s -> 0':s
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
REVERSE :: nil:cons -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c3:c4 -> c:c1:c2 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
last :: nil:cons -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
reverse :: nil:cons -> nil:cons
hole_c:c1:c21_14 :: c:c1:c2
hole_nil:cons2_14 :: nil:cons
hole_0':s3_14 :: 0':s
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c7:c8:c9:c106_14 :: c7:c8:c9:c10
hole_true:false7_14 :: true:false
hole_c11:c12:c138_14 :: c11:c12:c13
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_nil:cons10_14 :: Nat -> nil:cons
gen_0':s11_14 :: Nat -> 0':s
gen_c7:c8:c9:c1012_14 :: Nat -> c7:c8:c9:c10
gen_c11:c12:c1313_14 :: Nat -> c11:c12:c13


Lemmas:
LAST(gen_nil:cons10_14(+(2, n15_14))) -> *14_14, rt in Omega(n15_14)
eq(gen_0':s11_14(n73455_14), gen_0':s11_14(n73455_14)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_nil:cons10_14(0) <=> nil
gen_nil:cons10_14(+(x, 1)) <=> cons(0', gen_nil:cons10_14(x))
gen_0':s11_14(0) <=> 0'
gen_0':s11_14(+(x, 1)) <=> s(gen_0':s11_14(x))
gen_c7:c8:c9:c1012_14(0) <=> c7
gen_c7:c8:c9:c1012_14(+(x, 1)) <=> c10(gen_c7:c8:c9:c1012_14(x))
gen_c11:c12:c1313_14(0) <=> c11
gen_c11:c12:c1313_14(+(x, 1)) <=> c13(gen_c11:c12:c1313_14(x), c3, c)


The following defined symbols remain to be analysed:
EQ, DEL, REVERSE, del, last, reverse

They will be analysed ascendingly in the following order:
EQ < DEL
DEL < REVERSE
del < REVERSE
last < REVERSE
del < reverse
last < reverse

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s11_14(n74116_14), gen_0':s11_14(n74116_14)) -> gen_c7:c8:c9:c1012_14(n74116_14), rt in Omega(1 + n74116_14)

Induction Base:
EQ(gen_0':s11_14(0), gen_0':s11_14(0)) ->_R^Omega(1)
c7

Induction Step:
EQ(gen_0':s11_14(+(n74116_14, 1)), gen_0':s11_14(+(n74116_14, 1))) ->_R^Omega(1)
c10(EQ(gen_0':s11_14(n74116_14), gen_0':s11_14(n74116_14))) ->_IH
c10(gen_c7:c8:c9:c1012_14(c74117_14))

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:
LAST(nil) -> c
LAST(cons(z0, nil)) -> c1
LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
DEL(z0, nil) -> c3
DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF(true, z0, z1, z2) -> c5
IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
EQ(0', 0') -> c7
EQ(0', s(z0)) -> c8
EQ(s(z0), 0') -> c9
EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
REVERSE(nil) -> c11
REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
reverse(nil) -> nil
reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(z0, z1))))

Types:
LAST :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DEL :: 0':s -> nil:cons -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c7:c8:c9:c10 -> c3:c4
IF :: true:false -> 0':s -> 0':s -> nil:cons -> c5:c6
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c7:c8:c9:c10
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
0' :: 0':s
c7 :: c7:c8:c9:c10
s :: 0':s -> 0':s
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
REVERSE :: nil:cons -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c3:c4 -> c:c1:c2 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
last :: nil:cons -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
reverse :: nil:cons -> nil:cons
hole_c:c1:c21_14 :: c:c1:c2
hole_nil:cons2_14 :: nil:cons
hole_0':s3_14 :: 0':s
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c7:c8:c9:c106_14 :: c7:c8:c9:c10
hole_true:false7_14 :: true:false
hole_c11:c12:c138_14 :: c11:c12:c13
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_nil:cons10_14 :: Nat -> nil:cons
gen_0':s11_14 :: Nat -> 0':s
gen_c7:c8:c9:c1012_14 :: Nat -> c7:c8:c9:c10
gen_c11:c12:c1313_14 :: Nat -> c11:c12:c13


Lemmas:
LAST(gen_nil:cons10_14(+(2, n15_14))) -> *14_14, rt in Omega(n15_14)
eq(gen_0':s11_14(n73455_14), gen_0':s11_14(n73455_14)) -> true, rt in Omega(0)
EQ(gen_0':s11_14(n74116_14), gen_0':s11_14(n74116_14)) -> gen_c7:c8:c9:c1012_14(n74116_14), rt in Omega(1 + n74116_14)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_nil:cons10_14(0) <=> nil
gen_nil:cons10_14(+(x, 1)) <=> cons(0', gen_nil:cons10_14(x))
gen_0':s11_14(0) <=> 0'
gen_0':s11_14(+(x, 1)) <=> s(gen_0':s11_14(x))
gen_c7:c8:c9:c1012_14(0) <=> c7
gen_c7:c8:c9:c1012_14(+(x, 1)) <=> c10(gen_c7:c8:c9:c1012_14(x))
gen_c11:c12:c1313_14(0) <=> c11
gen_c11:c12:c1313_14(+(x, 1)) <=> c13(gen_c11:c12:c1313_14(x), c3, c)


The following defined symbols remain to be analysed:
DEL, REVERSE, del, last, reverse

They will be analysed ascendingly in the following order:
DEL < REVERSE
del < REVERSE
last < REVERSE
del < reverse
last < reverse

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
last(gen_nil:cons10_14(+(1, n76288_14))) -> gen_0':s11_14(0), rt in Omega(0)

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

Induction Step:
last(gen_nil:cons10_14(+(1, +(n76288_14, 1)))) ->_R^Omega(0)
last(cons(0', gen_nil:cons10_14(n76288_14))) ->_IH
gen_0':s11_14(0)

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:
LAST(nil) -> c
LAST(cons(z0, nil)) -> c1
LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
DEL(z0, nil) -> c3
DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF(true, z0, z1, z2) -> c5
IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
EQ(0', 0') -> c7
EQ(0', s(z0)) -> c8
EQ(s(z0), 0') -> c9
EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
REVERSE(nil) -> c11
REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
reverse(nil) -> nil
reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(z0, z1))))

Types:
LAST :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DEL :: 0':s -> nil:cons -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c7:c8:c9:c10 -> c3:c4
IF :: true:false -> 0':s -> 0':s -> nil:cons -> c5:c6
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c7:c8:c9:c10
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
0' :: 0':s
c7 :: c7:c8:c9:c10
s :: 0':s -> 0':s
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
REVERSE :: nil:cons -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c3:c4 -> c:c1:c2 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
last :: nil:cons -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
reverse :: nil:cons -> nil:cons
hole_c:c1:c21_14 :: c:c1:c2
hole_nil:cons2_14 :: nil:cons
hole_0':s3_14 :: 0':s
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c7:c8:c9:c106_14 :: c7:c8:c9:c10
hole_true:false7_14 :: true:false
hole_c11:c12:c138_14 :: c11:c12:c13
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_nil:cons10_14 :: Nat -> nil:cons
gen_0':s11_14 :: Nat -> 0':s
gen_c7:c8:c9:c1012_14 :: Nat -> c7:c8:c9:c10
gen_c11:c12:c1313_14 :: Nat -> c11:c12:c13


Lemmas:
LAST(gen_nil:cons10_14(+(2, n15_14))) -> *14_14, rt in Omega(n15_14)
eq(gen_0':s11_14(n73455_14), gen_0':s11_14(n73455_14)) -> true, rt in Omega(0)
EQ(gen_0':s11_14(n74116_14), gen_0':s11_14(n74116_14)) -> gen_c7:c8:c9:c1012_14(n74116_14), rt in Omega(1 + n74116_14)
last(gen_nil:cons10_14(+(1, n76288_14))) -> gen_0':s11_14(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_nil:cons10_14(0) <=> nil
gen_nil:cons10_14(+(x, 1)) <=> cons(0', gen_nil:cons10_14(x))
gen_0':s11_14(0) <=> 0'
gen_0':s11_14(+(x, 1)) <=> s(gen_0':s11_14(x))
gen_c7:c8:c9:c1012_14(0) <=> c7
gen_c7:c8:c9:c1012_14(+(x, 1)) <=> c10(gen_c7:c8:c9:c1012_14(x))
gen_c11:c12:c1313_14(0) <=> c11
gen_c11:c12:c1313_14(+(x, 1)) <=> c13(gen_c11:c12:c1313_14(x), c3, c)


The following defined symbols remain to be analysed:
REVERSE, reverse
----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REVERSE(gen_nil:cons10_14(n76868_14)) -> *14_14, rt in Omega(n76868_14)

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

Induction Step:
REVERSE(gen_nil:cons10_14(+(n76868_14, 1))) ->_R^Omega(1)
c13(REVERSE(del(last(cons(0', gen_nil:cons10_14(n76868_14))), cons(0', gen_nil:cons10_14(n76868_14)))), DEL(last(cons(0', gen_nil:cons10_14(n76868_14))), cons(0', gen_nil:cons10_14(n76868_14))), LAST(cons(0', gen_nil:cons10_14(n76868_14)))) ->_L^Omega(0)
c13(REVERSE(del(gen_0':s11_14(0), cons(0', gen_nil:cons10_14(n76868_14)))), DEL(last(cons(0', gen_nil:cons10_14(n76868_14))), cons(0', gen_nil:cons10_14(n76868_14))), LAST(cons(0', gen_nil:cons10_14(n76868_14)))) ->_R^Omega(0)
c13(REVERSE(if(eq(gen_0':s11_14(0), 0'), gen_0':s11_14(0), 0', gen_nil:cons10_14(n76868_14))), DEL(last(cons(0', gen_nil:cons10_14(n76868_14))), cons(0', gen_nil:cons10_14(n76868_14))), LAST(cons(0', gen_nil:cons10_14(n76868_14)))) ->_L^Omega(0)
c13(REVERSE(if(true, gen_0':s11_14(0), 0', gen_nil:cons10_14(n76868_14))), DEL(last(cons(0', gen_nil:cons10_14(n76868_14))), cons(0', gen_nil:cons10_14(n76868_14))), LAST(cons(0', gen_nil:cons10_14(n76868_14)))) ->_R^Omega(0)
c13(REVERSE(gen_nil:cons10_14(n76868_14)), DEL(last(cons(0', gen_nil:cons10_14(n76868_14))), cons(0', gen_nil:cons10_14(n76868_14))), LAST(cons(0', gen_nil:cons10_14(n76868_14)))) ->_IH
c13(*14_14, DEL(last(cons(0', gen_nil:cons10_14(n76868_14))), cons(0', gen_nil:cons10_14(n76868_14))), LAST(cons(0', gen_nil:cons10_14(n76868_14)))) ->_L^Omega(0)
c13(*14_14, DEL(gen_0':s11_14(0), cons(0', gen_nil:cons10_14(n76868_14))), LAST(cons(0', gen_nil:cons10_14(n76868_14)))) ->_R^Omega(1)
c13(*14_14, c4(IF(eq(gen_0':s11_14(0), 0'), gen_0':s11_14(0), 0', gen_nil:cons10_14(n76868_14)), EQ(gen_0':s11_14(0), 0')), LAST(cons(0', gen_nil:cons10_14(n76868_14)))) ->_L^Omega(0)
c13(*14_14, c4(IF(true, gen_0':s11_14(0), 0', gen_nil:cons10_14(n76868_14)), EQ(gen_0':s11_14(0), 0')), LAST(cons(0', gen_nil:cons10_14(n76868_14)))) ->_R^Omega(1)
c13(*14_14, c4(c5, EQ(gen_0':s11_14(0), 0')), LAST(cons(0', gen_nil:cons10_14(n76868_14)))) ->_L^Omega(1)
c13(*14_14, c4(c5, gen_c7:c8:c9:c1012_14(0)), LAST(cons(0', gen_nil:cons10_14(n76868_14))))

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

(24)
Obligation:
Innermost TRS:
Rules:
LAST(nil) -> c
LAST(cons(z0, nil)) -> c1
LAST(cons(z0, cons(z1, z2))) -> c2(LAST(cons(z1, z2)))
DEL(z0, nil) -> c3
DEL(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF(true, z0, z1, z2) -> c5
IF(false, z0, z1, z2) -> c6(DEL(z0, z2))
EQ(0', 0') -> c7
EQ(0', s(z0)) -> c8
EQ(s(z0), 0') -> c9
EQ(s(z0), s(z1)) -> c10(EQ(z0, z1))
REVERSE(nil) -> c11
REVERSE(cons(z0, z1)) -> c12(LAST(cons(z0, z1)))
REVERSE(cons(z0, z1)) -> c13(REVERSE(del(last(cons(z0, z1)), cons(z0, z1))), DEL(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
reverse(nil) -> nil
reverse(cons(z0, z1)) -> cons(last(cons(z0, z1)), reverse(del(last(cons(z0, z1)), cons(z0, z1))))

Types:
LAST :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DEL :: 0':s -> nil:cons -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c7:c8:c9:c10 -> c3:c4
IF :: true:false -> 0':s -> 0':s -> nil:cons -> c5:c6
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c7:c8:c9:c10
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
0' :: 0':s
c7 :: c7:c8:c9:c10
s :: 0':s -> 0':s
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
REVERSE :: nil:cons -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c3:c4 -> c:c1:c2 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
last :: nil:cons -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
reverse :: nil:cons -> nil:cons
hole_c:c1:c21_14 :: c:c1:c2
hole_nil:cons2_14 :: nil:cons
hole_0':s3_14 :: 0':s
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c7:c8:c9:c106_14 :: c7:c8:c9:c10
hole_true:false7_14 :: true:false
hole_c11:c12:c138_14 :: c11:c12:c13
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_nil:cons10_14 :: Nat -> nil:cons
gen_0':s11_14 :: Nat -> 0':s
gen_c7:c8:c9:c1012_14 :: Nat -> c7:c8:c9:c10
gen_c11:c12:c1313_14 :: Nat -> c11:c12:c13


Lemmas:
LAST(gen_nil:cons10_14(+(2, n15_14))) -> *14_14, rt in Omega(n15_14)
eq(gen_0':s11_14(n73455_14), gen_0':s11_14(n73455_14)) -> true, rt in Omega(0)
EQ(gen_0':s11_14(n74116_14), gen_0':s11_14(n74116_14)) -> gen_c7:c8:c9:c1012_14(n74116_14), rt in Omega(1 + n74116_14)
last(gen_nil:cons10_14(+(1, n76288_14))) -> gen_0':s11_14(0), rt in Omega(0)
REVERSE(gen_nil:cons10_14(n76868_14)) -> *14_14, rt in Omega(n76868_14)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_nil:cons10_14(0) <=> nil
gen_nil:cons10_14(+(x, 1)) <=> cons(0', gen_nil:cons10_14(x))
gen_0':s11_14(0) <=> 0'
gen_0':s11_14(+(x, 1)) <=> s(gen_0':s11_14(x))
gen_c7:c8:c9:c1012_14(0) <=> c7
gen_c7:c8:c9:c1012_14(+(x, 1)) <=> c10(gen_c7:c8:c9:c1012_14(x))
gen_c11:c12:c1313_14(0) <=> c11
gen_c11:c12:c1313_14(+(x, 1)) <=> c13(gen_c11:c12:c1313_14(x), c3, c)


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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
reverse(gen_nil:cons10_14(n85565_14)) -> gen_nil:cons10_14(n85565_14), rt in Omega(0)

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

Induction Step:
reverse(gen_nil:cons10_14(+(n85565_14, 1))) ->_R^Omega(0)
cons(last(cons(0', gen_nil:cons10_14(n85565_14))), reverse(del(last(cons(0', gen_nil:cons10_14(n85565_14))), cons(0', gen_nil:cons10_14(n85565_14))))) ->_L^Omega(0)
cons(gen_0':s11_14(0), reverse(del(last(cons(0', gen_nil:cons10_14(n85565_14))), cons(0', gen_nil:cons10_14(n85565_14))))) ->_L^Omega(0)
cons(gen_0':s11_14(0), reverse(del(gen_0':s11_14(0), cons(0', gen_nil:cons10_14(n85565_14))))) ->_R^Omega(0)
cons(gen_0':s11_14(0), reverse(if(eq(gen_0':s11_14(0), 0'), gen_0':s11_14(0), 0', gen_nil:cons10_14(n85565_14)))) ->_L^Omega(0)
cons(gen_0':s11_14(0), reverse(if(true, gen_0':s11_14(0), 0', gen_nil:cons10_14(n85565_14)))) ->_R^Omega(0)
cons(gen_0':s11_14(0), reverse(gen_nil:cons10_14(n85565_14))) ->_IH
cons(gen_0':s11_14(0), gen_nil:cons10_14(c85566_14))

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

(26)
BOUNDS(1, INF)