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:

   -'(z0, 0) -> c
   -'(s(z0), s(z1)) -> c1(-'(z0, z1))
   +'(0, z0) -> c2
   +'(s(z0), z1) -> c3(+'(z0, z1))
   *'(z0, 0) -> c4
   *'(z0, s(z1)) -> c5(+'(z0, *(z0, z1)), *'(z0, z1))
   F(s(z0)) -> c6(F(-(+(*(s(z0), s(z0)), *(s(z0), s(s(s(0))))), *(s(s(z0)), s(s(z0))))), -'(+(*(s(z0), s(z0)), *(s(z0), s(s(s(0))))), *(s(s(z0)), s(s(z0)))), +'(*(s(z0), s(z0)), *(s(z0), s(s(s(0))))), *'(s(z0), s(z0)))
   F(s(z0)) -> c7(F(-(+(*(s(z0), s(z0)), *(s(z0), s(s(s(0))))), *(s(s(z0)), s(s(z0))))), -'(+(*(s(z0), s(z0)), *(s(z0), s(s(s(0))))), *(s(s(z0)), s(s(z0)))), +'(*(s(z0), s(z0)), *(s(z0), s(s(s(0))))), *'(s(z0), s(s(s(0)))))
   F(s(z0)) -> c8(F(-(+(*(s(z0), s(z0)), *(s(z0), s(s(s(0))))), *(s(s(z0)), s(s(z0))))), -'(+(*(s(z0), s(z0)), *(s(z0), s(s(s(0))))), *(s(s(z0)), s(s(z0)))), *'(s(s(z0)), s(s(z0))))

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

   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   *(z0, 0) -> 0
   *(z0, s(z1)) -> +(z0, *(z0, z1))
   f(s(z0)) -> f(-(+(*(s(z0), s(z0)), *(s(z0), s(s(s(0))))), *(s(s(z0)), s(s(z0)))))

Rewrite Strategy: INNERMOST