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:

   F(true, z0, z1) -> c(F(and(gt(z0, z1), gt(z1, s(s(0)))), plus(s(0), z0), double(z1)), AND(gt(z0, z1), gt(z1, s(s(0)))), GT(z0, z1))
   F(true, z0, z1) -> c1(F(and(gt(z0, z1), gt(z1, s(s(0)))), plus(s(0), z0), double(z1)), AND(gt(z0, z1), gt(z1, s(s(0)))), GT(z1, s(s(0))))
   F(true, z0, z1) -> c2(F(and(gt(z0, z1), gt(z1, s(s(0)))), plus(s(0), z0), double(z1)), PLUS(s(0), z0))
   F(true, z0, z1) -> c3(F(and(gt(z0, z1), gt(z1, s(s(0)))), plus(s(0), z0), double(z1)), DOUBLE(z1))
   GT(0, z0) -> c4
   GT(s(z0), 0) -> c5
   GT(s(z0), s(z1)) -> c6(GT(z0, z1))
   AND(z0, true) -> c7
   AND(z0, false) -> c8
   PLUS(z0, 0) -> c9
   PLUS(z0, s(z1)) -> c10(PLUS(z0, z1))
   DOUBLE(0) -> c11
   DOUBLE(s(z0)) -> c12(DOUBLE(z0))

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

   f(true, z0, z1) -> f(and(gt(z0, z1), gt(z1, s(s(0)))), plus(s(0), z0), double(z1))
   gt(0, z0) -> false
   gt(s(z0), 0) -> true
   gt(s(z0), s(z1)) -> gt(z0, z1)
   and(z0, true) -> z0
   and(z0, false) -> false
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))

Rewrite Strategy: INNERMOST