YES
0 QTRS
↳1 AAECC Innermost (⇔, 8 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 QDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 QDP
↳31 QReductionProof (⇔, 0 ms)
↳32 QDP
↳33 TransformationProof (⇔, 0 ms)
↳34 QDP
↳35 QDPQMonotonicMRRProof (⇔, 7 ms)
↳36 QDP
↳37 PisEmptyProof (⇔, 0 ms)
↳38 YES
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
gcd(s(x), s(y)) → gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
min(x, 0) → 0
gcd(s(x), s(y)) → gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
gcd(s(x), s(y)) → gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
MIN(s(x), s(y)) → MIN(x, y)
MAX(s(x), s(y)) → MAX(x, y)
-1(s(x), s(y)) → -1(x, y)
GCD(s(x), s(y)) → GCD(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
GCD(s(x), s(y)) → -1(s(max(x, y)), s(min(x, y)))
GCD(s(x), s(y)) → MAX(x, y)
GCD(s(x), s(y)) → MIN(x, y)
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
gcd(s(x), s(y)) → gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
gcd(s(x), s(y)) → gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
From the DPs we obtained the following set of size-change graphs:
MAX(s(x), s(y)) → MAX(x, y)
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
gcd(s(x), s(y)) → gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
MAX(s(x), s(y)) → MAX(x, y)
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
MAX(s(x), s(y)) → MAX(x, y)
From the DPs we obtained the following set of size-change graphs:
MIN(s(x), s(y)) → MIN(x, y)
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
gcd(s(x), s(y)) → gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
MIN(s(x), s(y)) → MIN(x, y)
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
MIN(s(x), s(y)) → MIN(x, y)
From the DPs we obtained the following set of size-change graphs:
GCD(s(x), s(y)) → GCD(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
gcd(s(x), s(y)) → gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
GCD(s(x), s(y)) → GCD(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
gcd(s(x0), s(x1))
gcd(s(x0), s(x1))
GCD(s(x), s(y)) → GCD(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
GCD(s(x), s(y)) → GCD(-(max(x, y), min(x, y)), s(min(x, y))) → GCD(s(x), s(y)) → GCD(-(max(x, y), min(x, y)), s(min(x, y)))
GCD(s(x), s(y)) → GCD(-(max(x, y), min(x, y)), s(min(x, y)))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
GCD(s(x), s(y)) → GCD(-(max(x, y), min(x, y)), s(min(x, y)))
max(s(x), s(y)) → s(max(x, y))
-(s(x), s(y)) → -(x, y)
POL(-(x1, x2)) = x1
POL(0) = 0
POL(GCD(x1, x2)) = 2·x1 + x2
POL(max(x1, x2)) = x1 + x2
POL(min(x1, x2)) = x1
POL(s(x1)) = 1 + 2·x1
max(x, 0) → x
max(0, y) → y
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
-(x, 0) → x
min(x0, 0)
min(0, x0)
min(s(x0), s(x1))
max(x0, 0)
max(0, x0)
max(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))