WORST_CASE(Omega(n^1),?)
proof of input_GbOUivuCRA.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), 222 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 11 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), 30 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 345 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 179 ms]
(16) typed CpxTrs
(17) RewriteLemmaProof [LOWER BOUND(ID), 595 ms]
(18) BEST
    (19) proven lower bound
        (20) LowerBoundPropagationProof [FINISHED, 0 ms]
        (21) BOUNDS(n^1, INF)
    (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 56 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 67 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 42 ms]
        (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:

   remove(x', Cons(x, xs)) -> remove[Ite][True][Ite](!EQ(x', x), x', Cons(x, xs))
   remove(x, Nil) -> Nil
   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
   goal(xs) -> minsort(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][True][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][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:

   remove(x', Cons(x, xs)) -> remove[Ite][True][Ite](!EQ(x', x), x', Cons(x, xs))
   remove(x, Nil) -> Nil
   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
   goal(xs) -> minsort(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][True][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][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
   remove[Ite][True][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)
   remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
   remove(z0, Nil) -> Nil
   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
   goal(z0) -> minsort(z0)
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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
   REMOVE[ITE][TRUE][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))
   REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
   REMOVE(z0, Nil) -> c12
   MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
   MINSORT(Nil) -> c14
   APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
   APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
   NOTEMPTY(Cons(z0, z1)) -> c17
   NOTEMPTY(Nil) -> c18
   GOAL(z0) -> c19(MINSORT(z0))
S tuples:
   REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
   REMOVE(z0, Nil) -> c12
   MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
   MINSORT(Nil) -> c14
   APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
   APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
   NOTEMPTY(Cons(z0, z1)) -> c17
   NOTEMPTY(Nil) -> c18
   GOAL(z0) -> c19(MINSORT(z0))
K tuples:none
Defined Rule Symbols:   remove_2, minsort_1, appmin_3, notEmpty_1, goal_1, !EQ_2, <_2, remove[Ite][True][Ite]_3, appmin[Ite][True][Ite]_4

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

Compound Symbols:   c_1, c1, c2, c3, c4_1, c5, c6, c7_1, c8, c9_1, c10_1, c11_2, c12, c13_1, c14, c15_2, c16_2, c17, c18, c19_1


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

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

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

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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
   REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
   remove[Ite][True][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)
   remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
   remove(z0, Nil) -> Nil
   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
   goal(z0) -> minsort(z0)

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:

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

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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
   REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
   remove[Ite][True][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)
   remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
   remove(z0, Nil) -> Nil
   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
   goal(z0) -> minsort(z0)

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

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

(10)
Obligation:
Innermost TRS:
Rules:
REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
REMOVE(z0, Nil) -> c12
MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c14
APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c17
NOTEMPTY(Nil) -> c18
GOAL(z0) -> c19(MINSORT(z0))
!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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite][True][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)
remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
remove(z0, Nil) -> Nil
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
goal(z0) -> minsort(z0)

Types:
REMOVE :: S:0' -> Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c7:c8 -> c:c1:c2:c3 -> c11:c12
REMOVE[ITE][TRUE][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
Nil :: Cons:Nil
c12 :: c11:c12
MINSORT :: Cons:Nil -> c13:c14
c13 :: c15:c16 -> c13:c14
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c15:c16
c14 :: c13:c14
c15 :: c9:c10 -> c4:c5:c6 -> c15:c16
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
c16 :: c13:c14 -> c11:c12 -> c15:c16
remove :: S:0' -> Cons:Nil -> Cons:Nil
NOTEMPTY :: Cons:Nil -> c17:c18
c17 :: c17:c18
c18 :: c17:c18
GOAL :: Cons:Nil -> c19
c19 :: c13:c14 -> c19
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 :: c11:c12 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c15:c16 -> c9:c10
c10 :: c15:c16 -> c9:c10
remove[Ite][True][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
goal :: Cons:Nil -> Cons:Nil
hole_c11:c121_20 :: c11:c12
hole_S:0'2_20 :: S:0'
hole_Cons:Nil3_20 :: Cons:Nil
hole_c7:c84_20 :: c7:c8
hole_c:c1:c2:c35_20 :: c:c1:c2:c3
hole_False:True6_20 :: False:True
hole_c13:c147_20 :: c13:c14
hole_c15:c168_20 :: c15:c16
hole_c9:c109_20 :: c9:c10
hole_c4:c5:c610_20 :: c4:c5:c6
hole_c17:c1811_20 :: c17:c18
hole_c1912_20 :: c19
gen_S:0'13_20 :: Nat -> S:0'
gen_Cons:Nil14_20 :: Nat -> Cons:Nil
gen_c:c1:c2:c315_20 :: Nat -> c:c1:c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6

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

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

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

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

(12)
Obligation:
Innermost TRS:
Rules:
REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
REMOVE(z0, Nil) -> c12
MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c14
APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c17
NOTEMPTY(Nil) -> c18
GOAL(z0) -> c19(MINSORT(z0))
!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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite][True][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)
remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
remove(z0, Nil) -> Nil
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
goal(z0) -> minsort(z0)

Types:
REMOVE :: S:0' -> Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c7:c8 -> c:c1:c2:c3 -> c11:c12
REMOVE[ITE][TRUE][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
Nil :: Cons:Nil
c12 :: c11:c12
MINSORT :: Cons:Nil -> c13:c14
c13 :: c15:c16 -> c13:c14
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c15:c16
c14 :: c13:c14
c15 :: c9:c10 -> c4:c5:c6 -> c15:c16
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
c16 :: c13:c14 -> c11:c12 -> c15:c16
remove :: S:0' -> Cons:Nil -> Cons:Nil
NOTEMPTY :: Cons:Nil -> c17:c18
c17 :: c17:c18
c18 :: c17:c18
GOAL :: Cons:Nil -> c19
c19 :: c13:c14 -> c19
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 :: c11:c12 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c15:c16 -> c9:c10
c10 :: c15:c16 -> c9:c10
remove[Ite][True][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
goal :: Cons:Nil -> Cons:Nil
hole_c11:c121_20 :: c11:c12
hole_S:0'2_20 :: S:0'
hole_Cons:Nil3_20 :: Cons:Nil
hole_c7:c84_20 :: c7:c8
hole_c:c1:c2:c35_20 :: c:c1:c2:c3
hole_False:True6_20 :: False:True
hole_c13:c147_20 :: c13:c14
hole_c15:c168_20 :: c15:c16
hole_c9:c109_20 :: c9:c10
hole_c4:c5:c610_20 :: c4:c5:c6
hole_c17:c1811_20 :: c17:c18
hole_c1912_20 :: c19
gen_S:0'13_20 :: Nat -> S:0'
gen_Cons:Nil14_20 :: Nat -> Cons:Nil
gen_c:c1:c2:c315_20 :: Nat -> c:c1:c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6


Generator Equations:
gen_S:0'13_20(0) <=> 0'
gen_S:0'13_20(+(x, 1)) <=> S(gen_S:0'13_20(x))
gen_Cons:Nil14_20(0) <=> Nil
gen_Cons:Nil14_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil14_20(x))
gen_c:c1:c2:c315_20(0) <=> c1
gen_c:c1:c2:c315_20(+(x, 1)) <=> c(gen_c:c1:c2:c315_20(x))
gen_c4:c5:c616_20(0) <=> c5
gen_c4:c5:c616_20(+(x, 1)) <=> c4(gen_c4:c5:c616_20(x))


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

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

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

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

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

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

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:
REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
REMOVE(z0, Nil) -> c12
MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c14
APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c17
NOTEMPTY(Nil) -> c18
GOAL(z0) -> c19(MINSORT(z0))
!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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite][True][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)
remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
remove(z0, Nil) -> Nil
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
goal(z0) -> minsort(z0)

Types:
REMOVE :: S:0' -> Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c7:c8 -> c:c1:c2:c3 -> c11:c12
REMOVE[ITE][TRUE][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
Nil :: Cons:Nil
c12 :: c11:c12
MINSORT :: Cons:Nil -> c13:c14
c13 :: c15:c16 -> c13:c14
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c15:c16
c14 :: c13:c14
c15 :: c9:c10 -> c4:c5:c6 -> c15:c16
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
c16 :: c13:c14 -> c11:c12 -> c15:c16
remove :: S:0' -> Cons:Nil -> Cons:Nil
NOTEMPTY :: Cons:Nil -> c17:c18
c17 :: c17:c18
c18 :: c17:c18
GOAL :: Cons:Nil -> c19
c19 :: c13:c14 -> c19
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 :: c11:c12 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c15:c16 -> c9:c10
c10 :: c15:c16 -> c9:c10
remove[Ite][True][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
goal :: Cons:Nil -> Cons:Nil
hole_c11:c121_20 :: c11:c12
hole_S:0'2_20 :: S:0'
hole_Cons:Nil3_20 :: Cons:Nil
hole_c7:c84_20 :: c7:c8
hole_c:c1:c2:c35_20 :: c:c1:c2:c3
hole_False:True6_20 :: False:True
hole_c13:c147_20 :: c13:c14
hole_c15:c168_20 :: c15:c16
hole_c9:c109_20 :: c9:c10
hole_c4:c5:c610_20 :: c4:c5:c6
hole_c17:c1811_20 :: c17:c18
hole_c1912_20 :: c19
gen_S:0'13_20 :: Nat -> S:0'
gen_Cons:Nil14_20 :: Nat -> Cons:Nil
gen_c:c1:c2:c315_20 :: Nat -> c:c1:c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6


Lemmas:
!EQ(gen_S:0'13_20(n18_20), gen_S:0'13_20(+(1, n18_20))) -> False, rt in Omega(0)


Generator Equations:
gen_S:0'13_20(0) <=> 0'
gen_S:0'13_20(+(x, 1)) <=> S(gen_S:0'13_20(x))
gen_Cons:Nil14_20(0) <=> Nil
gen_Cons:Nil14_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil14_20(x))
gen_c:c1:c2:c315_20(0) <=> c1
gen_c:c1:c2:c315_20(+(x, 1)) <=> c(gen_c:c1:c2:c315_20(x))
gen_c4:c5:c616_20(0) <=> c5
gen_c4:c5:c616_20(+(x, 1)) <=> c4(gen_c4:c5:c616_20(x))


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

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

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
!EQ'(gen_S:0'13_20(n449_20), gen_S:0'13_20(+(1, n449_20))) -> gen_c:c1:c2:c315_20(n449_20), rt in Omega(0)

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

Induction Step:
!EQ'(gen_S:0'13_20(+(n449_20, 1)), gen_S:0'13_20(+(1, +(n449_20, 1)))) ->_R^Omega(0)
c(!EQ'(gen_S:0'13_20(n449_20), gen_S:0'13_20(+(1, n449_20)))) ->_IH
c(gen_c:c1:c2:c315_20(c450_20))

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:
REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
REMOVE(z0, Nil) -> c12
MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c14
APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c17
NOTEMPTY(Nil) -> c18
GOAL(z0) -> c19(MINSORT(z0))
!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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite][True][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)
remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
remove(z0, Nil) -> Nil
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
goal(z0) -> minsort(z0)

Types:
REMOVE :: S:0' -> Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c7:c8 -> c:c1:c2:c3 -> c11:c12
REMOVE[ITE][TRUE][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
Nil :: Cons:Nil
c12 :: c11:c12
MINSORT :: Cons:Nil -> c13:c14
c13 :: c15:c16 -> c13:c14
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c15:c16
c14 :: c13:c14
c15 :: c9:c10 -> c4:c5:c6 -> c15:c16
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
c16 :: c13:c14 -> c11:c12 -> c15:c16
remove :: S:0' -> Cons:Nil -> Cons:Nil
NOTEMPTY :: Cons:Nil -> c17:c18
c17 :: c17:c18
c18 :: c17:c18
GOAL :: Cons:Nil -> c19
c19 :: c13:c14 -> c19
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 :: c11:c12 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c15:c16 -> c9:c10
c10 :: c15:c16 -> c9:c10
remove[Ite][True][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
goal :: Cons:Nil -> Cons:Nil
hole_c11:c121_20 :: c11:c12
hole_S:0'2_20 :: S:0'
hole_Cons:Nil3_20 :: Cons:Nil
hole_c7:c84_20 :: c7:c8
hole_c:c1:c2:c35_20 :: c:c1:c2:c3
hole_False:True6_20 :: False:True
hole_c13:c147_20 :: c13:c14
hole_c15:c168_20 :: c15:c16
hole_c9:c109_20 :: c9:c10
hole_c4:c5:c610_20 :: c4:c5:c6
hole_c17:c1811_20 :: c17:c18
hole_c1912_20 :: c19
gen_S:0'13_20 :: Nat -> S:0'
gen_Cons:Nil14_20 :: Nat -> Cons:Nil
gen_c:c1:c2:c315_20 :: Nat -> c:c1:c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6


Lemmas:
!EQ(gen_S:0'13_20(n18_20), gen_S:0'13_20(+(1, n18_20))) -> False, rt in Omega(0)
!EQ'(gen_S:0'13_20(n449_20), gen_S:0'13_20(+(1, n449_20))) -> gen_c:c1:c2:c315_20(n449_20), rt in Omega(0)


Generator Equations:
gen_S:0'13_20(0) <=> 0'
gen_S:0'13_20(+(x, 1)) <=> S(gen_S:0'13_20(x))
gen_Cons:Nil14_20(0) <=> Nil
gen_Cons:Nil14_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil14_20(x))
gen_c:c1:c2:c315_20(0) <=> c1
gen_c:c1:c2:c315_20(+(x, 1)) <=> c(gen_c:c1:c2:c315_20(x))
gen_c4:c5:c616_20(0) <=> c5
gen_c4:c5:c616_20(+(x, 1)) <=> c4(gen_c4:c5:c616_20(x))


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

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

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REMOVE(gen_S:0'13_20(1), gen_Cons:Nil14_20(+(1, n1291_20))) -> *17_20, rt in Omega(n1291_20)

Induction Base:
REMOVE(gen_S:0'13_20(1), gen_Cons:Nil14_20(+(1, 0)))

Induction Step:
REMOVE(gen_S:0'13_20(1), gen_Cons:Nil14_20(+(1, +(n1291_20, 1)))) ->_R^Omega(1)
c11(REMOVE[ITE][TRUE][ITE](!EQ(gen_S:0'13_20(1), 0'), gen_S:0'13_20(1), Cons(0', gen_Cons:Nil14_20(+(1, n1291_20)))), !EQ'(gen_S:0'13_20(1), 0')) ->_R^Omega(0)
c11(REMOVE[ITE][TRUE][ITE](False, gen_S:0'13_20(1), Cons(0', gen_Cons:Nil14_20(+(1, n1291_20)))), !EQ'(gen_S:0'13_20(1), 0')) ->_R^Omega(0)
c11(c7(REMOVE(gen_S:0'13_20(1), gen_Cons:Nil14_20(+(1, n1291_20)))), !EQ'(gen_S:0'13_20(1), 0')) ->_IH
c11(c7(*17_20), !EQ'(gen_S:0'13_20(1), 0')) ->_R^Omega(0)
c11(c7(*17_20), c2)

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

(18)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
REMOVE(z0, Nil) -> c12
MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c14
APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c17
NOTEMPTY(Nil) -> c18
GOAL(z0) -> c19(MINSORT(z0))
!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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite][True][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)
remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
remove(z0, Nil) -> Nil
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
goal(z0) -> minsort(z0)

Types:
REMOVE :: S:0' -> Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c7:c8 -> c:c1:c2:c3 -> c11:c12
REMOVE[ITE][TRUE][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
Nil :: Cons:Nil
c12 :: c11:c12
MINSORT :: Cons:Nil -> c13:c14
c13 :: c15:c16 -> c13:c14
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c15:c16
c14 :: c13:c14
c15 :: c9:c10 -> c4:c5:c6 -> c15:c16
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
c16 :: c13:c14 -> c11:c12 -> c15:c16
remove :: S:0' -> Cons:Nil -> Cons:Nil
NOTEMPTY :: Cons:Nil -> c17:c18
c17 :: c17:c18
c18 :: c17:c18
GOAL :: Cons:Nil -> c19
c19 :: c13:c14 -> c19
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 :: c11:c12 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c15:c16 -> c9:c10
c10 :: c15:c16 -> c9:c10
remove[Ite][True][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
goal :: Cons:Nil -> Cons:Nil
hole_c11:c121_20 :: c11:c12
hole_S:0'2_20 :: S:0'
hole_Cons:Nil3_20 :: Cons:Nil
hole_c7:c84_20 :: c7:c8
hole_c:c1:c2:c35_20 :: c:c1:c2:c3
hole_False:True6_20 :: False:True
hole_c13:c147_20 :: c13:c14
hole_c15:c168_20 :: c15:c16
hole_c9:c109_20 :: c9:c10
hole_c4:c5:c610_20 :: c4:c5:c6
hole_c17:c1811_20 :: c17:c18
hole_c1912_20 :: c19
gen_S:0'13_20 :: Nat -> S:0'
gen_Cons:Nil14_20 :: Nat -> Cons:Nil
gen_c:c1:c2:c315_20 :: Nat -> c:c1:c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6


Lemmas:
!EQ(gen_S:0'13_20(n18_20), gen_S:0'13_20(+(1, n18_20))) -> False, rt in Omega(0)
!EQ'(gen_S:0'13_20(n449_20), gen_S:0'13_20(+(1, n449_20))) -> gen_c:c1:c2:c315_20(n449_20), rt in Omega(0)


Generator Equations:
gen_S:0'13_20(0) <=> 0'
gen_S:0'13_20(+(x, 1)) <=> S(gen_S:0'13_20(x))
gen_Cons:Nil14_20(0) <=> Nil
gen_Cons:Nil14_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil14_20(x))
gen_c:c1:c2:c315_20(0) <=> c1
gen_c:c1:c2:c315_20(+(x, 1)) <=> c(gen_c:c1:c2:c315_20(x))
gen_c4:c5:c616_20(0) <=> c5
gen_c4:c5:c616_20(+(x, 1)) <=> c4(gen_c4:c5:c616_20(x))


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

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

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

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

(21)
BOUNDS(n^1, INF)

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

(22)
Obligation:
Innermost TRS:
Rules:
REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
REMOVE(z0, Nil) -> c12
MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c14
APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c17
NOTEMPTY(Nil) -> c18
GOAL(z0) -> c19(MINSORT(z0))
!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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite][True][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)
remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
remove(z0, Nil) -> Nil
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
goal(z0) -> minsort(z0)

Types:
REMOVE :: S:0' -> Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c7:c8 -> c:c1:c2:c3 -> c11:c12
REMOVE[ITE][TRUE][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
Nil :: Cons:Nil
c12 :: c11:c12
MINSORT :: Cons:Nil -> c13:c14
c13 :: c15:c16 -> c13:c14
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c15:c16
c14 :: c13:c14
c15 :: c9:c10 -> c4:c5:c6 -> c15:c16
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
c16 :: c13:c14 -> c11:c12 -> c15:c16
remove :: S:0' -> Cons:Nil -> Cons:Nil
NOTEMPTY :: Cons:Nil -> c17:c18
c17 :: c17:c18
c18 :: c17:c18
GOAL :: Cons:Nil -> c19
c19 :: c13:c14 -> c19
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 :: c11:c12 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c15:c16 -> c9:c10
c10 :: c15:c16 -> c9:c10
remove[Ite][True][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
goal :: Cons:Nil -> Cons:Nil
hole_c11:c121_20 :: c11:c12
hole_S:0'2_20 :: S:0'
hole_Cons:Nil3_20 :: Cons:Nil
hole_c7:c84_20 :: c7:c8
hole_c:c1:c2:c35_20 :: c:c1:c2:c3
hole_False:True6_20 :: False:True
hole_c13:c147_20 :: c13:c14
hole_c15:c168_20 :: c15:c16
hole_c9:c109_20 :: c9:c10
hole_c4:c5:c610_20 :: c4:c5:c6
hole_c17:c1811_20 :: c17:c18
hole_c1912_20 :: c19
gen_S:0'13_20 :: Nat -> S:0'
gen_Cons:Nil14_20 :: Nat -> Cons:Nil
gen_c:c1:c2:c315_20 :: Nat -> c:c1:c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6


Lemmas:
!EQ(gen_S:0'13_20(n18_20), gen_S:0'13_20(+(1, n18_20))) -> False, rt in Omega(0)
!EQ'(gen_S:0'13_20(n449_20), gen_S:0'13_20(+(1, n449_20))) -> gen_c:c1:c2:c315_20(n449_20), rt in Omega(0)
REMOVE(gen_S:0'13_20(1), gen_Cons:Nil14_20(+(1, n1291_20))) -> *17_20, rt in Omega(n1291_20)


Generator Equations:
gen_S:0'13_20(0) <=> 0'
gen_S:0'13_20(+(x, 1)) <=> S(gen_S:0'13_20(x))
gen_Cons:Nil14_20(0) <=> Nil
gen_Cons:Nil14_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil14_20(x))
gen_c:c1:c2:c315_20(0) <=> c1
gen_c:c1:c2:c315_20(+(x, 1)) <=> c(gen_c:c1:c2:c315_20(x))
gen_c4:c5:c616_20(0) <=> c5
gen_c4:c5:c616_20(+(x, 1)) <=> c4(gen_c4:c5:c616_20(x))


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

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

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

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

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

Induction Step:
<(gen_S:0'13_20(+(n4502_20, 1)), gen_S:0'13_20(+(1, +(n4502_20, 1)))) ->_R^Omega(0)
<(gen_S:0'13_20(n4502_20), gen_S:0'13_20(+(1, n4502_20))) ->_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:
REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
REMOVE(z0, Nil) -> c12
MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c14
APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c17
NOTEMPTY(Nil) -> c18
GOAL(z0) -> c19(MINSORT(z0))
!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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite][True][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)
remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
remove(z0, Nil) -> Nil
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
goal(z0) -> minsort(z0)

Types:
REMOVE :: S:0' -> Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c7:c8 -> c:c1:c2:c3 -> c11:c12
REMOVE[ITE][TRUE][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
Nil :: Cons:Nil
c12 :: c11:c12
MINSORT :: Cons:Nil -> c13:c14
c13 :: c15:c16 -> c13:c14
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c15:c16
c14 :: c13:c14
c15 :: c9:c10 -> c4:c5:c6 -> c15:c16
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
c16 :: c13:c14 -> c11:c12 -> c15:c16
remove :: S:0' -> Cons:Nil -> Cons:Nil
NOTEMPTY :: Cons:Nil -> c17:c18
c17 :: c17:c18
c18 :: c17:c18
GOAL :: Cons:Nil -> c19
c19 :: c13:c14 -> c19
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 :: c11:c12 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c15:c16 -> c9:c10
c10 :: c15:c16 -> c9:c10
remove[Ite][True][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
goal :: Cons:Nil -> Cons:Nil
hole_c11:c121_20 :: c11:c12
hole_S:0'2_20 :: S:0'
hole_Cons:Nil3_20 :: Cons:Nil
hole_c7:c84_20 :: c7:c8
hole_c:c1:c2:c35_20 :: c:c1:c2:c3
hole_False:True6_20 :: False:True
hole_c13:c147_20 :: c13:c14
hole_c15:c168_20 :: c15:c16
hole_c9:c109_20 :: c9:c10
hole_c4:c5:c610_20 :: c4:c5:c6
hole_c17:c1811_20 :: c17:c18
hole_c1912_20 :: c19
gen_S:0'13_20 :: Nat -> S:0'
gen_Cons:Nil14_20 :: Nat -> Cons:Nil
gen_c:c1:c2:c315_20 :: Nat -> c:c1:c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6


Lemmas:
!EQ(gen_S:0'13_20(n18_20), gen_S:0'13_20(+(1, n18_20))) -> False, rt in Omega(0)
!EQ'(gen_S:0'13_20(n449_20), gen_S:0'13_20(+(1, n449_20))) -> gen_c:c1:c2:c315_20(n449_20), rt in Omega(0)
REMOVE(gen_S:0'13_20(1), gen_Cons:Nil14_20(+(1, n1291_20))) -> *17_20, rt in Omega(n1291_20)
<(gen_S:0'13_20(n4502_20), gen_S:0'13_20(+(1, n4502_20))) -> True, rt in Omega(0)


Generator Equations:
gen_S:0'13_20(0) <=> 0'
gen_S:0'13_20(+(x, 1)) <=> S(gen_S:0'13_20(x))
gen_Cons:Nil14_20(0) <=> Nil
gen_Cons:Nil14_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil14_20(x))
gen_c:c1:c2:c315_20(0) <=> c1
gen_c:c1:c2:c315_20(+(x, 1)) <=> c(gen_c:c1:c2:c315_20(x))
gen_c4:c5:c616_20(0) <=> c5
gen_c4:c5:c616_20(+(x, 1)) <=> c4(gen_c4:c5:c616_20(x))


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

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

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
<'(gen_S:0'13_20(n4968_20), gen_S:0'13_20(+(1, n4968_20))) -> gen_c4:c5:c616_20(n4968_20), rt in Omega(0)

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

Induction Step:
<'(gen_S:0'13_20(+(n4968_20, 1)), gen_S:0'13_20(+(1, +(n4968_20, 1)))) ->_R^Omega(0)
c4(<'(gen_S:0'13_20(n4968_20), gen_S:0'13_20(+(1, n4968_20)))) ->_IH
c4(gen_c4:c5:c616_20(c4969_20))

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:
REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
REMOVE(z0, Nil) -> c12
MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c14
APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c17
NOTEMPTY(Nil) -> c18
GOAL(z0) -> c19(MINSORT(z0))
!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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite][True][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)
remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
remove(z0, Nil) -> Nil
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
goal(z0) -> minsort(z0)

Types:
REMOVE :: S:0' -> Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c7:c8 -> c:c1:c2:c3 -> c11:c12
REMOVE[ITE][TRUE][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
Nil :: Cons:Nil
c12 :: c11:c12
MINSORT :: Cons:Nil -> c13:c14
c13 :: c15:c16 -> c13:c14
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c15:c16
c14 :: c13:c14
c15 :: c9:c10 -> c4:c5:c6 -> c15:c16
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
c16 :: c13:c14 -> c11:c12 -> c15:c16
remove :: S:0' -> Cons:Nil -> Cons:Nil
NOTEMPTY :: Cons:Nil -> c17:c18
c17 :: c17:c18
c18 :: c17:c18
GOAL :: Cons:Nil -> c19
c19 :: c13:c14 -> c19
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 :: c11:c12 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c15:c16 -> c9:c10
c10 :: c15:c16 -> c9:c10
remove[Ite][True][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
goal :: Cons:Nil -> Cons:Nil
hole_c11:c121_20 :: c11:c12
hole_S:0'2_20 :: S:0'
hole_Cons:Nil3_20 :: Cons:Nil
hole_c7:c84_20 :: c7:c8
hole_c:c1:c2:c35_20 :: c:c1:c2:c3
hole_False:True6_20 :: False:True
hole_c13:c147_20 :: c13:c14
hole_c15:c168_20 :: c15:c16
hole_c9:c109_20 :: c9:c10
hole_c4:c5:c610_20 :: c4:c5:c6
hole_c17:c1811_20 :: c17:c18
hole_c1912_20 :: c19
gen_S:0'13_20 :: Nat -> S:0'
gen_Cons:Nil14_20 :: Nat -> Cons:Nil
gen_c:c1:c2:c315_20 :: Nat -> c:c1:c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6


Lemmas:
!EQ(gen_S:0'13_20(n18_20), gen_S:0'13_20(+(1, n18_20))) -> False, rt in Omega(0)
!EQ'(gen_S:0'13_20(n449_20), gen_S:0'13_20(+(1, n449_20))) -> gen_c:c1:c2:c315_20(n449_20), rt in Omega(0)
REMOVE(gen_S:0'13_20(1), gen_Cons:Nil14_20(+(1, n1291_20))) -> *17_20, rt in Omega(n1291_20)
<(gen_S:0'13_20(n4502_20), gen_S:0'13_20(+(1, n4502_20))) -> True, rt in Omega(0)
<'(gen_S:0'13_20(n4968_20), gen_S:0'13_20(+(1, n4968_20))) -> gen_c4:c5:c616_20(n4968_20), rt in Omega(0)


Generator Equations:
gen_S:0'13_20(0) <=> 0'
gen_S:0'13_20(+(x, 1)) <=> S(gen_S:0'13_20(x))
gen_Cons:Nil14_20(0) <=> Nil
gen_Cons:Nil14_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil14_20(x))
gen_c:c1:c2:c315_20(0) <=> c1
gen_c:c1:c2:c315_20(+(x, 1)) <=> c(gen_c:c1:c2:c315_20(x))
gen_c4:c5:c616_20(0) <=> c5
gen_c4:c5:c616_20(+(x, 1)) <=> c4(gen_c4:c5:c616_20(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
remove < appmin
appmin = minsort

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
remove(gen_S:0'13_20(1), gen_Cons:Nil14_20(n5849_20)) -> gen_Cons:Nil14_20(n5849_20), rt in Omega(0)

Induction Base:
remove(gen_S:0'13_20(1), gen_Cons:Nil14_20(0)) ->_R^Omega(0)
Nil

Induction Step:
remove(gen_S:0'13_20(1), gen_Cons:Nil14_20(+(n5849_20, 1))) ->_R^Omega(0)
remove[Ite][True][Ite](!EQ(gen_S:0'13_20(1), 0'), gen_S:0'13_20(1), Cons(0', gen_Cons:Nil14_20(n5849_20))) ->_R^Omega(0)
remove[Ite][True][Ite](False, gen_S:0'13_20(1), Cons(0', gen_Cons:Nil14_20(n5849_20))) ->_R^Omega(0)
Cons(0', remove(gen_S:0'13_20(1), gen_Cons:Nil14_20(n5849_20))) ->_IH
Cons(0', gen_Cons:Nil14_20(c5850_20))

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

(28)
Obligation:
Innermost TRS:
Rules:
REMOVE(z0, Cons(z1, z2)) -> c11(REMOVE[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
REMOVE(z0, Nil) -> c12
MINSORT(Cons(z0, z1)) -> c13(APPMIN(z0, z1, Cons(z0, z1)))
MINSORT(Nil) -> c14
APPMIN(z0, Cons(z1, z2), z3) -> c15(APPMIN[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2), z3), <'(z1, z0))
APPMIN(z0, Nil, z1) -> c16(MINSORT(remove(z0, z1)), REMOVE(z0, z1))
NOTEMPTY(Cons(z0, z1)) -> c17
NOTEMPTY(Nil) -> c18
GOAL(z0) -> c19(MINSORT(z0))
!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][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(REMOVE(z0, z2))
REMOVE[ITE][TRUE][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][True][Ite](False, z0, Cons(z1, z2)) -> Cons(z1, remove(z0, z2))
remove[Ite][True][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)
remove(z0, Cons(z1, z2)) -> remove[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2))
remove(z0, Nil) -> Nil
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
goal(z0) -> minsort(z0)

Types:
REMOVE :: S:0' -> Cons:Nil -> c11:c12
Cons :: S:0' -> Cons:Nil -> Cons:Nil
c11 :: c7:c8 -> c:c1:c2:c3 -> c11:c12
REMOVE[ITE][TRUE][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
Nil :: Cons:Nil
c12 :: c11:c12
MINSORT :: Cons:Nil -> c13:c14
c13 :: c15:c16 -> c13:c14
APPMIN :: S:0' -> Cons:Nil -> Cons:Nil -> c15:c16
c14 :: c13:c14
c15 :: c9:c10 -> c4:c5:c6 -> c15:c16
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
c16 :: c13:c14 -> c11:c12 -> c15:c16
remove :: S:0' -> Cons:Nil -> Cons:Nil
NOTEMPTY :: Cons:Nil -> c17:c18
c17 :: c17:c18
c18 :: c17:c18
GOAL :: Cons:Nil -> c19
c19 :: c13:c14 -> c19
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 :: c11:c12 -> c7:c8
True :: False:True
c8 :: c7:c8
c9 :: c15:c16 -> c9:c10
c10 :: c15:c16 -> c9:c10
remove[Ite][True][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
goal :: Cons:Nil -> Cons:Nil
hole_c11:c121_20 :: c11:c12
hole_S:0'2_20 :: S:0'
hole_Cons:Nil3_20 :: Cons:Nil
hole_c7:c84_20 :: c7:c8
hole_c:c1:c2:c35_20 :: c:c1:c2:c3
hole_False:True6_20 :: False:True
hole_c13:c147_20 :: c13:c14
hole_c15:c168_20 :: c15:c16
hole_c9:c109_20 :: c9:c10
hole_c4:c5:c610_20 :: c4:c5:c6
hole_c17:c1811_20 :: c17:c18
hole_c1912_20 :: c19
gen_S:0'13_20 :: Nat -> S:0'
gen_Cons:Nil14_20 :: Nat -> Cons:Nil
gen_c:c1:c2:c315_20 :: Nat -> c:c1:c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6


Lemmas:
!EQ(gen_S:0'13_20(n18_20), gen_S:0'13_20(+(1, n18_20))) -> False, rt in Omega(0)
!EQ'(gen_S:0'13_20(n449_20), gen_S:0'13_20(+(1, n449_20))) -> gen_c:c1:c2:c315_20(n449_20), rt in Omega(0)
REMOVE(gen_S:0'13_20(1), gen_Cons:Nil14_20(+(1, n1291_20))) -> *17_20, rt in Omega(n1291_20)
<(gen_S:0'13_20(n4502_20), gen_S:0'13_20(+(1, n4502_20))) -> True, rt in Omega(0)
<'(gen_S:0'13_20(n4968_20), gen_S:0'13_20(+(1, n4968_20))) -> gen_c4:c5:c616_20(n4968_20), rt in Omega(0)
remove(gen_S:0'13_20(1), gen_Cons:Nil14_20(n5849_20)) -> gen_Cons:Nil14_20(n5849_20), rt in Omega(0)


Generator Equations:
gen_S:0'13_20(0) <=> 0'
gen_S:0'13_20(+(x, 1)) <=> S(gen_S:0'13_20(x))
gen_Cons:Nil14_20(0) <=> Nil
gen_Cons:Nil14_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil14_20(x))
gen_c:c1:c2:c315_20(0) <=> c1
gen_c:c1:c2:c315_20(+(x, 1)) <=> c(gen_c:c1:c2:c315_20(x))
gen_c4:c5:c616_20(0) <=> c5
gen_c4:c5:c616_20(+(x, 1)) <=> c4(gen_c4:c5:c616_20(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