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), 1771 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), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 386 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), 99 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 34 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 678 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 45 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 9 ms]
        (26) 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:

   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   MIN(cons(z0, nil)) -> c7
   MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
   IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
   IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
   REPLACE(z0, z1, nil) -> c11
   REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
   IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
   IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
   EMPTY(nil) -> c15
   EMPTY(cons(z0, z1)) -> c16
   HEAD(cons(z0, z1)) -> c17
   TAIL(nil) -> c18
   TAIL(cons(z0, z1)) -> c19
   SORT(z0) -> c20(SORTITER(z0, nil))
   SORTITER(z0, z1) -> c21(IF(empty(z0), z0, z1, append(z1, cons(min(z0), nil))), EMPTY(z0))
   SORTITER(z0, z1) -> c22(IF(empty(z0), z0, z1, append(z1, cons(min(z0), nil))), MIN(z0))
   IF(true, z0, z1, z2) -> c23
   IF(false, z0, z1, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0)), z2), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
   IF(false, z0, z1, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0)), z2), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
   IF(false, z0, z1, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0)), z2), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))

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

   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   min(cons(z0, nil)) -> z0
   min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
   if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
   if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
   replace(z0, z1, nil) -> nil
   replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
   if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
   if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   sort(z0) -> sortIter(z0, nil)
   sortIter(z0, z1) -> if(empty(z0), z0, z1, append(z1, cons(min(z0), nil)))
   if(true, z0, z1, z2) -> z1
   if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(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:

   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   MIN(cons(z0, nil)) -> c7
   MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
   IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
   IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
   REPLACE(z0, z1, nil) -> c11
   REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
   IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
   IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
   EMPTY(nil) -> c15
   EMPTY(cons(z0, z1)) -> c16
   HEAD(cons(z0, z1)) -> c17
   TAIL(nil) -> c18
   TAIL(cons(z0, z1)) -> c19
   SORT(z0) -> c20(SORTITER(z0, nil))
   SORTITER(z0, z1) -> c21(IF(empty(z0), z0, z1, append(z1, cons(min(z0), nil))), EMPTY(z0))
   SORTITER(z0, z1) -> c22(IF(empty(z0), z0, z1, append(z1, cons(min(z0), nil))), MIN(z0))
   IF(true, z0, z1, z2) -> c23
   IF(false, z0, z1, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0)), z2), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
   IF(false, z0, z1, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0)), z2), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
   IF(false, z0, z1, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0)), z2), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))

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

   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   min(cons(z0, nil)) -> z0
   min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
   if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
   if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
   replace(z0, z1, nil) -> nil
   replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
   if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
   if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   sort(z0) -> sortIter(z0, nil)
   sortIter(z0, z1) -> if(empty(z0), z0, z1, append(z1, cons(min(z0), nil)))
   if(true, z0, z1, z2) -> z1
   if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(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:

   EQ(0', 0') -> c
   EQ(0', s(z0)) -> c1
   EQ(s(z0), 0') -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LE(0', z0) -> c4
   LE(s(z0), 0') -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   MIN(cons(z0, nil)) -> c7
   MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
   IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
   IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
   REPLACE(z0, z1, nil) -> c11
   REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
   IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
   IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
   EMPTY(nil) -> c15
   EMPTY(cons(z0, z1)) -> c16
   HEAD(cons(z0, z1)) -> c17
   TAIL(nil) -> c18
   TAIL(cons(z0, z1)) -> c19
   SORT(z0) -> c20(SORTITER(z0, nil))
   SORTITER(z0, z1) -> c21(IF(empty(z0), z0, z1, append(z1, cons(min(z0), nil))), EMPTY(z0))
   SORTITER(z0, z1) -> c22(IF(empty(z0), z0, z1, append(z1, cons(min(z0), nil))), MIN(z0))
   IF(true, z0, z1, z2) -> c23
   IF(false, z0, z1, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0)), z2), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
   IF(false, z0, z1, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0)), z2), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
   IF(false, z0, z1, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0)), z2), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))

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

   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   min(cons(z0, nil)) -> z0
   min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
   if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
   if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
   replace(z0, z1, nil) -> nil
   replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
   if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
   if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   sort(z0) -> sortIter(z0, nil)
   sortIter(z0, z1) -> if(empty(z0), z0, z1, append(z1, cons(min(z0), nil)))
   if(true, z0, z1, z2) -> z1
   if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
SORTITER/1
IF/2
append/0

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

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

   EQ(0', 0') -> c
   EQ(0', s(z0)) -> c1
   EQ(s(z0), 0') -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LE(0', z0) -> c4
   LE(s(z0), 0') -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   MIN(cons(z0, nil)) -> c7
   MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
   IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
   IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
   REPLACE(z0, z1, nil) -> c11
   REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
   IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
   IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
   EMPTY(nil) -> c15
   EMPTY(cons(z0, z1)) -> c16
   HEAD(cons(z0, z1)) -> c17
   TAIL(nil) -> c18
   TAIL(cons(z0, z1)) -> c19
   SORT(z0) -> c20(SORTITER(z0))
   SORTITER(z0) -> c21(IF(empty(z0), z0, append(cons(min(z0), nil))), EMPTY(z0))
   SORTITER(z0) -> c22(IF(empty(z0), z0, append(cons(min(z0), nil))), MIN(z0))
   IF(true, z0, z2) -> c23
   IF(false, z0, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
   IF(false, z0, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
   IF(false, z0, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))

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

   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   min(cons(z0, nil)) -> z0
   min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
   if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
   if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
   replace(z0, z1, nil) -> nil
   replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
   if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
   if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   sort(z0) -> sortIter(z0, nil)
   sortIter(z0, z1) -> if(empty(z0), z0, z1, append(cons(min(z0), nil)))
   if(true, z0, z1, z2) -> z1
   if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

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

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

(8)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
MIN(cons(z0, nil)) -> c7
MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
REPLACE(z0, z1, nil) -> c11
REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
EMPTY(nil) -> c15
EMPTY(cons(z0, z1)) -> c16
HEAD(cons(z0, z1)) -> c17
TAIL(nil) -> c18
TAIL(cons(z0, z1)) -> c19
SORT(z0) -> c20(SORTITER(z0))
SORTITER(z0) -> c21(IF(empty(z0), z0, append(cons(min(z0), nil))), EMPTY(z0))
SORTITER(z0) -> c22(IF(empty(z0), z0, append(cons(min(z0), nil))), MIN(z0))
IF(true, z0, z2) -> c23
IF(false, z0, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
IF(false, z0, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
IF(false, z0, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
replace(z0, z1, nil) -> nil
replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
sort(z0) -> sortIter(z0, nil)
sortIter(z0, z1) -> if(empty(z0), z0, z1, append(cons(min(z0), nil)))
if(true, z0, z1, z2) -> z1
if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
MIN :: nil:cons:append -> c7:c8
cons :: 0':s -> nil:cons:append -> nil:cons:append
nil :: nil:cons:append
c7 :: c7:c8
c8 :: c9:c10 -> c4:c5:c6 -> c7:c8
IF_MIN :: true:false -> nil:cons:append -> c9:c10
le :: 0':s -> 0':s -> true:false
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
REPLACE :: 0':s -> 0':s -> nil:cons:append -> c11:c12
c11 :: c11:c12
c12 :: c13:c14 -> c:c1:c2:c3 -> c11:c12
IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons:append -> c13:c14
eq :: 0':s -> 0':s -> true:false
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14
EMPTY :: nil:cons:append -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
HEAD :: nil:cons:append -> c17
c17 :: c17
TAIL :: nil:cons:append -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
SORT :: nil:cons:append -> c20
c20 :: c21:c22 -> c20
SORTITER :: nil:cons:append -> c21:c22
c21 :: c23:c24:c25:c26 -> c15:c16 -> c21:c22
IF :: true:false -> nil:cons:append -> nil:cons:append -> c23:c24:c25:c26
empty :: nil:cons:append -> true:false
append :: nil:cons:append -> nil:cons:append
min :: nil:cons:append -> 0':s
c22 :: c23:c24:c25:c26 -> c7:c8 -> c21:c22
c23 :: c23:c24:c25:c26
c24 :: c21:c22 -> c11:c12 -> c7:c8 -> c23:c24:c25:c26
replace :: 0':s -> 0':s -> nil:cons:append -> nil:cons:append
head :: nil:cons:append -> 0':s
tail :: nil:cons:append -> nil:cons:append
c25 :: c21:c22 -> c11:c12 -> c17 -> c23:c24:c25:c26
c26 :: c21:c22 -> c11:c12 -> c18:c19 -> c23:c24:c25:c26
if_min :: true:false -> nil:cons:append -> 0':s
if_replace :: true:false -> 0':s -> 0':s -> nil:cons:append -> nil:cons:append
sort :: nil:cons:append -> nil:cons:append
sortIter :: nil:cons:append -> nil:cons:append -> nil:cons:append
if :: true:false -> nil:cons:append -> nil:cons:append -> nil:cons:append -> nil:cons:append
hole_c:c1:c2:c31_27 :: c:c1:c2:c3
hole_0':s2_27 :: 0':s
hole_c4:c5:c63_27 :: c4:c5:c6
hole_c7:c84_27 :: c7:c8
hole_nil:cons:append5_27 :: nil:cons:append
hole_c9:c106_27 :: c9:c10
hole_true:false7_27 :: true:false
hole_c11:c128_27 :: c11:c12
hole_c13:c149_27 :: c13:c14
hole_c15:c1610_27 :: c15:c16
hole_c1711_27 :: c17
hole_c18:c1912_27 :: c18:c19
hole_c2013_27 :: c20
hole_c21:c2214_27 :: c21:c22
hole_c23:c24:c25:c2615_27 :: c23:c24:c25:c26
gen_c:c1:c2:c316_27 :: Nat -> c:c1:c2:c3
gen_0':s17_27 :: Nat -> 0':s
gen_c4:c5:c618_27 :: Nat -> c4:c5:c6
gen_nil:cons:append19_27 :: Nat -> nil:cons:append

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
EQ, LE, MIN, le, REPLACE, eq, SORTITER, min, replace, sortIter

They will be analysed ascendingly in the following order:
EQ < REPLACE
LE < MIN
le < MIN
MIN < SORTITER
le < min
eq < REPLACE
REPLACE < SORTITER
eq < replace
min < SORTITER
replace < SORTITER
min < sortIter
replace < sortIter

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

(10)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
MIN(cons(z0, nil)) -> c7
MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
REPLACE(z0, z1, nil) -> c11
REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
EMPTY(nil) -> c15
EMPTY(cons(z0, z1)) -> c16
HEAD(cons(z0, z1)) -> c17
TAIL(nil) -> c18
TAIL(cons(z0, z1)) -> c19
SORT(z0) -> c20(SORTITER(z0))
SORTITER(z0) -> c21(IF(empty(z0), z0, append(cons(min(z0), nil))), EMPTY(z0))
SORTITER(z0) -> c22(IF(empty(z0), z0, append(cons(min(z0), nil))), MIN(z0))
IF(true, z0, z2) -> c23
IF(false, z0, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
IF(false, z0, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
IF(false, z0, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
replace(z0, z1, nil) -> nil
replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
sort(z0) -> sortIter(z0, nil)
sortIter(z0, z1) -> if(empty(z0), z0, z1, append(cons(min(z0), nil)))
if(true, z0, z1, z2) -> z1
if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
MIN :: nil:cons:append -> c7:c8
cons :: 0':s -> nil:cons:append -> nil:cons:append
nil :: nil:cons:append
c7 :: c7:c8
c8 :: c9:c10 -> c4:c5:c6 -> c7:c8
IF_MIN :: true:false -> nil:cons:append -> c9:c10
le :: 0':s -> 0':s -> true:false
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
REPLACE :: 0':s -> 0':s -> nil:cons:append -> c11:c12
c11 :: c11:c12
c12 :: c13:c14 -> c:c1:c2:c3 -> c11:c12
IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons:append -> c13:c14
eq :: 0':s -> 0':s -> true:false
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14
EMPTY :: nil:cons:append -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
HEAD :: nil:cons:append -> c17
c17 :: c17
TAIL :: nil:cons:append -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
SORT :: nil:cons:append -> c20
c20 :: c21:c22 -> c20
SORTITER :: nil:cons:append -> c21:c22
c21 :: c23:c24:c25:c26 -> c15:c16 -> c21:c22
IF :: true:false -> nil:cons:append -> nil:cons:append -> c23:c24:c25:c26
empty :: nil:cons:append -> true:false
append :: nil:cons:append -> nil:cons:append
min :: nil:cons:append -> 0':s
c22 :: c23:c24:c25:c26 -> c7:c8 -> c21:c22
c23 :: c23:c24:c25:c26
c24 :: c21:c22 -> c11:c12 -> c7:c8 -> c23:c24:c25:c26
replace :: 0':s -> 0':s -> nil:cons:append -> nil:cons:append
head :: nil:cons:append -> 0':s
tail :: nil:cons:append -> nil:cons:append
c25 :: c21:c22 -> c11:c12 -> c17 -> c23:c24:c25:c26
c26 :: c21:c22 -> c11:c12 -> c18:c19 -> c23:c24:c25:c26
if_min :: true:false -> nil:cons:append -> 0':s
if_replace :: true:false -> 0':s -> 0':s -> nil:cons:append -> nil:cons:append
sort :: nil:cons:append -> nil:cons:append
sortIter :: nil:cons:append -> nil:cons:append -> nil:cons:append
if :: true:false -> nil:cons:append -> nil:cons:append -> nil:cons:append -> nil:cons:append
hole_c:c1:c2:c31_27 :: c:c1:c2:c3
hole_0':s2_27 :: 0':s
hole_c4:c5:c63_27 :: c4:c5:c6
hole_c7:c84_27 :: c7:c8
hole_nil:cons:append5_27 :: nil:cons:append
hole_c9:c106_27 :: c9:c10
hole_true:false7_27 :: true:false
hole_c11:c128_27 :: c11:c12
hole_c13:c149_27 :: c13:c14
hole_c15:c1610_27 :: c15:c16
hole_c1711_27 :: c17
hole_c18:c1912_27 :: c18:c19
hole_c2013_27 :: c20
hole_c21:c2214_27 :: c21:c22
hole_c23:c24:c25:c2615_27 :: c23:c24:c25:c26
gen_c:c1:c2:c316_27 :: Nat -> c:c1:c2:c3
gen_0':s17_27 :: Nat -> 0':s
gen_c4:c5:c618_27 :: Nat -> c4:c5:c6
gen_nil:cons:append19_27 :: Nat -> nil:cons:append


Generator Equations:
gen_c:c1:c2:c316_27(0) <=> c
gen_c:c1:c2:c316_27(+(x, 1)) <=> c3(gen_c:c1:c2:c316_27(x))
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c4:c5:c618_27(0) <=> c4
gen_c4:c5:c618_27(+(x, 1)) <=> c6(gen_c4:c5:c618_27(x))
gen_nil:cons:append19_27(0) <=> nil
gen_nil:cons:append19_27(+(x, 1)) <=> cons(0', gen_nil:cons:append19_27(x))


The following defined symbols remain to be analysed:
EQ, LE, MIN, le, REPLACE, eq, SORTITER, min, replace, sortIter

They will be analysed ascendingly in the following order:
EQ < REPLACE
LE < MIN
le < MIN
MIN < SORTITER
le < min
eq < REPLACE
REPLACE < SORTITER
eq < replace
min < SORTITER
replace < SORTITER
min < sortIter
replace < sortIter

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s17_27(n21_27), gen_0':s17_27(n21_27)) -> gen_c:c1:c2:c316_27(n21_27), rt in Omega(1 + n21_27)

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

Induction Step:
EQ(gen_0':s17_27(+(n21_27, 1)), gen_0':s17_27(+(n21_27, 1))) ->_R^Omega(1)
c3(EQ(gen_0':s17_27(n21_27), gen_0':s17_27(n21_27))) ->_IH
c3(gen_c:c1:c2:c316_27(c22_27))

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:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
MIN(cons(z0, nil)) -> c7
MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
REPLACE(z0, z1, nil) -> c11
REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
EMPTY(nil) -> c15
EMPTY(cons(z0, z1)) -> c16
HEAD(cons(z0, z1)) -> c17
TAIL(nil) -> c18
TAIL(cons(z0, z1)) -> c19
SORT(z0) -> c20(SORTITER(z0))
SORTITER(z0) -> c21(IF(empty(z0), z0, append(cons(min(z0), nil))), EMPTY(z0))
SORTITER(z0) -> c22(IF(empty(z0), z0, append(cons(min(z0), nil))), MIN(z0))
IF(true, z0, z2) -> c23
IF(false, z0, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
IF(false, z0, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
IF(false, z0, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
replace(z0, z1, nil) -> nil
replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
sort(z0) -> sortIter(z0, nil)
sortIter(z0, z1) -> if(empty(z0), z0, z1, append(cons(min(z0), nil)))
if(true, z0, z1, z2) -> z1
if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
MIN :: nil:cons:append -> c7:c8
cons :: 0':s -> nil:cons:append -> nil:cons:append
nil :: nil:cons:append
c7 :: c7:c8
c8 :: c9:c10 -> c4:c5:c6 -> c7:c8
IF_MIN :: true:false -> nil:cons:append -> c9:c10
le :: 0':s -> 0':s -> true:false
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
REPLACE :: 0':s -> 0':s -> nil:cons:append -> c11:c12
c11 :: c11:c12
c12 :: c13:c14 -> c:c1:c2:c3 -> c11:c12
IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons:append -> c13:c14
eq :: 0':s -> 0':s -> true:false
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14
EMPTY :: nil:cons:append -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
HEAD :: nil:cons:append -> c17
c17 :: c17
TAIL :: nil:cons:append -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
SORT :: nil:cons:append -> c20
c20 :: c21:c22 -> c20
SORTITER :: nil:cons:append -> c21:c22
c21 :: c23:c24:c25:c26 -> c15:c16 -> c21:c22
IF :: true:false -> nil:cons:append -> nil:cons:append -> c23:c24:c25:c26
empty :: nil:cons:append -> true:false
append :: nil:cons:append -> nil:cons:append
min :: nil:cons:append -> 0':s
c22 :: c23:c24:c25:c26 -> c7:c8 -> c21:c22
c23 :: c23:c24:c25:c26
c24 :: c21:c22 -> c11:c12 -> c7:c8 -> c23:c24:c25:c26
replace :: 0':s -> 0':s -> nil:cons:append -> nil:cons:append
head :: nil:cons:append -> 0':s
tail :: nil:cons:append -> nil:cons:append
c25 :: c21:c22 -> c11:c12 -> c17 -> c23:c24:c25:c26
c26 :: c21:c22 -> c11:c12 -> c18:c19 -> c23:c24:c25:c26
if_min :: true:false -> nil:cons:append -> 0':s
if_replace :: true:false -> 0':s -> 0':s -> nil:cons:append -> nil:cons:append
sort :: nil:cons:append -> nil:cons:append
sortIter :: nil:cons:append -> nil:cons:append -> nil:cons:append
if :: true:false -> nil:cons:append -> nil:cons:append -> nil:cons:append -> nil:cons:append
hole_c:c1:c2:c31_27 :: c:c1:c2:c3
hole_0':s2_27 :: 0':s
hole_c4:c5:c63_27 :: c4:c5:c6
hole_c7:c84_27 :: c7:c8
hole_nil:cons:append5_27 :: nil:cons:append
hole_c9:c106_27 :: c9:c10
hole_true:false7_27 :: true:false
hole_c11:c128_27 :: c11:c12
hole_c13:c149_27 :: c13:c14
hole_c15:c1610_27 :: c15:c16
hole_c1711_27 :: c17
hole_c18:c1912_27 :: c18:c19
hole_c2013_27 :: c20
hole_c21:c2214_27 :: c21:c22
hole_c23:c24:c25:c2615_27 :: c23:c24:c25:c26
gen_c:c1:c2:c316_27 :: Nat -> c:c1:c2:c3
gen_0':s17_27 :: Nat -> 0':s
gen_c4:c5:c618_27 :: Nat -> c4:c5:c6
gen_nil:cons:append19_27 :: Nat -> nil:cons:append


Generator Equations:
gen_c:c1:c2:c316_27(0) <=> c
gen_c:c1:c2:c316_27(+(x, 1)) <=> c3(gen_c:c1:c2:c316_27(x))
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c4:c5:c618_27(0) <=> c4
gen_c4:c5:c618_27(+(x, 1)) <=> c6(gen_c4:c5:c618_27(x))
gen_nil:cons:append19_27(0) <=> nil
gen_nil:cons:append19_27(+(x, 1)) <=> cons(0', gen_nil:cons:append19_27(x))


The following defined symbols remain to be analysed:
EQ, LE, MIN, le, REPLACE, eq, SORTITER, min, replace, sortIter

They will be analysed ascendingly in the following order:
EQ < REPLACE
LE < MIN
le < MIN
MIN < SORTITER
le < min
eq < REPLACE
REPLACE < SORTITER
eq < replace
min < SORTITER
replace < SORTITER
min < sortIter
replace < sortIter

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
MIN(cons(z0, nil)) -> c7
MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
REPLACE(z0, z1, nil) -> c11
REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
EMPTY(nil) -> c15
EMPTY(cons(z0, z1)) -> c16
HEAD(cons(z0, z1)) -> c17
TAIL(nil) -> c18
TAIL(cons(z0, z1)) -> c19
SORT(z0) -> c20(SORTITER(z0))
SORTITER(z0) -> c21(IF(empty(z0), z0, append(cons(min(z0), nil))), EMPTY(z0))
SORTITER(z0) -> c22(IF(empty(z0), z0, append(cons(min(z0), nil))), MIN(z0))
IF(true, z0, z2) -> c23
IF(false, z0, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
IF(false, z0, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
IF(false, z0, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
replace(z0, z1, nil) -> nil
replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
sort(z0) -> sortIter(z0, nil)
sortIter(z0, z1) -> if(empty(z0), z0, z1, append(cons(min(z0), nil)))
if(true, z0, z1, z2) -> z1
if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
MIN :: nil:cons:append -> c7:c8
cons :: 0':s -> nil:cons:append -> nil:cons:append
nil :: nil:cons:append
c7 :: c7:c8
c8 :: c9:c10 -> c4:c5:c6 -> c7:c8
IF_MIN :: true:false -> nil:cons:append -> c9:c10
le :: 0':s -> 0':s -> true:false
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
REPLACE :: 0':s -> 0':s -> nil:cons:append -> c11:c12
c11 :: c11:c12
c12 :: c13:c14 -> c:c1:c2:c3 -> c11:c12
IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons:append -> c13:c14
eq :: 0':s -> 0':s -> true:false
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14
EMPTY :: nil:cons:append -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
HEAD :: nil:cons:append -> c17
c17 :: c17
TAIL :: nil:cons:append -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
SORT :: nil:cons:append -> c20
c20 :: c21:c22 -> c20
SORTITER :: nil:cons:append -> c21:c22
c21 :: c23:c24:c25:c26 -> c15:c16 -> c21:c22
IF :: true:false -> nil:cons:append -> nil:cons:append -> c23:c24:c25:c26
empty :: nil:cons:append -> true:false
append :: nil:cons:append -> nil:cons:append
min :: nil:cons:append -> 0':s
c22 :: c23:c24:c25:c26 -> c7:c8 -> c21:c22
c23 :: c23:c24:c25:c26
c24 :: c21:c22 -> c11:c12 -> c7:c8 -> c23:c24:c25:c26
replace :: 0':s -> 0':s -> nil:cons:append -> nil:cons:append
head :: nil:cons:append -> 0':s
tail :: nil:cons:append -> nil:cons:append
c25 :: c21:c22 -> c11:c12 -> c17 -> c23:c24:c25:c26
c26 :: c21:c22 -> c11:c12 -> c18:c19 -> c23:c24:c25:c26
if_min :: true:false -> nil:cons:append -> 0':s
if_replace :: true:false -> 0':s -> 0':s -> nil:cons:append -> nil:cons:append
sort :: nil:cons:append -> nil:cons:append
sortIter :: nil:cons:append -> nil:cons:append -> nil:cons:append
if :: true:false -> nil:cons:append -> nil:cons:append -> nil:cons:append -> nil:cons:append
hole_c:c1:c2:c31_27 :: c:c1:c2:c3
hole_0':s2_27 :: 0':s
hole_c4:c5:c63_27 :: c4:c5:c6
hole_c7:c84_27 :: c7:c8
hole_nil:cons:append5_27 :: nil:cons:append
hole_c9:c106_27 :: c9:c10
hole_true:false7_27 :: true:false
hole_c11:c128_27 :: c11:c12
hole_c13:c149_27 :: c13:c14
hole_c15:c1610_27 :: c15:c16
hole_c1711_27 :: c17
hole_c18:c1912_27 :: c18:c19
hole_c2013_27 :: c20
hole_c21:c2214_27 :: c21:c22
hole_c23:c24:c25:c2615_27 :: c23:c24:c25:c26
gen_c:c1:c2:c316_27 :: Nat -> c:c1:c2:c3
gen_0':s17_27 :: Nat -> 0':s
gen_c4:c5:c618_27 :: Nat -> c4:c5:c6
gen_nil:cons:append19_27 :: Nat -> nil:cons:append


Lemmas:
EQ(gen_0':s17_27(n21_27), gen_0':s17_27(n21_27)) -> gen_c:c1:c2:c316_27(n21_27), rt in Omega(1 + n21_27)


Generator Equations:
gen_c:c1:c2:c316_27(0) <=> c
gen_c:c1:c2:c316_27(+(x, 1)) <=> c3(gen_c:c1:c2:c316_27(x))
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c4:c5:c618_27(0) <=> c4
gen_c4:c5:c618_27(+(x, 1)) <=> c6(gen_c4:c5:c618_27(x))
gen_nil:cons:append19_27(0) <=> nil
gen_nil:cons:append19_27(+(x, 1)) <=> cons(0', gen_nil:cons:append19_27(x))


The following defined symbols remain to be analysed:
LE, MIN, le, REPLACE, eq, SORTITER, min, replace, sortIter

They will be analysed ascendingly in the following order:
LE < MIN
le < MIN
MIN < SORTITER
le < min
eq < REPLACE
REPLACE < SORTITER
eq < replace
min < SORTITER
replace < SORTITER
min < sortIter
replace < sortIter

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s17_27(n1115_27), gen_0':s17_27(n1115_27)) -> gen_c4:c5:c618_27(n1115_27), rt in Omega(1 + n1115_27)

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

Induction Step:
LE(gen_0':s17_27(+(n1115_27, 1)), gen_0':s17_27(+(n1115_27, 1))) ->_R^Omega(1)
c6(LE(gen_0':s17_27(n1115_27), gen_0':s17_27(n1115_27))) ->_IH
c6(gen_c4:c5:c618_27(c1116_27))

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:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
MIN(cons(z0, nil)) -> c7
MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
REPLACE(z0, z1, nil) -> c11
REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
EMPTY(nil) -> c15
EMPTY(cons(z0, z1)) -> c16
HEAD(cons(z0, z1)) -> c17
TAIL(nil) -> c18
TAIL(cons(z0, z1)) -> c19
SORT(z0) -> c20(SORTITER(z0))
SORTITER(z0) -> c21(IF(empty(z0), z0, append(cons(min(z0), nil))), EMPTY(z0))
SORTITER(z0) -> c22(IF(empty(z0), z0, append(cons(min(z0), nil))), MIN(z0))
IF(true, z0, z2) -> c23
IF(false, z0, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
IF(false, z0, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
IF(false, z0, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
replace(z0, z1, nil) -> nil
replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
sort(z0) -> sortIter(z0, nil)
sortIter(z0, z1) -> if(empty(z0), z0, z1, append(cons(min(z0), nil)))
if(true, z0, z1, z2) -> z1
if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
MIN :: nil:cons:append -> c7:c8
cons :: 0':s -> nil:cons:append -> nil:cons:append
nil :: nil:cons:append
c7 :: c7:c8
c8 :: c9:c10 -> c4:c5:c6 -> c7:c8
IF_MIN :: true:false -> nil:cons:append -> c9:c10
le :: 0':s -> 0':s -> true:false
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
REPLACE :: 0':s -> 0':s -> nil:cons:append -> c11:c12
c11 :: c11:c12
c12 :: c13:c14 -> c:c1:c2:c3 -> c11:c12
IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons:append -> c13:c14
eq :: 0':s -> 0':s -> true:false
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14
EMPTY :: nil:cons:append -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
HEAD :: nil:cons:append -> c17
c17 :: c17
TAIL :: nil:cons:append -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
SORT :: nil:cons:append -> c20
c20 :: c21:c22 -> c20
SORTITER :: nil:cons:append -> c21:c22
c21 :: c23:c24:c25:c26 -> c15:c16 -> c21:c22
IF :: true:false -> nil:cons:append -> nil:cons:append -> c23:c24:c25:c26
empty :: nil:cons:append -> true:false
append :: nil:cons:append -> nil:cons:append
min :: nil:cons:append -> 0':s
c22 :: c23:c24:c25:c26 -> c7:c8 -> c21:c22
c23 :: c23:c24:c25:c26
c24 :: c21:c22 -> c11:c12 -> c7:c8 -> c23:c24:c25:c26
replace :: 0':s -> 0':s -> nil:cons:append -> nil:cons:append
head :: nil:cons:append -> 0':s
tail :: nil:cons:append -> nil:cons:append
c25 :: c21:c22 -> c11:c12 -> c17 -> c23:c24:c25:c26
c26 :: c21:c22 -> c11:c12 -> c18:c19 -> c23:c24:c25:c26
if_min :: true:false -> nil:cons:append -> 0':s
if_replace :: true:false -> 0':s -> 0':s -> nil:cons:append -> nil:cons:append
sort :: nil:cons:append -> nil:cons:append
sortIter :: nil:cons:append -> nil:cons:append -> nil:cons:append
if :: true:false -> nil:cons:append -> nil:cons:append -> nil:cons:append -> nil:cons:append
hole_c:c1:c2:c31_27 :: c:c1:c2:c3
hole_0':s2_27 :: 0':s
hole_c4:c5:c63_27 :: c4:c5:c6
hole_c7:c84_27 :: c7:c8
hole_nil:cons:append5_27 :: nil:cons:append
hole_c9:c106_27 :: c9:c10
hole_true:false7_27 :: true:false
hole_c11:c128_27 :: c11:c12
hole_c13:c149_27 :: c13:c14
hole_c15:c1610_27 :: c15:c16
hole_c1711_27 :: c17
hole_c18:c1912_27 :: c18:c19
hole_c2013_27 :: c20
hole_c21:c2214_27 :: c21:c22
hole_c23:c24:c25:c2615_27 :: c23:c24:c25:c26
gen_c:c1:c2:c316_27 :: Nat -> c:c1:c2:c3
gen_0':s17_27 :: Nat -> 0':s
gen_c4:c5:c618_27 :: Nat -> c4:c5:c6
gen_nil:cons:append19_27 :: Nat -> nil:cons:append


Lemmas:
EQ(gen_0':s17_27(n21_27), gen_0':s17_27(n21_27)) -> gen_c:c1:c2:c316_27(n21_27), rt in Omega(1 + n21_27)
LE(gen_0':s17_27(n1115_27), gen_0':s17_27(n1115_27)) -> gen_c4:c5:c618_27(n1115_27), rt in Omega(1 + n1115_27)


Generator Equations:
gen_c:c1:c2:c316_27(0) <=> c
gen_c:c1:c2:c316_27(+(x, 1)) <=> c3(gen_c:c1:c2:c316_27(x))
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c4:c5:c618_27(0) <=> c4
gen_c4:c5:c618_27(+(x, 1)) <=> c6(gen_c4:c5:c618_27(x))
gen_nil:cons:append19_27(0) <=> nil
gen_nil:cons:append19_27(+(x, 1)) <=> cons(0', gen_nil:cons:append19_27(x))


The following defined symbols remain to be analysed:
le, MIN, REPLACE, eq, SORTITER, min, replace, sortIter

They will be analysed ascendingly in the following order:
le < MIN
MIN < SORTITER
le < min
eq < REPLACE
REPLACE < SORTITER
eq < replace
min < SORTITER
replace < SORTITER
min < sortIter
replace < sortIter

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

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

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

Induction Step:
le(gen_0':s17_27(+(n1983_27, 1)), gen_0':s17_27(+(n1983_27, 1))) ->_R^Omega(0)
le(gen_0':s17_27(n1983_27), gen_0':s17_27(n1983_27)) ->_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:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
MIN(cons(z0, nil)) -> c7
MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
REPLACE(z0, z1, nil) -> c11
REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
EMPTY(nil) -> c15
EMPTY(cons(z0, z1)) -> c16
HEAD(cons(z0, z1)) -> c17
TAIL(nil) -> c18
TAIL(cons(z0, z1)) -> c19
SORT(z0) -> c20(SORTITER(z0))
SORTITER(z0) -> c21(IF(empty(z0), z0, append(cons(min(z0), nil))), EMPTY(z0))
SORTITER(z0) -> c22(IF(empty(z0), z0, append(cons(min(z0), nil))), MIN(z0))
IF(true, z0, z2) -> c23
IF(false, z0, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
IF(false, z0, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
IF(false, z0, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
replace(z0, z1, nil) -> nil
replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
sort(z0) -> sortIter(z0, nil)
sortIter(z0, z1) -> if(empty(z0), z0, z1, append(cons(min(z0), nil)))
if(true, z0, z1, z2) -> z1
if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
MIN :: nil:cons:append -> c7:c8
cons :: 0':s -> nil:cons:append -> nil:cons:append
nil :: nil:cons:append
c7 :: c7:c8
c8 :: c9:c10 -> c4:c5:c6 -> c7:c8
IF_MIN :: true:false -> nil:cons:append -> c9:c10
le :: 0':s -> 0':s -> true:false
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
REPLACE :: 0':s -> 0':s -> nil:cons:append -> c11:c12
c11 :: c11:c12
c12 :: c13:c14 -> c:c1:c2:c3 -> c11:c12
IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons:append -> c13:c14
eq :: 0':s -> 0':s -> true:false
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14
EMPTY :: nil:cons:append -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
HEAD :: nil:cons:append -> c17
c17 :: c17
TAIL :: nil:cons:append -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
SORT :: nil:cons:append -> c20
c20 :: c21:c22 -> c20
SORTITER :: nil:cons:append -> c21:c22
c21 :: c23:c24:c25:c26 -> c15:c16 -> c21:c22
IF :: true:false -> nil:cons:append -> nil:cons:append -> c23:c24:c25:c26
empty :: nil:cons:append -> true:false
append :: nil:cons:append -> nil:cons:append
min :: nil:cons:append -> 0':s
c22 :: c23:c24:c25:c26 -> c7:c8 -> c21:c22
c23 :: c23:c24:c25:c26
c24 :: c21:c22 -> c11:c12 -> c7:c8 -> c23:c24:c25:c26
replace :: 0':s -> 0':s -> nil:cons:append -> nil:cons:append
head :: nil:cons:append -> 0':s
tail :: nil:cons:append -> nil:cons:append
c25 :: c21:c22 -> c11:c12 -> c17 -> c23:c24:c25:c26
c26 :: c21:c22 -> c11:c12 -> c18:c19 -> c23:c24:c25:c26
if_min :: true:false -> nil:cons:append -> 0':s
if_replace :: true:false -> 0':s -> 0':s -> nil:cons:append -> nil:cons:append
sort :: nil:cons:append -> nil:cons:append
sortIter :: nil:cons:append -> nil:cons:append -> nil:cons:append
if :: true:false -> nil:cons:append -> nil:cons:append -> nil:cons:append -> nil:cons:append
hole_c:c1:c2:c31_27 :: c:c1:c2:c3
hole_0':s2_27 :: 0':s
hole_c4:c5:c63_27 :: c4:c5:c6
hole_c7:c84_27 :: c7:c8
hole_nil:cons:append5_27 :: nil:cons:append
hole_c9:c106_27 :: c9:c10
hole_true:false7_27 :: true:false
hole_c11:c128_27 :: c11:c12
hole_c13:c149_27 :: c13:c14
hole_c15:c1610_27 :: c15:c16
hole_c1711_27 :: c17
hole_c18:c1912_27 :: c18:c19
hole_c2013_27 :: c20
hole_c21:c2214_27 :: c21:c22
hole_c23:c24:c25:c2615_27 :: c23:c24:c25:c26
gen_c:c1:c2:c316_27 :: Nat -> c:c1:c2:c3
gen_0':s17_27 :: Nat -> 0':s
gen_c4:c5:c618_27 :: Nat -> c4:c5:c6
gen_nil:cons:append19_27 :: Nat -> nil:cons:append


Lemmas:
EQ(gen_0':s17_27(n21_27), gen_0':s17_27(n21_27)) -> gen_c:c1:c2:c316_27(n21_27), rt in Omega(1 + n21_27)
LE(gen_0':s17_27(n1115_27), gen_0':s17_27(n1115_27)) -> gen_c4:c5:c618_27(n1115_27), rt in Omega(1 + n1115_27)
le(gen_0':s17_27(n1983_27), gen_0':s17_27(n1983_27)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c316_27(0) <=> c
gen_c:c1:c2:c316_27(+(x, 1)) <=> c3(gen_c:c1:c2:c316_27(x))
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c4:c5:c618_27(0) <=> c4
gen_c4:c5:c618_27(+(x, 1)) <=> c6(gen_c4:c5:c618_27(x))
gen_nil:cons:append19_27(0) <=> nil
gen_nil:cons:append19_27(+(x, 1)) <=> cons(0', gen_nil:cons:append19_27(x))


The following defined symbols remain to be analysed:
MIN, REPLACE, eq, SORTITER, min, replace, sortIter

They will be analysed ascendingly in the following order:
MIN < SORTITER
eq < REPLACE
REPLACE < SORTITER
eq < replace
min < SORTITER
replace < SORTITER
min < sortIter
replace < sortIter

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MIN(gen_nil:cons:append19_27(+(1, n2530_27))) -> *20_27, rt in Omega(n2530_27)

Induction Base:
MIN(gen_nil:cons:append19_27(+(1, 0)))

Induction Step:
MIN(gen_nil:cons:append19_27(+(1, +(n2530_27, 1)))) ->_R^Omega(1)
c8(IF_MIN(le(0', 0'), cons(0', cons(0', gen_nil:cons:append19_27(n2530_27)))), LE(0', 0')) ->_L^Omega(0)
c8(IF_MIN(true, cons(0', cons(0', gen_nil:cons:append19_27(n2530_27)))), LE(0', 0')) ->_R^Omega(1)
c8(c9(MIN(cons(0', gen_nil:cons:append19_27(n2530_27)))), LE(0', 0')) ->_IH
c8(c9(*20_27), LE(0', 0')) ->_L^Omega(1)
c8(c9(*20_27), gen_c4:c5:c618_27(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:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
MIN(cons(z0, nil)) -> c7
MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
REPLACE(z0, z1, nil) -> c11
REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
EMPTY(nil) -> c15
EMPTY(cons(z0, z1)) -> c16
HEAD(cons(z0, z1)) -> c17
TAIL(nil) -> c18
TAIL(cons(z0, z1)) -> c19
SORT(z0) -> c20(SORTITER(z0))
SORTITER(z0) -> c21(IF(empty(z0), z0, append(cons(min(z0), nil))), EMPTY(z0))
SORTITER(z0) -> c22(IF(empty(z0), z0, append(cons(min(z0), nil))), MIN(z0))
IF(true, z0, z2) -> c23
IF(false, z0, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
IF(false, z0, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
IF(false, z0, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
replace(z0, z1, nil) -> nil
replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
sort(z0) -> sortIter(z0, nil)
sortIter(z0, z1) -> if(empty(z0), z0, z1, append(cons(min(z0), nil)))
if(true, z0, z1, z2) -> z1
if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
MIN :: nil:cons:append -> c7:c8
cons :: 0':s -> nil:cons:append -> nil:cons:append
nil :: nil:cons:append
c7 :: c7:c8
c8 :: c9:c10 -> c4:c5:c6 -> c7:c8
IF_MIN :: true:false -> nil:cons:append -> c9:c10
le :: 0':s -> 0':s -> true:false
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
REPLACE :: 0':s -> 0':s -> nil:cons:append -> c11:c12
c11 :: c11:c12
c12 :: c13:c14 -> c:c1:c2:c3 -> c11:c12
IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons:append -> c13:c14
eq :: 0':s -> 0':s -> true:false
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14
EMPTY :: nil:cons:append -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
HEAD :: nil:cons:append -> c17
c17 :: c17
TAIL :: nil:cons:append -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
SORT :: nil:cons:append -> c20
c20 :: c21:c22 -> c20
SORTITER :: nil:cons:append -> c21:c22
c21 :: c23:c24:c25:c26 -> c15:c16 -> c21:c22
IF :: true:false -> nil:cons:append -> nil:cons:append -> c23:c24:c25:c26
empty :: nil:cons:append -> true:false
append :: nil:cons:append -> nil:cons:append
min :: nil:cons:append -> 0':s
c22 :: c23:c24:c25:c26 -> c7:c8 -> c21:c22
c23 :: c23:c24:c25:c26
c24 :: c21:c22 -> c11:c12 -> c7:c8 -> c23:c24:c25:c26
replace :: 0':s -> 0':s -> nil:cons:append -> nil:cons:append
head :: nil:cons:append -> 0':s
tail :: nil:cons:append -> nil:cons:append
c25 :: c21:c22 -> c11:c12 -> c17 -> c23:c24:c25:c26
c26 :: c21:c22 -> c11:c12 -> c18:c19 -> c23:c24:c25:c26
if_min :: true:false -> nil:cons:append -> 0':s
if_replace :: true:false -> 0':s -> 0':s -> nil:cons:append -> nil:cons:append
sort :: nil:cons:append -> nil:cons:append
sortIter :: nil:cons:append -> nil:cons:append -> nil:cons:append
if :: true:false -> nil:cons:append -> nil:cons:append -> nil:cons:append -> nil:cons:append
hole_c:c1:c2:c31_27 :: c:c1:c2:c3
hole_0':s2_27 :: 0':s
hole_c4:c5:c63_27 :: c4:c5:c6
hole_c7:c84_27 :: c7:c8
hole_nil:cons:append5_27 :: nil:cons:append
hole_c9:c106_27 :: c9:c10
hole_true:false7_27 :: true:false
hole_c11:c128_27 :: c11:c12
hole_c13:c149_27 :: c13:c14
hole_c15:c1610_27 :: c15:c16
hole_c1711_27 :: c17
hole_c18:c1912_27 :: c18:c19
hole_c2013_27 :: c20
hole_c21:c2214_27 :: c21:c22
hole_c23:c24:c25:c2615_27 :: c23:c24:c25:c26
gen_c:c1:c2:c316_27 :: Nat -> c:c1:c2:c3
gen_0':s17_27 :: Nat -> 0':s
gen_c4:c5:c618_27 :: Nat -> c4:c5:c6
gen_nil:cons:append19_27 :: Nat -> nil:cons:append


Lemmas:
EQ(gen_0':s17_27(n21_27), gen_0':s17_27(n21_27)) -> gen_c:c1:c2:c316_27(n21_27), rt in Omega(1 + n21_27)
LE(gen_0':s17_27(n1115_27), gen_0':s17_27(n1115_27)) -> gen_c4:c5:c618_27(n1115_27), rt in Omega(1 + n1115_27)
le(gen_0':s17_27(n1983_27), gen_0':s17_27(n1983_27)) -> true, rt in Omega(0)
MIN(gen_nil:cons:append19_27(+(1, n2530_27))) -> *20_27, rt in Omega(n2530_27)


Generator Equations:
gen_c:c1:c2:c316_27(0) <=> c
gen_c:c1:c2:c316_27(+(x, 1)) <=> c3(gen_c:c1:c2:c316_27(x))
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c4:c5:c618_27(0) <=> c4
gen_c4:c5:c618_27(+(x, 1)) <=> c6(gen_c4:c5:c618_27(x))
gen_nil:cons:append19_27(0) <=> nil
gen_nil:cons:append19_27(+(x, 1)) <=> cons(0', gen_nil:cons:append19_27(x))


The following defined symbols remain to be analysed:
eq, REPLACE, SORTITER, min, replace, sortIter

They will be analysed ascendingly in the following order:
eq < REPLACE
REPLACE < SORTITER
eq < replace
min < SORTITER
replace < SORTITER
min < sortIter
replace < sortIter

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eq(gen_0':s17_27(n6879_27), gen_0':s17_27(n6879_27)) -> true, rt in Omega(0)

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

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

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:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
MIN(cons(z0, nil)) -> c7
MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
REPLACE(z0, z1, nil) -> c11
REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
EMPTY(nil) -> c15
EMPTY(cons(z0, z1)) -> c16
HEAD(cons(z0, z1)) -> c17
TAIL(nil) -> c18
TAIL(cons(z0, z1)) -> c19
SORT(z0) -> c20(SORTITER(z0))
SORTITER(z0) -> c21(IF(empty(z0), z0, append(cons(min(z0), nil))), EMPTY(z0))
SORTITER(z0) -> c22(IF(empty(z0), z0, append(cons(min(z0), nil))), MIN(z0))
IF(true, z0, z2) -> c23
IF(false, z0, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
IF(false, z0, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
IF(false, z0, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
replace(z0, z1, nil) -> nil
replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
sort(z0) -> sortIter(z0, nil)
sortIter(z0, z1) -> if(empty(z0), z0, z1, append(cons(min(z0), nil)))
if(true, z0, z1, z2) -> z1
if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
MIN :: nil:cons:append -> c7:c8
cons :: 0':s -> nil:cons:append -> nil:cons:append
nil :: nil:cons:append
c7 :: c7:c8
c8 :: c9:c10 -> c4:c5:c6 -> c7:c8
IF_MIN :: true:false -> nil:cons:append -> c9:c10
le :: 0':s -> 0':s -> true:false
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
REPLACE :: 0':s -> 0':s -> nil:cons:append -> c11:c12
c11 :: c11:c12
c12 :: c13:c14 -> c:c1:c2:c3 -> c11:c12
IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons:append -> c13:c14
eq :: 0':s -> 0':s -> true:false
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14
EMPTY :: nil:cons:append -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
HEAD :: nil:cons:append -> c17
c17 :: c17
TAIL :: nil:cons:append -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
SORT :: nil:cons:append -> c20
c20 :: c21:c22 -> c20
SORTITER :: nil:cons:append -> c21:c22
c21 :: c23:c24:c25:c26 -> c15:c16 -> c21:c22
IF :: true:false -> nil:cons:append -> nil:cons:append -> c23:c24:c25:c26
empty :: nil:cons:append -> true:false
append :: nil:cons:append -> nil:cons:append
min :: nil:cons:append -> 0':s
c22 :: c23:c24:c25:c26 -> c7:c8 -> c21:c22
c23 :: c23:c24:c25:c26
c24 :: c21:c22 -> c11:c12 -> c7:c8 -> c23:c24:c25:c26
replace :: 0':s -> 0':s -> nil:cons:append -> nil:cons:append
head :: nil:cons:append -> 0':s
tail :: nil:cons:append -> nil:cons:append
c25 :: c21:c22 -> c11:c12 -> c17 -> c23:c24:c25:c26
c26 :: c21:c22 -> c11:c12 -> c18:c19 -> c23:c24:c25:c26
if_min :: true:false -> nil:cons:append -> 0':s
if_replace :: true:false -> 0':s -> 0':s -> nil:cons:append -> nil:cons:append
sort :: nil:cons:append -> nil:cons:append
sortIter :: nil:cons:append -> nil:cons:append -> nil:cons:append
if :: true:false -> nil:cons:append -> nil:cons:append -> nil:cons:append -> nil:cons:append
hole_c:c1:c2:c31_27 :: c:c1:c2:c3
hole_0':s2_27 :: 0':s
hole_c4:c5:c63_27 :: c4:c5:c6
hole_c7:c84_27 :: c7:c8
hole_nil:cons:append5_27 :: nil:cons:append
hole_c9:c106_27 :: c9:c10
hole_true:false7_27 :: true:false
hole_c11:c128_27 :: c11:c12
hole_c13:c149_27 :: c13:c14
hole_c15:c1610_27 :: c15:c16
hole_c1711_27 :: c17
hole_c18:c1912_27 :: c18:c19
hole_c2013_27 :: c20
hole_c21:c2214_27 :: c21:c22
hole_c23:c24:c25:c2615_27 :: c23:c24:c25:c26
gen_c:c1:c2:c316_27 :: Nat -> c:c1:c2:c3
gen_0':s17_27 :: Nat -> 0':s
gen_c4:c5:c618_27 :: Nat -> c4:c5:c6
gen_nil:cons:append19_27 :: Nat -> nil:cons:append


Lemmas:
EQ(gen_0':s17_27(n21_27), gen_0':s17_27(n21_27)) -> gen_c:c1:c2:c316_27(n21_27), rt in Omega(1 + n21_27)
LE(gen_0':s17_27(n1115_27), gen_0':s17_27(n1115_27)) -> gen_c4:c5:c618_27(n1115_27), rt in Omega(1 + n1115_27)
le(gen_0':s17_27(n1983_27), gen_0':s17_27(n1983_27)) -> true, rt in Omega(0)
MIN(gen_nil:cons:append19_27(+(1, n2530_27))) -> *20_27, rt in Omega(n2530_27)
eq(gen_0':s17_27(n6879_27), gen_0':s17_27(n6879_27)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c316_27(0) <=> c
gen_c:c1:c2:c316_27(+(x, 1)) <=> c3(gen_c:c1:c2:c316_27(x))
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c4:c5:c618_27(0) <=> c4
gen_c4:c5:c618_27(+(x, 1)) <=> c6(gen_c4:c5:c618_27(x))
gen_nil:cons:append19_27(0) <=> nil
gen_nil:cons:append19_27(+(x, 1)) <=> cons(0', gen_nil:cons:append19_27(x))


The following defined symbols remain to be analysed:
REPLACE, SORTITER, min, replace, sortIter

They will be analysed ascendingly in the following order:
REPLACE < SORTITER
min < SORTITER
replace < SORTITER
min < sortIter
replace < sortIter

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
min(gen_nil:cons:append19_27(+(1, n8298_27))) -> gen_0':s17_27(0), rt in Omega(0)

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

Induction Step:
min(gen_nil:cons:append19_27(+(1, +(n8298_27, 1)))) ->_R^Omega(0)
if_min(le(0', 0'), cons(0', cons(0', gen_nil:cons:append19_27(n8298_27)))) ->_L^Omega(0)
if_min(true, cons(0', cons(0', gen_nil:cons:append19_27(n8298_27)))) ->_R^Omega(0)
min(cons(0', gen_nil:cons:append19_27(n8298_27))) ->_IH
gen_0':s17_27(0)

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

(26)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
MIN(cons(z0, nil)) -> c7
MIN(cons(z0, cons(z1, z2))) -> c8(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1))
IF_MIN(true, cons(z0, cons(z1, z2))) -> c9(MIN(cons(z0, z2)))
IF_MIN(false, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z1, z2)))
REPLACE(z0, z1, nil) -> c11
REPLACE(z0, z1, cons(z2, z3)) -> c12(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2))
IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c13
IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c14(REPLACE(z0, z1, z3))
EMPTY(nil) -> c15
EMPTY(cons(z0, z1)) -> c16
HEAD(cons(z0, z1)) -> c17
TAIL(nil) -> c18
TAIL(cons(z0, z1)) -> c19
SORT(z0) -> c20(SORTITER(z0))
SORTITER(z0) -> c21(IF(empty(z0), z0, append(cons(min(z0), nil))), EMPTY(z0))
SORTITER(z0) -> c22(IF(empty(z0), z0, append(cons(min(z0), nil))), MIN(z0))
IF(true, z0, z2) -> c23
IF(false, z0, z2) -> c24(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), MIN(z0))
IF(false, z0, z2) -> c25(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), HEAD(z0))
IF(false, z0, z2) -> c26(SORTITER(replace(min(z0), head(z0), tail(z0))), REPLACE(min(z0), head(z0), tail(z0)), TAIL(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
min(cons(z0, nil)) -> z0
min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2)))
if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2))
if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2))
replace(z0, z1, nil) -> nil
replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3))
if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3)
if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
sort(z0) -> sortIter(z0, nil)
sortIter(z0, z1) -> if(empty(z0), z0, z1, append(cons(min(z0), nil)))
if(true, z0, z1, z2) -> z1
if(false, z0, z1, z2) -> sortIter(replace(min(z0), head(z0), tail(z0)), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
MIN :: nil:cons:append -> c7:c8
cons :: 0':s -> nil:cons:append -> nil:cons:append
nil :: nil:cons:append
c7 :: c7:c8
c8 :: c9:c10 -> c4:c5:c6 -> c7:c8
IF_MIN :: true:false -> nil:cons:append -> c9:c10
le :: 0':s -> 0':s -> true:false
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
REPLACE :: 0':s -> 0':s -> nil:cons:append -> c11:c12
c11 :: c11:c12
c12 :: c13:c14 -> c:c1:c2:c3 -> c11:c12
IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons:append -> c13:c14
eq :: 0':s -> 0':s -> true:false
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14
EMPTY :: nil:cons:append -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
HEAD :: nil:cons:append -> c17
c17 :: c17
TAIL :: nil:cons:append -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
SORT :: nil:cons:append -> c20
c20 :: c21:c22 -> c20
SORTITER :: nil:cons:append -> c21:c22
c21 :: c23:c24:c25:c26 -> c15:c16 -> c21:c22
IF :: true:false -> nil:cons:append -> nil:cons:append -> c23:c24:c25:c26
empty :: nil:cons:append -> true:false
append :: nil:cons:append -> nil:cons:append
min :: nil:cons:append -> 0':s
c22 :: c23:c24:c25:c26 -> c7:c8 -> c21:c22
c23 :: c23:c24:c25:c26
c24 :: c21:c22 -> c11:c12 -> c7:c8 -> c23:c24:c25:c26
replace :: 0':s -> 0':s -> nil:cons:append -> nil:cons:append
head :: nil:cons:append -> 0':s
tail :: nil:cons:append -> nil:cons:append
c25 :: c21:c22 -> c11:c12 -> c17 -> c23:c24:c25:c26
c26 :: c21:c22 -> c11:c12 -> c18:c19 -> c23:c24:c25:c26
if_min :: true:false -> nil:cons:append -> 0':s
if_replace :: true:false -> 0':s -> 0':s -> nil:cons:append -> nil:cons:append
sort :: nil:cons:append -> nil:cons:append
sortIter :: nil:cons:append -> nil:cons:append -> nil:cons:append
if :: true:false -> nil:cons:append -> nil:cons:append -> nil:cons:append -> nil:cons:append
hole_c:c1:c2:c31_27 :: c:c1:c2:c3
hole_0':s2_27 :: 0':s
hole_c4:c5:c63_27 :: c4:c5:c6
hole_c7:c84_27 :: c7:c8
hole_nil:cons:append5_27 :: nil:cons:append
hole_c9:c106_27 :: c9:c10
hole_true:false7_27 :: true:false
hole_c11:c128_27 :: c11:c12
hole_c13:c149_27 :: c13:c14
hole_c15:c1610_27 :: c15:c16
hole_c1711_27 :: c17
hole_c18:c1912_27 :: c18:c19
hole_c2013_27 :: c20
hole_c21:c2214_27 :: c21:c22
hole_c23:c24:c25:c2615_27 :: c23:c24:c25:c26
gen_c:c1:c2:c316_27 :: Nat -> c:c1:c2:c3
gen_0':s17_27 :: Nat -> 0':s
gen_c4:c5:c618_27 :: Nat -> c4:c5:c6
gen_nil:cons:append19_27 :: Nat -> nil:cons:append


Lemmas:
EQ(gen_0':s17_27(n21_27), gen_0':s17_27(n21_27)) -> gen_c:c1:c2:c316_27(n21_27), rt in Omega(1 + n21_27)
LE(gen_0':s17_27(n1115_27), gen_0':s17_27(n1115_27)) -> gen_c4:c5:c618_27(n1115_27), rt in Omega(1 + n1115_27)
le(gen_0':s17_27(n1983_27), gen_0':s17_27(n1983_27)) -> true, rt in Omega(0)
MIN(gen_nil:cons:append19_27(+(1, n2530_27))) -> *20_27, rt in Omega(n2530_27)
eq(gen_0':s17_27(n6879_27), gen_0':s17_27(n6879_27)) -> true, rt in Omega(0)
min(gen_nil:cons:append19_27(+(1, n8298_27))) -> gen_0':s17_27(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c316_27(0) <=> c
gen_c:c1:c2:c316_27(+(x, 1)) <=> c3(gen_c:c1:c2:c316_27(x))
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c4:c5:c618_27(0) <=> c4
gen_c4:c5:c618_27(+(x, 1)) <=> c6(gen_c4:c5:c618_27(x))
gen_nil:cons:append19_27(0) <=> nil
gen_nil:cons:append19_27(+(x, 1)) <=> cons(0', gen_nil:cons:append19_27(x))


The following defined symbols remain to be analysed:
replace, SORTITER, sortIter

They will be analysed ascendingly in the following order:
replace < SORTITER
replace < sortIter