WORST_CASE(NON_POLY,?)
proof of input_eA1waILs0b.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 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), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 293 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [FINISHED, 764 ms]
(14) BOUNDS(EXP, INF)


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

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


The TRS R consists of the following rules:

   sort(l) -> st(0, l)
   st(n, l) -> cond1(member(n, l), n, l)
   cond1(true, n, l) -> cons(n, st(s(n), l))
   cond1(false, n, l) -> cond2(gt(n, max(l)), n, l)
   cond2(true, n, l) -> nil
   cond2(false, n, l) -> st(s(n), l)
   member(n, nil) -> false
   member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
   or(x, true) -> true
   or(x, false) -> x
   equal(0, 0) -> true
   equal(s(x), 0) -> false
   equal(0, s(y)) -> false
   equal(s(x), s(y)) -> equal(x, y)
   gt(0, v) -> false
   gt(s(u), 0) -> true
   gt(s(u), s(v)) -> gt(u, v)
   max(nil) -> 0
   max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
   if(true, u, v) -> u
   if(false, u, v) -> v

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:
   sort(z0) -> st(0, z0)
   st(z0, z1) -> cond1(member(z0, z1), z0, z1)
   cond1(true, z0, z1) -> cons(z0, st(s(z0), z1))
   cond1(false, z0, z1) -> cond2(gt(z0, max(z1)), z0, z1)
   cond2(true, z0, z1) -> nil
   cond2(false, z0, z1) -> st(s(z0), z1)
   member(z0, nil) -> false
   member(z0, cons(z1, z2)) -> or(equal(z0, z1), member(z0, z2))
   or(z0, true) -> true
   or(z0, false) -> z0
   equal(0, 0) -> true
   equal(s(z0), 0) -> false
   equal(0, s(z0)) -> false
   equal(s(z0), s(z1)) -> equal(z0, z1)
   gt(0, z0) -> false
   gt(s(z0), 0) -> true
   gt(s(z0), s(z1)) -> gt(z0, z1)
   max(nil) -> 0
   max(cons(z0, z1)) -> if(gt(z0, max(z1)), z0, max(z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
Tuples:
   SORT(z0) -> c(ST(0, z0))
   ST(z0, z1) -> c1(COND1(member(z0, z1), z0, z1), MEMBER(z0, z1))
   COND1(true, z0, z1) -> c2(ST(s(z0), z1))
   COND1(false, z0, z1) -> c3(COND2(gt(z0, max(z1)), z0, z1), GT(z0, max(z1)), MAX(z1))
   COND2(true, z0, z1) -> c4
   COND2(false, z0, z1) -> c5(ST(s(z0), z1))
   MEMBER(z0, nil) -> c6
   MEMBER(z0, cons(z1, z2)) -> c7(OR(equal(z0, z1), member(z0, z2)), EQUAL(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c8(OR(equal(z0, z1), member(z0, z2)), MEMBER(z0, z2))
   OR(z0, true) -> c9
   OR(z0, false) -> c10
   EQUAL(0, 0) -> c11
   EQUAL(s(z0), 0) -> c12
   EQUAL(0, s(z0)) -> c13
   EQUAL(s(z0), s(z1)) -> c14(EQUAL(z0, z1))
   GT(0, z0) -> c15
   GT(s(z0), 0) -> c16
   GT(s(z0), s(z1)) -> c17(GT(z0, z1))
   MAX(nil) -> c18
   MAX(cons(z0, z1)) -> c19(IF(gt(z0, max(z1)), z0, max(z1)), GT(z0, max(z1)), MAX(z1))
   MAX(cons(z0, z1)) -> c20(IF(gt(z0, max(z1)), z0, max(z1)), MAX(z1))
   IF(true, z0, z1) -> c21
   IF(false, z0, z1) -> c22
S tuples:
   SORT(z0) -> c(ST(0, z0))
   ST(z0, z1) -> c1(COND1(member(z0, z1), z0, z1), MEMBER(z0, z1))
   COND1(true, z0, z1) -> c2(ST(s(z0), z1))
   COND1(false, z0, z1) -> c3(COND2(gt(z0, max(z1)), z0, z1), GT(z0, max(z1)), MAX(z1))
   COND2(true, z0, z1) -> c4
   COND2(false, z0, z1) -> c5(ST(s(z0), z1))
   MEMBER(z0, nil) -> c6
   MEMBER(z0, cons(z1, z2)) -> c7(OR(equal(z0, z1), member(z0, z2)), EQUAL(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c8(OR(equal(z0, z1), member(z0, z2)), MEMBER(z0, z2))
   OR(z0, true) -> c9
   OR(z0, false) -> c10
   EQUAL(0, 0) -> c11
   EQUAL(s(z0), 0) -> c12
   EQUAL(0, s(z0)) -> c13
   EQUAL(s(z0), s(z1)) -> c14(EQUAL(z0, z1))
   GT(0, z0) -> c15
   GT(s(z0), 0) -> c16
   GT(s(z0), s(z1)) -> c17(GT(z0, z1))
   MAX(nil) -> c18
   MAX(cons(z0, z1)) -> c19(IF(gt(z0, max(z1)), z0, max(z1)), GT(z0, max(z1)), MAX(z1))
   MAX(cons(z0, z1)) -> c20(IF(gt(z0, max(z1)), z0, max(z1)), MAX(z1))
   IF(true, z0, z1) -> c21
   IF(false, z0, z1) -> c22
K tuples:none
Defined Rule Symbols:   sort_1, st_2, cond1_3, cond2_3, member_2, or_2, equal_2, gt_2, max_1, if_3

Defined Pair Symbols:   SORT_1, ST_2, COND1_3, COND2_3, MEMBER_2, OR_2, EQUAL_2, GT_2, MAX_1, IF_3

Compound Symbols:   c_1, c1_2, c2_1, c3_3, c4, c5_1, c6, c7_2, c8_2, c9, c10, c11, c12, c13, c14_1, c15, c16, c17_1, c18, c19_3, c20_2, c21, c22


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

(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(EXP, INF).


The TRS R consists of the following rules:

   SORT(z0) -> c(ST(0, z0))
   ST(z0, z1) -> c1(COND1(member(z0, z1), z0, z1), MEMBER(z0, z1))
   COND1(true, z0, z1) -> c2(ST(s(z0), z1))
   COND1(false, z0, z1) -> c3(COND2(gt(z0, max(z1)), z0, z1), GT(z0, max(z1)), MAX(z1))
   COND2(true, z0, z1) -> c4
   COND2(false, z0, z1) -> c5(ST(s(z0), z1))
   MEMBER(z0, nil) -> c6
   MEMBER(z0, cons(z1, z2)) -> c7(OR(equal(z0, z1), member(z0, z2)), EQUAL(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c8(OR(equal(z0, z1), member(z0, z2)), MEMBER(z0, z2))
   OR(z0, true) -> c9
   OR(z0, false) -> c10
   EQUAL(0, 0) -> c11
   EQUAL(s(z0), 0) -> c12
   EQUAL(0, s(z0)) -> c13
   EQUAL(s(z0), s(z1)) -> c14(EQUAL(z0, z1))
   GT(0, z0) -> c15
   GT(s(z0), 0) -> c16
   GT(s(z0), s(z1)) -> c17(GT(z0, z1))
   MAX(nil) -> c18
   MAX(cons(z0, z1)) -> c19(IF(gt(z0, max(z1)), z0, max(z1)), GT(z0, max(z1)), MAX(z1))
   MAX(cons(z0, z1)) -> c20(IF(gt(z0, max(z1)), z0, max(z1)), MAX(z1))
   IF(true, z0, z1) -> c21
   IF(false, z0, z1) -> c22

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

   sort(z0) -> st(0, z0)
   st(z0, z1) -> cond1(member(z0, z1), z0, z1)
   cond1(true, z0, z1) -> cons(z0, st(s(z0), z1))
   cond1(false, z0, z1) -> cond2(gt(z0, max(z1)), z0, z1)
   cond2(true, z0, z1) -> nil
   cond2(false, z0, z1) -> st(s(z0), z1)
   member(z0, nil) -> false
   member(z0, cons(z1, z2)) -> or(equal(z0, z1), member(z0, z2))
   or(z0, true) -> true
   or(z0, false) -> z0
   equal(0, 0) -> true
   equal(s(z0), 0) -> false
   equal(0, s(z0)) -> false
   equal(s(z0), s(z1)) -> equal(z0, z1)
   gt(0, z0) -> false
   gt(s(z0), 0) -> true
   gt(s(z0), s(z1)) -> gt(z0, z1)
   max(nil) -> 0
   max(cons(z0, z1)) -> if(gt(z0, max(z1)), z0, max(z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1

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(EXP, INF).


The TRS R consists of the following rules:

   SORT(z0) -> c(ST(0', z0))
   ST(z0, z1) -> c1(COND1(member(z0, z1), z0, z1), MEMBER(z0, z1))
   COND1(true, z0, z1) -> c2(ST(s(z0), z1))
   COND1(false, z0, z1) -> c3(COND2(gt(z0, max(z1)), z0, z1), GT(z0, max(z1)), MAX(z1))
   COND2(true, z0, z1) -> c4
   COND2(false, z0, z1) -> c5(ST(s(z0), z1))
   MEMBER(z0, nil) -> c6
   MEMBER(z0, cons(z1, z2)) -> c7(OR(equal(z0, z1), member(z0, z2)), EQUAL(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c8(OR(equal(z0, z1), member(z0, z2)), MEMBER(z0, z2))
   OR(z0, true) -> c9
   OR(z0, false) -> c10
   EQUAL(0', 0') -> c11
   EQUAL(s(z0), 0') -> c12
   EQUAL(0', s(z0)) -> c13
   EQUAL(s(z0), s(z1)) -> c14(EQUAL(z0, z1))
   GT(0', z0) -> c15
   GT(s(z0), 0') -> c16
   GT(s(z0), s(z1)) -> c17(GT(z0, z1))
   MAX(nil) -> c18
   MAX(cons(z0, z1)) -> c19(IF(gt(z0, max(z1)), z0, max(z1)), GT(z0, max(z1)), MAX(z1))
   MAX(cons(z0, z1)) -> c20(IF(gt(z0, max(z1)), z0, max(z1)), MAX(z1))
   IF(true, z0, z1) -> c21
   IF(false, z0, z1) -> c22

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

   sort(z0) -> st(0', z0)
   st(z0, z1) -> cond1(member(z0, z1), z0, z1)
   cond1(true, z0, z1) -> cons(z0, st(s(z0), z1))
   cond1(false, z0, z1) -> cond2(gt(z0, max(z1)), z0, z1)
   cond2(true, z0, z1) -> nil
   cond2(false, z0, z1) -> st(s(z0), z1)
   member(z0, nil) -> false
   member(z0, cons(z1, z2)) -> or(equal(z0, z1), member(z0, z2))
   or(z0, true) -> true
   or(z0, false) -> z0
   equal(0', 0') -> true
   equal(s(z0), 0') -> false
   equal(0', s(z0)) -> false
   equal(s(z0), s(z1)) -> equal(z0, z1)
   gt(0', z0) -> false
   gt(s(z0), 0') -> true
   gt(s(z0), s(z1)) -> gt(z0, z1)
   max(nil) -> 0'
   max(cons(z0, z1)) -> if(gt(z0, max(z1)), z0, max(z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1

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

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

(8)
Obligation:
Innermost TRS:
Rules:
SORT(z0) -> c(ST(0', z0))
ST(z0, z1) -> c1(COND1(member(z0, z1), z0, z1), MEMBER(z0, z1))
COND1(true, z0, z1) -> c2(ST(s(z0), z1))
COND1(false, z0, z1) -> c3(COND2(gt(z0, max(z1)), z0, z1), GT(z0, max(z1)), MAX(z1))
COND2(true, z0, z1) -> c4
COND2(false, z0, z1) -> c5(ST(s(z0), z1))
MEMBER(z0, nil) -> c6
MEMBER(z0, cons(z1, z2)) -> c7(OR(equal(z0, z1), member(z0, z2)), EQUAL(z0, z1))
MEMBER(z0, cons(z1, z2)) -> c8(OR(equal(z0, z1), member(z0, z2)), MEMBER(z0, z2))
OR(z0, true) -> c9
OR(z0, false) -> c10
EQUAL(0', 0') -> c11
EQUAL(s(z0), 0') -> c12
EQUAL(0', s(z0)) -> c13
EQUAL(s(z0), s(z1)) -> c14(EQUAL(z0, z1))
GT(0', z0) -> c15
GT(s(z0), 0') -> c16
GT(s(z0), s(z1)) -> c17(GT(z0, z1))
MAX(nil) -> c18
MAX(cons(z0, z1)) -> c19(IF(gt(z0, max(z1)), z0, max(z1)), GT(z0, max(z1)), MAX(z1))
MAX(cons(z0, z1)) -> c20(IF(gt(z0, max(z1)), z0, max(z1)), MAX(z1))
IF(true, z0, z1) -> c21
IF(false, z0, z1) -> c22
sort(z0) -> st(0', z0)
st(z0, z1) -> cond1(member(z0, z1), z0, z1)
cond1(true, z0, z1) -> cons(z0, st(s(z0), z1))
cond1(false, z0, z1) -> cond2(gt(z0, max(z1)), z0, z1)
cond2(true, z0, z1) -> nil
cond2(false, z0, z1) -> st(s(z0), z1)
member(z0, nil) -> false
member(z0, cons(z1, z2)) -> or(equal(z0, z1), member(z0, z2))
or(z0, true) -> true
or(z0, false) -> z0
equal(0', 0') -> true
equal(s(z0), 0') -> false
equal(0', s(z0)) -> false
equal(s(z0), s(z1)) -> equal(z0, z1)
gt(0', z0) -> false
gt(s(z0), 0') -> true
gt(s(z0), s(z1)) -> gt(z0, z1)
max(nil) -> 0'
max(cons(z0, z1)) -> if(gt(z0, max(z1)), z0, max(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1

Types:
SORT :: nil:cons -> c
c :: c1 -> c
ST :: 0':s -> nil:cons -> c1
0' :: 0':s
c1 :: c2:c3 -> c6:c7:c8 -> c1
COND1 :: true:false -> 0':s -> nil:cons -> c2:c3
member :: 0':s -> nil:cons -> true:false
MEMBER :: 0':s -> nil:cons -> c6:c7:c8
true :: true:false
c2 :: c1 -> c2:c3
s :: 0':s -> 0':s
false :: true:false
c3 :: c4:c5 -> c15:c16:c17 -> c18:c19:c20 -> c2:c3
COND2 :: true:false -> 0':s -> nil:cons -> c4:c5
gt :: 0':s -> 0':s -> true:false
max :: nil:cons -> 0':s
GT :: 0':s -> 0':s -> c15:c16:c17
MAX :: nil:cons -> c18:c19:c20
c4 :: c4:c5
c5 :: c1 -> c4:c5
nil :: nil:cons
c6 :: c6:c7:c8
cons :: 0':s -> nil:cons -> nil:cons
c7 :: c9:c10 -> c11:c12:c13:c14 -> c6:c7:c8
OR :: true:false -> true:false -> c9:c10
equal :: 0':s -> 0':s -> true:false
EQUAL :: 0':s -> 0':s -> c11:c12:c13:c14
c8 :: c9:c10 -> c6:c7:c8 -> c6:c7:c8
c9 :: c9:c10
c10 :: c9:c10
c11 :: c11:c12:c13:c14
c12 :: c11:c12:c13:c14
c13 :: c11:c12:c13:c14
c14 :: c11:c12:c13:c14 -> c11:c12:c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19:c20
c19 :: c21:c22 -> c15:c16:c17 -> c18:c19:c20 -> c18:c19:c20
IF :: true:false -> 0':s -> 0':s -> c21:c22
c20 :: c21:c22 -> c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22
c22 :: c21:c22
sort :: nil:cons -> nil:cons
st :: 0':s -> nil:cons -> nil:cons
cond1 :: true:false -> 0':s -> nil:cons -> nil:cons
cond2 :: true:false -> 0':s -> nil:cons -> nil:cons
or :: true:false -> true:false -> true:false
if :: true:false -> 0':s -> 0':s -> 0':s
hole_c1_23 :: c
hole_nil:cons2_23 :: nil:cons
hole_c13_23 :: c1
hole_0':s4_23 :: 0':s
hole_c2:c35_23 :: c2:c3
hole_c6:c7:c86_23 :: c6:c7:c8
hole_true:false7_23 :: true:false
hole_c4:c58_23 :: c4:c5
hole_c15:c16:c179_23 :: c15:c16:c17
hole_c18:c19:c2010_23 :: c18:c19:c20
hole_c9:c1011_23 :: c9:c10
hole_c11:c12:c13:c1412_23 :: c11:c12:c13:c14
hole_c21:c2213_23 :: c21:c22
gen_nil:cons14_23 :: Nat -> nil:cons
gen_0':s15_23 :: Nat -> 0':s
gen_c6:c7:c816_23 :: Nat -> c6:c7:c8
gen_c15:c16:c1717_23 :: Nat -> c15:c16:c17
gen_c18:c19:c2018_23 :: Nat -> c18:c19:c20
gen_c11:c12:c13:c1419_23 :: Nat -> c11:c12:c13:c14

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
ST, member, MEMBER, gt, max, GT, MAX, equal, EQUAL, st

They will be analysed ascendingly in the following order:
member < ST
MEMBER < ST
gt < ST
max < ST
GT < ST
MAX < ST
member < MEMBER
equal < member
member < st
equal < MEMBER
EQUAL < MEMBER
gt < max
gt < MAX
gt < st
max < MAX
max < st
GT < MAX

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

(10)
Obligation:
Innermost TRS:
Rules:
SORT(z0) -> c(ST(0', z0))
ST(z0, z1) -> c1(COND1(member(z0, z1), z0, z1), MEMBER(z0, z1))
COND1(true, z0, z1) -> c2(ST(s(z0), z1))
COND1(false, z0, z1) -> c3(COND2(gt(z0, max(z1)), z0, z1), GT(z0, max(z1)), MAX(z1))
COND2(true, z0, z1) -> c4
COND2(false, z0, z1) -> c5(ST(s(z0), z1))
MEMBER(z0, nil) -> c6
MEMBER(z0, cons(z1, z2)) -> c7(OR(equal(z0, z1), member(z0, z2)), EQUAL(z0, z1))
MEMBER(z0, cons(z1, z2)) -> c8(OR(equal(z0, z1), member(z0, z2)), MEMBER(z0, z2))
OR(z0, true) -> c9
OR(z0, false) -> c10
EQUAL(0', 0') -> c11
EQUAL(s(z0), 0') -> c12
EQUAL(0', s(z0)) -> c13
EQUAL(s(z0), s(z1)) -> c14(EQUAL(z0, z1))
GT(0', z0) -> c15
GT(s(z0), 0') -> c16
GT(s(z0), s(z1)) -> c17(GT(z0, z1))
MAX(nil) -> c18
MAX(cons(z0, z1)) -> c19(IF(gt(z0, max(z1)), z0, max(z1)), GT(z0, max(z1)), MAX(z1))
MAX(cons(z0, z1)) -> c20(IF(gt(z0, max(z1)), z0, max(z1)), MAX(z1))
IF(true, z0, z1) -> c21
IF(false, z0, z1) -> c22
sort(z0) -> st(0', z0)
st(z0, z1) -> cond1(member(z0, z1), z0, z1)
cond1(true, z0, z1) -> cons(z0, st(s(z0), z1))
cond1(false, z0, z1) -> cond2(gt(z0, max(z1)), z0, z1)
cond2(true, z0, z1) -> nil
cond2(false, z0, z1) -> st(s(z0), z1)
member(z0, nil) -> false
member(z0, cons(z1, z2)) -> or(equal(z0, z1), member(z0, z2))
or(z0, true) -> true
or(z0, false) -> z0
equal(0', 0') -> true
equal(s(z0), 0') -> false
equal(0', s(z0)) -> false
equal(s(z0), s(z1)) -> equal(z0, z1)
gt(0', z0) -> false
gt(s(z0), 0') -> true
gt(s(z0), s(z1)) -> gt(z0, z1)
max(nil) -> 0'
max(cons(z0, z1)) -> if(gt(z0, max(z1)), z0, max(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1

Types:
SORT :: nil:cons -> c
c :: c1 -> c
ST :: 0':s -> nil:cons -> c1
0' :: 0':s
c1 :: c2:c3 -> c6:c7:c8 -> c1
COND1 :: true:false -> 0':s -> nil:cons -> c2:c3
member :: 0':s -> nil:cons -> true:false
MEMBER :: 0':s -> nil:cons -> c6:c7:c8
true :: true:false
c2 :: c1 -> c2:c3
s :: 0':s -> 0':s
false :: true:false
c3 :: c4:c5 -> c15:c16:c17 -> c18:c19:c20 -> c2:c3
COND2 :: true:false -> 0':s -> nil:cons -> c4:c5
gt :: 0':s -> 0':s -> true:false
max :: nil:cons -> 0':s
GT :: 0':s -> 0':s -> c15:c16:c17
MAX :: nil:cons -> c18:c19:c20
c4 :: c4:c5
c5 :: c1 -> c4:c5
nil :: nil:cons
c6 :: c6:c7:c8
cons :: 0':s -> nil:cons -> nil:cons
c7 :: c9:c10 -> c11:c12:c13:c14 -> c6:c7:c8
OR :: true:false -> true:false -> c9:c10
equal :: 0':s -> 0':s -> true:false
EQUAL :: 0':s -> 0':s -> c11:c12:c13:c14
c8 :: c9:c10 -> c6:c7:c8 -> c6:c7:c8
c9 :: c9:c10
c10 :: c9:c10
c11 :: c11:c12:c13:c14
c12 :: c11:c12:c13:c14
c13 :: c11:c12:c13:c14
c14 :: c11:c12:c13:c14 -> c11:c12:c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19:c20
c19 :: c21:c22 -> c15:c16:c17 -> c18:c19:c20 -> c18:c19:c20
IF :: true:false -> 0':s -> 0':s -> c21:c22
c20 :: c21:c22 -> c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22
c22 :: c21:c22
sort :: nil:cons -> nil:cons
st :: 0':s -> nil:cons -> nil:cons
cond1 :: true:false -> 0':s -> nil:cons -> nil:cons
cond2 :: true:false -> 0':s -> nil:cons -> nil:cons
or :: true:false -> true:false -> true:false
if :: true:false -> 0':s -> 0':s -> 0':s
hole_c1_23 :: c
hole_nil:cons2_23 :: nil:cons
hole_c13_23 :: c1
hole_0':s4_23 :: 0':s
hole_c2:c35_23 :: c2:c3
hole_c6:c7:c86_23 :: c6:c7:c8
hole_true:false7_23 :: true:false
hole_c4:c58_23 :: c4:c5
hole_c15:c16:c179_23 :: c15:c16:c17
hole_c18:c19:c2010_23 :: c18:c19:c20
hole_c9:c1011_23 :: c9:c10
hole_c11:c12:c13:c1412_23 :: c11:c12:c13:c14
hole_c21:c2213_23 :: c21:c22
gen_nil:cons14_23 :: Nat -> nil:cons
gen_0':s15_23 :: Nat -> 0':s
gen_c6:c7:c816_23 :: Nat -> c6:c7:c8
gen_c15:c16:c1717_23 :: Nat -> c15:c16:c17
gen_c18:c19:c2018_23 :: Nat -> c18:c19:c20
gen_c11:c12:c13:c1419_23 :: Nat -> c11:c12:c13:c14


Generator Equations:
gen_nil:cons14_23(0) <=> nil
gen_nil:cons14_23(+(x, 1)) <=> cons(0', gen_nil:cons14_23(x))
gen_0':s15_23(0) <=> 0'
gen_0':s15_23(+(x, 1)) <=> s(gen_0':s15_23(x))
gen_c6:c7:c816_23(0) <=> c6
gen_c6:c7:c816_23(+(x, 1)) <=> c8(c9, gen_c6:c7:c816_23(x))
gen_c15:c16:c1717_23(0) <=> c15
gen_c15:c16:c1717_23(+(x, 1)) <=> c17(gen_c15:c16:c1717_23(x))
gen_c18:c19:c2018_23(0) <=> c18
gen_c18:c19:c2018_23(+(x, 1)) <=> c19(c21, c15, gen_c18:c19:c2018_23(x))
gen_c11:c12:c13:c1419_23(0) <=> c11
gen_c11:c12:c13:c1419_23(+(x, 1)) <=> c14(gen_c11:c12:c13:c1419_23(x))


The following defined symbols remain to be analysed:
gt, ST, member, MEMBER, max, GT, MAX, equal, EQUAL, st

They will be analysed ascendingly in the following order:
member < ST
MEMBER < ST
gt < ST
max < ST
GT < ST
MAX < ST
member < MEMBER
equal < member
member < st
equal < MEMBER
EQUAL < MEMBER
gt < max
gt < MAX
gt < st
max < MAX
max < st
GT < MAX

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
gt(gen_0':s15_23(n21_23), gen_0':s15_23(n21_23)) -> false, rt in Omega(0)

Induction Base:
gt(gen_0':s15_23(0), gen_0':s15_23(0)) ->_R^Omega(0)
false

Induction Step:
gt(gen_0':s15_23(+(n21_23, 1)), gen_0':s15_23(+(n21_23, 1))) ->_R^Omega(0)
gt(gen_0':s15_23(n21_23), gen_0':s15_23(n21_23)) ->_IH
false

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

(12)
Obligation:
Innermost TRS:
Rules:
SORT(z0) -> c(ST(0', z0))
ST(z0, z1) -> c1(COND1(member(z0, z1), z0, z1), MEMBER(z0, z1))
COND1(true, z0, z1) -> c2(ST(s(z0), z1))
COND1(false, z0, z1) -> c3(COND2(gt(z0, max(z1)), z0, z1), GT(z0, max(z1)), MAX(z1))
COND2(true, z0, z1) -> c4
COND2(false, z0, z1) -> c5(ST(s(z0), z1))
MEMBER(z0, nil) -> c6
MEMBER(z0, cons(z1, z2)) -> c7(OR(equal(z0, z1), member(z0, z2)), EQUAL(z0, z1))
MEMBER(z0, cons(z1, z2)) -> c8(OR(equal(z0, z1), member(z0, z2)), MEMBER(z0, z2))
OR(z0, true) -> c9
OR(z0, false) -> c10
EQUAL(0', 0') -> c11
EQUAL(s(z0), 0') -> c12
EQUAL(0', s(z0)) -> c13
EQUAL(s(z0), s(z1)) -> c14(EQUAL(z0, z1))
GT(0', z0) -> c15
GT(s(z0), 0') -> c16
GT(s(z0), s(z1)) -> c17(GT(z0, z1))
MAX(nil) -> c18
MAX(cons(z0, z1)) -> c19(IF(gt(z0, max(z1)), z0, max(z1)), GT(z0, max(z1)), MAX(z1))
MAX(cons(z0, z1)) -> c20(IF(gt(z0, max(z1)), z0, max(z1)), MAX(z1))
IF(true, z0, z1) -> c21
IF(false, z0, z1) -> c22
sort(z0) -> st(0', z0)
st(z0, z1) -> cond1(member(z0, z1), z0, z1)
cond1(true, z0, z1) -> cons(z0, st(s(z0), z1))
cond1(false, z0, z1) -> cond2(gt(z0, max(z1)), z0, z1)
cond2(true, z0, z1) -> nil
cond2(false, z0, z1) -> st(s(z0), z1)
member(z0, nil) -> false
member(z0, cons(z1, z2)) -> or(equal(z0, z1), member(z0, z2))
or(z0, true) -> true
or(z0, false) -> z0
equal(0', 0') -> true
equal(s(z0), 0') -> false
equal(0', s(z0)) -> false
equal(s(z0), s(z1)) -> equal(z0, z1)
gt(0', z0) -> false
gt(s(z0), 0') -> true
gt(s(z0), s(z1)) -> gt(z0, z1)
max(nil) -> 0'
max(cons(z0, z1)) -> if(gt(z0, max(z1)), z0, max(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1

Types:
SORT :: nil:cons -> c
c :: c1 -> c
ST :: 0':s -> nil:cons -> c1
0' :: 0':s
c1 :: c2:c3 -> c6:c7:c8 -> c1
COND1 :: true:false -> 0':s -> nil:cons -> c2:c3
member :: 0':s -> nil:cons -> true:false
MEMBER :: 0':s -> nil:cons -> c6:c7:c8
true :: true:false
c2 :: c1 -> c2:c3
s :: 0':s -> 0':s
false :: true:false
c3 :: c4:c5 -> c15:c16:c17 -> c18:c19:c20 -> c2:c3
COND2 :: true:false -> 0':s -> nil:cons -> c4:c5
gt :: 0':s -> 0':s -> true:false
max :: nil:cons -> 0':s
GT :: 0':s -> 0':s -> c15:c16:c17
MAX :: nil:cons -> c18:c19:c20
c4 :: c4:c5
c5 :: c1 -> c4:c5
nil :: nil:cons
c6 :: c6:c7:c8
cons :: 0':s -> nil:cons -> nil:cons
c7 :: c9:c10 -> c11:c12:c13:c14 -> c6:c7:c8
OR :: true:false -> true:false -> c9:c10
equal :: 0':s -> 0':s -> true:false
EQUAL :: 0':s -> 0':s -> c11:c12:c13:c14
c8 :: c9:c10 -> c6:c7:c8 -> c6:c7:c8
c9 :: c9:c10
c10 :: c9:c10
c11 :: c11:c12:c13:c14
c12 :: c11:c12:c13:c14
c13 :: c11:c12:c13:c14
c14 :: c11:c12:c13:c14 -> c11:c12:c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19:c20
c19 :: c21:c22 -> c15:c16:c17 -> c18:c19:c20 -> c18:c19:c20
IF :: true:false -> 0':s -> 0':s -> c21:c22
c20 :: c21:c22 -> c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22
c22 :: c21:c22
sort :: nil:cons -> nil:cons
st :: 0':s -> nil:cons -> nil:cons
cond1 :: true:false -> 0':s -> nil:cons -> nil:cons
cond2 :: true:false -> 0':s -> nil:cons -> nil:cons
or :: true:false -> true:false -> true:false
if :: true:false -> 0':s -> 0':s -> 0':s
hole_c1_23 :: c
hole_nil:cons2_23 :: nil:cons
hole_c13_23 :: c1
hole_0':s4_23 :: 0':s
hole_c2:c35_23 :: c2:c3
hole_c6:c7:c86_23 :: c6:c7:c8
hole_true:false7_23 :: true:false
hole_c4:c58_23 :: c4:c5
hole_c15:c16:c179_23 :: c15:c16:c17
hole_c18:c19:c2010_23 :: c18:c19:c20
hole_c9:c1011_23 :: c9:c10
hole_c11:c12:c13:c1412_23 :: c11:c12:c13:c14
hole_c21:c2213_23 :: c21:c22
gen_nil:cons14_23 :: Nat -> nil:cons
gen_0':s15_23 :: Nat -> 0':s
gen_c6:c7:c816_23 :: Nat -> c6:c7:c8
gen_c15:c16:c1717_23 :: Nat -> c15:c16:c17
gen_c18:c19:c2018_23 :: Nat -> c18:c19:c20
gen_c11:c12:c13:c1419_23 :: Nat -> c11:c12:c13:c14


Lemmas:
gt(gen_0':s15_23(n21_23), gen_0':s15_23(n21_23)) -> false, rt in Omega(0)


Generator Equations:
gen_nil:cons14_23(0) <=> nil
gen_nil:cons14_23(+(x, 1)) <=> cons(0', gen_nil:cons14_23(x))
gen_0':s15_23(0) <=> 0'
gen_0':s15_23(+(x, 1)) <=> s(gen_0':s15_23(x))
gen_c6:c7:c816_23(0) <=> c6
gen_c6:c7:c816_23(+(x, 1)) <=> c8(c9, gen_c6:c7:c816_23(x))
gen_c15:c16:c1717_23(0) <=> c15
gen_c15:c16:c1717_23(+(x, 1)) <=> c17(gen_c15:c16:c1717_23(x))
gen_c18:c19:c2018_23(0) <=> c18
gen_c18:c19:c2018_23(+(x, 1)) <=> c19(c21, c15, gen_c18:c19:c2018_23(x))
gen_c11:c12:c13:c1419_23(0) <=> c11
gen_c11:c12:c13:c1419_23(+(x, 1)) <=> c14(gen_c11:c12:c13:c1419_23(x))


The following defined symbols remain to be analysed:
max, ST, member, MEMBER, GT, MAX, equal, EQUAL, st

They will be analysed ascendingly in the following order:
member < ST
MEMBER < ST
max < ST
GT < ST
MAX < ST
member < MEMBER
equal < member
member < st
equal < MEMBER
EQUAL < MEMBER
max < MAX
max < st
GT < MAX

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

(13) RewriteLemmaProof (FINISHED)
Proved the following rewrite lemma:
max(gen_nil:cons14_23(n516_23)) -> gen_0':s15_23(0), rt in Omega(EXP)

Induction Base:
max(gen_nil:cons14_23(0)) ->_R^Omega(0)
0'

Induction Step:
max(gen_nil:cons14_23(+(n516_23, 1))) ->_R^Omega(0)
if(gt(0', max(gen_nil:cons14_23(n516_23))), 0', max(gen_nil:cons14_23(n516_23))) ->_IH
if(gt(0', gen_0':s15_23(0)), 0', max(gen_nil:cons14_23(n516_23))) ->_L^Omega(0)
if(false, 0', max(gen_nil:cons14_23(n516_23))) ->_IH
if(false, 0', gen_0':s15_23(0)) ->_R^Omega(0)
gen_0':s15_23(0)

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

(14)
BOUNDS(EXP, INF)