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:

   LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
   COND(true, z0, z1) -> c1
   COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
   LE(0, z0) -> c3
   LE(s(z0), 0) -> c4
   LE(s(z0), s(z1)) -> c5(LE(z0, z1))
   DOUBLE(0) -> c6
   DOUBLE(s(z0)) -> c7(DOUBLE(z0))
   SQUARE(0) -> c8
   SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
   SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
   PLUS(z0, 0) -> c11
   PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))

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

   log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
   cond(true, z0, z1) -> s(0)
   cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   square(0) -> 0
   square(s(z0)) -> s(plus(square(z0), double(z0)))
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))

Rewrite Strategy: INNERMOST