WORST_CASE(Omega(n^2),?)
proof of input_D842BnRqlZ.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 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), 7 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 302 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 185 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), 757 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 0 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 101 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 51 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 966 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), 91 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(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(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(z0, 0) -> c16
   GE(0, s(z0)) -> c17
   GE(s(z0), s(z1)) -> c18(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(z0, 0) -> c16
   GE(0, s(z0)) -> c17
   GE(s(z0), s(z1)) -> c18(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_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(z0, 0) -> c16
   GE(0, s(z0)) -> c17
   GE(s(z0), s(z1)) -> c18(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(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(z0, 0') -> c16
   GE(0', s(z0)) -> c17
   GE(s(z0), s(z1)) -> c18(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(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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: 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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: Nat -> c13:c14:c15


Generator Equations:
gen_nil:cons11_19(0) <=> nil
gen_nil:cons11_19(+(x, 1)) <=> cons(0', gen_nil:cons11_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c16:c17:c1813_19(0) <=> c16
gen_c16:c17:c1813_19(+(x, 1)) <=> c18(gen_c16:c17:c1813_19(x))
gen_c9:c10:c11:c1214_19(0) <=> c9
gen_c9:c10:c11:c1214_19(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_19(x))
gen_c13:c14:c1515_19(0) <=> c13
gen_c13:c14:c1515_19(+(x, 1)) <=> c15(gen_c13:c14:c1515_19(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_19(n17_19), gen_0':s12_19(n17_19)) -> true, rt in Omega(0)

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

Induction Step:
ge(gen_0':s12_19(+(n17_19, 1)), gen_0':s12_19(+(n17_19, 1))) ->_R^Omega(0)
ge(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) ->_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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> true, rt in Omega(0)


Generator Equations:
gen_nil:cons11_19(0) <=> nil
gen_nil:cons11_19(+(x, 1)) <=> cons(0', gen_nil:cons11_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c16:c17:c1813_19(0) <=> c16
gen_c16:c17:c1813_19(+(x, 1)) <=> c18(gen_c16:c17:c1813_19(x))
gen_c9:c10:c11:c1214_19(0) <=> c9
gen_c9:c10:c11:c1214_19(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_19(x))
gen_c13:c14:c1515_19(0) <=> c13
gen_c13:c14:c1515_19(+(x, 1)) <=> c15(gen_c13:c14:c1515_19(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_19(n471_19), gen_0':s12_19(n471_19)) -> gen_c16:c17:c1813_19(n471_19), rt in Omega(1 + n471_19)

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

Induction Step:
GE(gen_0':s12_19(+(n471_19, 1)), gen_0':s12_19(+(n471_19, 1))) ->_R^Omega(1)
c18(GE(gen_0':s12_19(n471_19), gen_0':s12_19(n471_19))) ->_IH
c18(gen_c16:c17:c1813_19(c472_19))

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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> true, rt in Omega(0)


Generator Equations:
gen_nil:cons11_19(0) <=> nil
gen_nil:cons11_19(+(x, 1)) <=> cons(0', gen_nil:cons11_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c16:c17:c1813_19(0) <=> c16
gen_c16:c17:c1813_19(+(x, 1)) <=> c18(gen_c16:c17:c1813_19(x))
gen_c9:c10:c11:c1214_19(0) <=> c9
gen_c9:c10:c11:c1214_19(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_19(x))
gen_c13:c14:c1515_19(0) <=> c13
gen_c13:c14:c1515_19(+(x, 1)) <=> c15(gen_c13:c14:c1515_19(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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> true, rt in Omega(0)
GE(gen_0':s12_19(n471_19), gen_0':s12_19(n471_19)) -> gen_c16:c17:c1813_19(n471_19), rt in Omega(1 + n471_19)


Generator Equations:
gen_nil:cons11_19(0) <=> nil
gen_nil:cons11_19(+(x, 1)) <=> cons(0', gen_nil:cons11_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c16:c17:c1813_19(0) <=> c16
gen_c16:c17:c1813_19(+(x, 1)) <=> c18(gen_c16:c17:c1813_19(x))
gen_c9:c10:c11:c1214_19(0) <=> c9
gen_c9:c10:c11:c1214_19(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_19(x))
gen_c13:c14:c1515_19(0) <=> c13
gen_c13:c14:c1515_19(+(x, 1)) <=> c15(gen_c13:c14:c1515_19(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_19(+(1, n1250_19))) -> *16_19, rt in Omega(n1250_19)

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

Induction Step:
MAX(gen_nil:cons11_19(+(1, +(n1250_19, 1)))) ->_R^Omega(1)
c2(IF1(ge(0', 0'), 0', 0', gen_nil:cons11_19(n1250_19)), GE(0', 0')) ->_L^Omega(0)
c2(IF1(true, 0', 0', gen_nil:cons11_19(n1250_19)), GE(0', 0')) ->_R^Omega(1)
c2(c3(MAX(cons(0', gen_nil:cons11_19(n1250_19)))), GE(0', 0')) ->_IH
c2(c3(*16_19), GE(0', 0')) ->_L^Omega(1)
c2(c3(*16_19), gen_c16:c17:c1813_19(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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> true, rt in Omega(0)
GE(gen_0':s12_19(n471_19), gen_0':s12_19(n471_19)) -> gen_c16:c17:c1813_19(n471_19), rt in Omega(1 + n471_19)
MAX(gen_nil:cons11_19(+(1, n1250_19))) -> *16_19, rt in Omega(n1250_19)


Generator Equations:
gen_nil:cons11_19(0) <=> nil
gen_nil:cons11_19(+(x, 1)) <=> cons(0', gen_nil:cons11_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c16:c17:c1813_19(0) <=> c16
gen_c16:c17:c1813_19(+(x, 1)) <=> c18(gen_c16:c17:c1813_19(x))
gen_c9:c10:c11:c1214_19(0) <=> c9
gen_c9:c10:c11:c1214_19(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_19(x))
gen_c13:c14:c1515_19(0) <=> c13
gen_c13:c14:c1515_19(+(x, 1)) <=> c15(gen_c13:c14:c1515_19(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_19(n6786_19), gen_0':s12_19(n6786_19)) -> true, rt in Omega(0)

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

Induction Step:
eq(gen_0':s12_19(+(n6786_19, 1)), gen_0':s12_19(+(n6786_19, 1))) ->_R^Omega(0)
eq(gen_0':s12_19(n6786_19), gen_0':s12_19(n6786_19)) ->_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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> true, rt in Omega(0)
GE(gen_0':s12_19(n471_19), gen_0':s12_19(n471_19)) -> gen_c16:c17:c1813_19(n471_19), rt in Omega(1 + n471_19)
MAX(gen_nil:cons11_19(+(1, n1250_19))) -> *16_19, rt in Omega(n1250_19)
eq(gen_0':s12_19(n6786_19), gen_0':s12_19(n6786_19)) -> true, rt in Omega(0)


Generator Equations:
gen_nil:cons11_19(0) <=> nil
gen_nil:cons11_19(+(x, 1)) <=> cons(0', gen_nil:cons11_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c16:c17:c1813_19(0) <=> c16
gen_c16:c17:c1813_19(+(x, 1)) <=> c18(gen_c16:c17:c1813_19(x))
gen_c9:c10:c11:c1214_19(0) <=> c9
gen_c9:c10:c11:c1214_19(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_19(x))
gen_c13:c14:c1515_19(0) <=> c13
gen_c13:c14:c1515_19(+(x, 1)) <=> c15(gen_c13:c14:c1515_19(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_19(n7531_19), gen_0':s12_19(n7531_19)) -> gen_c9:c10:c11:c1214_19(n7531_19), rt in Omega(1 + n7531_19)

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

Induction Step:
EQ(gen_0':s12_19(+(n7531_19, 1)), gen_0':s12_19(+(n7531_19, 1))) ->_R^Omega(1)
c12(EQ(gen_0':s12_19(n7531_19), gen_0':s12_19(n7531_19))) ->_IH
c12(gen_c9:c10:c11:c1214_19(c7532_19))

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

(24)
Obligation:
Innermost TRS:
Rules:
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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> true, rt in Omega(0)
GE(gen_0':s12_19(n471_19), gen_0':s12_19(n471_19)) -> gen_c16:c17:c1813_19(n471_19), rt in Omega(1 + n471_19)
MAX(gen_nil:cons11_19(+(1, n1250_19))) -> *16_19, rt in Omega(n1250_19)
eq(gen_0':s12_19(n6786_19), gen_0':s12_19(n6786_19)) -> true, rt in Omega(0)
EQ(gen_0':s12_19(n7531_19), gen_0':s12_19(n7531_19)) -> gen_c9:c10:c11:c1214_19(n7531_19), rt in Omega(1 + n7531_19)


Generator Equations:
gen_nil:cons11_19(0) <=> nil
gen_nil:cons11_19(+(x, 1)) <=> cons(0', gen_nil:cons11_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c16:c17:c1813_19(0) <=> c16
gen_c16:c17:c1813_19(+(x, 1)) <=> c18(gen_c16:c17:c1813_19(x))
gen_c9:c10:c11:c1214_19(0) <=> c9
gen_c9:c10:c11:c1214_19(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_19(x))
gen_c13:c14:c1515_19(0) <=> c13
gen_c13:c14:c1515_19(+(x, 1)) <=> c15(gen_c13:c14:c1515_19(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_19(+(1, n9799_19))) -> gen_0':s12_19(0), rt in Omega(0)

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

Induction Step:
max(gen_nil:cons11_19(+(1, +(n9799_19, 1)))) ->_R^Omega(0)
if1(ge(0', 0'), 0', 0', gen_nil:cons11_19(n9799_19)) ->_L^Omega(0)
if1(true, 0', 0', gen_nil:cons11_19(n9799_19)) ->_R^Omega(0)
max(cons(0', gen_nil:cons11_19(n9799_19))) ->_IH
gen_0':s12_19(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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> true, rt in Omega(0)
GE(gen_0':s12_19(n471_19), gen_0':s12_19(n471_19)) -> gen_c16:c17:c1813_19(n471_19), rt in Omega(1 + n471_19)
MAX(gen_nil:cons11_19(+(1, n1250_19))) -> *16_19, rt in Omega(n1250_19)
eq(gen_0':s12_19(n6786_19), gen_0':s12_19(n6786_19)) -> true, rt in Omega(0)
EQ(gen_0':s12_19(n7531_19), gen_0':s12_19(n7531_19)) -> gen_c9:c10:c11:c1214_19(n7531_19), rt in Omega(1 + n7531_19)
max(gen_nil:cons11_19(+(1, n9799_19))) -> gen_0':s12_19(0), rt in Omega(0)


Generator Equations:
gen_nil:cons11_19(0) <=> nil
gen_nil:cons11_19(+(x, 1)) <=> cons(0', gen_nil:cons11_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c16:c17:c1813_19(0) <=> c16
gen_c16:c17:c1813_19(+(x, 1)) <=> c18(gen_c16:c17:c1813_19(x))
gen_c9:c10:c11:c1214_19(0) <=> c9
gen_c9:c10:c11:c1214_19(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_19(x))
gen_c13:c14:c1515_19(0) <=> c13
gen_c13:c14:c1515_19(+(x, 1)) <=> c15(gen_c13:c14:c1515_19(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_19(n10640_19)) -> *16_19, rt in Omega(n10640_19 + n10640_19^2)

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

Induction Step:
SORT(gen_nil:cons11_19(+(n10640_19, 1))) ->_R^Omega(1)
c15(SORT(del(max(cons(0', gen_nil:cons11_19(n10640_19))), cons(0', gen_nil:cons11_19(n10640_19)))), DEL(max(cons(0', gen_nil:cons11_19(n10640_19))), cons(0', gen_nil:cons11_19(n10640_19))), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_L^Omega(0)
c15(SORT(del(gen_0':s12_19(0), cons(0', gen_nil:cons11_19(n10640_19)))), DEL(max(cons(0', gen_nil:cons11_19(n10640_19))), cons(0', gen_nil:cons11_19(n10640_19))), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_R^Omega(0)
c15(SORT(if2(eq(gen_0':s12_19(0), 0'), gen_0':s12_19(0), 0', gen_nil:cons11_19(n10640_19))), DEL(max(cons(0', gen_nil:cons11_19(n10640_19))), cons(0', gen_nil:cons11_19(n10640_19))), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_L^Omega(0)
c15(SORT(if2(true, gen_0':s12_19(0), 0', gen_nil:cons11_19(n10640_19))), DEL(max(cons(0', gen_nil:cons11_19(n10640_19))), cons(0', gen_nil:cons11_19(n10640_19))), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_R^Omega(0)
c15(SORT(gen_nil:cons11_19(n10640_19)), DEL(max(cons(0', gen_nil:cons11_19(n10640_19))), cons(0', gen_nil:cons11_19(n10640_19))), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_IH
c15(*16_19, DEL(max(cons(0', gen_nil:cons11_19(n10640_19))), cons(0', gen_nil:cons11_19(n10640_19))), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_L^Omega(0)
c15(*16_19, DEL(gen_0':s12_19(0), cons(0', gen_nil:cons11_19(n10640_19))), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_R^Omega(1)
c15(*16_19, c6(IF2(eq(gen_0':s12_19(0), 0'), gen_0':s12_19(0), 0', gen_nil:cons11_19(n10640_19)), EQ(gen_0':s12_19(0), 0')), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_L^Omega(0)
c15(*16_19, c6(IF2(true, gen_0':s12_19(0), 0', gen_nil:cons11_19(n10640_19)), EQ(gen_0':s12_19(0), 0')), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_R^Omega(1)
c15(*16_19, c6(c7, EQ(gen_0':s12_19(0), 0')), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_L^Omega(1)
c15(*16_19, c6(c7, gen_c9:c10:c11:c1214_19(0)), MAX(cons(0', gen_nil:cons11_19(n10640_19)))) ->_L^Omega(n10640_19)
c15(*16_19, c6(c7, gen_c9:c10:c11:c1214_19(0)), *16_19)

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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> true, rt in Omega(0)
GE(gen_0':s12_19(n471_19), gen_0':s12_19(n471_19)) -> gen_c16:c17:c1813_19(n471_19), rt in Omega(1 + n471_19)
MAX(gen_nil:cons11_19(+(1, n1250_19))) -> *16_19, rt in Omega(n1250_19)
eq(gen_0':s12_19(n6786_19), gen_0':s12_19(n6786_19)) -> true, rt in Omega(0)
EQ(gen_0':s12_19(n7531_19), gen_0':s12_19(n7531_19)) -> gen_c9:c10:c11:c1214_19(n7531_19), rt in Omega(1 + n7531_19)
max(gen_nil:cons11_19(+(1, n9799_19))) -> gen_0':s12_19(0), rt in Omega(0)


Generator Equations:
gen_nil:cons11_19(0) <=> nil
gen_nil:cons11_19(+(x, 1)) <=> cons(0', gen_nil:cons11_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c16:c17:c1813_19(0) <=> c16
gen_c16:c17:c1813_19(+(x, 1)) <=> c18(gen_c16:c17:c1813_19(x))
gen_c9:c10:c11:c1214_19(0) <=> c9
gen_c9:c10:c11:c1214_19(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_19(x))
gen_c13:c14:c1515_19(0) <=> c13
gen_c13:c14:c1515_19(+(x, 1)) <=> c15(gen_c13:c14:c1515_19(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(z0, 0') -> c16
GE(0', s(z0)) -> c17
GE(s(z0), s(z1)) -> c18(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(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 -> 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
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
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
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_19 :: c:c1:c2
hole_nil:cons2_19 :: nil:cons
hole_0':s3_19 :: 0':s
hole_c3:c44_19 :: c3:c4
hole_c16:c17:c185_19 :: c16:c17:c18
hole_true:false6_19 :: true:false
hole_c5:c67_19 :: c5:c6
hole_c7:c88_19 :: c7:c8
hole_c9:c10:c11:c129_19 :: c9:c10:c11:c12
hole_c13:c14:c1510_19 :: c13:c14:c15
gen_nil:cons11_19 :: Nat -> nil:cons
gen_0':s12_19 :: Nat -> 0':s
gen_c16:c17:c1813_19 :: Nat -> c16:c17:c18
gen_c9:c10:c11:c1214_19 :: Nat -> c9:c10:c11:c12
gen_c13:c14:c1515_19 :: Nat -> c13:c14:c15


Lemmas:
ge(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> true, rt in Omega(0)
GE(gen_0':s12_19(n471_19), gen_0':s12_19(n471_19)) -> gen_c16:c17:c1813_19(n471_19), rt in Omega(1 + n471_19)
MAX(gen_nil:cons11_19(+(1, n1250_19))) -> *16_19, rt in Omega(n1250_19)
eq(gen_0':s12_19(n6786_19), gen_0':s12_19(n6786_19)) -> true, rt in Omega(0)
EQ(gen_0':s12_19(n7531_19), gen_0':s12_19(n7531_19)) -> gen_c9:c10:c11:c1214_19(n7531_19), rt in Omega(1 + n7531_19)
max(gen_nil:cons11_19(+(1, n9799_19))) -> gen_0':s12_19(0), rt in Omega(0)
SORT(gen_nil:cons11_19(n10640_19)) -> *16_19, rt in Omega(n10640_19 + n10640_19^2)


Generator Equations:
gen_nil:cons11_19(0) <=> nil
gen_nil:cons11_19(+(x, 1)) <=> cons(0', gen_nil:cons11_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c16:c17:c1813_19(0) <=> c16
gen_c16:c17:c1813_19(+(x, 1)) <=> c18(gen_c16:c17:c1813_19(x))
gen_c9:c10:c11:c1214_19(0) <=> c9
gen_c9:c10:c11:c1214_19(+(x, 1)) <=> c12(gen_c9:c10:c11:c1214_19(x))
gen_c13:c14:c1515_19(0) <=> c13
gen_c13:c14:c1515_19(+(x, 1)) <=> c15(gen_c13:c14:c1515_19(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_19(n20138_19)) -> gen_nil:cons11_19(n20138_19), rt in Omega(0)

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

Induction Step:
sort(gen_nil:cons11_19(+(n20138_19, 1))) ->_R^Omega(0)
cons(max(cons(0', gen_nil:cons11_19(n20138_19))), sort(del(max(cons(0', gen_nil:cons11_19(n20138_19))), cons(0', gen_nil:cons11_19(n20138_19))))) ->_L^Omega(0)
cons(gen_0':s12_19(0), sort(del(max(cons(0', gen_nil:cons11_19(n20138_19))), cons(0', gen_nil:cons11_19(n20138_19))))) ->_L^Omega(0)
cons(gen_0':s12_19(0), sort(del(gen_0':s12_19(0), cons(0', gen_nil:cons11_19(n20138_19))))) ->_R^Omega(0)
cons(gen_0':s12_19(0), sort(if2(eq(gen_0':s12_19(0), 0'), gen_0':s12_19(0), 0', gen_nil:cons11_19(n20138_19)))) ->_L^Omega(0)
cons(gen_0':s12_19(0), sort(if2(true, gen_0':s12_19(0), 0', gen_nil:cons11_19(n20138_19)))) ->_R^Omega(0)
cons(gen_0':s12_19(0), sort(gen_nil:cons11_19(n20138_19))) ->_IH
cons(gen_0':s12_19(0), gen_nil:cons11_19(c20139_19))

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

(34)
BOUNDS(1, INF)