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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 241 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxRelTRS
(9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) typed CpxTrs
(11) OrderProof [LOWER BOUND(ID), 1 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 336 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 89 ms]
(16) typed CpxTrs
(17) RewriteLemmaProof [LOWER BOUND(ID), 85 ms]
(18) typed CpxTrs
(19) RewriteLemmaProof [LOWER BOUND(ID), 218 ms]
(20) typed CpxTrs
(21) RewriteLemmaProof [LOWER BOUND(ID), 68 ms]
(22) typed CpxTrs
(23) RewriteLemmaProof [LOWER BOUND(ID), 1278 ms]
(24) BEST
    (25) proven lower bound
        (26) LowerBoundPropagationProof [FINISHED, 0 ms]
        (27) BOUNDS(n^1, INF)
    (28) typed CpxTrs


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

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


The TRS R consists of the following rules:

   minsort(Cons(x, xs)) -> appmin(x, xs, Cons(x, xs))
   minsort(Nil) -> Nil
   appmin(min, Cons(x, xs), xs') -> appmin[Ite][True][Ite](<(x, min), min, Cons(x, xs), xs')
   appmin(min, Nil, xs) -> Cons(min, minsort(remove(min, xs)))
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   remove(x', Cons(x, xs)) -> remove[Ite](!EQ(x', x), x', Cons(x, xs))

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

   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0, S(y)) -> False
   !EQ(S(x), 0) -> False
   !EQ(0, 0) -> True
   <(S(x), S(y)) -> <(x, y)
   <(0, S(y)) -> True
   <(x, 0) -> False
   remove[Ite](False, x', Cons(x, xs)) -> Cons(x, remove(x', xs))
   appmin[Ite][True][Ite](True, min, Cons(x, xs), xs') -> appmin(x, xs, xs')
   remove[Ite](True, x', Cons(x, xs)) -> xs
   appmin[Ite][True][Ite](False, min, Cons(x, xs), xs') -> appmin(min, xs, xs')

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

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


The TRS R consists of the following rules:

   minsort(Cons(x, xs)) -> appmin(x, xs, Cons(x, xs))
   minsort(Nil) -> Nil
   appmin(min, Cons(x, xs), xs') -> appmin[Ite][True][Ite](<(x, min), min, Cons(x, xs), xs')
   appmin(min, Nil, xs) -> Cons(min, minsort(remove(min, xs)))
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   remove(x', Cons(x, xs)) -> remove[Ite](!EQ(x', x), x', Cons(x, xs))

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

   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0, S(y)) -> False
   !EQ(S(x), 0) -> False
   !EQ(0, 0) -> True
   <(S(x), S(y)) -> <(x, y)
   <(0, S(y)) -> True
   <(x, 0) -> False
   remove[Ite](False, x', Cons(x, xs)) -> Cons(x, remove(x', xs))
   appmin[Ite][True][Ite](True, min, Cons(x, xs), xs') -> appmin(x, xs, xs')
   remove[Ite](True, x', Cons(x, xs)) -> xs
   appmin[Ite][True][Ite](False, min, Cons(x, xs), xs') -> appmin(min, xs, xs')

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   <(S(z0), S(z1)) -> <(z0, z1)
   <(0, S(z0)) -> True
   <(z0, 0) -> False
   remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
   remove[Ite](True, z0, Cons(z1, z2)) -> z2
   appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
   appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
   minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
   minsort(Nil) -> Nil
   appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
   appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))
Tuples:
   !EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
   !EQ'(0, S(z0)) -> c1
   !EQ'(S(z0), 0) -> c2
   !EQ'(0, 0) -> c3
   <'(S(z0), S(z1)) -> c4(<'(z0, z1))
   <'(0, S(z0)) -> c5
   <'(z0, 0) -> c6
   REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
   REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
   APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
   APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
   MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
   MINSORT(Nil) -> c12
   APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
   APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
   NOTEMPTY(Cons(z0, z1)) -> c15
   NOTEMPTY(Nil) -> c16
   REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
S tuples:
   MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
   MINSORT(Nil) -> c12
   APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
   APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
   NOTEMPTY(Cons(z0, z1)) -> c15
   NOTEMPTY(Nil) -> c16
   REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
K tuples:none
Defined Rule Symbols:   minsort_1, appmin_3, notEmpty_1, remove_2, !EQ_2, <_2, remove[Ite]_3, appmin[Ite][True][Ite]_4

Defined Pair Symbols:   !EQ'_2, <'_2, REMOVE[ITE]_3, APPMIN[ITE][TRUE][ITE]_4, MINSORT_1, APPMIN_3, NOTEMPTY_1, REMOVE_2

Compound Symbols:   c_1, c1, c2, c3, c4_1, c5, c6, c7_1, c8, c9_1, c10_1, c11_1, c12, c13_2, c14_2, c15, c16, c17_2


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

(5) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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

   MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
   MINSORT(Nil) -> c12
   APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
   APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
   NOTEMPTY(Cons(z0, z1)) -> c15
   NOTEMPTY(Nil) -> c16
   REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))

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

   !EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
   !EQ'(0, S(z0)) -> c1
   !EQ'(S(z0), 0) -> c2
   !EQ'(0, 0) -> c3
   <'(S(z0), S(z1)) -> c4(<'(z0, z1))
   <'(0, S(z0)) -> c5
   <'(z0, 0) -> c6
   REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
   REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
   APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
   APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   <(S(z0), S(z1)) -> <(z0, z1)
   <(0, S(z0)) -> True
   <(z0, 0) -> False
   remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
   remove[Ite](True, z0, Cons(z1, z2)) -> z2
   appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
   appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
   minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
   minsort(Nil) -> Nil
   appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
   appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

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

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

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

   MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
   MINSORT(Nil) -> c12
   APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
   APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
   NOTEMPTY(Cons(z0, z1)) -> c15
   NOTEMPTY(Nil) -> c16
   REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))

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

   !EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
   !EQ'(0', S(z0)) -> c1
   !EQ'(S(z0), 0') -> c2
   !EQ'(0', 0') -> c3
   <'(S(z0), S(z1)) -> c4(<'(z0, z1))
   <'(0', S(z0)) -> c5
   <'(z0, 0') -> c6
   REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
   REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
   APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
   APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0', S(z0)) -> False
   !EQ(S(z0), 0') -> False
   !EQ(0', 0') -> True
   <(S(z0), S(z1)) -> <(z0, z1)
   <(0', S(z0)) -> True
   <(z0, 0') -> False
   remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
   remove[Ite](True, z0, Cons(z1, z2)) -> z2
   appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
   appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
   minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
   minsort(Nil) -> Nil
   appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
   appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

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

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

(10)
Obligation:
Innermost TRS:
Rules:
MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c12
APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c15
NOTEMPTY(Nil) -> c16
REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
<'(S(z0), S(z1)) -> c4(<'(z0, z1))
<'(0', S(z0)) -> c5
<'(z0, 0') -> c6
REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite](True, z0, Cons(z1, z2)) -> z2
appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
minsort(Nil) -> Nil
appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

Types:
MINSORT :: Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c13:c14 -> c11:c12
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c13:c14
Nil :: Cons:Nil
c12 :: c11:c12
c13 :: c9:c10 -> c4:c5:c6 -> c13:c14
APPMIN[ITE][TRUE][ITE] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> c9:c10
< :: S:0' -> S:0' -> False:True
<' :: S:0' -> S:0' -> c4:c5:c6
c14 :: c11:c12 -> c17 -> c13:c14
remove :: S:0' -> Cons:Nil -> Cons:Nil
REMOVE :: S:0' -> Cons:Nil -> c17
NOTEMPTY :: Cons:Nil -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
c17 :: c7:c8 -> c:c1:c2:c3 -> c17
REMOVE[ITE] :: False:True -> S:0' -> Cons:Nil -> c7:c8
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
S :: S:0' -> S:0'
c :: c:c1:c2:c3 -> c:c1:c2:c3
0' :: S:0'
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c4:c5:c6 -> c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6
False :: False:True
c7 :: c17 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c13:c14 -> c9:c10
c10 :: c13:c14 -> c9:c10
remove[Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil
appmin[Ite][True][Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
appmin :: S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
minsort :: Cons:Nil -> Cons:Nil
notEmpty :: Cons:Nil -> False:True
hole_c11:c121_18 :: c11:c12
hole_Cons:Nil2_18 :: Cons:Nil
hole_S:0'3_18 :: S:0'
hole_c13:c144_18 :: c13:c14
hole_c9:c105_18 :: c9:c10
hole_c4:c5:c66_18 :: c4:c5:c6
hole_False:True7_18 :: False:True
hole_c178_18 :: c17
hole_c15:c169_18 :: c15:c16
hole_c7:c810_18 :: c7:c8
hole_c:c1:c2:c311_18 :: c:c1:c2:c3
gen_Cons:Nil12_18 :: Nat -> Cons:Nil
gen_S:0'13_18 :: Nat -> S:0'
gen_c4:c5:c614_18 :: Nat -> c4:c5:c6
gen_c:c1:c2:c315_18 :: Nat -> c:c1:c2:c3

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

(11) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MINSORT, APPMIN, <, <', remove, REMOVE, !EQ, !EQ', appmin, minsort

They will be analysed ascendingly in the following order:
MINSORT = APPMIN
< < APPMIN
<' < APPMIN
remove < APPMIN
REMOVE < APPMIN
< < appmin
!EQ < remove
remove < appmin
!EQ < REMOVE
!EQ' < REMOVE
appmin = minsort

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

(12)
Obligation:
Innermost TRS:
Rules:
MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c12
APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c15
NOTEMPTY(Nil) -> c16
REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
<'(S(z0), S(z1)) -> c4(<'(z0, z1))
<'(0', S(z0)) -> c5
<'(z0, 0') -> c6
REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite](True, z0, Cons(z1, z2)) -> z2
appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
minsort(Nil) -> Nil
appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

Types:
MINSORT :: Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c13:c14 -> c11:c12
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c13:c14
Nil :: Cons:Nil
c12 :: c11:c12
c13 :: c9:c10 -> c4:c5:c6 -> c13:c14
APPMIN[ITE][TRUE][ITE] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> c9:c10
< :: S:0' -> S:0' -> False:True
<' :: S:0' -> S:0' -> c4:c5:c6
c14 :: c11:c12 -> c17 -> c13:c14
remove :: S:0' -> Cons:Nil -> Cons:Nil
REMOVE :: S:0' -> Cons:Nil -> c17
NOTEMPTY :: Cons:Nil -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
c17 :: c7:c8 -> c:c1:c2:c3 -> c17
REMOVE[ITE] :: False:True -> S:0' -> Cons:Nil -> c7:c8
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
S :: S:0' -> S:0'
c :: c:c1:c2:c3 -> c:c1:c2:c3
0' :: S:0'
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c4:c5:c6 -> c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6
False :: False:True
c7 :: c17 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c13:c14 -> c9:c10
c10 :: c13:c14 -> c9:c10
remove[Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil
appmin[Ite][True][Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
appmin :: S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
minsort :: Cons:Nil -> Cons:Nil
notEmpty :: Cons:Nil -> False:True
hole_c11:c121_18 :: c11:c12
hole_Cons:Nil2_18 :: Cons:Nil
hole_S:0'3_18 :: S:0'
hole_c13:c144_18 :: c13:c14
hole_c9:c105_18 :: c9:c10
hole_c4:c5:c66_18 :: c4:c5:c6
hole_False:True7_18 :: False:True
hole_c178_18 :: c17
hole_c15:c169_18 :: c15:c16
hole_c7:c810_18 :: c7:c8
hole_c:c1:c2:c311_18 :: c:c1:c2:c3
gen_Cons:Nil12_18 :: Nat -> Cons:Nil
gen_S:0'13_18 :: Nat -> S:0'
gen_c4:c5:c614_18 :: Nat -> c4:c5:c6
gen_c:c1:c2:c315_18 :: Nat -> c:c1:c2:c3


Generator Equations:
gen_Cons:Nil12_18(0) <=> Nil
gen_Cons:Nil12_18(+(x, 1)) <=> Cons(0', gen_Cons:Nil12_18(x))
gen_S:0'13_18(0) <=> 0'
gen_S:0'13_18(+(x, 1)) <=> S(gen_S:0'13_18(x))
gen_c4:c5:c614_18(0) <=> c5
gen_c4:c5:c614_18(+(x, 1)) <=> c4(gen_c4:c5:c614_18(x))
gen_c:c1:c2:c315_18(0) <=> c1
gen_c:c1:c2:c315_18(+(x, 1)) <=> c(gen_c:c1:c2:c315_18(x))


The following defined symbols remain to be analysed:
<, MINSORT, APPMIN, <', remove, REMOVE, !EQ, !EQ', appmin, minsort

They will be analysed ascendingly in the following order:
MINSORT = APPMIN
< < APPMIN
<' < APPMIN
remove < APPMIN
REMOVE < APPMIN
< < appmin
!EQ < remove
remove < appmin
!EQ < REMOVE
!EQ' < REMOVE
appmin = minsort

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
<(gen_S:0'13_18(n17_18), gen_S:0'13_18(+(1, n17_18))) -> True, rt in Omega(0)

Induction Base:
<(gen_S:0'13_18(0), gen_S:0'13_18(+(1, 0))) ->_R^Omega(0)
True

Induction Step:
<(gen_S:0'13_18(+(n17_18, 1)), gen_S:0'13_18(+(1, +(n17_18, 1)))) ->_R^Omega(0)
<(gen_S:0'13_18(n17_18), gen_S:0'13_18(+(1, n17_18))) ->_IH
True

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

(14)
Obligation:
Innermost TRS:
Rules:
MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c12
APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c15
NOTEMPTY(Nil) -> c16
REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
<'(S(z0), S(z1)) -> c4(<'(z0, z1))
<'(0', S(z0)) -> c5
<'(z0, 0') -> c6
REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite](True, z0, Cons(z1, z2)) -> z2
appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
minsort(Nil) -> Nil
appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

Types:
MINSORT :: Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c13:c14 -> c11:c12
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c13:c14
Nil :: Cons:Nil
c12 :: c11:c12
c13 :: c9:c10 -> c4:c5:c6 -> c13:c14
APPMIN[ITE][TRUE][ITE] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> c9:c10
< :: S:0' -> S:0' -> False:True
<' :: S:0' -> S:0' -> c4:c5:c6
c14 :: c11:c12 -> c17 -> c13:c14
remove :: S:0' -> Cons:Nil -> Cons:Nil
REMOVE :: S:0' -> Cons:Nil -> c17
NOTEMPTY :: Cons:Nil -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
c17 :: c7:c8 -> c:c1:c2:c3 -> c17
REMOVE[ITE] :: False:True -> S:0' -> Cons:Nil -> c7:c8
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
S :: S:0' -> S:0'
c :: c:c1:c2:c3 -> c:c1:c2:c3
0' :: S:0'
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c4:c5:c6 -> c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6
False :: False:True
c7 :: c17 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c13:c14 -> c9:c10
c10 :: c13:c14 -> c9:c10
remove[Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil
appmin[Ite][True][Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
appmin :: S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
minsort :: Cons:Nil -> Cons:Nil
notEmpty :: Cons:Nil -> False:True
hole_c11:c121_18 :: c11:c12
hole_Cons:Nil2_18 :: Cons:Nil
hole_S:0'3_18 :: S:0'
hole_c13:c144_18 :: c13:c14
hole_c9:c105_18 :: c9:c10
hole_c4:c5:c66_18 :: c4:c5:c6
hole_False:True7_18 :: False:True
hole_c178_18 :: c17
hole_c15:c169_18 :: c15:c16
hole_c7:c810_18 :: c7:c8
hole_c:c1:c2:c311_18 :: c:c1:c2:c3
gen_Cons:Nil12_18 :: Nat -> Cons:Nil
gen_S:0'13_18 :: Nat -> S:0'
gen_c4:c5:c614_18 :: Nat -> c4:c5:c6
gen_c:c1:c2:c315_18 :: Nat -> c:c1:c2:c3


Lemmas:
<(gen_S:0'13_18(n17_18), gen_S:0'13_18(+(1, n17_18))) -> True, rt in Omega(0)


Generator Equations:
gen_Cons:Nil12_18(0) <=> Nil
gen_Cons:Nil12_18(+(x, 1)) <=> Cons(0', gen_Cons:Nil12_18(x))
gen_S:0'13_18(0) <=> 0'
gen_S:0'13_18(+(x, 1)) <=> S(gen_S:0'13_18(x))
gen_c4:c5:c614_18(0) <=> c5
gen_c4:c5:c614_18(+(x, 1)) <=> c4(gen_c4:c5:c614_18(x))
gen_c:c1:c2:c315_18(0) <=> c1
gen_c:c1:c2:c315_18(+(x, 1)) <=> c(gen_c:c1:c2:c315_18(x))


The following defined symbols remain to be analysed:
<', MINSORT, APPMIN, remove, REMOVE, !EQ, !EQ', appmin, minsort

They will be analysed ascendingly in the following order:
MINSORT = APPMIN
<' < APPMIN
remove < APPMIN
REMOVE < APPMIN
!EQ < remove
remove < appmin
!EQ < REMOVE
!EQ' < REMOVE
appmin = minsort

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
<'(gen_S:0'13_18(n391_18), gen_S:0'13_18(+(1, n391_18))) -> gen_c4:c5:c614_18(n391_18), rt in Omega(0)

Induction Base:
<'(gen_S:0'13_18(0), gen_S:0'13_18(+(1, 0))) ->_R^Omega(0)
c5

Induction Step:
<'(gen_S:0'13_18(+(n391_18, 1)), gen_S:0'13_18(+(1, +(n391_18, 1)))) ->_R^Omega(0)
c4(<'(gen_S:0'13_18(n391_18), gen_S:0'13_18(+(1, n391_18)))) ->_IH
c4(gen_c4:c5:c614_18(c392_18))

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

(16)
Obligation:
Innermost TRS:
Rules:
MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c12
APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c15
NOTEMPTY(Nil) -> c16
REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
<'(S(z0), S(z1)) -> c4(<'(z0, z1))
<'(0', S(z0)) -> c5
<'(z0, 0') -> c6
REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite](True, z0, Cons(z1, z2)) -> z2
appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
minsort(Nil) -> Nil
appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

Types:
MINSORT :: Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c13:c14 -> c11:c12
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c13:c14
Nil :: Cons:Nil
c12 :: c11:c12
c13 :: c9:c10 -> c4:c5:c6 -> c13:c14
APPMIN[ITE][TRUE][ITE] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> c9:c10
< :: S:0' -> S:0' -> False:True
<' :: S:0' -> S:0' -> c4:c5:c6
c14 :: c11:c12 -> c17 -> c13:c14
remove :: S:0' -> Cons:Nil -> Cons:Nil
REMOVE :: S:0' -> Cons:Nil -> c17
NOTEMPTY :: Cons:Nil -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
c17 :: c7:c8 -> c:c1:c2:c3 -> c17
REMOVE[ITE] :: False:True -> S:0' -> Cons:Nil -> c7:c8
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
S :: S:0' -> S:0'
c :: c:c1:c2:c3 -> c:c1:c2:c3
0' :: S:0'
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c4:c5:c6 -> c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6
False :: False:True
c7 :: c17 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c13:c14 -> c9:c10
c10 :: c13:c14 -> c9:c10
remove[Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil
appmin[Ite][True][Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
appmin :: S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
minsort :: Cons:Nil -> Cons:Nil
notEmpty :: Cons:Nil -> False:True
hole_c11:c121_18 :: c11:c12
hole_Cons:Nil2_18 :: Cons:Nil
hole_S:0'3_18 :: S:0'
hole_c13:c144_18 :: c13:c14
hole_c9:c105_18 :: c9:c10
hole_c4:c5:c66_18 :: c4:c5:c6
hole_False:True7_18 :: False:True
hole_c178_18 :: c17
hole_c15:c169_18 :: c15:c16
hole_c7:c810_18 :: c7:c8
hole_c:c1:c2:c311_18 :: c:c1:c2:c3
gen_Cons:Nil12_18 :: Nat -> Cons:Nil
gen_S:0'13_18 :: Nat -> S:0'
gen_c4:c5:c614_18 :: Nat -> c4:c5:c6
gen_c:c1:c2:c315_18 :: Nat -> c:c1:c2:c3


Lemmas:
<(gen_S:0'13_18(n17_18), gen_S:0'13_18(+(1, n17_18))) -> True, rt in Omega(0)
<'(gen_S:0'13_18(n391_18), gen_S:0'13_18(+(1, n391_18))) -> gen_c4:c5:c614_18(n391_18), rt in Omega(0)


Generator Equations:
gen_Cons:Nil12_18(0) <=> Nil
gen_Cons:Nil12_18(+(x, 1)) <=> Cons(0', gen_Cons:Nil12_18(x))
gen_S:0'13_18(0) <=> 0'
gen_S:0'13_18(+(x, 1)) <=> S(gen_S:0'13_18(x))
gen_c4:c5:c614_18(0) <=> c5
gen_c4:c5:c614_18(+(x, 1)) <=> c4(gen_c4:c5:c614_18(x))
gen_c:c1:c2:c315_18(0) <=> c1
gen_c:c1:c2:c315_18(+(x, 1)) <=> c(gen_c:c1:c2:c315_18(x))


The following defined symbols remain to be analysed:
!EQ, MINSORT, APPMIN, remove, REMOVE, !EQ', appmin, minsort

They will be analysed ascendingly in the following order:
MINSORT = APPMIN
remove < APPMIN
REMOVE < APPMIN
!EQ < remove
remove < appmin
!EQ < REMOVE
!EQ' < REMOVE
appmin = minsort

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
!EQ(gen_S:0'13_18(n1083_18), gen_S:0'13_18(+(1, n1083_18))) -> False, rt in Omega(0)

Induction Base:
!EQ(gen_S:0'13_18(0), gen_S:0'13_18(+(1, 0))) ->_R^Omega(0)
False

Induction Step:
!EQ(gen_S:0'13_18(+(n1083_18, 1)), gen_S:0'13_18(+(1, +(n1083_18, 1)))) ->_R^Omega(0)
!EQ(gen_S:0'13_18(n1083_18), gen_S:0'13_18(+(1, n1083_18))) ->_IH
False

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

(18)
Obligation:
Innermost TRS:
Rules:
MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c12
APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c15
NOTEMPTY(Nil) -> c16
REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
<'(S(z0), S(z1)) -> c4(<'(z0, z1))
<'(0', S(z0)) -> c5
<'(z0, 0') -> c6
REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite](True, z0, Cons(z1, z2)) -> z2
appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
minsort(Nil) -> Nil
appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

Types:
MINSORT :: Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c13:c14 -> c11:c12
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c13:c14
Nil :: Cons:Nil
c12 :: c11:c12
c13 :: c9:c10 -> c4:c5:c6 -> c13:c14
APPMIN[ITE][TRUE][ITE] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> c9:c10
< :: S:0' -> S:0' -> False:True
<' :: S:0' -> S:0' -> c4:c5:c6
c14 :: c11:c12 -> c17 -> c13:c14
remove :: S:0' -> Cons:Nil -> Cons:Nil
REMOVE :: S:0' -> Cons:Nil -> c17
NOTEMPTY :: Cons:Nil -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
c17 :: c7:c8 -> c:c1:c2:c3 -> c17
REMOVE[ITE] :: False:True -> S:0' -> Cons:Nil -> c7:c8
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
S :: S:0' -> S:0'
c :: c:c1:c2:c3 -> c:c1:c2:c3
0' :: S:0'
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c4:c5:c6 -> c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6
False :: False:True
c7 :: c17 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c13:c14 -> c9:c10
c10 :: c13:c14 -> c9:c10
remove[Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil
appmin[Ite][True][Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
appmin :: S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
minsort :: Cons:Nil -> Cons:Nil
notEmpty :: Cons:Nil -> False:True
hole_c11:c121_18 :: c11:c12
hole_Cons:Nil2_18 :: Cons:Nil
hole_S:0'3_18 :: S:0'
hole_c13:c144_18 :: c13:c14
hole_c9:c105_18 :: c9:c10
hole_c4:c5:c66_18 :: c4:c5:c6
hole_False:True7_18 :: False:True
hole_c178_18 :: c17
hole_c15:c169_18 :: c15:c16
hole_c7:c810_18 :: c7:c8
hole_c:c1:c2:c311_18 :: c:c1:c2:c3
gen_Cons:Nil12_18 :: Nat -> Cons:Nil
gen_S:0'13_18 :: Nat -> S:0'
gen_c4:c5:c614_18 :: Nat -> c4:c5:c6
gen_c:c1:c2:c315_18 :: Nat -> c:c1:c2:c3


Lemmas:
<(gen_S:0'13_18(n17_18), gen_S:0'13_18(+(1, n17_18))) -> True, rt in Omega(0)
<'(gen_S:0'13_18(n391_18), gen_S:0'13_18(+(1, n391_18))) -> gen_c4:c5:c614_18(n391_18), rt in Omega(0)
!EQ(gen_S:0'13_18(n1083_18), gen_S:0'13_18(+(1, n1083_18))) -> False, rt in Omega(0)


Generator Equations:
gen_Cons:Nil12_18(0) <=> Nil
gen_Cons:Nil12_18(+(x, 1)) <=> Cons(0', gen_Cons:Nil12_18(x))
gen_S:0'13_18(0) <=> 0'
gen_S:0'13_18(+(x, 1)) <=> S(gen_S:0'13_18(x))
gen_c4:c5:c614_18(0) <=> c5
gen_c4:c5:c614_18(+(x, 1)) <=> c4(gen_c4:c5:c614_18(x))
gen_c:c1:c2:c315_18(0) <=> c1
gen_c:c1:c2:c315_18(+(x, 1)) <=> c(gen_c:c1:c2:c315_18(x))


The following defined symbols remain to be analysed:
remove, MINSORT, APPMIN, REMOVE, !EQ', appmin, minsort

They will be analysed ascendingly in the following order:
MINSORT = APPMIN
remove < APPMIN
REMOVE < APPMIN
remove < appmin
!EQ' < REMOVE
appmin = minsort

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
remove(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, n1504_18))) -> *16_18, rt in Omega(0)

Induction Base:
remove(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, 0)))

Induction Step:
remove(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, +(n1504_18, 1)))) ->_R^Omega(0)
remove[Ite](!EQ(gen_S:0'13_18(1), 0'), gen_S:0'13_18(1), Cons(0', gen_Cons:Nil12_18(+(1, n1504_18)))) ->_R^Omega(0)
remove[Ite](False, gen_S:0'13_18(1), Cons(0', gen_Cons:Nil12_18(+(1, n1504_18)))) ->_R^Omega(0)
Cons(0', remove(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, n1504_18)))) ->_IH
Cons(0', *16_18)

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:
MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c12
APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c15
NOTEMPTY(Nil) -> c16
REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
<'(S(z0), S(z1)) -> c4(<'(z0, z1))
<'(0', S(z0)) -> c5
<'(z0, 0') -> c6
REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite](True, z0, Cons(z1, z2)) -> z2
appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
minsort(Nil) -> Nil
appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

Types:
MINSORT :: Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c13:c14 -> c11:c12
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c13:c14
Nil :: Cons:Nil
c12 :: c11:c12
c13 :: c9:c10 -> c4:c5:c6 -> c13:c14
APPMIN[ITE][TRUE][ITE] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> c9:c10
< :: S:0' -> S:0' -> False:True
<' :: S:0' -> S:0' -> c4:c5:c6
c14 :: c11:c12 -> c17 -> c13:c14
remove :: S:0' -> Cons:Nil -> Cons:Nil
REMOVE :: S:0' -> Cons:Nil -> c17
NOTEMPTY :: Cons:Nil -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
c17 :: c7:c8 -> c:c1:c2:c3 -> c17
REMOVE[ITE] :: False:True -> S:0' -> Cons:Nil -> c7:c8
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
S :: S:0' -> S:0'
c :: c:c1:c2:c3 -> c:c1:c2:c3
0' :: S:0'
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c4:c5:c6 -> c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6
False :: False:True
c7 :: c17 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c13:c14 -> c9:c10
c10 :: c13:c14 -> c9:c10
remove[Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil
appmin[Ite][True][Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
appmin :: S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
minsort :: Cons:Nil -> Cons:Nil
notEmpty :: Cons:Nil -> False:True
hole_c11:c121_18 :: c11:c12
hole_Cons:Nil2_18 :: Cons:Nil
hole_S:0'3_18 :: S:0'
hole_c13:c144_18 :: c13:c14
hole_c9:c105_18 :: c9:c10
hole_c4:c5:c66_18 :: c4:c5:c6
hole_False:True7_18 :: False:True
hole_c178_18 :: c17
hole_c15:c169_18 :: c15:c16
hole_c7:c810_18 :: c7:c8
hole_c:c1:c2:c311_18 :: c:c1:c2:c3
gen_Cons:Nil12_18 :: Nat -> Cons:Nil
gen_S:0'13_18 :: Nat -> S:0'
gen_c4:c5:c614_18 :: Nat -> c4:c5:c6
gen_c:c1:c2:c315_18 :: Nat -> c:c1:c2:c3


Lemmas:
<(gen_S:0'13_18(n17_18), gen_S:0'13_18(+(1, n17_18))) -> True, rt in Omega(0)
<'(gen_S:0'13_18(n391_18), gen_S:0'13_18(+(1, n391_18))) -> gen_c4:c5:c614_18(n391_18), rt in Omega(0)
!EQ(gen_S:0'13_18(n1083_18), gen_S:0'13_18(+(1, n1083_18))) -> False, rt in Omega(0)
remove(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, n1504_18))) -> *16_18, rt in Omega(0)


Generator Equations:
gen_Cons:Nil12_18(0) <=> Nil
gen_Cons:Nil12_18(+(x, 1)) <=> Cons(0', gen_Cons:Nil12_18(x))
gen_S:0'13_18(0) <=> 0'
gen_S:0'13_18(+(x, 1)) <=> S(gen_S:0'13_18(x))
gen_c4:c5:c614_18(0) <=> c5
gen_c4:c5:c614_18(+(x, 1)) <=> c4(gen_c4:c5:c614_18(x))
gen_c:c1:c2:c315_18(0) <=> c1
gen_c:c1:c2:c315_18(+(x, 1)) <=> c(gen_c:c1:c2:c315_18(x))


The following defined symbols remain to be analysed:
!EQ', MINSORT, APPMIN, REMOVE, appmin, minsort

They will be analysed ascendingly in the following order:
MINSORT = APPMIN
REMOVE < APPMIN
!EQ' < REMOVE
appmin = minsort

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
!EQ'(gen_S:0'13_18(n3203_18), gen_S:0'13_18(+(1, n3203_18))) -> gen_c:c1:c2:c315_18(n3203_18), rt in Omega(0)

Induction Base:
!EQ'(gen_S:0'13_18(0), gen_S:0'13_18(+(1, 0))) ->_R^Omega(0)
c1

Induction Step:
!EQ'(gen_S:0'13_18(+(n3203_18, 1)), gen_S:0'13_18(+(1, +(n3203_18, 1)))) ->_R^Omega(0)
c(!EQ'(gen_S:0'13_18(n3203_18), gen_S:0'13_18(+(1, n3203_18)))) ->_IH
c(gen_c:c1:c2:c315_18(c3204_18))

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

(22)
Obligation:
Innermost TRS:
Rules:
MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c12
APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c15
NOTEMPTY(Nil) -> c16
REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
<'(S(z0), S(z1)) -> c4(<'(z0, z1))
<'(0', S(z0)) -> c5
<'(z0, 0') -> c6
REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite](True, z0, Cons(z1, z2)) -> z2
appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
minsort(Nil) -> Nil
appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

Types:
MINSORT :: Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c13:c14 -> c11:c12
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c13:c14
Nil :: Cons:Nil
c12 :: c11:c12
c13 :: c9:c10 -> c4:c5:c6 -> c13:c14
APPMIN[ITE][TRUE][ITE] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> c9:c10
< :: S:0' -> S:0' -> False:True
<' :: S:0' -> S:0' -> c4:c5:c6
c14 :: c11:c12 -> c17 -> c13:c14
remove :: S:0' -> Cons:Nil -> Cons:Nil
REMOVE :: S:0' -> Cons:Nil -> c17
NOTEMPTY :: Cons:Nil -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
c17 :: c7:c8 -> c:c1:c2:c3 -> c17
REMOVE[ITE] :: False:True -> S:0' -> Cons:Nil -> c7:c8
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
S :: S:0' -> S:0'
c :: c:c1:c2:c3 -> c:c1:c2:c3
0' :: S:0'
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c4:c5:c6 -> c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6
False :: False:True
c7 :: c17 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c13:c14 -> c9:c10
c10 :: c13:c14 -> c9:c10
remove[Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil
appmin[Ite][True][Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
appmin :: S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
minsort :: Cons:Nil -> Cons:Nil
notEmpty :: Cons:Nil -> False:True
hole_c11:c121_18 :: c11:c12
hole_Cons:Nil2_18 :: Cons:Nil
hole_S:0'3_18 :: S:0'
hole_c13:c144_18 :: c13:c14
hole_c9:c105_18 :: c9:c10
hole_c4:c5:c66_18 :: c4:c5:c6
hole_False:True7_18 :: False:True
hole_c178_18 :: c17
hole_c15:c169_18 :: c15:c16
hole_c7:c810_18 :: c7:c8
hole_c:c1:c2:c311_18 :: c:c1:c2:c3
gen_Cons:Nil12_18 :: Nat -> Cons:Nil
gen_S:0'13_18 :: Nat -> S:0'
gen_c4:c5:c614_18 :: Nat -> c4:c5:c6
gen_c:c1:c2:c315_18 :: Nat -> c:c1:c2:c3


Lemmas:
<(gen_S:0'13_18(n17_18), gen_S:0'13_18(+(1, n17_18))) -> True, rt in Omega(0)
<'(gen_S:0'13_18(n391_18), gen_S:0'13_18(+(1, n391_18))) -> gen_c4:c5:c614_18(n391_18), rt in Omega(0)
!EQ(gen_S:0'13_18(n1083_18), gen_S:0'13_18(+(1, n1083_18))) -> False, rt in Omega(0)
remove(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, n1504_18))) -> *16_18, rt in Omega(0)
!EQ'(gen_S:0'13_18(n3203_18), gen_S:0'13_18(+(1, n3203_18))) -> gen_c:c1:c2:c315_18(n3203_18), rt in Omega(0)


Generator Equations:
gen_Cons:Nil12_18(0) <=> Nil
gen_Cons:Nil12_18(+(x, 1)) <=> Cons(0', gen_Cons:Nil12_18(x))
gen_S:0'13_18(0) <=> 0'
gen_S:0'13_18(+(x, 1)) <=> S(gen_S:0'13_18(x))
gen_c4:c5:c614_18(0) <=> c5
gen_c4:c5:c614_18(+(x, 1)) <=> c4(gen_c4:c5:c614_18(x))
gen_c:c1:c2:c315_18(0) <=> c1
gen_c:c1:c2:c315_18(+(x, 1)) <=> c(gen_c:c1:c2:c315_18(x))


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

They will be analysed ascendingly in the following order:
MINSORT = APPMIN
REMOVE < APPMIN
appmin = minsort

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REMOVE(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, n4218_18))) -> *16_18, rt in Omega(n4218_18)

Induction Base:
REMOVE(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, 0)))

Induction Step:
REMOVE(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, +(n4218_18, 1)))) ->_R^Omega(1)
c17(REMOVE[ITE](!EQ(gen_S:0'13_18(1), 0'), gen_S:0'13_18(1), Cons(0', gen_Cons:Nil12_18(+(1, n4218_18)))), !EQ'(gen_S:0'13_18(1), 0')) ->_R^Omega(0)
c17(REMOVE[ITE](False, gen_S:0'13_18(1), Cons(0', gen_Cons:Nil12_18(+(1, n4218_18)))), !EQ'(gen_S:0'13_18(1), 0')) ->_R^Omega(0)
c17(c7(REMOVE(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, n4218_18)))), !EQ'(gen_S:0'13_18(1), 0')) ->_IH
c17(c7(*16_18), !EQ'(gen_S:0'13_18(1), 0')) ->_R^Omega(0)
c17(c7(*16_18), c2)

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

(24)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c12
APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c15
NOTEMPTY(Nil) -> c16
REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
<'(S(z0), S(z1)) -> c4(<'(z0, z1))
<'(0', S(z0)) -> c5
<'(z0, 0') -> c6
REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite](True, z0, Cons(z1, z2)) -> z2
appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
minsort(Nil) -> Nil
appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

Types:
MINSORT :: Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c13:c14 -> c11:c12
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c13:c14
Nil :: Cons:Nil
c12 :: c11:c12
c13 :: c9:c10 -> c4:c5:c6 -> c13:c14
APPMIN[ITE][TRUE][ITE] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> c9:c10
< :: S:0' -> S:0' -> False:True
<' :: S:0' -> S:0' -> c4:c5:c6
c14 :: c11:c12 -> c17 -> c13:c14
remove :: S:0' -> Cons:Nil -> Cons:Nil
REMOVE :: S:0' -> Cons:Nil -> c17
NOTEMPTY :: Cons:Nil -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
c17 :: c7:c8 -> c:c1:c2:c3 -> c17
REMOVE[ITE] :: False:True -> S:0' -> Cons:Nil -> c7:c8
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
S :: S:0' -> S:0'
c :: c:c1:c2:c3 -> c:c1:c2:c3
0' :: S:0'
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c4:c5:c6 -> c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6
False :: False:True
c7 :: c17 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c13:c14 -> c9:c10
c10 :: c13:c14 -> c9:c10
remove[Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil
appmin[Ite][True][Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
appmin :: S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
minsort :: Cons:Nil -> Cons:Nil
notEmpty :: Cons:Nil -> False:True
hole_c11:c121_18 :: c11:c12
hole_Cons:Nil2_18 :: Cons:Nil
hole_S:0'3_18 :: S:0'
hole_c13:c144_18 :: c13:c14
hole_c9:c105_18 :: c9:c10
hole_c4:c5:c66_18 :: c4:c5:c6
hole_False:True7_18 :: False:True
hole_c178_18 :: c17
hole_c15:c169_18 :: c15:c16
hole_c7:c810_18 :: c7:c8
hole_c:c1:c2:c311_18 :: c:c1:c2:c3
gen_Cons:Nil12_18 :: Nat -> Cons:Nil
gen_S:0'13_18 :: Nat -> S:0'
gen_c4:c5:c614_18 :: Nat -> c4:c5:c6
gen_c:c1:c2:c315_18 :: Nat -> c:c1:c2:c3


Lemmas:
<(gen_S:0'13_18(n17_18), gen_S:0'13_18(+(1, n17_18))) -> True, rt in Omega(0)
<'(gen_S:0'13_18(n391_18), gen_S:0'13_18(+(1, n391_18))) -> gen_c4:c5:c614_18(n391_18), rt in Omega(0)
!EQ(gen_S:0'13_18(n1083_18), gen_S:0'13_18(+(1, n1083_18))) -> False, rt in Omega(0)
remove(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, n1504_18))) -> *16_18, rt in Omega(0)
!EQ'(gen_S:0'13_18(n3203_18), gen_S:0'13_18(+(1, n3203_18))) -> gen_c:c1:c2:c315_18(n3203_18), rt in Omega(0)


Generator Equations:
gen_Cons:Nil12_18(0) <=> Nil
gen_Cons:Nil12_18(+(x, 1)) <=> Cons(0', gen_Cons:Nil12_18(x))
gen_S:0'13_18(0) <=> 0'
gen_S:0'13_18(+(x, 1)) <=> S(gen_S:0'13_18(x))
gen_c4:c5:c614_18(0) <=> c5
gen_c4:c5:c614_18(+(x, 1)) <=> c4(gen_c4:c5:c614_18(x))
gen_c:c1:c2:c315_18(0) <=> c1
gen_c:c1:c2:c315_18(+(x, 1)) <=> c(gen_c:c1:c2:c315_18(x))


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

They will be analysed ascendingly in the following order:
MINSORT = APPMIN
REMOVE < APPMIN
appmin = minsort

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

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

(27)
BOUNDS(n^1, INF)

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

(28)
Obligation:
Innermost TRS:
Rules:
MINSORT(Cons(z0, z1)) -> c11(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c12
APPMIN(z0, Cons(z1, z2), z3) -> c13(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c14(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c15
NOTEMPTY(Nil) -> c16
REMOVE(z0, Cons(z1, z2)) -> c17(REMOVE[ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
<'(S(z0), S(z1)) -> c4(<'(z0, z1))
<'(0', S(z0)) -> c5
<'(z0, 0') -> c6
REMOVE[ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE](True, z0, Cons(z1, z2)) -> c8
APPMIN[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) -> c9(APPMIN(z1, z2, z3))
APPMIN[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c10(APPMIN(z0, z2, z3))
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
remove[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite](True, z0, Cons(z1, z2)) -> z2
appmin[Ite][True][Ite](True, z0, Cons(z1, z2), z3) -> appmin(z1, z2, z3)
appmin[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> appmin(z0, z2, z3)
minsort(Cons(z0, z1)) -> appmin(z0, z1, Cons(z0, z1))
minsort(Nil) -> Nil
appmin(z0, Cons(z1, z2), z3) -> appmin[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2), z3)
appmin(z0, Nil, z1) -> Cons(z0, minsort(remove(z0, z1)))
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
remove(z0, Cons(z1, z2)) -> remove[Ite](!EQ(z0, z1), z0, Cons(z1, z2))

Types:
MINSORT :: Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c13:c14 -> c11:c12
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c13:c14
Nil :: Cons:Nil
c12 :: c11:c12
c13 :: c9:c10 -> c4:c5:c6 -> c13:c14
APPMIN[ITE][TRUE][ITE] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> c9:c10
< :: S:0' -> S:0' -> False:True
<' :: S:0' -> S:0' -> c4:c5:c6
c14 :: c11:c12 -> c17 -> c13:c14
remove :: S:0' -> Cons:Nil -> Cons:Nil
REMOVE :: S:0' -> Cons:Nil -> c17
NOTEMPTY :: Cons:Nil -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
c17 :: c7:c8 -> c:c1:c2:c3 -> c17
REMOVE[ITE] :: False:True -> S:0' -> Cons:Nil -> c7:c8
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
S :: S:0' -> S:0'
c :: c:c1:c2:c3 -> c:c1:c2:c3
0' :: S:0'
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c4:c5:c6 -> c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6
False :: False:True
c7 :: c17 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c13:c14 -> c9:c10
c10 :: c13:c14 -> c9:c10
remove[Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil
appmin[Ite][True][Ite] :: False:True -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
appmin :: S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
minsort :: Cons:Nil -> Cons:Nil
notEmpty :: Cons:Nil -> False:True
hole_c11:c121_18 :: c11:c12
hole_Cons:Nil2_18 :: Cons:Nil
hole_S:0'3_18 :: S:0'
hole_c13:c144_18 :: c13:c14
hole_c9:c105_18 :: c9:c10
hole_c4:c5:c66_18 :: c4:c5:c6
hole_False:True7_18 :: False:True
hole_c178_18 :: c17
hole_c15:c169_18 :: c15:c16
hole_c7:c810_18 :: c7:c8
hole_c:c1:c2:c311_18 :: c:c1:c2:c3
gen_Cons:Nil12_18 :: Nat -> Cons:Nil
gen_S:0'13_18 :: Nat -> S:0'
gen_c4:c5:c614_18 :: Nat -> c4:c5:c6
gen_c:c1:c2:c315_18 :: Nat -> c:c1:c2:c3


Lemmas:
<(gen_S:0'13_18(n17_18), gen_S:0'13_18(+(1, n17_18))) -> True, rt in Omega(0)
<'(gen_S:0'13_18(n391_18), gen_S:0'13_18(+(1, n391_18))) -> gen_c4:c5:c614_18(n391_18), rt in Omega(0)
!EQ(gen_S:0'13_18(n1083_18), gen_S:0'13_18(+(1, n1083_18))) -> False, rt in Omega(0)
remove(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, n1504_18))) -> *16_18, rt in Omega(0)
!EQ'(gen_S:0'13_18(n3203_18), gen_S:0'13_18(+(1, n3203_18))) -> gen_c:c1:c2:c315_18(n3203_18), rt in Omega(0)
REMOVE(gen_S:0'13_18(1), gen_Cons:Nil12_18(+(1, n4218_18))) -> *16_18, rt in Omega(n4218_18)


Generator Equations:
gen_Cons:Nil12_18(0) <=> Nil
gen_Cons:Nil12_18(+(x, 1)) <=> Cons(0', gen_Cons:Nil12_18(x))
gen_S:0'13_18(0) <=> 0'
gen_S:0'13_18(+(x, 1)) <=> S(gen_S:0'13_18(x))
gen_c4:c5:c614_18(0) <=> c5
gen_c4:c5:c614_18(+(x, 1)) <=> c4(gen_c4:c5:c614_18(x))
gen_c:c1:c2:c315_18(0) <=> c1
gen_c:c1:c2:c315_18(+(x, 1)) <=> c(gen_c:c1:c2:c315_18(x))


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

They will be analysed ascendingly in the following order:
MINSORT = APPMIN
appmin = minsort