WORST_CASE(Omega(n^1),?)
proof of input_GMC79AchIX.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 8 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 337 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), 153 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 44 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 22 ms]
        (22) typed CpxTrs


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

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


The TRS R consists of the following rules:

   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)
   if(true, x, y) -> x
   if(false, x, y) -> y
   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)) -> if(le(x, y), min(x, z), min(y, z))
   del(x, nil) -> nil
   del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, 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)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   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)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, 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))
   IF(true, z0, z1) -> c7
   IF(false, z0, z1) -> c8
   MINSORT(nil) -> c9
   MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
   MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
   MIN(z0, nil) -> c12
   MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
   MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
   MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
   DEL(z0, nil) -> c16
   DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
   DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))
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))
   IF(true, z0, z1) -> c7
   IF(false, z0, z1) -> c8
   MINSORT(nil) -> c9
   MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
   MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
   MIN(z0, nil) -> c12
   MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
   MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
   MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
   DEL(z0, nil) -> c16
   DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
   DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))
K tuples:none
Defined Rule Symbols:   le_2, eq_2, if_3, minsort_1, min_2, del_2

Defined Pair Symbols:   LE_2, EQ_2, IF_3, MINSORT_1, MIN_2, DEL_2

Compound Symbols:   c, c1, c2_1, c3, c4, c5, c6_1, c7, c8, c9, c10_1, c11_3, c12, c13_2, c14_2, c15_2, c16, c17_2, c18_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^1, 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))
   IF(true, z0, z1) -> c7
   IF(false, z0, z1) -> c8
   MINSORT(nil) -> c9
   MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
   MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
   MIN(z0, nil) -> c12
   MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
   MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
   MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
   DEL(z0, nil) -> c16
   DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
   DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))

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)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   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)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, 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^1, 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))
   IF(true, z0, z1) -> c7
   IF(false, z0, z1) -> c8
   MINSORT(nil) -> c9
   MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
   MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
   MIN(z0, nil) -> c12
   MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
   MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
   MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
   DEL(z0, nil) -> c16
   DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
   DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))

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)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   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)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, 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))
IF(true, z0, z1) -> c7
IF(false, z0, z1) -> c8
MINSORT(nil) -> c9
MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c12
MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))
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)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, z2)))

Types:
LE :: 0':s:nil:cons -> 0':s:nil:cons -> c:c1:c2
0' :: 0':s:nil:cons
c :: c:c1:c2
s :: 0':s:nil:cons -> 0':s:nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s:nil:cons -> 0':s:nil:cons -> 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
IF :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> c7:c8
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c7:c8
MINSORT :: 0':s:nil:cons -> c9:c10:c11
nil :: 0':s:nil:cons
c9 :: c9:c10:c11
cons :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
c10 :: c12:c13:c14:c15 -> c9:c10:c11
MIN :: 0':s:nil:cons -> 0':s:nil:cons -> c12:c13:c14:c15
c11 :: c9:c10:c11 -> c16:c17:c18 -> c12:c13:c14:c15 -> c9:c10:c11
del :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
min :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
DEL :: 0':s:nil:cons -> 0':s:nil:cons -> c16:c17:c18
c12 :: c12:c13:c14:c15
c13 :: c7:c8 -> c:c1:c2 -> c12:c13:c14:c15
le :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c14 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c16:c17:c18
c17 :: c7:c8 -> c3:c4:c5:c6 -> c16:c17:c18
eq :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c18 :: c7:c8 -> c16:c17:c18 -> c16:c17:c18
if :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
minsort :: 0':s:nil:cons -> 0':s:nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s:nil:cons2_19 :: 0':s:nil:cons
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c84_19 :: c7:c8
hole_true:false5_19 :: true:false
hole_c9:c10:c116_19 :: c9:c10:c11
hole_c12:c13:c14:c157_19 :: c12:c13:c14:c15
hole_c16:c17:c188_19 :: c16:c17:c18
gen_c:c1:c29_19 :: Nat -> c:c1:c2
gen_0':s:nil:cons10_19 :: Nat -> 0':s:nil:cons
gen_c3:c4:c5:c611_19 :: Nat -> c3:c4:c5:c6
gen_c9:c10:c1112_19 :: Nat -> c9:c10:c11
gen_c12:c13:c14:c1513_19 :: Nat -> c12:c13:c14:c15
gen_c16:c17:c1814_19 :: Nat -> c16:c17:c18

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

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

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

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

(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))
IF(true, z0, z1) -> c7
IF(false, z0, z1) -> c8
MINSORT(nil) -> c9
MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c12
MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))
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)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, z2)))

Types:
LE :: 0':s:nil:cons -> 0':s:nil:cons -> c:c1:c2
0' :: 0':s:nil:cons
c :: c:c1:c2
s :: 0':s:nil:cons -> 0':s:nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s:nil:cons -> 0':s:nil:cons -> 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
IF :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> c7:c8
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c7:c8
MINSORT :: 0':s:nil:cons -> c9:c10:c11
nil :: 0':s:nil:cons
c9 :: c9:c10:c11
cons :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
c10 :: c12:c13:c14:c15 -> c9:c10:c11
MIN :: 0':s:nil:cons -> 0':s:nil:cons -> c12:c13:c14:c15
c11 :: c9:c10:c11 -> c16:c17:c18 -> c12:c13:c14:c15 -> c9:c10:c11
del :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
min :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
DEL :: 0':s:nil:cons -> 0':s:nil:cons -> c16:c17:c18
c12 :: c12:c13:c14:c15
c13 :: c7:c8 -> c:c1:c2 -> c12:c13:c14:c15
le :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c14 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c16:c17:c18
c17 :: c7:c8 -> c3:c4:c5:c6 -> c16:c17:c18
eq :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c18 :: c7:c8 -> c16:c17:c18 -> c16:c17:c18
if :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
minsort :: 0':s:nil:cons -> 0':s:nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s:nil:cons2_19 :: 0':s:nil:cons
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c84_19 :: c7:c8
hole_true:false5_19 :: true:false
hole_c9:c10:c116_19 :: c9:c10:c11
hole_c12:c13:c14:c157_19 :: c12:c13:c14:c15
hole_c16:c17:c188_19 :: c16:c17:c18
gen_c:c1:c29_19 :: Nat -> c:c1:c2
gen_0':s:nil:cons10_19 :: Nat -> 0':s:nil:cons
gen_c3:c4:c5:c611_19 :: Nat -> c3:c4:c5:c6
gen_c9:c10:c1112_19 :: Nat -> c9:c10:c11
gen_c12:c13:c14:c1513_19 :: Nat -> c12:c13:c14:c15
gen_c16:c17:c1814_19 :: Nat -> c16:c17:c18


Generator Equations:
gen_c:c1:c29_19(0) <=> c
gen_c:c1:c29_19(+(x, 1)) <=> c2(gen_c:c1:c29_19(x))
gen_0':s:nil:cons10_19(0) <=> 0'
gen_0':s:nil:cons10_19(+(x, 1)) <=> s(gen_0':s:nil:cons10_19(x))
gen_c3:c4:c5:c611_19(0) <=> c3
gen_c3:c4:c5:c611_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c611_19(x))
gen_c9:c10:c1112_19(0) <=> c9
gen_c9:c10:c1112_19(+(x, 1)) <=> c11(gen_c9:c10:c1112_19(x), c16, c12)
gen_c12:c13:c14:c1513_19(0) <=> c12
gen_c12:c13:c14:c1513_19(+(x, 1)) <=> c14(c7, gen_c12:c13:c14:c1513_19(x))
gen_c16:c17:c1814_19(0) <=> c16
gen_c16:c17:c1814_19(+(x, 1)) <=> c18(c7, gen_c16:c17:c1814_19(x))


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

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

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s:nil:cons10_19(n16_19), gen_0':s:nil:cons10_19(n16_19)) -> gen_c:c1:c29_19(n16_19), rt in Omega(1 + n16_19)

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

Induction Step:
LE(gen_0':s:nil:cons10_19(+(n16_19, 1)), gen_0':s:nil:cons10_19(+(n16_19, 1))) ->_R^Omega(1)
c2(LE(gen_0':s:nil:cons10_19(n16_19), gen_0':s:nil:cons10_19(n16_19))) ->_IH
c2(gen_c:c1:c29_19(c17_19))

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))
IF(true, z0, z1) -> c7
IF(false, z0, z1) -> c8
MINSORT(nil) -> c9
MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c12
MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))
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)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, z2)))

Types:
LE :: 0':s:nil:cons -> 0':s:nil:cons -> c:c1:c2
0' :: 0':s:nil:cons
c :: c:c1:c2
s :: 0':s:nil:cons -> 0':s:nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s:nil:cons -> 0':s:nil:cons -> 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
IF :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> c7:c8
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c7:c8
MINSORT :: 0':s:nil:cons -> c9:c10:c11
nil :: 0':s:nil:cons
c9 :: c9:c10:c11
cons :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
c10 :: c12:c13:c14:c15 -> c9:c10:c11
MIN :: 0':s:nil:cons -> 0':s:nil:cons -> c12:c13:c14:c15
c11 :: c9:c10:c11 -> c16:c17:c18 -> c12:c13:c14:c15 -> c9:c10:c11
del :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
min :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
DEL :: 0':s:nil:cons -> 0':s:nil:cons -> c16:c17:c18
c12 :: c12:c13:c14:c15
c13 :: c7:c8 -> c:c1:c2 -> c12:c13:c14:c15
le :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c14 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c16:c17:c18
c17 :: c7:c8 -> c3:c4:c5:c6 -> c16:c17:c18
eq :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c18 :: c7:c8 -> c16:c17:c18 -> c16:c17:c18
if :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
minsort :: 0':s:nil:cons -> 0':s:nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s:nil:cons2_19 :: 0':s:nil:cons
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c84_19 :: c7:c8
hole_true:false5_19 :: true:false
hole_c9:c10:c116_19 :: c9:c10:c11
hole_c12:c13:c14:c157_19 :: c12:c13:c14:c15
hole_c16:c17:c188_19 :: c16:c17:c18
gen_c:c1:c29_19 :: Nat -> c:c1:c2
gen_0':s:nil:cons10_19 :: Nat -> 0':s:nil:cons
gen_c3:c4:c5:c611_19 :: Nat -> c3:c4:c5:c6
gen_c9:c10:c1112_19 :: Nat -> c9:c10:c11
gen_c12:c13:c14:c1513_19 :: Nat -> c12:c13:c14:c15
gen_c16:c17:c1814_19 :: Nat -> c16:c17:c18


Generator Equations:
gen_c:c1:c29_19(0) <=> c
gen_c:c1:c29_19(+(x, 1)) <=> c2(gen_c:c1:c29_19(x))
gen_0':s:nil:cons10_19(0) <=> 0'
gen_0':s:nil:cons10_19(+(x, 1)) <=> s(gen_0':s:nil:cons10_19(x))
gen_c3:c4:c5:c611_19(0) <=> c3
gen_c3:c4:c5:c611_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c611_19(x))
gen_c9:c10:c1112_19(0) <=> c9
gen_c9:c10:c1112_19(+(x, 1)) <=> c11(gen_c9:c10:c1112_19(x), c16, c12)
gen_c12:c13:c14:c1513_19(0) <=> c12
gen_c12:c13:c14:c1513_19(+(x, 1)) <=> c14(c7, gen_c12:c13:c14:c1513_19(x))
gen_c16:c17:c1814_19(0) <=> c16
gen_c16:c17:c1814_19(+(x, 1)) <=> c18(c7, gen_c16:c17:c1814_19(x))


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

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

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

(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))
IF(true, z0, z1) -> c7
IF(false, z0, z1) -> c8
MINSORT(nil) -> c9
MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c12
MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))
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)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, z2)))

Types:
LE :: 0':s:nil:cons -> 0':s:nil:cons -> c:c1:c2
0' :: 0':s:nil:cons
c :: c:c1:c2
s :: 0':s:nil:cons -> 0':s:nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s:nil:cons -> 0':s:nil:cons -> 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
IF :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> c7:c8
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c7:c8
MINSORT :: 0':s:nil:cons -> c9:c10:c11
nil :: 0':s:nil:cons
c9 :: c9:c10:c11
cons :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
c10 :: c12:c13:c14:c15 -> c9:c10:c11
MIN :: 0':s:nil:cons -> 0':s:nil:cons -> c12:c13:c14:c15
c11 :: c9:c10:c11 -> c16:c17:c18 -> c12:c13:c14:c15 -> c9:c10:c11
del :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
min :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
DEL :: 0':s:nil:cons -> 0':s:nil:cons -> c16:c17:c18
c12 :: c12:c13:c14:c15
c13 :: c7:c8 -> c:c1:c2 -> c12:c13:c14:c15
le :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c14 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c16:c17:c18
c17 :: c7:c8 -> c3:c4:c5:c6 -> c16:c17:c18
eq :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c18 :: c7:c8 -> c16:c17:c18 -> c16:c17:c18
if :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
minsort :: 0':s:nil:cons -> 0':s:nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s:nil:cons2_19 :: 0':s:nil:cons
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c84_19 :: c7:c8
hole_true:false5_19 :: true:false
hole_c9:c10:c116_19 :: c9:c10:c11
hole_c12:c13:c14:c157_19 :: c12:c13:c14:c15
hole_c16:c17:c188_19 :: c16:c17:c18
gen_c:c1:c29_19 :: Nat -> c:c1:c2
gen_0':s:nil:cons10_19 :: Nat -> 0':s:nil:cons
gen_c3:c4:c5:c611_19 :: Nat -> c3:c4:c5:c6
gen_c9:c10:c1112_19 :: Nat -> c9:c10:c11
gen_c12:c13:c14:c1513_19 :: Nat -> c12:c13:c14:c15
gen_c16:c17:c1814_19 :: Nat -> c16:c17:c18


Lemmas:
LE(gen_0':s:nil:cons10_19(n16_19), gen_0':s:nil:cons10_19(n16_19)) -> gen_c:c1:c29_19(n16_19), rt in Omega(1 + n16_19)


Generator Equations:
gen_c:c1:c29_19(0) <=> c
gen_c:c1:c29_19(+(x, 1)) <=> c2(gen_c:c1:c29_19(x))
gen_0':s:nil:cons10_19(0) <=> 0'
gen_0':s:nil:cons10_19(+(x, 1)) <=> s(gen_0':s:nil:cons10_19(x))
gen_c3:c4:c5:c611_19(0) <=> c3
gen_c3:c4:c5:c611_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c611_19(x))
gen_c9:c10:c1112_19(0) <=> c9
gen_c9:c10:c1112_19(+(x, 1)) <=> c11(gen_c9:c10:c1112_19(x), c16, c12)
gen_c12:c13:c14:c1513_19(0) <=> c12
gen_c12:c13:c14:c1513_19(+(x, 1)) <=> c14(c7, gen_c12:c13:c14:c1513_19(x))
gen_c16:c17:c1814_19(0) <=> c16
gen_c16:c17:c1814_19(+(x, 1)) <=> c18(c7, gen_c16:c17:c1814_19(x))


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

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

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s:nil:cons10_19(n728_19), gen_0':s:nil:cons10_19(n728_19)) -> gen_c3:c4:c5:c611_19(n728_19), rt in Omega(1 + n728_19)

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

Induction Step:
EQ(gen_0':s:nil:cons10_19(+(n728_19, 1)), gen_0':s:nil:cons10_19(+(n728_19, 1))) ->_R^Omega(1)
c6(EQ(gen_0':s:nil:cons10_19(n728_19), gen_0':s:nil:cons10_19(n728_19))) ->_IH
c6(gen_c3:c4:c5:c611_19(c729_19))

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))
IF(true, z0, z1) -> c7
IF(false, z0, z1) -> c8
MINSORT(nil) -> c9
MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c12
MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))
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)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, z2)))

Types:
LE :: 0':s:nil:cons -> 0':s:nil:cons -> c:c1:c2
0' :: 0':s:nil:cons
c :: c:c1:c2
s :: 0':s:nil:cons -> 0':s:nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s:nil:cons -> 0':s:nil:cons -> 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
IF :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> c7:c8
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c7:c8
MINSORT :: 0':s:nil:cons -> c9:c10:c11
nil :: 0':s:nil:cons
c9 :: c9:c10:c11
cons :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
c10 :: c12:c13:c14:c15 -> c9:c10:c11
MIN :: 0':s:nil:cons -> 0':s:nil:cons -> c12:c13:c14:c15
c11 :: c9:c10:c11 -> c16:c17:c18 -> c12:c13:c14:c15 -> c9:c10:c11
del :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
min :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
DEL :: 0':s:nil:cons -> 0':s:nil:cons -> c16:c17:c18
c12 :: c12:c13:c14:c15
c13 :: c7:c8 -> c:c1:c2 -> c12:c13:c14:c15
le :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c14 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c16:c17:c18
c17 :: c7:c8 -> c3:c4:c5:c6 -> c16:c17:c18
eq :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c18 :: c7:c8 -> c16:c17:c18 -> c16:c17:c18
if :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
minsort :: 0':s:nil:cons -> 0':s:nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s:nil:cons2_19 :: 0':s:nil:cons
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c84_19 :: c7:c8
hole_true:false5_19 :: true:false
hole_c9:c10:c116_19 :: c9:c10:c11
hole_c12:c13:c14:c157_19 :: c12:c13:c14:c15
hole_c16:c17:c188_19 :: c16:c17:c18
gen_c:c1:c29_19 :: Nat -> c:c1:c2
gen_0':s:nil:cons10_19 :: Nat -> 0':s:nil:cons
gen_c3:c4:c5:c611_19 :: Nat -> c3:c4:c5:c6
gen_c9:c10:c1112_19 :: Nat -> c9:c10:c11
gen_c12:c13:c14:c1513_19 :: Nat -> c12:c13:c14:c15
gen_c16:c17:c1814_19 :: Nat -> c16:c17:c18


Lemmas:
LE(gen_0':s:nil:cons10_19(n16_19), gen_0':s:nil:cons10_19(n16_19)) -> gen_c:c1:c29_19(n16_19), rt in Omega(1 + n16_19)
EQ(gen_0':s:nil:cons10_19(n728_19), gen_0':s:nil:cons10_19(n728_19)) -> gen_c3:c4:c5:c611_19(n728_19), rt in Omega(1 + n728_19)


Generator Equations:
gen_c:c1:c29_19(0) <=> c
gen_c:c1:c29_19(+(x, 1)) <=> c2(gen_c:c1:c29_19(x))
gen_0':s:nil:cons10_19(0) <=> 0'
gen_0':s:nil:cons10_19(+(x, 1)) <=> s(gen_0':s:nil:cons10_19(x))
gen_c3:c4:c5:c611_19(0) <=> c3
gen_c3:c4:c5:c611_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c611_19(x))
gen_c9:c10:c1112_19(0) <=> c9
gen_c9:c10:c1112_19(+(x, 1)) <=> c11(gen_c9:c10:c1112_19(x), c16, c12)
gen_c12:c13:c14:c1513_19(0) <=> c12
gen_c12:c13:c14:c1513_19(+(x, 1)) <=> c14(c7, gen_c12:c13:c14:c1513_19(x))
gen_c16:c17:c1814_19(0) <=> c16
gen_c16:c17:c1814_19(+(x, 1)) <=> c18(c7, gen_c16:c17:c1814_19(x))


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

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

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

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

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

Induction Step:
le(gen_0':s:nil:cons10_19(+(n1816_19, 1)), gen_0':s:nil:cons10_19(+(n1816_19, 1))) ->_R^Omega(0)
le(gen_0':s:nil:cons10_19(n1816_19), gen_0':s:nil:cons10_19(n1816_19)) ->_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))
IF(true, z0, z1) -> c7
IF(false, z0, z1) -> c8
MINSORT(nil) -> c9
MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c12
MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))
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)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, z2)))

Types:
LE :: 0':s:nil:cons -> 0':s:nil:cons -> c:c1:c2
0' :: 0':s:nil:cons
c :: c:c1:c2
s :: 0':s:nil:cons -> 0':s:nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s:nil:cons -> 0':s:nil:cons -> 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
IF :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> c7:c8
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c7:c8
MINSORT :: 0':s:nil:cons -> c9:c10:c11
nil :: 0':s:nil:cons
c9 :: c9:c10:c11
cons :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
c10 :: c12:c13:c14:c15 -> c9:c10:c11
MIN :: 0':s:nil:cons -> 0':s:nil:cons -> c12:c13:c14:c15
c11 :: c9:c10:c11 -> c16:c17:c18 -> c12:c13:c14:c15 -> c9:c10:c11
del :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
min :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
DEL :: 0':s:nil:cons -> 0':s:nil:cons -> c16:c17:c18
c12 :: c12:c13:c14:c15
c13 :: c7:c8 -> c:c1:c2 -> c12:c13:c14:c15
le :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c14 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c16:c17:c18
c17 :: c7:c8 -> c3:c4:c5:c6 -> c16:c17:c18
eq :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c18 :: c7:c8 -> c16:c17:c18 -> c16:c17:c18
if :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
minsort :: 0':s:nil:cons -> 0':s:nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s:nil:cons2_19 :: 0':s:nil:cons
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c84_19 :: c7:c8
hole_true:false5_19 :: true:false
hole_c9:c10:c116_19 :: c9:c10:c11
hole_c12:c13:c14:c157_19 :: c12:c13:c14:c15
hole_c16:c17:c188_19 :: c16:c17:c18
gen_c:c1:c29_19 :: Nat -> c:c1:c2
gen_0':s:nil:cons10_19 :: Nat -> 0':s:nil:cons
gen_c3:c4:c5:c611_19 :: Nat -> c3:c4:c5:c6
gen_c9:c10:c1112_19 :: Nat -> c9:c10:c11
gen_c12:c13:c14:c1513_19 :: Nat -> c12:c13:c14:c15
gen_c16:c17:c1814_19 :: Nat -> c16:c17:c18


Lemmas:
LE(gen_0':s:nil:cons10_19(n16_19), gen_0':s:nil:cons10_19(n16_19)) -> gen_c:c1:c29_19(n16_19), rt in Omega(1 + n16_19)
EQ(gen_0':s:nil:cons10_19(n728_19), gen_0':s:nil:cons10_19(n728_19)) -> gen_c3:c4:c5:c611_19(n728_19), rt in Omega(1 + n728_19)
le(gen_0':s:nil:cons10_19(n1816_19), gen_0':s:nil:cons10_19(n1816_19)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c29_19(0) <=> c
gen_c:c1:c29_19(+(x, 1)) <=> c2(gen_c:c1:c29_19(x))
gen_0':s:nil:cons10_19(0) <=> 0'
gen_0':s:nil:cons10_19(+(x, 1)) <=> s(gen_0':s:nil:cons10_19(x))
gen_c3:c4:c5:c611_19(0) <=> c3
gen_c3:c4:c5:c611_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c611_19(x))
gen_c9:c10:c1112_19(0) <=> c9
gen_c9:c10:c1112_19(+(x, 1)) <=> c11(gen_c9:c10:c1112_19(x), c16, c12)
gen_c12:c13:c14:c1513_19(0) <=> c12
gen_c12:c13:c14:c1513_19(+(x, 1)) <=> c14(c7, gen_c12:c13:c14:c1513_19(x))
gen_c16:c17:c1814_19(0) <=> c16
gen_c16:c17:c1814_19(+(x, 1)) <=> c18(c7, gen_c16:c17:c1814_19(x))


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

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

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

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

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

Induction Step:
eq(gen_0':s:nil:cons10_19(+(n2350_19, 1)), gen_0':s:nil:cons10_19(+(n2350_19, 1))) ->_R^Omega(0)
eq(gen_0':s:nil:cons10_19(n2350_19), gen_0':s:nil:cons10_19(n2350_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:
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))
IF(true, z0, z1) -> c7
IF(false, z0, z1) -> c8
MINSORT(nil) -> c9
MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
MIN(z0, nil) -> c12
MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
DEL(z0, nil) -> c16
DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))
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)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, z2)))

Types:
LE :: 0':s:nil:cons -> 0':s:nil:cons -> c:c1:c2
0' :: 0':s:nil:cons
c :: c:c1:c2
s :: 0':s:nil:cons -> 0':s:nil:cons
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
EQ :: 0':s:nil:cons -> 0':s:nil:cons -> 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
IF :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> c7:c8
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c7:c8
MINSORT :: 0':s:nil:cons -> c9:c10:c11
nil :: 0':s:nil:cons
c9 :: c9:c10:c11
cons :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
c10 :: c12:c13:c14:c15 -> c9:c10:c11
MIN :: 0':s:nil:cons -> 0':s:nil:cons -> c12:c13:c14:c15
c11 :: c9:c10:c11 -> c16:c17:c18 -> c12:c13:c14:c15 -> c9:c10:c11
del :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
min :: 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
DEL :: 0':s:nil:cons -> 0':s:nil:cons -> c16:c17:c18
c12 :: c12:c13:c14:c15
c13 :: c7:c8 -> c:c1:c2 -> c12:c13:c14:c15
le :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c14 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c7:c8 -> c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c16:c17:c18
c17 :: c7:c8 -> c3:c4:c5:c6 -> c16:c17:c18
eq :: 0':s:nil:cons -> 0':s:nil:cons -> true:false
c18 :: c7:c8 -> c16:c17:c18 -> c16:c17:c18
if :: true:false -> 0':s:nil:cons -> 0':s:nil:cons -> 0':s:nil:cons
minsort :: 0':s:nil:cons -> 0':s:nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s:nil:cons2_19 :: 0':s:nil:cons
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c84_19 :: c7:c8
hole_true:false5_19 :: true:false
hole_c9:c10:c116_19 :: c9:c10:c11
hole_c12:c13:c14:c157_19 :: c12:c13:c14:c15
hole_c16:c17:c188_19 :: c16:c17:c18
gen_c:c1:c29_19 :: Nat -> c:c1:c2
gen_0':s:nil:cons10_19 :: Nat -> 0':s:nil:cons
gen_c3:c4:c5:c611_19 :: Nat -> c3:c4:c5:c6
gen_c9:c10:c1112_19 :: Nat -> c9:c10:c11
gen_c12:c13:c14:c1513_19 :: Nat -> c12:c13:c14:c15
gen_c16:c17:c1814_19 :: Nat -> c16:c17:c18


Lemmas:
LE(gen_0':s:nil:cons10_19(n16_19), gen_0':s:nil:cons10_19(n16_19)) -> gen_c:c1:c29_19(n16_19), rt in Omega(1 + n16_19)
EQ(gen_0':s:nil:cons10_19(n728_19), gen_0':s:nil:cons10_19(n728_19)) -> gen_c3:c4:c5:c611_19(n728_19), rt in Omega(1 + n728_19)
le(gen_0':s:nil:cons10_19(n1816_19), gen_0':s:nil:cons10_19(n1816_19)) -> true, rt in Omega(0)
eq(gen_0':s:nil:cons10_19(n2350_19), gen_0':s:nil:cons10_19(n2350_19)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c29_19(0) <=> c
gen_c:c1:c29_19(+(x, 1)) <=> c2(gen_c:c1:c29_19(x))
gen_0':s:nil:cons10_19(0) <=> 0'
gen_0':s:nil:cons10_19(+(x, 1)) <=> s(gen_0':s:nil:cons10_19(x))
gen_c3:c4:c5:c611_19(0) <=> c3
gen_c3:c4:c5:c611_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c611_19(x))
gen_c9:c10:c1112_19(0) <=> c9
gen_c9:c10:c1112_19(+(x, 1)) <=> c11(gen_c9:c10:c1112_19(x), c16, c12)
gen_c12:c13:c14:c1513_19(0) <=> c12
gen_c12:c13:c14:c1513_19(+(x, 1)) <=> c14(c7, gen_c12:c13:c14:c1513_19(x))
gen_c16:c17:c1814_19(0) <=> c16
gen_c16:c17:c1814_19(+(x, 1)) <=> c18(c7, gen_c16:c17:c1814_19(x))


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 < DEL
del < minsort