WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 2089 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 33 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 313 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), 126 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 53 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 593 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 30 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 25 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 16 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 573 ms]
        (30) typed CpxTrs


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

(0)
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))
   MINSORT(nil) -> c7
   MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
   MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
   MIN(nil) -> c10
   MIN(cons(z0, nil)) -> c11
   MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
   IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
   IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
   RM(z0, nil) -> c15
   RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF2(true, z0, z1, z2) -> c17(RM(z0, z2))
   IF2(false, z0, z1, z2) -> c18(RM(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)
   minsort(nil) -> nil
   minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
   min(nil) -> 0
   min(cons(z0, nil)) -> z0
   min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> min(cons(z0, z2))
   if1(false, z0, z1, z2) -> min(cons(z1, z2))
   rm(z0, nil) -> nil
   rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
   if2(true, z0, z1, z2) -> rm(z0, z2)
   if2(false, z0, z1, z2) -> cons(z1, rm(z0, z2))

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

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
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))
   MINSORT(nil) -> c7
   MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
   MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
   MIN(nil) -> c10
   MIN(cons(z0, nil)) -> c11
   MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
   IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
   IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
   RM(z0, nil) -> c15
   RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF2(true, z0, z1, z2) -> c17(RM(z0, z2))
   IF2(false, z0, z1, z2) -> c18(RM(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)
   minsort(nil) -> nil
   minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
   min(nil) -> 0
   min(cons(z0, nil)) -> z0
   min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> min(cons(z0, z2))
   if1(false, z0, z1, z2) -> min(cons(z1, z2))
   rm(z0, nil) -> nil
   rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
   if2(true, z0, z1, z2) -> rm(z0, z2)
   if2(false, z0, z1, z2) -> cons(z1, rm(z0, z2))

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

(3) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(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))
   MINSORT(nil) -> c7
   MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
   MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
   MIN(nil) -> c10
   MIN(cons(z0, nil)) -> c11
   MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
   IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
   IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
   RM(z0, nil) -> c15
   RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF2(true, z0, z1, z2) -> c17(RM(z0, z2))
   IF2(false, z0, z1, z2) -> c18(RM(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)
   minsort(nil) -> nil
   minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
   min(nil) -> 0'
   min(cons(z0, nil)) -> z0
   min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> min(cons(z0, z2))
   if1(false, z0, z1, z2) -> min(cons(z1, z2))
   rm(z0, nil) -> nil
   rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
   if2(true, z0, z1, z2) -> rm(z0, z2)
   if2(false, z0, z1, z2) -> cons(z1, rm(z0, z2))

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
IF2/2

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

(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))
   MINSORT(nil) -> c7
   MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
   MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
   MIN(nil) -> c10
   MIN(cons(z0, nil)) -> c11
   MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
   IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
   IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
   RM(z0, nil) -> c15
   RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
   IF2(true, z0, z2) -> c17(RM(z0, z2))
   IF2(false, z0, z2) -> c18(RM(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)
   minsort(nil) -> nil
   minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
   min(nil) -> 0'
   min(cons(z0, nil)) -> z0
   min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> min(cons(z0, z2))
   if1(false, z0, z1, z2) -> min(cons(z1, z2))
   rm(z0, nil) -> nil
   rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
   if2(true, z0, z1, z2) -> rm(z0, z2)
   if2(false, z0, z1, z2) -> cons(z1, rm(z0, z2))

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

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered 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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons

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

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

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

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

(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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons


Generator Equations:
gen_c:c1:c211_19(0) <=> c
gen_c:c1:c211_19(+(x, 1)) <=> c2(gen_c:c1:c211_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c3:c4:c5:c613_19(0) <=> c3
gen_c3:c4:c5:c613_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_19(x))
gen_c7:c8:c914_19(0) <=> c7
gen_c7:c8:c914_19(+(x, 1)) <=> c9(gen_c7:c8:c914_19(x), c15, c10)
gen_nil:cons15_19(0) <=> nil
gen_nil:cons15_19(+(x, 1)) <=> cons(0', gen_nil:cons15_19(x))


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

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

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

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

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

Induction Step:
LE(gen_0':s12_19(+(n17_19, 1)), gen_0':s12_19(+(n17_19, 1))) ->_R^Omega(1)
c2(LE(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19))) ->_IH
c2(gen_c:c1:c211_19(c18_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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons


Generator Equations:
gen_c:c1:c211_19(0) <=> c
gen_c:c1:c211_19(+(x, 1)) <=> c2(gen_c:c1:c211_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c3:c4:c5:c613_19(0) <=> c3
gen_c3:c4:c5:c613_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_19(x))
gen_c7:c8:c914_19(0) <=> c7
gen_c7:c8:c914_19(+(x, 1)) <=> c9(gen_c7:c8:c914_19(x), c15, c10)
gen_nil:cons15_19(0) <=> nil
gen_nil:cons15_19(+(x, 1)) <=> cons(0', gen_nil:cons15_19(x))


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

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

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

(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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons


Lemmas:
LE(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c211_19(n17_19), rt in Omega(1 + n17_19)


Generator Equations:
gen_c:c1:c211_19(0) <=> c
gen_c:c1:c211_19(+(x, 1)) <=> c2(gen_c:c1:c211_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c3:c4:c5:c613_19(0) <=> c3
gen_c3:c4:c5:c613_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_19(x))
gen_c7:c8:c914_19(0) <=> c7
gen_c7:c8:c914_19(+(x, 1)) <=> c9(gen_c7:c8:c914_19(x), c15, c10)
gen_nil:cons15_19(0) <=> nil
gen_nil:cons15_19(+(x, 1)) <=> cons(0', gen_nil:cons15_19(x))


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

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

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

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

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

Induction Step:
EQ(gen_0':s12_19(+(n722_19, 1)), gen_0':s12_19(+(n722_19, 1))) ->_R^Omega(1)
c6(EQ(gen_0':s12_19(n722_19), gen_0':s12_19(n722_19))) ->_IH
c6(gen_c3:c4:c5:c613_19(c723_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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons


Lemmas:
LE(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c211_19(n17_19), rt in Omega(1 + n17_19)
EQ(gen_0':s12_19(n722_19), gen_0':s12_19(n722_19)) -> gen_c3:c4:c5:c613_19(n722_19), rt in Omega(1 + n722_19)


Generator Equations:
gen_c:c1:c211_19(0) <=> c
gen_c:c1:c211_19(+(x, 1)) <=> c2(gen_c:c1:c211_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c3:c4:c5:c613_19(0) <=> c3
gen_c3:c4:c5:c613_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_19(x))
gen_c7:c8:c914_19(0) <=> c7
gen_c7:c8:c914_19(+(x, 1)) <=> c9(gen_c7:c8:c914_19(x), c15, c10)
gen_nil:cons15_19(0) <=> nil
gen_nil:cons15_19(+(x, 1)) <=> cons(0', gen_nil:cons15_19(x))


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

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

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

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

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

Induction Step:
le(gen_0':s12_19(+(n1803_19, 1)), gen_0':s12_19(+(n1803_19, 1))) ->_R^Omega(0)
le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons


Lemmas:
LE(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c211_19(n17_19), rt in Omega(1 + n17_19)
EQ(gen_0':s12_19(n722_19), gen_0':s12_19(n722_19)) -> gen_c3:c4:c5:c613_19(n722_19), rt in Omega(1 + n722_19)
le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c211_19(0) <=> c
gen_c:c1:c211_19(+(x, 1)) <=> c2(gen_c:c1:c211_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c3:c4:c5:c613_19(0) <=> c3
gen_c3:c4:c5:c613_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_19(x))
gen_c7:c8:c914_19(0) <=> c7
gen_c7:c8:c914_19(+(x, 1)) <=> c9(gen_c7:c8:c914_19(x), c15, c10)
gen_nil:cons15_19(0) <=> nil
gen_nil:cons15_19(+(x, 1)) <=> cons(0', gen_nil:cons15_19(x))


The following defined symbols remain to be analysed:
MIN, MINSORT, rm, min, RM, eq, minsort

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

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MIN(gen_nil:cons15_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19)

Induction Base:
MIN(gen_nil:cons15_19(+(1, 0)))

Induction Step:
MIN(gen_nil:cons15_19(+(1, +(n2270_19, 1)))) ->_R^Omega(1)
c12(IF1(le(0', 0'), 0', 0', gen_nil:cons15_19(n2270_19)), LE(0', 0')) ->_L^Omega(0)
c12(IF1(true, 0', 0', gen_nil:cons15_19(n2270_19)), LE(0', 0')) ->_R^Omega(1)
c12(c13(MIN(cons(0', gen_nil:cons15_19(n2270_19)))), LE(0', 0')) ->_IH
c12(c13(*16_19), LE(0', 0')) ->_L^Omega(1)
c12(c13(*16_19), gen_c:c1:c211_19(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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons


Lemmas:
LE(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c211_19(n17_19), rt in Omega(1 + n17_19)
EQ(gen_0':s12_19(n722_19), gen_0':s12_19(n722_19)) -> gen_c3:c4:c5:c613_19(n722_19), rt in Omega(1 + n722_19)
le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0)
MIN(gen_nil:cons15_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19)


Generator Equations:
gen_c:c1:c211_19(0) <=> c
gen_c:c1:c211_19(+(x, 1)) <=> c2(gen_c:c1:c211_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c3:c4:c5:c613_19(0) <=> c3
gen_c3:c4:c5:c613_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_19(x))
gen_c7:c8:c914_19(0) <=> c7
gen_c7:c8:c914_19(+(x, 1)) <=> c9(gen_c7:c8:c914_19(x), c15, c10)
gen_nil:cons15_19(0) <=> nil
gen_nil:cons15_19(+(x, 1)) <=> cons(0', gen_nil:cons15_19(x))


The following defined symbols remain to be analysed:
min, MINSORT, rm, RM, eq, minsort

They will be analysed ascendingly in the following order:
rm < MINSORT
min < MINSORT
RM < MINSORT
eq < rm
rm < minsort
min < minsort
eq < RM

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
min(gen_nil:cons15_19(+(1, n7813_19))) -> gen_0':s12_19(0), rt in Omega(0)

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

Induction Step:
min(gen_nil:cons15_19(+(1, +(n7813_19, 1)))) ->_R^Omega(0)
if1(le(0', 0'), 0', 0', gen_nil:cons15_19(n7813_19)) ->_L^Omega(0)
if1(true, 0', 0', gen_nil:cons15_19(n7813_19)) ->_R^Omega(0)
min(cons(0', gen_nil:cons15_19(n7813_19))) ->_IH
gen_0':s12_19(0)

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

(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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons


Lemmas:
LE(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c211_19(n17_19), rt in Omega(1 + n17_19)
EQ(gen_0':s12_19(n722_19), gen_0':s12_19(n722_19)) -> gen_c3:c4:c5:c613_19(n722_19), rt in Omega(1 + n722_19)
le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0)
MIN(gen_nil:cons15_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19)
min(gen_nil:cons15_19(+(1, n7813_19))) -> gen_0':s12_19(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_19(0) <=> c
gen_c:c1:c211_19(+(x, 1)) <=> c2(gen_c:c1:c211_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c3:c4:c5:c613_19(0) <=> c3
gen_c3:c4:c5:c613_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_19(x))
gen_c7:c8:c914_19(0) <=> c7
gen_c7:c8:c914_19(+(x, 1)) <=> c9(gen_c7:c8:c914_19(x), c15, c10)
gen_nil:cons15_19(0) <=> nil
gen_nil:cons15_19(+(x, 1)) <=> cons(0', gen_nil:cons15_19(x))


The following defined symbols remain to be analysed:
eq, MINSORT, rm, RM, minsort

They will be analysed ascendingly in the following order:
rm < MINSORT
RM < MINSORT
eq < rm
rm < minsort
eq < RM

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

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

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

Induction Step:
eq(gen_0':s12_19(+(n8653_19, 1)), gen_0':s12_19(+(n8653_19, 1))) ->_R^Omega(0)
eq(gen_0':s12_19(n8653_19), gen_0':s12_19(n8653_19)) ->_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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons


Lemmas:
LE(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c211_19(n17_19), rt in Omega(1 + n17_19)
EQ(gen_0':s12_19(n722_19), gen_0':s12_19(n722_19)) -> gen_c3:c4:c5:c613_19(n722_19), rt in Omega(1 + n722_19)
le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0)
MIN(gen_nil:cons15_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19)
min(gen_nil:cons15_19(+(1, n7813_19))) -> gen_0':s12_19(0), rt in Omega(0)
eq(gen_0':s12_19(n8653_19), gen_0':s12_19(n8653_19)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c211_19(0) <=> c
gen_c:c1:c211_19(+(x, 1)) <=> c2(gen_c:c1:c211_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c3:c4:c5:c613_19(0) <=> c3
gen_c3:c4:c5:c613_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_19(x))
gen_c7:c8:c914_19(0) <=> c7
gen_c7:c8:c914_19(+(x, 1)) <=> c9(gen_c7:c8:c914_19(x), c15, c10)
gen_nil:cons15_19(0) <=> nil
gen_nil:cons15_19(+(x, 1)) <=> cons(0', gen_nil:cons15_19(x))


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

They will be analysed ascendingly in the following order:
rm < MINSORT
RM < MINSORT
rm < minsort

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
rm(gen_0':s12_19(0), gen_nil:cons15_19(n9410_19)) -> gen_nil:cons15_19(0), rt in Omega(0)

Induction Base:
rm(gen_0':s12_19(0), gen_nil:cons15_19(0)) ->_R^Omega(0)
nil

Induction Step:
rm(gen_0':s12_19(0), gen_nil:cons15_19(+(n9410_19, 1))) ->_R^Omega(0)
if2(eq(gen_0':s12_19(0), 0'), gen_0':s12_19(0), 0', gen_nil:cons15_19(n9410_19)) ->_L^Omega(0)
if2(true, gen_0':s12_19(0), 0', gen_nil:cons15_19(n9410_19)) ->_R^Omega(0)
rm(gen_0':s12_19(0), gen_nil:cons15_19(n9410_19)) ->_IH
gen_nil:cons15_19(0)

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

(28)
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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons


Lemmas:
LE(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c211_19(n17_19), rt in Omega(1 + n17_19)
EQ(gen_0':s12_19(n722_19), gen_0':s12_19(n722_19)) -> gen_c3:c4:c5:c613_19(n722_19), rt in Omega(1 + n722_19)
le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0)
MIN(gen_nil:cons15_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19)
min(gen_nil:cons15_19(+(1, n7813_19))) -> gen_0':s12_19(0), rt in Omega(0)
eq(gen_0':s12_19(n8653_19), gen_0':s12_19(n8653_19)) -> true, rt in Omega(0)
rm(gen_0':s12_19(0), gen_nil:cons15_19(n9410_19)) -> gen_nil:cons15_19(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_19(0) <=> c
gen_c:c1:c211_19(+(x, 1)) <=> c2(gen_c:c1:c211_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c3:c4:c5:c613_19(0) <=> c3
gen_c3:c4:c5:c613_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_19(x))
gen_c7:c8:c914_19(0) <=> c7
gen_c7:c8:c914_19(+(x, 1)) <=> c9(gen_c7:c8:c914_19(x), c15, c10)
gen_nil:cons15_19(0) <=> nil
gen_nil:cons15_19(+(x, 1)) <=> cons(0', gen_nil:cons15_19(x))


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

They will be analysed ascendingly in the following order:
RM < MINSORT

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
RM(gen_0':s12_19(0), gen_nil:cons15_19(n10630_19)) -> *16_19, rt in Omega(n10630_19)

Induction Base:
RM(gen_0':s12_19(0), gen_nil:cons15_19(0))

Induction Step:
RM(gen_0':s12_19(0), gen_nil:cons15_19(+(n10630_19, 1))) ->_R^Omega(1)
c16(IF2(eq(gen_0':s12_19(0), 0'), gen_0':s12_19(0), gen_nil:cons15_19(n10630_19)), EQ(gen_0':s12_19(0), 0')) ->_L^Omega(0)
c16(IF2(true, gen_0':s12_19(0), gen_nil:cons15_19(n10630_19)), EQ(gen_0':s12_19(0), 0')) ->_R^Omega(1)
c16(c17(RM(gen_0':s12_19(0), gen_nil:cons15_19(n10630_19))), EQ(gen_0':s12_19(0), 0')) ->_IH
c16(c17(*16_19), EQ(gen_0':s12_19(0), 0')) ->_L^Omega(1)
c16(c17(*16_19), gen_c3:c4:c5:c613_19(0))

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

(30)
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))
MINSORT(nil) -> c7
MINSORT(cons(z0, z1)) -> c8(MIN(cons(z0, z1)))
MINSORT(cons(z0, z1)) -> c9(MINSORT(rm(min(cons(z0, z1)), cons(z0, z1))), RM(min(cons(z0, z1)), cons(z0, z1)), MIN(cons(z0, z1)))
MIN(nil) -> c10
MIN(cons(z0, nil)) -> c11
MIN(cons(z0, cons(z1, z2))) -> c12(IF1(le(z0, z1), z0, z1, z2), LE(z0, z1))
IF1(true, z0, z1, z2) -> c13(MIN(cons(z0, z2)))
IF1(false, z0, z1, z2) -> c14(MIN(cons(z1, z2)))
RM(z0, nil) -> c15
RM(z0, cons(z1, z2)) -> c16(IF2(eq(z0, z1), z0, z2), EQ(z0, z1))
IF2(true, z0, z2) -> c17(RM(z0, z2))
IF2(false, z0, z2) -> c18(RM(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)
minsort(nil) -> nil
minsort(cons(z0, z1)) -> cons(min(cons(z0, z1)), minsort(rm(min(cons(z0, z1)), cons(z0, z1))))
min(nil) -> 0'
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if1(le(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> min(cons(z0, z2))
if1(false, z0, z1, z2) -> min(cons(z1, z2))
rm(z0, nil) -> nil
rm(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2)
if2(true, z0, z1, z2) -> rm(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, rm(z0, 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
MINSORT :: nil:cons -> c7:c8:c9
nil :: nil:cons
c7 :: c7:c8:c9
cons :: 0':s -> nil:cons -> nil:cons
c8 :: c10:c11:c12 -> c7:c8:c9
MIN :: nil:cons -> c10:c11:c12
c9 :: c7:c8:c9 -> c15:c16 -> c10:c11:c12 -> c7:c8:c9
rm :: 0':s -> nil:cons -> nil:cons
min :: nil:cons -> 0':s
RM :: 0':s -> nil:cons -> c15:c16
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c13:c14 -> c:c1:c2 -> c10:c11:c12
IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c13:c14
le :: 0':s -> 0':s -> true:false
true :: true:false
c13 :: c10:c11:c12 -> c13:c14
false :: true:false
c14 :: c10:c11:c12 -> c13:c14
c15 :: c15:c16
c16 :: c17:c18 -> c3:c4:c5:c6 -> c15:c16
IF2 :: true:false -> 0':s -> nil:cons -> c17:c18
eq :: 0':s -> 0':s -> true:false
c17 :: c15:c16 -> c17:c18
c18 :: c15:c16 -> c17:c18
minsort :: nil:cons -> nil:cons
if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s
if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_19 :: c:c1:c2
hole_0':s2_19 :: 0':s
hole_c3:c4:c5:c63_19 :: c3:c4:c5:c6
hole_c7:c8:c94_19 :: c7:c8:c9
hole_nil:cons5_19 :: nil:cons
hole_c10:c11:c126_19 :: c10:c11:c12
hole_c15:c167_19 :: c15:c16
hole_c13:c148_19 :: c13:c14
hole_true:false9_19 :: true:false
hole_c17:c1810_19 :: c17:c18
gen_c:c1:c211_19 :: Nat -> c:c1:c2
gen_0':s12_19 :: Nat -> 0':s
gen_c3:c4:c5:c613_19 :: Nat -> c3:c4:c5:c6
gen_c7:c8:c914_19 :: Nat -> c7:c8:c9
gen_nil:cons15_19 :: Nat -> nil:cons


Lemmas:
LE(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c211_19(n17_19), rt in Omega(1 + n17_19)
EQ(gen_0':s12_19(n722_19), gen_0':s12_19(n722_19)) -> gen_c3:c4:c5:c613_19(n722_19), rt in Omega(1 + n722_19)
le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0)
MIN(gen_nil:cons15_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19)
min(gen_nil:cons15_19(+(1, n7813_19))) -> gen_0':s12_19(0), rt in Omega(0)
eq(gen_0':s12_19(n8653_19), gen_0':s12_19(n8653_19)) -> true, rt in Omega(0)
rm(gen_0':s12_19(0), gen_nil:cons15_19(n9410_19)) -> gen_nil:cons15_19(0), rt in Omega(0)
RM(gen_0':s12_19(0), gen_nil:cons15_19(n10630_19)) -> *16_19, rt in Omega(n10630_19)


Generator Equations:
gen_c:c1:c211_19(0) <=> c
gen_c:c1:c211_19(+(x, 1)) <=> c2(gen_c:c1:c211_19(x))
gen_0':s12_19(0) <=> 0'
gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x))
gen_c3:c4:c5:c613_19(0) <=> c3
gen_c3:c4:c5:c613_19(+(x, 1)) <=> c6(gen_c3:c4:c5:c613_19(x))
gen_c7:c8:c914_19(0) <=> c7
gen_c7:c8:c914_19(+(x, 1)) <=> c9(gen_c7:c8:c914_19(x), c15, c10)
gen_nil:cons15_19(0) <=> nil
gen_nil:cons15_19(+(x, 1)) <=> cons(0', gen_nil:cons15_19(x))


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