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:

   MINUS(0, z0) -> c
   MINUS(s(z0), 0) -> c1
   MINUS(s(z0), s(z1)) -> c2(MINUS(z0, z1))
   MOD(z0, 0) -> c3
   MOD(z0, s(z1)) -> c4(IF(lt(z0, s(z1)), z0, s(z1)), LT(z0, s(z1)))
   IF(true, z0, z1) -> c5
   IF(false, z0, z1) -> c6(MOD(minus(z0, z1), z1), MINUS(z0, z1))
   GCD(z0, 0) -> c7
   GCD(0, s(z0)) -> c8
   GCD(s(z0), s(z1)) -> c9(GCD(mod(s(z0), s(z1)), mod(s(z1), s(z0))), MOD(s(z0), s(z1)))
   GCD(s(z0), s(z1)) -> c10(GCD(mod(s(z0), s(z1)), mod(s(z1), s(z0))), MOD(s(z1), s(z0)))
   LT(z0, 0) -> c11
   LT(0, s(z0)) -> c12
   LT(s(z0), s(z1)) -> c13(LT(z0, z1))

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

   minus(0, z0) -> 0
   minus(s(z0), 0) -> s(z0)
   minus(s(z0), s(z1)) -> minus(z0, z1)
   mod(z0, 0) -> 0
   mod(z0, s(z1)) -> if(lt(z0, s(z1)), z0, s(z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> mod(minus(z0, z1), z1)
   gcd(z0, 0) -> z0
   gcd(0, s(z0)) -> s(z0)
   gcd(s(z0), s(z1)) -> gcd(mod(s(z0), s(z1)), mod(s(z1), s(z0)))
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)

Rewrite Strategy: INNERMOST