KILLED
proof of /export/starexec/sandbox/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:

   QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
   QS(z0, nil) -> c1
   QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
   QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
   QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
   QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
   QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
   FILTERLOW(z0, nil) -> c7
   FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
   IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
   FILTERHIGH(z0, nil) -> c11
   FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
   IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
   IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
   GE(z0, 0) -> c15
   GE(0, s(z0)) -> c16
   GE(s(z0), s(z1)) -> c17(GE(z0, z1))
   APPEND(nil, ys) -> c18
   APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
   LENGTH(nil) -> c20
   LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
   HALF(0) -> c22
   HALF(s(0)) -> c23
   HALF(s(s(z0))) -> c24(HALF(z0))
   GET(z0, nil) -> c25
   GET(z0, cons(z1, nil)) -> c26
   GET(0, cons(z0, cons(z1, z2))) -> c27
   GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))

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

   qsort(z0) -> qs(half(length(z0)), z0)
   qs(z0, nil) -> nil
   qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
   filterlow(z0, nil) -> nil
   filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> filterlow(z0, z2)
   if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
   filterhigh(z0, nil) -> nil
   filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
   if2(true, z0, z1, z2) -> filterhigh(z0, z2)
   if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   append(nil, ys) -> ys
   append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   get(z0, nil) -> 0
   get(z0, cons(z1, nil)) -> z1
   get(0, cons(z0, cons(z1, z2))) -> z0
   get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

Rewrite Strategy: INNERMOST