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:

   MIN(0, z0) -> c
   MIN(z0, 0) -> c1
   MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
   MAX(0, z0) -> c3
   MAX(z0, 0) -> c4
   MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
   TWICE(0) -> c6
   TWICE(s(z0)) -> c7(TWICE(z0))
   -'(z0, 0) -> c8
   -'(s(z0), s(z1)) -> c9(-'(z0, z1))
   P(s(z0)) -> c10
   F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
   F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
   F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))

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

   min(0, z0) -> 0
   min(z0, 0) -> 0
   min(s(z0), s(z1)) -> s(min(z0, z1))
   max(0, z0) -> z0
   max(z0, 0) -> z0
   max(s(z0), s(z1)) -> s(max(z0, z1))
   twice(0) -> 0
   twice(s(z0)) -> s(s(twice(z0)))
   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   p(s(z0)) -> z0
   f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

Rewrite Strategy: INNERMOST