KILLED
proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS


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

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


The TRS R consists of the following rules:

   AVERAGE(z0, z1) -> c1(IF(ge(z0, z1), z0, z1), GE(z0, z1))
   IF(true, z0, z1) -> c2(AVERITER(z1, z0, z1))
   IF(false, z0, z1) -> c3(AVERITER(z0, z1, z0))
   AVERITER(z0, z1, z2) -> c4(IFITER(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IFITER(true, z0, z1, z2) -> c5
   IFITER(false, z0, z1, z2) -> c6(AVERITER(plus(z0, s(s(s(0)))), plus(z1, s(0)), plus(z2, s(0))), PLUS(z0, s(s(s(0)))))
   IFITER(false, z0, z1, z2) -> c7(AVERITER(plus(z0, s(s(s(0)))), plus(z1, s(0)), plus(z2, s(0))), PLUS(z1, s(0)))
   IFITER(false, z0, z1, z2) -> c8(AVERITER(plus(z0, s(s(s(0)))), plus(z1, s(0)), plus(z2, s(0))), PLUS(z2, s(0)))
   APPEND(nil, z0) -> c9
   APPEND(cons(z0, z1), z2) -> c10
   LOW(z0, nil) -> c11
   LOW(z0, cons(z1, z2)) -> c12(IF_LOW(ge(z1, z0), z0, cons(z1, z2)), GE(z1, z0))
   IF_LOW(false, z0, cons(z1, z2)) -> c13(LOW(z0, z2))
   IF_LOW(true, z0, cons(z1, z2)) -> c14(LOW(z0, z2))
   HIGH(z0, nil) -> c15
   HIGH(z0, cons(z1, z2)) -> c16(IF_HIGH(ge(z1, z0), z0, cons(z1, z2)), GE(z1, z0))
   IF_HIGH(false, z0, cons(z1, z2)) -> c17(HIGH(z0, z2))
   IF_HIGH(true, z0, cons(z1, z2)) -> c18(AVERAGE(z1, z1))
   IF_HIGH(true, z0, cons(z1, z2)) -> c19(HIGH(z0, z2))
   QUICKSORT(z0) -> c20(IFQUICK(isempty(z0), z0), ISEMPTY(z0))
   IFQUICK(true, z0) -> c21
   IFQUICK(false, z0) -> c22(APPEND(quicksort(low(head(z0), tail(z0))), cons(tail(z0), quicksort(high(head(z0), tail(z0))))), QUICKSORT(low(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
   IFQUICK(false, z0) -> c23(APPEND(quicksort(low(head(z0), tail(z0))), cons(tail(z0), quicksort(high(head(z0), tail(z0))))), QUICKSORT(low(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
   IFQUICK(false, z0) -> c24(APPEND(quicksort(low(head(z0), tail(z0))), cons(tail(z0), quicksort(high(head(z0), tail(z0))))), TAIL(z0))
   IFQUICK(false, z0) -> c25(APPEND(quicksort(low(head(z0), tail(z0))), cons(tail(z0), quicksort(high(head(z0), tail(z0))))), QUICKSORT(high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
   IFQUICK(false, z0) -> c26(APPEND(quicksort(low(head(z0), tail(z0))), cons(tail(z0), quicksort(high(head(z0), tail(z0))))), QUICKSORT(high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
   PLUS(0, z0) -> c27
   PLUS(s(z0), z1) -> c28(PLUS(z0, z1))
   ISEMPTY(nil) -> c29
   ISEMPTY(cons(z0, z1)) -> c30
   HEAD(nil) -> c31
   HEAD(cons(z0, z1)) -> c32
   TAIL(nil) -> c33
   TAIL(cons(z0, z1)) -> c34
   GE(z0, 0) -> c35
   GE(0, s(z0)) -> c36
   GE(s(z0), s(z1)) -> c37(GE(z0, z1))
   A -> c38
   A -> c39

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

   average(z0, z1) -> if(ge(z0, z1), z0, z1)
   if(true, z0, z1) -> averIter(z1, z0, z1)
   if(false, z0, z1) -> averIter(z0, z1, z0)
   averIter(z0, z1, z2) -> ifIter(ge(z0, z1), z0, z1, z2)
   ifIter(true, z0, z1, z2) -> z2
   ifIter(false, z0, z1, z2) -> averIter(plus(z0, s(s(s(0)))), plus(z1, s(0)), plus(z2, s(0)))
   append(nil, z0) -> z0
   append(cons(z0, z1), z2) -> cons(z0, app(z1, z2))
   low(z0, nil) -> nil
   low(z0, cons(z1, z2)) -> if_low(ge(z1, z0), z0, cons(z1, z2))
   if_low(false, z0, cons(z1, z2)) -> cons(z1, low(z0, z2))
   if_low(true, z0, cons(z1, z2)) -> low(z0, z2)
   high(z0, nil) -> nil
   high(z0, cons(z1, z2)) -> if_high(ge(z1, z0), z0, cons(z1, z2))
   if_high(false, z0, cons(z1, z2)) -> high(z0, z2)
   if_high(true, z0, cons(z1, z2)) -> cons(average(z1, z1), high(z0, z2))
   quicksort(z0) -> ifquick(isempty(z0), z0)
   ifquick(true, z0) -> nil
   ifquick(false, z0) -> append(quicksort(low(head(z0), tail(z0))), cons(tail(z0), quicksort(high(head(z0), tail(z0)))))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   isempty(nil) -> true
   isempty(cons(z0, z1)) -> false
   head(nil) -> error
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> b
   a -> c

Rewrite Strategy: INNERMOST