WORST_CASE(?,O(1))
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, 1).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 284 ms]
(2) CpxRelTRS
(3) NarrowingOnBasicTermsTerminatesProof [FINISHED, 0 ms]
(4) BOUNDS(1, 1)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

   GCD(z0, 0) -> c
   GCD(0, z0) -> c1
   GCD(s(z0), s(z1)) -> c2(GCD(s(z0), -(z1, z0)))
   GCD(s(z0), s(z1)) -> c3(GCD(-(z0, z1), s(z1)))

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

   gcd(z0, 0) -> z0
   gcd(0, z0) -> z0
   gcd(s(z0), s(z1)) -> if(<(z0, z1), gcd(s(z0), -(z1, z0)), gcd(-(z0, z1), s(z1)))

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

   GCD(z0, 0) -> c
   GCD(0, z0) -> c1
   GCD(s(z0), s(z1)) -> c2(GCD(s(z0), -(z1, z0)))
   GCD(s(z0), s(z1)) -> c3(GCD(-(z0, z1), s(z1)))

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

   gcd(z0, 0) -> z0
   gcd(0, z0) -> z0
   gcd(s(z0), s(z1)) -> if(<(z0, z1), gcd(s(z0), -(z1, z0)), gcd(-(z0, z1), s(z1)))

Rewrite Strategy: INNERMOST
----------------------------------------

(3) NarrowingOnBasicTermsTerminatesProof (FINISHED)
Constant runtime complexity proven by termination of constructor-based narrowing.

The maximal most general narrowing sequences give rise to the following rewrite sequences:

gcd(s(x0), s(x1)) ->^* if(<(x0, x1), gcd(s(x0), -(x1, x0)), gcd(-(x0, x1), s(x1)))

GCD(s(x0), s(x1)) ->^* c3(GCD(-(x0, x1), s(x1)))

GCD(s(x0), s(x1)) ->^* c2(GCD(s(x0), -(x1, x0)))

GCD(0, x0) ->^* c1

GCD(x0, 0) ->^* c




----------------------------------------

(4)
BOUNDS(1, 1)