0.00/0.55
0.00/0.55
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
gcd(x, 0) → x
0.00/0.55
gcd(0, y) → y
0.00/0.55
gcd(s(x), s(y)) → if(<(x, y), gcd(s(x), -(y, x)), gcd(-(x, y), s(y)))
Rewrite Strategy: INNERMOST
0.00/0.55
0.00/0.55
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
0.00/0.55
0.00/0.55
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
gcd(z0, 0) → z0
0.00/0.55
gcd(0, z0) → z0
0.00/0.55
gcd(s(z0), s(z1)) → if(<(z0, z1), gcd(s(z0), -(z1, z0)), gcd(-(z0, z1), s(z1)))
Tuples:
GCD(s(z0), s(z1)) → c2(GCD(s(z0), -(z1, z0)), GCD(-(z0, z1), s(z1)))
S tuples:
GCD(s(z0), s(z1)) → c2(GCD(s(z0), -(z1, z0)), GCD(-(z0, z1), s(z1)))
K tuples:none
Defined Rule Symbols:
gcd
Defined Pair Symbols:
GCD
Compound Symbols:
c2
0.00/0.55
0.00/0.55
(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
0.00/0.55
0.00/0.55
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
gcd(z0, 0) → z0
0.00/0.55
gcd(0, z0) → z0
0.00/0.55
gcd(s(z0), s(z1)) → if(<(z0, z1), gcd(s(z0), -(z1, z0)), gcd(-(z0, z1), s(z1)))
Tuples:
GCD(s(z0), s(z1)) → c2
S tuples:
GCD(s(z0), s(z1)) → c2
K tuples:none
Defined Rule Symbols:
gcd
Defined Pair Symbols:
GCD
Compound Symbols:
c2
0.00/0.55
0.00/0.55
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
GCD(s(z0), s(z1)) → c2
0.00/0.55
0.00/0.55
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
gcd(z0, 0) → z0
0.00/0.55
gcd(0, z0) → z0
0.00/0.55
gcd(s(z0), s(z1)) → if(<(z0, z1), gcd(s(z0), -(z1, z0)), gcd(-(z0, z1), s(z1)))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
gcd
Defined Pair Symbols:none
Compound Symbols:none
0.00/0.55
0.00/0.55
(7) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
0.00/0.55
0.00/0.55
(8) BOUNDS(O(1), O(1))
0.00/0.55