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


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 43 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 28 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 446 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 144 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 60 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 60 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 590 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 0 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 661 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 48 ms]
        (30) typed CpxTrs
        (31) RewriteLemmaProof [LOWER BOUND(ID), 77 ms]
        (32) typed CpxTrs
        (33) RewriteLemmaProof [LOWER BOUND(ID), 51 ms]
        (34) typed CpxTrs


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

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


The TRS R consists of the following rules:

   eq(0, 0) -> true
   eq(0, s(x)) -> false
   eq(s(x), 0) -> false
   eq(s(x), s(y)) -> eq(x, y)
   le(0, y) -> true
   le(s(x), 0) -> false
   le(s(x), s(y)) -> le(x, y)
   app(nil, y) -> y
   app(add(n, x), y) -> add(n, app(x, y))
   min(add(n, nil)) -> n
   min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x)))
   if_min(true, add(n, add(m, x))) -> min(add(n, x))
   if_min(false, add(n, add(m, x))) -> min(add(m, x))
   head(add(n, x)) -> n
   tail(add(n, x)) -> x
   tail(nil) -> nil
   null(nil) -> true
   null(add(n, x)) -> false
   rm(n, nil) -> nil
   rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x))
   if_rm(true, n, add(m, x)) -> rm(n, x)
   if_rm(false, n, add(m, x)) -> add(m, rm(n, x))
   minsort(x) -> mins(x, nil, nil)
   mins(x, y, z) -> if(null(x), x, y, z)
   if(true, x, y, z) -> z
   if(false, x, y, z) -> if2(eq(head(x), min(x)), x, y, z)
   if2(true, x, y, z) -> mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
   if2(false, x, y, z) -> mins(tail(x), add(head(x), y), z)

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   app(nil, z0) -> z0
   app(add(z0, z1), z2) -> add(z0, app(z1, z2))
   min(add(z0, nil)) -> z0
   min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
   if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
   if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
   head(add(z0, z1)) -> z0
   tail(add(z0, z1)) -> z1
   tail(nil) -> nil
   null(nil) -> true
   null(add(z0, z1)) -> false
   rm(z0, nil) -> nil
   rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
   if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
   if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
   minsort(z0) -> mins(z0, nil, nil)
   mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
   if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
   if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)
Tuples:
   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   APP(nil, z0) -> c7
   APP(add(z0, z1), z2) -> c8(APP(z1, z2))
   MIN(add(z0, nil)) -> c9
   MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
   IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
   IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
   HEAD(add(z0, z1)) -> c13
   TAIL(add(z0, z1)) -> c14
   TAIL(nil) -> c15
   NULL(nil) -> c16
   NULL(add(z0, z1)) -> c17
   RM(z0, nil) -> c18
   RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
   IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
   IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
   MINSORT(z0) -> c22(MINS(z0, nil, nil))
   MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
   IF(true, z0, z1, z2) -> c24
   IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
   IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
   IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
   IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
   IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
   IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
   IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
S tuples:
   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   APP(nil, z0) -> c7
   APP(add(z0, z1), z2) -> c8(APP(z1, z2))
   MIN(add(z0, nil)) -> c9
   MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
   IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
   IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
   HEAD(add(z0, z1)) -> c13
   TAIL(add(z0, z1)) -> c14
   TAIL(nil) -> c15
   NULL(nil) -> c16
   NULL(add(z0, z1)) -> c17
   RM(z0, nil) -> c18
   RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
   IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
   IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
   MINSORT(z0) -> c22(MINS(z0, nil, nil))
   MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
   IF(true, z0, z1, z2) -> c24
   IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
   IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
   IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
   IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
   IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
   IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
   IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
K tuples:none
Defined Rule Symbols:   eq_2, le_2, app_2, min_1, if_min_2, head_1, tail_1, null_1, rm_2, if_rm_3, minsort_1, mins_3, if_4, if2_4

Defined Pair Symbols:   EQ_2, LE_2, APP_2, MIN_1, IF_MIN_2, HEAD_1, TAIL_1, NULL_1, RM_2, IF_RM_3, MINSORT_1, MINS_3, IF_4, IF2_4

Compound Symbols:   c, c1, c2, c3_1, c4, c5, c6_1, c7, c8_1, c9, c10_2, c11_1, c12_1, c13, c14, c15, c16, c17, c18, c19_2, c20_1, c21_1, c22_1, c23_2, c24, c25_3, c26_3, c27_4, c28_4, c29_3, c30_2, c31_2


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

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

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


The TRS R consists of the following rules:

   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   APP(nil, z0) -> c7
   APP(add(z0, z1), z2) -> c8(APP(z1, z2))
   MIN(add(z0, nil)) -> c9
   MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
   IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
   IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
   HEAD(add(z0, z1)) -> c13
   TAIL(add(z0, z1)) -> c14
   TAIL(nil) -> c15
   NULL(nil) -> c16
   NULL(add(z0, z1)) -> c17
   RM(z0, nil) -> c18
   RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
   IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
   IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
   MINSORT(z0) -> c22(MINS(z0, nil, nil))
   MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
   IF(true, z0, z1, z2) -> c24
   IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
   IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
   IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
   IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
   IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
   IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
   IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))

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

   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   app(nil, z0) -> z0
   app(add(z0, z1), z2) -> add(z0, app(z1, z2))
   min(add(z0, nil)) -> z0
   min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
   if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
   if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
   head(add(z0, z1)) -> z0
   tail(add(z0, z1)) -> z1
   tail(nil) -> nil
   null(nil) -> true
   null(add(z0, z1)) -> false
   rm(z0, nil) -> nil
   rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
   if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
   if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
   minsort(z0) -> mins(z0, nil, nil)
   mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
   if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
   if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

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

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

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


The TRS R consists of the following rules:

   EQ(0', 0') -> c
   EQ(0', s(z0)) -> c1
   EQ(s(z0), 0') -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LE(0', z0) -> c4
   LE(s(z0), 0') -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   APP(nil, z0) -> c7
   APP(add(z0, z1), z2) -> c8(APP(z1, z2))
   MIN(add(z0, nil)) -> c9
   MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
   IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
   IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
   HEAD(add(z0, z1)) -> c13
   TAIL(add(z0, z1)) -> c14
   TAIL(nil) -> c15
   NULL(nil) -> c16
   NULL(add(z0, z1)) -> c17
   RM(z0, nil) -> c18
   RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
   IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
   IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
   MINSORT(z0) -> c22(MINS(z0, nil, nil))
   MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
   IF(true, z0, z1, z2) -> c24
   IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
   IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
   IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
   IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
   IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
   IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
   IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))

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

   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   app(nil, z0) -> z0
   app(add(z0, z1), z2) -> add(z0, app(z1, z2))
   min(add(z0, nil)) -> z0
   min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
   if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
   if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
   head(add(z0, z1)) -> z0
   tail(add(z0, z1)) -> z1
   tail(nil) -> nil
   null(nil) -> true
   null(add(z0, z1)) -> false
   rm(z0, nil) -> nil
   rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
   if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
   if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
   minsort(z0) -> mins(z0, nil, nil)
   mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
   if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
   if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

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

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

(8)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add

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

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

They will be analysed ascendingly in the following order:
EQ < RM
EQ < MINS
LE < MIN
APP < MINS
le < MIN
MIN < MINS
le < min
eq < RM
RM < MINS
eq < MINS
eq < rm
eq < mins
min < MINS
app < MINS
rm < MINS
min < mins
app < mins
rm < mins

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

(10)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
EQ, LE, APP, MIN, le, RM, eq, MINS, min, app, rm, mins

They will be analysed ascendingly in the following order:
EQ < RM
EQ < MINS
LE < MIN
APP < MINS
le < MIN
MIN < MINS
le < min
eq < RM
RM < MINS
eq < MINS
eq < rm
eq < mins
min < MINS
app < MINS
rm < MINS
min < mins
app < mins
rm < mins

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

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

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

Induction Step:
EQ(gen_0':s19_32(+(n24_32, 1)), gen_0':s19_32(+(n24_32, 1))) ->_R^Omega(1)
c3(EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32))) ->_IH
c3(gen_c:c1:c2:c318_32(c25_32))

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

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
EQ, LE, APP, MIN, le, RM, eq, MINS, min, app, rm, mins

They will be analysed ascendingly in the following order:
EQ < RM
EQ < MINS
LE < MIN
APP < MINS
le < MIN
MIN < MINS
le < min
eq < RM
RM < MINS
eq < MINS
eq < rm
eq < mins
min < MINS
app < MINS
rm < MINS
min < mins
app < mins
rm < mins

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Lemmas:
EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32)) -> gen_c:c1:c2:c318_32(n24_32), rt in Omega(1 + n24_32)


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
LE, APP, MIN, le, RM, eq, MINS, min, app, rm, mins

They will be analysed ascendingly in the following order:
LE < MIN
APP < MINS
le < MIN
MIN < MINS
le < min
eq < RM
RM < MINS
eq < MINS
eq < rm
eq < mins
min < MINS
app < MINS
rm < MINS
min < mins
app < mins
rm < mins

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

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

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

Induction Step:
LE(gen_0':s19_32(+(n1191_32, 1)), gen_0':s19_32(+(n1191_32, 1))) ->_R^Omega(1)
c6(LE(gen_0':s19_32(n1191_32), gen_0':s19_32(n1191_32))) ->_IH
c6(gen_c4:c5:c620_32(c1192_32))

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

(18)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Lemmas:
EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32)) -> gen_c:c1:c2:c318_32(n24_32), rt in Omega(1 + n24_32)
LE(gen_0':s19_32(n1191_32), gen_0':s19_32(n1191_32)) -> gen_c4:c5:c620_32(n1191_32), rt in Omega(1 + n1191_32)


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
APP, MIN, le, RM, eq, MINS, min, app, rm, mins

They will be analysed ascendingly in the following order:
APP < MINS
le < MIN
MIN < MINS
le < min
eq < RM
RM < MINS
eq < MINS
eq < rm
eq < mins
min < MINS
app < MINS
rm < MINS
min < mins
app < mins
rm < mins

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APP(gen_nil:add22_32(n2132_32), gen_nil:add22_32(b)) -> gen_c7:c821_32(n2132_32), rt in Omega(1 + n2132_32)

Induction Base:
APP(gen_nil:add22_32(0), gen_nil:add22_32(b)) ->_R^Omega(1)
c7

Induction Step:
APP(gen_nil:add22_32(+(n2132_32, 1)), gen_nil:add22_32(b)) ->_R^Omega(1)
c8(APP(gen_nil:add22_32(n2132_32), gen_nil:add22_32(b))) ->_IH
c8(gen_c7:c821_32(c2133_32))

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

(20)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Lemmas:
EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32)) -> gen_c:c1:c2:c318_32(n24_32), rt in Omega(1 + n24_32)
LE(gen_0':s19_32(n1191_32), gen_0':s19_32(n1191_32)) -> gen_c4:c5:c620_32(n1191_32), rt in Omega(1 + n1191_32)
APP(gen_nil:add22_32(n2132_32), gen_nil:add22_32(b)) -> gen_c7:c821_32(n2132_32), rt in Omega(1 + n2132_32)


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
le, MIN, RM, eq, MINS, min, app, rm, mins

They will be analysed ascendingly in the following order:
le < MIN
MIN < MINS
le < min
eq < RM
RM < MINS
eq < MINS
eq < rm
eq < mins
min < MINS
app < MINS
rm < MINS
min < mins
app < mins
rm < mins

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_0':s19_32(n3395_32), gen_0':s19_32(n3395_32)) -> true, rt in Omega(0)

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

Induction Step:
le(gen_0':s19_32(+(n3395_32, 1)), gen_0':s19_32(+(n3395_32, 1))) ->_R^Omega(0)
le(gen_0':s19_32(n3395_32), gen_0':s19_32(n3395_32)) ->_IH
true

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

(22)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Lemmas:
EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32)) -> gen_c:c1:c2:c318_32(n24_32), rt in Omega(1 + n24_32)
LE(gen_0':s19_32(n1191_32), gen_0':s19_32(n1191_32)) -> gen_c4:c5:c620_32(n1191_32), rt in Omega(1 + n1191_32)
APP(gen_nil:add22_32(n2132_32), gen_nil:add22_32(b)) -> gen_c7:c821_32(n2132_32), rt in Omega(1 + n2132_32)
le(gen_0':s19_32(n3395_32), gen_0':s19_32(n3395_32)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
MIN, RM, eq, MINS, min, app, rm, mins

They will be analysed ascendingly in the following order:
MIN < MINS
eq < RM
RM < MINS
eq < MINS
eq < rm
eq < mins
min < MINS
app < MINS
rm < MINS
min < mins
app < mins
rm < mins

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MIN(gen_nil:add22_32(+(1, n4006_32))) -> *23_32, rt in Omega(n4006_32)

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

Induction Step:
MIN(gen_nil:add22_32(+(1, +(n4006_32, 1)))) ->_R^Omega(1)
c10(IF_MIN(le(0', 0'), add(0', add(0', gen_nil:add22_32(n4006_32)))), LE(0', 0')) ->_L^Omega(0)
c10(IF_MIN(true, add(0', add(0', gen_nil:add22_32(n4006_32)))), LE(0', 0')) ->_R^Omega(1)
c10(c11(MIN(add(0', gen_nil:add22_32(n4006_32)))), LE(0', 0')) ->_IH
c10(c11(*23_32), LE(0', 0')) ->_L^Omega(1)
c10(c11(*23_32), gen_c4:c5:c620_32(0))

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

(24)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Lemmas:
EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32)) -> gen_c:c1:c2:c318_32(n24_32), rt in Omega(1 + n24_32)
LE(gen_0':s19_32(n1191_32), gen_0':s19_32(n1191_32)) -> gen_c4:c5:c620_32(n1191_32), rt in Omega(1 + n1191_32)
APP(gen_nil:add22_32(n2132_32), gen_nil:add22_32(b)) -> gen_c7:c821_32(n2132_32), rt in Omega(1 + n2132_32)
le(gen_0':s19_32(n3395_32), gen_0':s19_32(n3395_32)) -> true, rt in Omega(0)
MIN(gen_nil:add22_32(+(1, n4006_32))) -> *23_32, rt in Omega(n4006_32)


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
eq, RM, MINS, min, app, rm, mins

They will be analysed ascendingly in the following order:
eq < RM
RM < MINS
eq < MINS
eq < rm
eq < mins
min < MINS
app < MINS
rm < MINS
min < mins
app < mins
rm < mins

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

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

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

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

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

(26)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Lemmas:
EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32)) -> gen_c:c1:c2:c318_32(n24_32), rt in Omega(1 + n24_32)
LE(gen_0':s19_32(n1191_32), gen_0':s19_32(n1191_32)) -> gen_c4:c5:c620_32(n1191_32), rt in Omega(1 + n1191_32)
APP(gen_nil:add22_32(n2132_32), gen_nil:add22_32(b)) -> gen_c7:c821_32(n2132_32), rt in Omega(1 + n2132_32)
le(gen_0':s19_32(n3395_32), gen_0':s19_32(n3395_32)) -> true, rt in Omega(0)
MIN(gen_nil:add22_32(+(1, n4006_32))) -> *23_32, rt in Omega(n4006_32)
eq(gen_0':s19_32(n9287_32), gen_0':s19_32(n9287_32)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
RM, MINS, min, app, rm, mins

They will be analysed ascendingly in the following order:
RM < MINS
min < MINS
app < MINS
rm < MINS
min < mins
app < mins
rm < mins

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
RM(gen_0':s19_32(0), gen_nil:add22_32(n10182_32)) -> *23_32, rt in Omega(n10182_32)

Induction Base:
RM(gen_0':s19_32(0), gen_nil:add22_32(0))

Induction Step:
RM(gen_0':s19_32(0), gen_nil:add22_32(+(n10182_32, 1))) ->_R^Omega(1)
c19(IF_RM(eq(gen_0':s19_32(0), 0'), gen_0':s19_32(0), add(0', gen_nil:add22_32(n10182_32))), EQ(gen_0':s19_32(0), 0')) ->_L^Omega(0)
c19(IF_RM(true, gen_0':s19_32(0), add(0', gen_nil:add22_32(n10182_32))), EQ(gen_0':s19_32(0), 0')) ->_R^Omega(1)
c19(c20(RM(gen_0':s19_32(0), gen_nil:add22_32(n10182_32))), EQ(gen_0':s19_32(0), 0')) ->_IH
c19(c20(*23_32), EQ(gen_0':s19_32(0), 0')) ->_L^Omega(1)
c19(c20(*23_32), gen_c:c1:c2:c318_32(0))

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

(28)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Lemmas:
EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32)) -> gen_c:c1:c2:c318_32(n24_32), rt in Omega(1 + n24_32)
LE(gen_0':s19_32(n1191_32), gen_0':s19_32(n1191_32)) -> gen_c4:c5:c620_32(n1191_32), rt in Omega(1 + n1191_32)
APP(gen_nil:add22_32(n2132_32), gen_nil:add22_32(b)) -> gen_c7:c821_32(n2132_32), rt in Omega(1 + n2132_32)
le(gen_0':s19_32(n3395_32), gen_0':s19_32(n3395_32)) -> true, rt in Omega(0)
MIN(gen_nil:add22_32(+(1, n4006_32))) -> *23_32, rt in Omega(n4006_32)
eq(gen_0':s19_32(n9287_32), gen_0':s19_32(n9287_32)) -> true, rt in Omega(0)
RM(gen_0':s19_32(0), gen_nil:add22_32(n10182_32)) -> *23_32, rt in Omega(n10182_32)


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
min, MINS, app, rm, mins

They will be analysed ascendingly in the following order:
min < MINS
app < MINS
rm < MINS
min < mins
app < mins
rm < mins

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
min(gen_nil:add22_32(+(1, n18906_32))) -> gen_0':s19_32(0), rt in Omega(0)

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

Induction Step:
min(gen_nil:add22_32(+(1, +(n18906_32, 1)))) ->_R^Omega(0)
if_min(le(0', 0'), add(0', add(0', gen_nil:add22_32(n18906_32)))) ->_L^Omega(0)
if_min(true, add(0', add(0', gen_nil:add22_32(n18906_32)))) ->_R^Omega(0)
min(add(0', gen_nil:add22_32(n18906_32))) ->_IH
gen_0':s19_32(0)

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

(30)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Lemmas:
EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32)) -> gen_c:c1:c2:c318_32(n24_32), rt in Omega(1 + n24_32)
LE(gen_0':s19_32(n1191_32), gen_0':s19_32(n1191_32)) -> gen_c4:c5:c620_32(n1191_32), rt in Omega(1 + n1191_32)
APP(gen_nil:add22_32(n2132_32), gen_nil:add22_32(b)) -> gen_c7:c821_32(n2132_32), rt in Omega(1 + n2132_32)
le(gen_0':s19_32(n3395_32), gen_0':s19_32(n3395_32)) -> true, rt in Omega(0)
MIN(gen_nil:add22_32(+(1, n4006_32))) -> *23_32, rt in Omega(n4006_32)
eq(gen_0':s19_32(n9287_32), gen_0':s19_32(n9287_32)) -> true, rt in Omega(0)
RM(gen_0':s19_32(0), gen_nil:add22_32(n10182_32)) -> *23_32, rt in Omega(n10182_32)
min(gen_nil:add22_32(+(1, n18906_32))) -> gen_0':s19_32(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
app, MINS, rm, mins

They will be analysed ascendingly in the following order:
app < MINS
rm < MINS
app < mins
rm < mins

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
app(gen_nil:add22_32(n20050_32), gen_nil:add22_32(b)) -> gen_nil:add22_32(+(n20050_32, b)), rt in Omega(0)

Induction Base:
app(gen_nil:add22_32(0), gen_nil:add22_32(b)) ->_R^Omega(0)
gen_nil:add22_32(b)

Induction Step:
app(gen_nil:add22_32(+(n20050_32, 1)), gen_nil:add22_32(b)) ->_R^Omega(0)
add(0', app(gen_nil:add22_32(n20050_32), gen_nil:add22_32(b))) ->_IH
add(0', gen_nil:add22_32(+(b, c20051_32)))

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

(32)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Lemmas:
EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32)) -> gen_c:c1:c2:c318_32(n24_32), rt in Omega(1 + n24_32)
LE(gen_0':s19_32(n1191_32), gen_0':s19_32(n1191_32)) -> gen_c4:c5:c620_32(n1191_32), rt in Omega(1 + n1191_32)
APP(gen_nil:add22_32(n2132_32), gen_nil:add22_32(b)) -> gen_c7:c821_32(n2132_32), rt in Omega(1 + n2132_32)
le(gen_0':s19_32(n3395_32), gen_0':s19_32(n3395_32)) -> true, rt in Omega(0)
MIN(gen_nil:add22_32(+(1, n4006_32))) -> *23_32, rt in Omega(n4006_32)
eq(gen_0':s19_32(n9287_32), gen_0':s19_32(n9287_32)) -> true, rt in Omega(0)
RM(gen_0':s19_32(0), gen_nil:add22_32(n10182_32)) -> *23_32, rt in Omega(n10182_32)
min(gen_nil:add22_32(+(1, n18906_32))) -> gen_0':s19_32(0), rt in Omega(0)
app(gen_nil:add22_32(n20050_32), gen_nil:add22_32(b)) -> gen_nil:add22_32(+(n20050_32, b)), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
rm, MINS, mins

They will be analysed ascendingly in the following order:
rm < MINS
rm < mins

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
rm(gen_0':s19_32(0), gen_nil:add22_32(n22821_32)) -> gen_nil:add22_32(0), rt in Omega(0)

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

Induction Step:
rm(gen_0':s19_32(0), gen_nil:add22_32(+(n22821_32, 1))) ->_R^Omega(0)
if_rm(eq(gen_0':s19_32(0), 0'), gen_0':s19_32(0), add(0', gen_nil:add22_32(n22821_32))) ->_L^Omega(0)
if_rm(true, gen_0':s19_32(0), add(0', gen_nil:add22_32(n22821_32))) ->_R^Omega(0)
rm(gen_0':s19_32(0), gen_nil:add22_32(n22821_32)) ->_IH
gen_nil:add22_32(0)

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

(34)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
MIN(add(z0, nil)) -> c9
MIN(add(z0, add(z1, z2))) -> c10(IF_MIN(le(z0, z1), add(z0, add(z1, z2))), LE(z0, z1))
IF_MIN(true, add(z0, add(z1, z2))) -> c11(MIN(add(z0, z2)))
IF_MIN(false, add(z0, add(z1, z2))) -> c12(MIN(add(z1, z2)))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
TAIL(nil) -> c15
NULL(nil) -> c16
NULL(add(z0, z1)) -> c17
RM(z0, nil) -> c18
RM(z0, add(z1, z2)) -> c19(IF_RM(eq(z0, z1), z0, add(z1, z2)), EQ(z0, z1))
IF_RM(true, z0, add(z1, z2)) -> c20(RM(z0, z2))
IF_RM(false, z0, add(z1, z2)) -> c21(RM(z0, z2))
MINSORT(z0) -> c22(MINS(z0, nil, nil))
MINS(z0, z1, z2) -> c23(IF(null(z0), z0, z1, z2), NULL(z0))
IF(true, z0, z1, z2) -> c24
IF(false, z0, z1, z2) -> c25(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), HEAD(z0))
IF(false, z0, z1, z2) -> c26(IF2(eq(head(z0), min(z0)), z0, z1, z2), EQ(head(z0), min(z0)), MIN(z0))
IF2(true, z0, z1, z2) -> c27(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), HEAD(z0))
IF2(true, z0, z1, z2) -> c28(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(rm(head(z0), tail(z0)), z1), RM(head(z0), tail(z0)), TAIL(z0))
IF2(true, z0, z1, z2) -> c29(MINS(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil))), APP(z2, add(head(z0), nil)), HEAD(z0))
IF2(false, z0, z1, z2) -> c30(MINS(tail(z0), add(head(z0), z1), z2), TAIL(z0))
IF2(false, z0, z1, z2) -> c31(MINS(tail(z0), add(head(z0), z1), z2), HEAD(z0))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
min(add(z0, nil)) -> z0
min(add(z0, add(z1, z2))) -> if_min(le(z0, z1), add(z0, add(z1, z2)))
if_min(true, add(z0, add(z1, z2))) -> min(add(z0, z2))
if_min(false, add(z0, add(z1, z2))) -> min(add(z1, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
tail(nil) -> nil
null(nil) -> true
null(add(z0, z1)) -> false
rm(z0, nil) -> nil
rm(z0, add(z1, z2)) -> if_rm(eq(z0, z1), z0, add(z1, z2))
if_rm(true, z0, add(z1, z2)) -> rm(z0, z2)
if_rm(false, z0, add(z1, z2)) -> add(z1, rm(z0, z2))
minsort(z0) -> mins(z0, nil, nil)
mins(z0, z1, z2) -> if(null(z0), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> if2(eq(head(z0), min(z0)), z0, z1, z2)
if2(true, z0, z1, z2) -> mins(app(rm(head(z0), tail(z0)), z1), nil, app(z2, add(head(z0), nil)))
if2(false, z0, z1, z2) -> mins(tail(z0), add(head(z0), z1), z2)

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
MIN :: nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_MIN :: true:false -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14:c15
c14 :: c14:c15
c15 :: c14:c15
NULL :: nil:add -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
RM :: 0':s -> nil:add -> c18:c19
c18 :: c18:c19
c19 :: c20:c21 -> c:c1:c2:c3 -> c18:c19
IF_RM :: true:false -> 0':s -> nil:add -> c20:c21
eq :: 0':s -> 0':s -> true:false
c20 :: c18:c19 -> c20:c21
c21 :: c18:c19 -> c20:c21
MINSORT :: nil:add -> c22
c22 :: c23 -> c22
MINS :: nil:add -> nil:add -> nil:add -> c23
c23 :: c24:c25:c26 -> c16:c17 -> c23
IF :: true:false -> nil:add -> nil:add -> nil:add -> c24:c25:c26
null :: nil:add -> true:false
c24 :: c24:c25:c26
c25 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c13 -> c24:c25:c26
IF2 :: true:false -> nil:add -> nil:add -> nil:add -> c27:c28:c29:c30:c31
head :: nil:add -> 0':s
min :: nil:add -> 0':s
c26 :: c27:c28:c29:c30:c31 -> c:c1:c2:c3 -> c9:c10 -> c24:c25:c26
c27 :: c23 -> c7:c8 -> c18:c19 -> c13 -> c27:c28:c29:c30:c31
app :: nil:add -> nil:add -> nil:add
rm :: 0':s -> nil:add -> nil:add
tail :: nil:add -> nil:add
c28 :: c23 -> c7:c8 -> c18:c19 -> c14:c15 -> c27:c28:c29:c30:c31
c29 :: c23 -> c7:c8 -> c13 -> c27:c28:c29:c30:c31
c30 :: c23 -> c14:c15 -> c27:c28:c29:c30:c31
c31 :: c23 -> c13 -> c27:c28:c29:c30:c31
if_min :: true:false -> nil:add -> 0':s
if_rm :: true:false -> 0':s -> nil:add -> nil:add
minsort :: nil:add -> nil:add
mins :: nil:add -> nil:add -> nil:add -> nil:add
if :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
if2 :: true:false -> nil:add -> nil:add -> nil:add -> nil:add
hole_c:c1:c2:c31_32 :: c:c1:c2:c3
hole_0':s2_32 :: 0':s
hole_c4:c5:c63_32 :: c4:c5:c6
hole_c7:c84_32 :: c7:c8
hole_nil:add5_32 :: nil:add
hole_c9:c106_32 :: c9:c10
hole_c11:c127_32 :: c11:c12
hole_true:false8_32 :: true:false
hole_c139_32 :: c13
hole_c14:c1510_32 :: c14:c15
hole_c16:c1711_32 :: c16:c17
hole_c18:c1912_32 :: c18:c19
hole_c20:c2113_32 :: c20:c21
hole_c2214_32 :: c22
hole_c2315_32 :: c23
hole_c24:c25:c2616_32 :: c24:c25:c26
hole_c27:c28:c29:c30:c3117_32 :: c27:c28:c29:c30:c31
gen_c:c1:c2:c318_32 :: Nat -> c:c1:c2:c3
gen_0':s19_32 :: Nat -> 0':s
gen_c4:c5:c620_32 :: Nat -> c4:c5:c6
gen_c7:c821_32 :: Nat -> c7:c8
gen_nil:add22_32 :: Nat -> nil:add


Lemmas:
EQ(gen_0':s19_32(n24_32), gen_0':s19_32(n24_32)) -> gen_c:c1:c2:c318_32(n24_32), rt in Omega(1 + n24_32)
LE(gen_0':s19_32(n1191_32), gen_0':s19_32(n1191_32)) -> gen_c4:c5:c620_32(n1191_32), rt in Omega(1 + n1191_32)
APP(gen_nil:add22_32(n2132_32), gen_nil:add22_32(b)) -> gen_c7:c821_32(n2132_32), rt in Omega(1 + n2132_32)
le(gen_0':s19_32(n3395_32), gen_0':s19_32(n3395_32)) -> true, rt in Omega(0)
MIN(gen_nil:add22_32(+(1, n4006_32))) -> *23_32, rt in Omega(n4006_32)
eq(gen_0':s19_32(n9287_32), gen_0':s19_32(n9287_32)) -> true, rt in Omega(0)
RM(gen_0':s19_32(0), gen_nil:add22_32(n10182_32)) -> *23_32, rt in Omega(n10182_32)
min(gen_nil:add22_32(+(1, n18906_32))) -> gen_0':s19_32(0), rt in Omega(0)
app(gen_nil:add22_32(n20050_32), gen_nil:add22_32(b)) -> gen_nil:add22_32(+(n20050_32, b)), rt in Omega(0)
rm(gen_0':s19_32(0), gen_nil:add22_32(n22821_32)) -> gen_nil:add22_32(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c318_32(0) <=> c
gen_c:c1:c2:c318_32(+(x, 1)) <=> c3(gen_c:c1:c2:c318_32(x))
gen_0':s19_32(0) <=> 0'
gen_0':s19_32(+(x, 1)) <=> s(gen_0':s19_32(x))
gen_c4:c5:c620_32(0) <=> c4
gen_c4:c5:c620_32(+(x, 1)) <=> c6(gen_c4:c5:c620_32(x))
gen_c7:c821_32(0) <=> c7
gen_c7:c821_32(+(x, 1)) <=> c8(gen_c7:c821_32(x))
gen_nil:add22_32(0) <=> nil
gen_nil:add22_32(+(x, 1)) <=> add(0', gen_nil:add22_32(x))


The following defined symbols remain to be analysed:
MINS, mins