WORST_CASE(Omega(n^2),?)
proof of input_SUsDiiQbpO.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), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 1 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 367 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 219 ms]
(14) BEST
    (15) proven lower bound
        (16) LowerBoundPropagationProof [FINISHED, 0 ms]
        (17) BOUNDS(n^1, INF)
    (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 730 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 43 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 123 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 80 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 1058 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), 94 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:

   max(nil) -> 0
   max(cons(x, nil)) -> x
   max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs)
   if1(true, x, y, xs) -> max(cons(x, xs))
   if1(false, x, y, xs) -> max(cons(y, xs))
   del(x, nil) -> nil
   del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs)
   if2(true, x, y, xs) -> xs
   if2(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)
   sort(nil) -> nil
   sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
   ge(0, 0) -> true
   ge(s(x), 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)

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:
   max(nil) -> 0
   max(cons(z0, nil)) -> z0
   max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> max(cons(z0, z2))
   if1(false, z0, z1, z2) -> max(cons(z1, z2))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
   if2(true, z0, z1, z2) -> z2
   if2(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)
   sort(nil) -> nil
   sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
   ge(0, 0) -> true
   ge(s(z0), 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
Tuples:
   MAX(nil) -> c
   MAX(cons(z0, nil)) -> c1
   MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
   IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
   DEL(z0, nil) -> c5
   DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF2(true, z0, z1, z2) -> c7
   IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
   EQ(0, 0) -> c9
   EQ(0, s(z0)) -> c10
   EQ(s(z0), 0) -> c11
   EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
   SORT(nil) -> c13
   SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
   SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
   GE(0, 0) -> c16
   GE(s(z0), 0) -> c17
   GE(0, s(z0)) -> c18
   GE(s(z0), s(z1)) -> c19(GE(z0, z1))
S tuples:
   MAX(nil) -> c
   MAX(cons(z0, nil)) -> c1
   MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
   IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
   DEL(z0, nil) -> c5
   DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF2(true, z0, z1, z2) -> c7
   IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
   EQ(0, 0) -> c9
   EQ(0, s(z0)) -> c10
   EQ(s(z0), 0) -> c11
   EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
   SORT(nil) -> c13
   SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
   SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
   GE(0, 0) -> c16
   GE(s(z0), 0) -> c17
   GE(0, s(z0)) -> c18
   GE(s(z0), s(z1)) -> c19(GE(z0, z1))
K tuples:none
Defined Rule Symbols:   max_1, if1_4, del_2, if2_4, eq_2, sort_1, ge_2

Defined Pair Symbols:   MAX_1, IF1_4, DEL_2, IF2_4, EQ_2, SORT_1, GE_2

Compound Symbols:   c, c1, c2_2, c3_1, c4_1, c5, c6_2, c7, c8_1, c9, c10, c11, c12_1, c13, c14_1, c15_3, c16, c17, c18, c19_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:

   MAX(nil) -> c
   MAX(cons(z0, nil)) -> c1
   MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
   IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
   DEL(z0, nil) -> c5
   DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF2(true, z0, z1, z2) -> c7
   IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
   EQ(0, 0) -> c9
   EQ(0, s(z0)) -> c10
   EQ(s(z0), 0) -> c11
   EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
   SORT(nil) -> c13
   SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
   SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
   GE(0, 0) -> c16
   GE(s(z0), 0) -> c17
   GE(0, s(z0)) -> c18
   GE(s(z0), s(z1)) -> c19(GE(z0, z1))

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

   max(nil) -> 0
   max(cons(z0, nil)) -> z0
   max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> max(cons(z0, z2))
   if1(false, z0, z1, z2) -> max(cons(z1, z2))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
   if2(true, z0, z1, z2) -> z2
   if2(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)
   sort(nil) -> nil
   sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
   ge(0, 0) -> true
   ge(s(z0), 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(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:

   MAX(nil) -> c
   MAX(cons(z0, nil)) -> c1
   MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
   IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
   DEL(z0, nil) -> c5
   DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF2(true, z0, z1, z2) -> c7
   IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
   EQ(0', 0') -> c9
   EQ(0', s(z0)) -> c10
   EQ(s(z0), 0') -> c11
   EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
   SORT(nil) -> c13
   SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
   SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
   GE(0', 0') -> c16
   GE(s(z0), 0') -> c17
   GE(0', s(z0)) -> c18
   GE(s(z0), s(z1)) -> c19(GE(z0, z1))

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

   max(nil) -> 0'
   max(cons(z0, nil)) -> z0
   max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> max(cons(z0, z2))
   if1(false, z0, z1, z2) -> max(cons(z1, z2))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
   if2(true, z0, z1, z2) -> z2
   if2(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)
   sort(nil) -> nil
   sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
   ge(0', 0') -> true
   ge(s(z0), 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)

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

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

(8)
Obligation:
Innermost TRS:
Rules:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MAX, ge, GE, DEL, eq, EQ, SORT, del, max, sort

They will be analysed ascendingly in the following order:
ge < MAX
GE < MAX
MAX < SORT
ge < max
eq < DEL
EQ < DEL
DEL < SORT
eq < del
del < SORT
max < SORT
del < sort
max < sort

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

(10)
Obligation:
Innermost TRS:
Rules:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15


Generator Equations:
gen_nil:cons11_20(0) <=> nil
gen_nil:cons11_20(+(x, 1)) <=> cons(0', gen_nil:cons11_20(x))
gen_0':s12_20(0) <=> 0'
gen_0':s12_20(+(x, 1)) <=> s(gen_0':s12_20(x))
gen_c16:c17:c18:c1913_20(0) <=> c16
gen_c16:c17:c18:c1913_20(+(x, 1)) <=> c19(gen_c16:c17:c18:c1913_20(x))
gen_c9:c10:c11:c1214_20(0) <=> c9
gen_c9:c10:c11:c1214_20(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_20(x))
gen_c13:c14:c1515_20(0) <=> c13
gen_c13:c14:c1515_20(+(x, 1)) <=> c15(gen_c13:c14:c1515_20(x), c5, c)


The following defined symbols remain to be analysed:
ge, MAX, GE, DEL, eq, EQ, SORT, del, max, sort

They will be analysed ascendingly in the following order:
ge < MAX
GE < MAX
MAX < SORT
ge < max
eq < DEL
EQ < DEL
DEL < SORT
eq < del
del < SORT
max < SORT
del < sort
max < sort

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s12_20(n17_20), gen_0':s12_20(n17_20)) -> true, rt in Omega(0)

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

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

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

(12)
Obligation:
Innermost TRS:
Rules:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_20(n17_20), gen_0':s12_20(n17_20)) -> true, rt in Omega(0)


Generator Equations:
gen_nil:cons11_20(0) <=> nil
gen_nil:cons11_20(+(x, 1)) <=> cons(0', gen_nil:cons11_20(x))
gen_0':s12_20(0) <=> 0'
gen_0':s12_20(+(x, 1)) <=> s(gen_0':s12_20(x))
gen_c16:c17:c18:c1913_20(0) <=> c16
gen_c16:c17:c18:c1913_20(+(x, 1)) <=> c19(gen_c16:c17:c18:c1913_20(x))
gen_c9:c10:c11:c1214_20(0) <=> c9
gen_c9:c10:c11:c1214_20(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_20(x))
gen_c13:c14:c1515_20(0) <=> c13
gen_c13:c14:c1515_20(+(x, 1)) <=> c15(gen_c13:c14:c1515_20(x), c5, c)


The following defined symbols remain to be analysed:
GE, MAX, DEL, eq, EQ, SORT, del, max, sort

They will be analysed ascendingly in the following order:
GE < MAX
MAX < SORT
eq < DEL
EQ < DEL
DEL < SORT
eq < del
del < SORT
max < SORT
del < sort
max < sort

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s12_20(n696_20), gen_0':s12_20(n696_20)) -> gen_c16:c17:c18:c1913_20(n696_20), rt in Omega(1 + n696_20)

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

Induction Step:
GE(gen_0':s12_20(+(n696_20, 1)), gen_0':s12_20(+(n696_20, 1))) ->_R^Omega(1)
c19(GE(gen_0':s12_20(n696_20), gen_0':s12_20(n696_20))) ->_IH
c19(gen_c16:c17:c18:c1913_20(c697_20))

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

(14)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_20(n17_20), gen_0':s12_20(n17_20)) -> true, rt in Omega(0)


Generator Equations:
gen_nil:cons11_20(0) <=> nil
gen_nil:cons11_20(+(x, 1)) <=> cons(0', gen_nil:cons11_20(x))
gen_0':s12_20(0) <=> 0'
gen_0':s12_20(+(x, 1)) <=> s(gen_0':s12_20(x))
gen_c16:c17:c18:c1913_20(0) <=> c16
gen_c16:c17:c18:c1913_20(+(x, 1)) <=> c19(gen_c16:c17:c18:c1913_20(x))
gen_c9:c10:c11:c1214_20(0) <=> c9
gen_c9:c10:c11:c1214_20(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_20(x))
gen_c13:c14:c1515_20(0) <=> c13
gen_c13:c14:c1515_20(+(x, 1)) <=> c15(gen_c13:c14:c1515_20(x), c5, c)


The following defined symbols remain to be analysed:
GE, MAX, DEL, eq, EQ, SORT, del, max, sort

They will be analysed ascendingly in the following order:
GE < MAX
MAX < SORT
eq < DEL
EQ < DEL
DEL < SORT
eq < del
del < SORT
max < SORT
del < sort
max < sort

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_20(n17_20), gen_0':s12_20(n17_20)) -> true, rt in Omega(0)
GE(gen_0':s12_20(n696_20), gen_0':s12_20(n696_20)) -> gen_c16:c17:c18:c1913_20(n696_20), rt in Omega(1 + n696_20)


Generator Equations:
gen_nil:cons11_20(0) <=> nil
gen_nil:cons11_20(+(x, 1)) <=> cons(0', gen_nil:cons11_20(x))
gen_0':s12_20(0) <=> 0'
gen_0':s12_20(+(x, 1)) <=> s(gen_0':s12_20(x))
gen_c16:c17:c18:c1913_20(0) <=> c16
gen_c16:c17:c18:c1913_20(+(x, 1)) <=> c19(gen_c16:c17:c18:c1913_20(x))
gen_c9:c10:c11:c1214_20(0) <=> c9
gen_c9:c10:c11:c1214_20(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_20(x))
gen_c13:c14:c1515_20(0) <=> c13
gen_c13:c14:c1515_20(+(x, 1)) <=> c15(gen_c13:c14:c1515_20(x), c5, c)


The following defined symbols remain to be analysed:
MAX, DEL, eq, EQ, SORT, del, max, sort

They will be analysed ascendingly in the following order:
MAX < SORT
eq < DEL
EQ < DEL
DEL < SORT
eq < del
del < SORT
max < SORT
del < sort
max < sort

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MAX(gen_nil:cons11_20(+(1, n1791_20))) -> *16_20, rt in Omega(n1791_20)

Induction Base:
MAX(gen_nil:cons11_20(+(1, 0)))

Induction Step:
MAX(gen_nil:cons11_20(+(1, +(n1791_20, 1)))) ->_R^Omega(1)
c2(IF1(ge(0', 0'), 0', 0', gen_nil:cons11_20(n1791_20)), GE(0', 0')) ->_L^Omega(0)
c2(IF1(true, 0', 0', gen_nil:cons11_20(n1791_20)), GE(0', 0')) ->_R^Omega(1)
c2(c3(MAX(cons(0', gen_nil:cons11_20(n1791_20)))), GE(0', 0')) ->_IH
c2(c3(*16_20), GE(0', 0')) ->_L^Omega(1)
c2(c3(*16_20), gen_c16:c17:c18:c1913_20(0))

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:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_20(n17_20), gen_0':s12_20(n17_20)) -> true, rt in Omega(0)
GE(gen_0':s12_20(n696_20), gen_0':s12_20(n696_20)) -> gen_c16:c17:c18:c1913_20(n696_20), rt in Omega(1 + n696_20)
MAX(gen_nil:cons11_20(+(1, n1791_20))) -> *16_20, rt in Omega(n1791_20)


Generator Equations:
gen_nil:cons11_20(0) <=> nil
gen_nil:cons11_20(+(x, 1)) <=> cons(0', gen_nil:cons11_20(x))
gen_0':s12_20(0) <=> 0'
gen_0':s12_20(+(x, 1)) <=> s(gen_0':s12_20(x))
gen_c16:c17:c18:c1913_20(0) <=> c16
gen_c16:c17:c18:c1913_20(+(x, 1)) <=> c19(gen_c16:c17:c18:c1913_20(x))
gen_c9:c10:c11:c1214_20(0) <=> c9
gen_c9:c10:c11:c1214_20(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_20(x))
gen_c13:c14:c1515_20(0) <=> c13
gen_c13:c14:c1515_20(+(x, 1)) <=> c15(gen_c13:c14:c1515_20(x), c5, c)


The following defined symbols remain to be analysed:
eq, DEL, EQ, SORT, del, max, sort

They will be analysed ascendingly in the following order:
eq < DEL
EQ < DEL
DEL < SORT
eq < del
del < SORT
max < SORT
del < sort
max < sort

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eq(gen_0':s12_20(n7343_20), gen_0':s12_20(n7343_20)) -> true, rt in Omega(0)

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

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

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:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_20(n17_20), gen_0':s12_20(n17_20)) -> true, rt in Omega(0)
GE(gen_0':s12_20(n696_20), gen_0':s12_20(n696_20)) -> gen_c16:c17:c18:c1913_20(n696_20), rt in Omega(1 + n696_20)
MAX(gen_nil:cons11_20(+(1, n1791_20))) -> *16_20, rt in Omega(n1791_20)
eq(gen_0':s12_20(n7343_20), gen_0':s12_20(n7343_20)) -> true, rt in Omega(0)


Generator Equations:
gen_nil:cons11_20(0) <=> nil
gen_nil:cons11_20(+(x, 1)) <=> cons(0', gen_nil:cons11_20(x))
gen_0':s12_20(0) <=> 0'
gen_0':s12_20(+(x, 1)) <=> s(gen_0':s12_20(x))
gen_c16:c17:c18:c1913_20(0) <=> c16
gen_c16:c17:c18:c1913_20(+(x, 1)) <=> c19(gen_c16:c17:c18:c1913_20(x))
gen_c9:c10:c11:c1214_20(0) <=> c9
gen_c9:c10:c11:c1214_20(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_20(x))
gen_c13:c14:c1515_20(0) <=> c13
gen_c13:c14:c1515_20(+(x, 1)) <=> c15(gen_c13:c14:c1515_20(x), c5, c)


The following defined symbols remain to be analysed:
EQ, DEL, SORT, del, max, sort

They will be analysed ascendingly in the following order:
EQ < DEL
DEL < SORT
del < SORT
max < SORT
del < sort
max < sort

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s12_20(n8100_20), gen_0':s12_20(n8100_20)) -> gen_c9:c10:c11:c1214_20(n8100_20), rt in Omega(1 + n8100_20)

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

Induction Step:
EQ(gen_0':s12_20(+(n8100_20, 1)), gen_0':s12_20(+(n8100_20, 1))) ->_R^Omega(1)
c12(EQ(gen_0':s12_20(n8100_20), gen_0':s12_20(n8100_20))) ->_IH
c12(gen_c9:c10:c11:c1214_20(c8101_20))

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:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_20(n17_20), gen_0':s12_20(n17_20)) -> true, rt in Omega(0)
GE(gen_0':s12_20(n696_20), gen_0':s12_20(n696_20)) -> gen_c16:c17:c18:c1913_20(n696_20), rt in Omega(1 + n696_20)
MAX(gen_nil:cons11_20(+(1, n1791_20))) -> *16_20, rt in Omega(n1791_20)
eq(gen_0':s12_20(n7343_20), gen_0':s12_20(n7343_20)) -> true, rt in Omega(0)
EQ(gen_0':s12_20(n8100_20), gen_0':s12_20(n8100_20)) -> gen_c9:c10:c11:c1214_20(n8100_20), rt in Omega(1 + n8100_20)


Generator Equations:
gen_nil:cons11_20(0) <=> nil
gen_nil:cons11_20(+(x, 1)) <=> cons(0', gen_nil:cons11_20(x))
gen_0':s12_20(0) <=> 0'
gen_0':s12_20(+(x, 1)) <=> s(gen_0':s12_20(x))
gen_c16:c17:c18:c1913_20(0) <=> c16
gen_c16:c17:c18:c1913_20(+(x, 1)) <=> c19(gen_c16:c17:c18:c1913_20(x))
gen_c9:c10:c11:c1214_20(0) <=> c9
gen_c9:c10:c11:c1214_20(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_20(x))
gen_c13:c14:c1515_20(0) <=> c13
gen_c13:c14:c1515_20(+(x, 1)) <=> c15(gen_c13:c14:c1515_20(x), c5, c)


The following defined symbols remain to be analysed:
DEL, SORT, del, max, sort

They will be analysed ascendingly in the following order:
DEL < SORT
del < SORT
max < SORT
del < sort
max < sort

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
max(gen_nil:cons11_20(+(1, n10382_20))) -> gen_0':s12_20(0), rt in Omega(0)

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

Induction Step:
max(gen_nil:cons11_20(+(1, +(n10382_20, 1)))) ->_R^Omega(0)
if1(ge(0', 0'), 0', 0', gen_nil:cons11_20(n10382_20)) ->_L^Omega(0)
if1(true, 0', 0', gen_nil:cons11_20(n10382_20)) ->_R^Omega(0)
max(cons(0', gen_nil:cons11_20(n10382_20))) ->_IH
gen_0':s12_20(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:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_20(n17_20), gen_0':s12_20(n17_20)) -> true, rt in Omega(0)
GE(gen_0':s12_20(n696_20), gen_0':s12_20(n696_20)) -> gen_c16:c17:c18:c1913_20(n696_20), rt in Omega(1 + n696_20)
MAX(gen_nil:cons11_20(+(1, n1791_20))) -> *16_20, rt in Omega(n1791_20)
eq(gen_0':s12_20(n7343_20), gen_0':s12_20(n7343_20)) -> true, rt in Omega(0)
EQ(gen_0':s12_20(n8100_20), gen_0':s12_20(n8100_20)) -> gen_c9:c10:c11:c1214_20(n8100_20), rt in Omega(1 + n8100_20)
max(gen_nil:cons11_20(+(1, n10382_20))) -> gen_0':s12_20(0), rt in Omega(0)


Generator Equations:
gen_nil:cons11_20(0) <=> nil
gen_nil:cons11_20(+(x, 1)) <=> cons(0', gen_nil:cons11_20(x))
gen_0':s12_20(0) <=> 0'
gen_0':s12_20(+(x, 1)) <=> s(gen_0':s12_20(x))
gen_c16:c17:c18:c1913_20(0) <=> c16
gen_c16:c17:c18:c1913_20(+(x, 1)) <=> c19(gen_c16:c17:c18:c1913_20(x))
gen_c9:c10:c11:c1214_20(0) <=> c9
gen_c9:c10:c11:c1214_20(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_20(x))
gen_c13:c14:c1515_20(0) <=> c13
gen_c13:c14:c1515_20(+(x, 1)) <=> c15(gen_c13:c14:c1515_20(x), c5, c)


The following defined symbols remain to be analysed:
SORT, sort
----------------------------------------

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SORT(gen_nil:cons11_20(n11241_20)) -> *16_20, rt in Omega(n11241_20 + n11241_20^2)

Induction Base:
SORT(gen_nil:cons11_20(0))

Induction Step:
SORT(gen_nil:cons11_20(+(n11241_20, 1))) ->_R^Omega(1)
c15(SORT(del(max(cons(0', gen_nil:cons11_20(n11241_20))), cons(0', gen_nil:cons11_20(n11241_20)))), DEL(max(cons(0', gen_nil:cons11_20(n11241_20))), cons(0', gen_nil:cons11_20(n11241_20))), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_L^Omega(0)
c15(SORT(del(gen_0':s12_20(0), cons(0', gen_nil:cons11_20(n11241_20)))), DEL(max(cons(0', gen_nil:cons11_20(n11241_20))), cons(0', gen_nil:cons11_20(n11241_20))), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_R^Omega(0)
c15(SORT(if2(eq(gen_0':s12_20(0), 0'), gen_0':s12_20(0), 0', gen_nil:cons11_20(n11241_20))), DEL(max(cons(0', gen_nil:cons11_20(n11241_20))), cons(0', gen_nil:cons11_20(n11241_20))), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_L^Omega(0)
c15(SORT(if2(true, gen_0':s12_20(0), 0', gen_nil:cons11_20(n11241_20))), DEL(max(cons(0', gen_nil:cons11_20(n11241_20))), cons(0', gen_nil:cons11_20(n11241_20))), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_R^Omega(0)
c15(SORT(gen_nil:cons11_20(n11241_20)), DEL(max(cons(0', gen_nil:cons11_20(n11241_20))), cons(0', gen_nil:cons11_20(n11241_20))), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_IH
c15(*16_20, DEL(max(cons(0', gen_nil:cons11_20(n11241_20))), cons(0', gen_nil:cons11_20(n11241_20))), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_L^Omega(0)
c15(*16_20, DEL(gen_0':s12_20(0), cons(0', gen_nil:cons11_20(n11241_20))), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_R^Omega(1)
c15(*16_20, c6(IF2(eq(gen_0':s12_20(0), 0'), gen_0':s12_20(0), 0', gen_nil:cons11_20(n11241_20)), EQ(gen_0':s12_20(0), 0')), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_L^Omega(0)
c15(*16_20, c6(IF2(true, gen_0':s12_20(0), 0', gen_nil:cons11_20(n11241_20)), EQ(gen_0':s12_20(0), 0')), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_R^Omega(1)
c15(*16_20, c6(c7, EQ(gen_0':s12_20(0), 0')), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_L^Omega(1)
c15(*16_20, c6(c7, gen_c9:c10:c11:c1214_20(0)), MAX(cons(0', gen_nil:cons11_20(n11241_20)))) ->_L^Omega(n11241_20)
c15(*16_20, c6(c7, gen_c9:c10:c11:c1214_20(0)), *16_20)

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:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_20(n17_20), gen_0':s12_20(n17_20)) -> true, rt in Omega(0)
GE(gen_0':s12_20(n696_20), gen_0':s12_20(n696_20)) -> gen_c16:c17:c18:c1913_20(n696_20), rt in Omega(1 + n696_20)
MAX(gen_nil:cons11_20(+(1, n1791_20))) -> *16_20, rt in Omega(n1791_20)
eq(gen_0':s12_20(n7343_20), gen_0':s12_20(n7343_20)) -> true, rt in Omega(0)
EQ(gen_0':s12_20(n8100_20), gen_0':s12_20(n8100_20)) -> gen_c9:c10:c11:c1214_20(n8100_20), rt in Omega(1 + n8100_20)
max(gen_nil:cons11_20(+(1, n10382_20))) -> gen_0':s12_20(0), rt in Omega(0)


Generator Equations:
gen_nil:cons11_20(0) <=> nil
gen_nil:cons11_20(+(x, 1)) <=> cons(0', gen_nil:cons11_20(x))
gen_0':s12_20(0) <=> 0'
gen_0':s12_20(+(x, 1)) <=> s(gen_0':s12_20(x))
gen_c16:c17:c18:c1913_20(0) <=> c16
gen_c16:c17:c18:c1913_20(+(x, 1)) <=> c19(gen_c16:c17:c18:c1913_20(x))
gen_c9:c10:c11:c1214_20(0) <=> c9
gen_c9:c10:c11:c1214_20(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_20(x))
gen_c13:c14:c1515_20(0) <=> c13
gen_c13:c14:c1515_20(+(x, 1)) <=> c15(gen_c13:c14:c1515_20(x), c5, c)


The following defined symbols remain to be analysed:
SORT, sort
----------------------------------------

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

(31)
BOUNDS(n^2, INF)

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

(32)
Obligation:
Innermost TRS:
Rules:
MAX(nil) -> c
MAX(cons(z0, nil)) -> c1
MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2)))
DEL(z0, nil) -> c5
DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
IF2(true, z0, z1, z2) -> c7
IF2(false, z0, z1, z2) -> c8(DEL(z0, z2))
EQ(0', 0') -> c9
EQ(0', s(z0)) -> c10
EQ(s(z0), 0') -> c11
EQ(s(z0), s(z1)) -> c12(EQ(z0, z1))
SORT(nil) -> c13
SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1)))
SORT(cons(z0, z1)) -> c15(SORT(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1)))
GE(0', 0') -> c16
GE(s(z0), 0') -> c17
GE(0', s(z0)) -> c18
GE(s(z0), s(z1)) -> c19(GE(z0, z1))
max(nil) -> 0'
max(cons(z0, nil)) -> z0
max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> max(cons(z0, z2))
if1(false, z0, z1, z2) -> max(cons(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> z2
if2(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)
sort(nil) -> nil
sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(del(max(cons(z0, z1)), cons(z0, z1))))
ge(0', 0') -> true
ge(s(z0), 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
MAX :: nil:cons -> c:c1:c2
nil :: nil:cons
c :: c:c1:c2
cons :: 0':s -> nil:cons -> nil:cons
c1 :: c:c1:c2
c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c16:c17:c18:c19
true :: true:false
c3 :: c:c1:c2 -> c3:c4
false :: true:false
c4 :: c:c1:c2 -> c3:c4
DEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c9:c10:c11:c12
c7 :: c7:c8
c8 :: c5:c6 -> c7:c8
0' :: 0':s
c9 :: c9:c10:c11:c12
s :: 0':s -> 0':s
c10 :: c9:c10:c11:c12
c11 :: c9:c10:c11:c12
c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12
SORT :: nil:cons -> c13:c14:c15
c13 :: c13:c14:c15
c14 :: c:c1:c2 -> c13:c14:c15
c15 :: c13:c14:c15 -> c5:c6 -> c:c1:c2 -> c13:c14:c15
del :: 0':s -> nil:cons -> nil:cons
max :: nil:cons -> 0':s
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
sort :: nil:cons -> nil:cons
hole_c:c1:c21_20 :: c:c1:c2
hole_nil:cons2_20 :: nil:cons
hole_0':s3_20 :: 0':s
hole_c3:c44_20 :: c3:c4
hole_c16:c17:c18:c195_20 :: c16:c17:c18:c19
hole_true:false6_20 :: true:false
hole_c5:c67_20 :: c5:c6
hole_c7:c88_20 :: c7:c8
hole_c9:c10:c11:c129_20 :: c9:c10:c11:c12
hole_c13:c14:c1510_20 :: c13:c14:c15
gen_nil:cons11_20 :: Nat -> nil:cons
gen_0':s12_20 :: Nat -> 0':s
gen_c16:c17:c18:c1913_20 :: Nat -> c16:c17:c18:c19
gen_c9:c10:c11:c1214_20 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_20 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_20(n17_20), gen_0':s12_20(n17_20)) -> true, rt in Omega(0)
GE(gen_0':s12_20(n696_20), gen_0':s12_20(n696_20)) -> gen_c16:c17:c18:c1913_20(n696_20), rt in Omega(1 + n696_20)
MAX(gen_nil:cons11_20(+(1, n1791_20))) -> *16_20, rt in Omega(n1791_20)
eq(gen_0':s12_20(n7343_20), gen_0':s12_20(n7343_20)) -> true, rt in Omega(0)
EQ(gen_0':s12_20(n8100_20), gen_0':s12_20(n8100_20)) -> gen_c9:c10:c11:c1214_20(n8100_20), rt in Omega(1 + n8100_20)
max(gen_nil:cons11_20(+(1, n10382_20))) -> gen_0':s12_20(0), rt in Omega(0)
SORT(gen_nil:cons11_20(n11241_20)) -> *16_20, rt in Omega(n11241_20 + n11241_20^2)


Generator Equations:
gen_nil:cons11_20(0) <=> nil
gen_nil:cons11_20(+(x, 1)) <=> cons(0', gen_nil:cons11_20(x))
gen_0':s12_20(0) <=> 0'
gen_0':s12_20(+(x, 1)) <=> s(gen_0':s12_20(x))
gen_c16:c17:c18:c1913_20(0) <=> c16
gen_c16:c17:c18:c1913_20(+(x, 1)) <=> c19(gen_c16:c17:c18:c1913_20(x))
gen_c9:c10:c11:c1214_20(0) <=> c9
gen_c9:c10:c11:c1214_20(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_20(x))
gen_c13:c14:c1515_20(0) <=> c13
gen_c13:c14:c1515_20(+(x, 1)) <=> c15(gen_c13:c14:c1515_20(x), c5, c)


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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sort(gen_nil:cons11_20(n20835_20)) -> gen_nil:cons11_20(n20835_20), rt in Omega(0)

Induction Base:
sort(gen_nil:cons11_20(0)) ->_R^Omega(0)
nil

Induction Step:
sort(gen_nil:cons11_20(+(n20835_20, 1))) ->_R^Omega(0)
cons(max(cons(0', gen_nil:cons11_20(n20835_20))), sort(del(max(cons(0', gen_nil:cons11_20(n20835_20))), cons(0', gen_nil:cons11_20(n20835_20))))) ->_L^Omega(0)
cons(gen_0':s12_20(0), sort(del(max(cons(0', gen_nil:cons11_20(n20835_20))), cons(0', gen_nil:cons11_20(n20835_20))))) ->_L^Omega(0)
cons(gen_0':s12_20(0), sort(del(gen_0':s12_20(0), cons(0', gen_nil:cons11_20(n20835_20))))) ->_R^Omega(0)
cons(gen_0':s12_20(0), sort(if2(eq(gen_0':s12_20(0), 0'), gen_0':s12_20(0), 0', gen_nil:cons11_20(n20835_20)))) ->_L^Omega(0)
cons(gen_0':s12_20(0), sort(if2(true, gen_0':s12_20(0), 0', gen_nil:cons11_20(n20835_20)))) ->_R^Omega(0)
cons(gen_0':s12_20(0), sort(gen_nil:cons11_20(n20835_20))) ->_IH
cons(gen_0':s12_20(0), gen_nil:cons11_20(c20836_20))

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

(34)
BOUNDS(1, INF)