WORST_CASE(Omega(n^2),?)
proof of input_ud3yWHgaec.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), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 391 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 204 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 46 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 689 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 7 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 50 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 1028 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), 114 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:

   le(0, y) -> true
   le(s(x), 0) -> false
   le(s(x), s(y)) -> le(x, y)
   eq(0, 0) -> true
   eq(0, s(y)) -> false
   eq(s(x), 0) -> false
   eq(s(x), s(y)) -> eq(x, y)
   if1(true, x, y, xs) -> min(x, xs)
   if1(false, x, y, xs) -> min(y, xs)
   if2(true, x, y, xs) -> xs
   if2(false, x, y, xs) -> cons(y, del(x, xs))
   minsort(nil) -> nil
   minsort(cons(x, y)) -> cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
   min(x, nil) -> x
   min(x, cons(y, z)) -> if1(le(x, y), x, y, z)
   del(x, nil) -> nil
   del(x, cons(y, z)) -> if2(eq(x, y), x, y, z)

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:
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   if1(true, z0, z1, z2) -> min(z0, z2)
   if1(false, z0, z1, z2) -> min(z1, z2)
   if2(true, z0, z1, z2) -> z2
   if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
   minsort(nil) -> nil
   minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
   min(z0, nil) -> z0
   min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
Tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   EQ(0, 0) -> c3
   EQ(0, s(z0)) -> c4
   EQ(s(z0), 0) -> c5
   EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
   IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
   IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
   IF2(true, z0, z1, z2) -> c9
   IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
   MINSORT(nil) -> c11
   MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
   MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
   MIN(z0, nil) -> c14
   MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
   DEL(z0, nil) -> c16
   DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
S tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   EQ(0, 0) -> c3
   EQ(0, s(z0)) -> c4
   EQ(s(z0), 0) -> c5
   EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
   IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
   IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
   IF2(true, z0, z1, z2) -> c9
   IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
   MINSORT(nil) -> c11
   MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
   MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
   MIN(z0, nil) -> c14
   MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
   DEL(z0, nil) -> c16
   DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
K tuples:none
Defined Rule Symbols:   le_2, eq_2, if1_4, if2_4, minsort_1, min_2, del_2

Defined Pair Symbols:   LE_2, EQ_2, IF1_4, IF2_4, MINSORT_1, MIN_2, DEL_2

Compound Symbols:   c, c1, c2_1, c3, c4, c5, c6_1, c7_1, c8_1, c9, c10_1, c11, c12_1, c13_3, c14, c15_2, c16, c17_2


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

(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:

   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   EQ(0, 0) -> c3
   EQ(0, s(z0)) -> c4
   EQ(s(z0), 0) -> c5
   EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
   IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
   IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
   IF2(true, z0, z1, z2) -> c9
   IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
   MINSORT(nil) -> c11
   MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
   MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
   MIN(z0, nil) -> c14
   MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
   DEL(z0, nil) -> c16
   DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))

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

   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   if1(true, z0, z1, z2) -> min(z0, z2)
   if1(false, z0, z1, z2) -> min(z1, z2)
   if2(true, z0, z1, z2) -> z2
   if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
   minsort(nil) -> nil
   minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
   min(z0, nil) -> z0
   min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

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:

   LE(0', z0) -> c
   LE(s(z0), 0') -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   EQ(0', 0') -> c3
   EQ(0', s(z0)) -> c4
   EQ(s(z0), 0') -> c5
   EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
   IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
   IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
   IF2(true, z0, z1, z2) -> c9
   IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
   MINSORT(nil) -> c11
   MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
   MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
   MIN(z0, nil) -> c14
   MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
   DEL(z0, nil) -> c16
   DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))

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

   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   if1(true, z0, z1, z2) -> min(z0, z2)
   if1(false, z0, z1, z2) -> min(z1, z2)
   if2(true, z0, z1, z2) -> z2
   if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
   minsort(nil) -> nil
   minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
   min(z0, nil) -> z0
   min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

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

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

(8)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LE, EQ, MIN, DEL, MINSORT, del, min, le, eq, minsort

They will be analysed ascendingly in the following order:
LE < MIN
EQ < DEL
MIN < MINSORT
le < MIN
DEL < MINSORT
eq < DEL
del < MINSORT
min < MINSORT
eq < del
del < minsort
le < min
min < minsort

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

(10)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s12_18(0) <=> 0'
gen_0':s12_18(+(x, 1)) <=> s(gen_0':s12_18(x))
gen_c3:c4:c5:c613_18(0) <=> c3
gen_c3:c4:c5:c613_18(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_18(x))
gen_nil:cons14_18(0) <=> nil
gen_nil:cons14_18(+(x, 1)) <=> cons(0', gen_nil:cons14_18(x))
gen_c11:c12:c1315_18(0) <=> c11
gen_c11:c12:c1315_18(+(x, 1)) <=> c13(gen_c11:c12:c1315_18(x), c16, c14)


The following defined symbols remain to be analysed:
LE, EQ, MIN, DEL, MINSORT, del, min, le, eq, minsort

They will be analysed ascendingly in the following order:
LE < MIN
EQ < DEL
MIN < MINSORT
le < MIN
DEL < MINSORT
eq < DEL
del < MINSORT
min < MINSORT
eq < del
del < minsort
le < min
min < minsort

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s12_18(n17_18), gen_0':s12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18)

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

Induction Step:
LE(gen_0':s12_18(+(n17_18, 1)), gen_0':s12_18(+(n17_18, 1))) ->_R^Omega(1)
c2(LE(gen_0':s12_18(n17_18), gen_0':s12_18(n17_18))) ->_IH
c2(gen_c:c1:c211_18(c18_18))

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

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s12_18(0) <=> 0'
gen_0':s12_18(+(x, 1)) <=> s(gen_0':s12_18(x))
gen_c3:c4:c5:c613_18(0) <=> c3
gen_c3:c4:c5:c613_18(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_18(x))
gen_nil:cons14_18(0) <=> nil
gen_nil:cons14_18(+(x, 1)) <=> cons(0', gen_nil:cons14_18(x))
gen_c11:c12:c1315_18(0) <=> c11
gen_c11:c12:c1315_18(+(x, 1)) <=> c13(gen_c11:c12:c1315_18(x), c16, c14)


The following defined symbols remain to be analysed:
LE, EQ, MIN, DEL, MINSORT, del, min, le, eq, minsort

They will be analysed ascendingly in the following order:
LE < MIN
EQ < DEL
MIN < MINSORT
le < MIN
DEL < MINSORT
eq < DEL
del < MINSORT
min < MINSORT
eq < del
del < minsort
le < min
min < minsort

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13


Lemmas:
LE(gen_0':s12_18(n17_18), gen_0':s12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s12_18(0) <=> 0'
gen_0':s12_18(+(x, 1)) <=> s(gen_0':s12_18(x))
gen_c3:c4:c5:c613_18(0) <=> c3
gen_c3:c4:c5:c613_18(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_18(x))
gen_nil:cons14_18(0) <=> nil
gen_nil:cons14_18(+(x, 1)) <=> cons(0', gen_nil:cons14_18(x))
gen_c11:c12:c1315_18(0) <=> c11
gen_c11:c12:c1315_18(+(x, 1)) <=> c13(gen_c11:c12:c1315_18(x), c16, c14)


The following defined symbols remain to be analysed:
EQ, MIN, DEL, MINSORT, del, min, le, eq, minsort

They will be analysed ascendingly in the following order:
EQ < DEL
MIN < MINSORT
le < MIN
DEL < MINSORT
eq < DEL
del < MINSORT
min < MINSORT
eq < del
del < minsort
le < min
min < minsort

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s12_18(n702_18), gen_0':s12_18(n702_18)) -> gen_c3:c4:c5:c613_18(n702_18), rt in Omega(1 + n702_18)

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

Induction Step:
EQ(gen_0':s12_18(+(n702_18, 1)), gen_0':s12_18(+(n702_18, 1))) ->_R^Omega(1)
c6(EQ(gen_0':s12_18(n702_18), gen_0':s12_18(n702_18))) ->_IH
c6(gen_c3:c4:c5:c613_18(c703_18))

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

(18)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13


Lemmas:
LE(gen_0':s12_18(n17_18), gen_0':s12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18)
EQ(gen_0':s12_18(n702_18), gen_0':s12_18(n702_18)) -> gen_c3:c4:c5:c613_18(n702_18), rt in Omega(1 + n702_18)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s12_18(0) <=> 0'
gen_0':s12_18(+(x, 1)) <=> s(gen_0':s12_18(x))
gen_c3:c4:c5:c613_18(0) <=> c3
gen_c3:c4:c5:c613_18(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_18(x))
gen_nil:cons14_18(0) <=> nil
gen_nil:cons14_18(+(x, 1)) <=> cons(0', gen_nil:cons14_18(x))
gen_c11:c12:c1315_18(0) <=> c11
gen_c11:c12:c1315_18(+(x, 1)) <=> c13(gen_c11:c12:c1315_18(x), c16, c14)


The following defined symbols remain to be analysed:
le, MIN, DEL, MINSORT, del, min, eq, minsort

They will be analysed ascendingly in the following order:
MIN < MINSORT
le < MIN
DEL < MINSORT
eq < DEL
del < MINSORT
min < MINSORT
eq < del
del < minsort
le < min
min < minsort

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_0':s12_18(n1763_18), gen_0':s12_18(n1763_18)) -> true, rt in Omega(0)

Induction Base:
le(gen_0':s12_18(0), gen_0':s12_18(0)) ->_R^Omega(0)
true

Induction Step:
le(gen_0':s12_18(+(n1763_18, 1)), gen_0':s12_18(+(n1763_18, 1))) ->_R^Omega(0)
le(gen_0':s12_18(n1763_18), gen_0':s12_18(n1763_18)) ->_IH
true

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

(20)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13


Lemmas:
LE(gen_0':s12_18(n17_18), gen_0':s12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18)
EQ(gen_0':s12_18(n702_18), gen_0':s12_18(n702_18)) -> gen_c3:c4:c5:c613_18(n702_18), rt in Omega(1 + n702_18)
le(gen_0':s12_18(n1763_18), gen_0':s12_18(n1763_18)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s12_18(0) <=> 0'
gen_0':s12_18(+(x, 1)) <=> s(gen_0':s12_18(x))
gen_c3:c4:c5:c613_18(0) <=> c3
gen_c3:c4:c5:c613_18(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_18(x))
gen_nil:cons14_18(0) <=> nil
gen_nil:cons14_18(+(x, 1)) <=> cons(0', gen_nil:cons14_18(x))
gen_c11:c12:c1315_18(0) <=> c11
gen_c11:c12:c1315_18(+(x, 1)) <=> c13(gen_c11:c12:c1315_18(x), c16, c14)


The following defined symbols remain to be analysed:
MIN, DEL, MINSORT, del, min, eq, minsort

They will be analysed ascendingly in the following order:
MIN < MINSORT
DEL < MINSORT
eq < DEL
del < MINSORT
min < MINSORT
eq < del
del < minsort
min < minsort

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MIN(gen_0':s12_18(0), gen_nil:cons14_18(n2212_18)) -> *16_18, rt in Omega(n2212_18)

Induction Base:
MIN(gen_0':s12_18(0), gen_nil:cons14_18(0))

Induction Step:
MIN(gen_0':s12_18(0), gen_nil:cons14_18(+(n2212_18, 1))) ->_R^Omega(1)
c15(IF1(le(gen_0':s12_18(0), 0'), gen_0':s12_18(0), 0', gen_nil:cons14_18(n2212_18)), LE(gen_0':s12_18(0), 0')) ->_L^Omega(0)
c15(IF1(true, gen_0':s12_18(0), 0', gen_nil:cons14_18(n2212_18)), LE(gen_0':s12_18(0), 0')) ->_R^Omega(1)
c15(c7(MIN(gen_0':s12_18(0), gen_nil:cons14_18(n2212_18))), LE(gen_0':s12_18(0), 0')) ->_IH
c15(c7(*16_18), LE(gen_0':s12_18(0), 0')) ->_L^Omega(1)
c15(c7(*16_18), gen_c:c1:c211_18(0))

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

(22)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13


Lemmas:
LE(gen_0':s12_18(n17_18), gen_0':s12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18)
EQ(gen_0':s12_18(n702_18), gen_0':s12_18(n702_18)) -> gen_c3:c4:c5:c613_18(n702_18), rt in Omega(1 + n702_18)
le(gen_0':s12_18(n1763_18), gen_0':s12_18(n1763_18)) -> true, rt in Omega(0)
MIN(gen_0':s12_18(0), gen_nil:cons14_18(n2212_18)) -> *16_18, rt in Omega(n2212_18)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s12_18(0) <=> 0'
gen_0':s12_18(+(x, 1)) <=> s(gen_0':s12_18(x))
gen_c3:c4:c5:c613_18(0) <=> c3
gen_c3:c4:c5:c613_18(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_18(x))
gen_nil:cons14_18(0) <=> nil
gen_nil:cons14_18(+(x, 1)) <=> cons(0', gen_nil:cons14_18(x))
gen_c11:c12:c1315_18(0) <=> c11
gen_c11:c12:c1315_18(+(x, 1)) <=> c13(gen_c11:c12:c1315_18(x), c16, c14)


The following defined symbols remain to be analysed:
min, DEL, MINSORT, del, eq, minsort

They will be analysed ascendingly in the following order:
DEL < MINSORT
eq < DEL
del < MINSORT
min < MINSORT
eq < del
del < minsort
min < minsort

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
min(gen_0':s12_18(0), gen_nil:cons14_18(n7613_18)) -> gen_0':s12_18(0), rt in Omega(0)

Induction Base:
min(gen_0':s12_18(0), gen_nil:cons14_18(0)) ->_R^Omega(0)
gen_0':s12_18(0)

Induction Step:
min(gen_0':s12_18(0), gen_nil:cons14_18(+(n7613_18, 1))) ->_R^Omega(0)
if1(le(gen_0':s12_18(0), 0'), gen_0':s12_18(0), 0', gen_nil:cons14_18(n7613_18)) ->_L^Omega(0)
if1(true, gen_0':s12_18(0), 0', gen_nil:cons14_18(n7613_18)) ->_R^Omega(0)
min(gen_0':s12_18(0), gen_nil:cons14_18(n7613_18)) ->_IH
gen_0':s12_18(0)

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

(24)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13


Lemmas:
LE(gen_0':s12_18(n17_18), gen_0':s12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18)
EQ(gen_0':s12_18(n702_18), gen_0':s12_18(n702_18)) -> gen_c3:c4:c5:c613_18(n702_18), rt in Omega(1 + n702_18)
le(gen_0':s12_18(n1763_18), gen_0':s12_18(n1763_18)) -> true, rt in Omega(0)
MIN(gen_0':s12_18(0), gen_nil:cons14_18(n2212_18)) -> *16_18, rt in Omega(n2212_18)
min(gen_0':s12_18(0), gen_nil:cons14_18(n7613_18)) -> gen_0':s12_18(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s12_18(0) <=> 0'
gen_0':s12_18(+(x, 1)) <=> s(gen_0':s12_18(x))
gen_c3:c4:c5:c613_18(0) <=> c3
gen_c3:c4:c5:c613_18(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_18(x))
gen_nil:cons14_18(0) <=> nil
gen_nil:cons14_18(+(x, 1)) <=> cons(0', gen_nil:cons14_18(x))
gen_c11:c12:c1315_18(0) <=> c11
gen_c11:c12:c1315_18(+(x, 1)) <=> c13(gen_c11:c12:c1315_18(x), c16, c14)


The following defined symbols remain to be analysed:
eq, DEL, MINSORT, del, minsort

They will be analysed ascendingly in the following order:
DEL < MINSORT
eq < DEL
del < MINSORT
eq < del
del < minsort

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eq(gen_0':s12_18(n8848_18), gen_0':s12_18(n8848_18)) -> true, rt in Omega(0)

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

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

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:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13


Lemmas:
LE(gen_0':s12_18(n17_18), gen_0':s12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18)
EQ(gen_0':s12_18(n702_18), gen_0':s12_18(n702_18)) -> gen_c3:c4:c5:c613_18(n702_18), rt in Omega(1 + n702_18)
le(gen_0':s12_18(n1763_18), gen_0':s12_18(n1763_18)) -> true, rt in Omega(0)
MIN(gen_0':s12_18(0), gen_nil:cons14_18(n2212_18)) -> *16_18, rt in Omega(n2212_18)
min(gen_0':s12_18(0), gen_nil:cons14_18(n7613_18)) -> gen_0':s12_18(0), rt in Omega(0)
eq(gen_0':s12_18(n8848_18), gen_0':s12_18(n8848_18)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s12_18(0) <=> 0'
gen_0':s12_18(+(x, 1)) <=> s(gen_0':s12_18(x))
gen_c3:c4:c5:c613_18(0) <=> c3
gen_c3:c4:c5:c613_18(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_18(x))
gen_nil:cons14_18(0) <=> nil
gen_nil:cons14_18(+(x, 1)) <=> cons(0', gen_nil:cons14_18(x))
gen_c11:c12:c1315_18(0) <=> c11
gen_c11:c12:c1315_18(+(x, 1)) <=> c13(gen_c11:c12:c1315_18(x), c16, c14)


The following defined symbols remain to be analysed:
DEL, MINSORT, del, minsort

They will be analysed ascendingly in the following order:
DEL < MINSORT
del < MINSORT
del < minsort

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MINSORT(gen_nil:cons14_18(n10575_18)) -> *16_18, rt in Omega(n10575_18 + n10575_18^2)

Induction Base:
MINSORT(gen_nil:cons14_18(0))

Induction Step:
MINSORT(gen_nil:cons14_18(+(n10575_18, 1))) ->_R^Omega(1)
c13(MINSORT(del(min(0', gen_nil:cons14_18(n10575_18)), cons(0', gen_nil:cons14_18(n10575_18)))), DEL(min(0', gen_nil:cons14_18(n10575_18)), cons(0', gen_nil:cons14_18(n10575_18))), MIN(0', gen_nil:cons14_18(n10575_18))) ->_L^Omega(0)
c13(MINSORT(del(gen_0':s12_18(0), cons(0', gen_nil:cons14_18(n10575_18)))), DEL(min(0', gen_nil:cons14_18(n10575_18)), cons(0', gen_nil:cons14_18(n10575_18))), MIN(0', gen_nil:cons14_18(n10575_18))) ->_R^Omega(0)
c13(MINSORT(if2(eq(gen_0':s12_18(0), 0'), gen_0':s12_18(0), 0', gen_nil:cons14_18(n10575_18))), DEL(min(0', gen_nil:cons14_18(n10575_18)), cons(0', gen_nil:cons14_18(n10575_18))), MIN(0', gen_nil:cons14_18(n10575_18))) ->_L^Omega(0)
c13(MINSORT(if2(true, gen_0':s12_18(0), 0', gen_nil:cons14_18(n10575_18))), DEL(min(0', gen_nil:cons14_18(n10575_18)), cons(0', gen_nil:cons14_18(n10575_18))), MIN(0', gen_nil:cons14_18(n10575_18))) ->_R^Omega(0)
c13(MINSORT(gen_nil:cons14_18(n10575_18)), DEL(min(0', gen_nil:cons14_18(n10575_18)), cons(0', gen_nil:cons14_18(n10575_18))), MIN(0', gen_nil:cons14_18(n10575_18))) ->_IH
c13(*16_18, DEL(min(0', gen_nil:cons14_18(n10575_18)), cons(0', gen_nil:cons14_18(n10575_18))), MIN(0', gen_nil:cons14_18(n10575_18))) ->_L^Omega(0)
c13(*16_18, DEL(gen_0':s12_18(0), cons(0', gen_nil:cons14_18(n10575_18))), MIN(0', gen_nil:cons14_18(n10575_18))) ->_R^Omega(1)
c13(*16_18, c17(IF2(eq(gen_0':s12_18(0), 0'), gen_0':s12_18(0), 0', gen_nil:cons14_18(n10575_18)), EQ(gen_0':s12_18(0), 0')), MIN(0', gen_nil:cons14_18(n10575_18))) ->_L^Omega(0)
c13(*16_18, c17(IF2(true, gen_0':s12_18(0), 0', gen_nil:cons14_18(n10575_18)), EQ(gen_0':s12_18(0), 0')), MIN(0', gen_nil:cons14_18(n10575_18))) ->_R^Omega(1)
c13(*16_18, c17(c9, EQ(gen_0':s12_18(0), 0')), MIN(0', gen_nil:cons14_18(n10575_18))) ->_L^Omega(1)
c13(*16_18, c17(c9, gen_c3:c4:c5:c613_18(0)), MIN(0', gen_nil:cons14_18(n10575_18))) ->_L^Omega(n10575_18)
c13(*16_18, c17(c9, gen_c3:c4:c5:c613_18(0)), *16_18)

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:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13


Lemmas:
LE(gen_0':s12_18(n17_18), gen_0':s12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18)
EQ(gen_0':s12_18(n702_18), gen_0':s12_18(n702_18)) -> gen_c3:c4:c5:c613_18(n702_18), rt in Omega(1 + n702_18)
le(gen_0':s12_18(n1763_18), gen_0':s12_18(n1763_18)) -> true, rt in Omega(0)
MIN(gen_0':s12_18(0), gen_nil:cons14_18(n2212_18)) -> *16_18, rt in Omega(n2212_18)
min(gen_0':s12_18(0), gen_nil:cons14_18(n7613_18)) -> gen_0':s12_18(0), rt in Omega(0)
eq(gen_0':s12_18(n8848_18), gen_0':s12_18(n8848_18)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s12_18(0) <=> 0'
gen_0':s12_18(+(x, 1)) <=> s(gen_0':s12_18(x))
gen_c3:c4:c5:c613_18(0) <=> c3
gen_c3:c4:c5:c613_18(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_18(x))
gen_nil:cons14_18(0) <=> nil
gen_nil:cons14_18(+(x, 1)) <=> cons(0', gen_nil:cons14_18(x))
gen_c11:c12:c1315_18(0) <=> c11
gen_c11:c12:c1315_18(+(x, 1)) <=> c13(gen_c11:c12:c1315_18(x), c16, c14)


The following defined symbols remain to be analysed:
MINSORT, minsort
----------------------------------------

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

(31)
BOUNDS(n^2, INF)

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

(32)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
EQ(0', 0') -> c3
EQ(0', s(z0)) -> c4
EQ(s(z0), 0') -> c5
EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
IF1(true, z0, z1, z2) -> c7(MIN(z0, z2))
IF1(false, z0, z1, z2) -> c8(MIN(z1, z2))
IF2(true, z0, z1, z2) -> c9
IF2(false, z0, z1, z2) -> c10(DEL(z0, z2))
MINSORT(nil) -> c11
MINSORT(cons(z0, z1)) -> c12(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c13(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c14
MIN(z0, cons(z1, z2)) -> c15(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
if1(true, z0, z1, z2) -> min(z0, z2)
if1(false, z0, z1, z2) -> min(z1, z2)
if2(true, z0, z1, z2) -> z2
if2(false, z0, z1, z2) -> cons(z1, del(z0, z2))
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
min(z0, nil) -> z0
min(z0, cons(z1, z2)) -> if1(le(z0, z1), z0, z1, z2)
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s -> 0':s -> c3:c4:c5:c6
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8
true :: true:false
c7 :: c14:c15 -> c7:c8
MIN :: 0':s -> nil:cons -> c14:c15
false :: true:false
c8 :: c14:c15 -> c7:c8
IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c9:c10
c9 :: c9:c10
c10 :: c16:c17 -> c9:c10
DEL :: 0':s -> nil:cons -> c16:c17
MINSORT :: nil:cons -> c11:c12:c13
nil :: nil:cons
c11 :: c11:c12:c13
cons :: 0':s -> nil:cons -> nil:cons
c12 :: c14:c15 -> c11:c12:c13
c13 :: c11:c12:c13 -> c16:c17 -> c14:c15 -> c11:c12:c13
del :: 0':s -> nil:cons -> nil:cons
min :: 0':s -> nil:cons -> 0':s
c14 :: c14:c15
c15 :: c7:c8 -> c:c1:c2 -> c14:c15
le :: 0':s -> 0':s -> true:false
c16 :: c16:c17
c17 :: c9:c10 -> c3:c4:c5:c6 -> c16:c17
eq :: 0':s -> 0':s -> true:false
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
minsort :: nil:cons -> nil:cons
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s2_18 :: 0':s
hole_c3:c4:c5:c63_18 :: c3:c4:c5:c6
hole_c7:c84_18 :: c7:c8
hole_true:false5_18 :: true:false
hole_nil:cons6_18 :: nil:cons
hole_c14:c157_18 :: c14:c15
hole_c9:c108_18 :: c9:c10
hole_c16:c179_18 :: c16:c17
hole_c11:c12:c1310_18 :: c11:c12:c13
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s12_18 :: Nat -> 0':s
gen_c3:c4:c5:c613_18 :: Nat -> c3:c4:c5:c6
gen_nil:cons14_18 :: Nat -> nil:cons
gen_c11:c12:c1315_18 :: Nat -> c11:c12:c13


Lemmas:
LE(gen_0':s12_18(n17_18), gen_0':s12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18)
EQ(gen_0':s12_18(n702_18), gen_0':s12_18(n702_18)) -> gen_c3:c4:c5:c613_18(n702_18), rt in Omega(1 + n702_18)
le(gen_0':s12_18(n1763_18), gen_0':s12_18(n1763_18)) -> true, rt in Omega(0)
MIN(gen_0':s12_18(0), gen_nil:cons14_18(n2212_18)) -> *16_18, rt in Omega(n2212_18)
min(gen_0':s12_18(0), gen_nil:cons14_18(n7613_18)) -> gen_0':s12_18(0), rt in Omega(0)
eq(gen_0':s12_18(n8848_18), gen_0':s12_18(n8848_18)) -> true, rt in Omega(0)
MINSORT(gen_nil:cons14_18(n10575_18)) -> *16_18, rt in Omega(n10575_18 + n10575_18^2)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s12_18(0) <=> 0'
gen_0':s12_18(+(x, 1)) <=> s(gen_0':s12_18(x))
gen_c3:c4:c5:c613_18(0) <=> c3
gen_c3:c4:c5:c613_18(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_18(x))
gen_nil:cons14_18(0) <=> nil
gen_nil:cons14_18(+(x, 1)) <=> cons(0', gen_nil:cons14_18(x))
gen_c11:c12:c1315_18(0) <=> c11
gen_c11:c12:c1315_18(+(x, 1)) <=> c13(gen_c11:c12:c1315_18(x), c16, c14)


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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
minsort(gen_nil:cons14_18(n20881_18)) -> gen_nil:cons14_18(n20881_18), rt in Omega(0)

Induction Base:
minsort(gen_nil:cons14_18(0)) ->_R^Omega(0)
nil

Induction Step:
minsort(gen_nil:cons14_18(+(n20881_18, 1))) ->_R^Omega(0)
cons(min(0', gen_nil:cons14_18(n20881_18)), minsort(del(min(0', gen_nil:cons14_18(n20881_18)), cons(0', gen_nil:cons14_18(n20881_18))))) ->_L^Omega(0)
cons(gen_0':s12_18(0), minsort(del(min(0', gen_nil:cons14_18(n20881_18)), cons(0', gen_nil:cons14_18(n20881_18))))) ->_L^Omega(0)
cons(gen_0':s12_18(0), minsort(del(gen_0':s12_18(0), cons(0', gen_nil:cons14_18(n20881_18))))) ->_R^Omega(0)
cons(gen_0':s12_18(0), minsort(if2(eq(gen_0':s12_18(0), 0'), gen_0':s12_18(0), 0', gen_nil:cons14_18(n20881_18)))) ->_L^Omega(0)
cons(gen_0':s12_18(0), minsort(if2(true, gen_0':s12_18(0), 0', gen_nil:cons14_18(n20881_18)))) ->_R^Omega(0)
cons(gen_0':s12_18(0), minsort(gen_nil:cons14_18(n20881_18))) ->_IH
cons(gen_0':s12_18(0), gen_nil:cons14_18(c20882_18))

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

(34)
BOUNDS(1, INF)