(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
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), z) → gcd(-(max(x, y), min(x, y)), s(min(x, y)), z)
gcd(x, s(y), s(z)) → gcd(x, -(max(y, z), min(y, z)), s(min(y, z)))
gcd(s(x), y, s(z)) → gcd(-(max(x, z), min(x, z)), y, s(min(x, z)))
gcd(x, 0, 0) → x
gcd(0, y, 0) → y
gcd(0, 0, z) → z
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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), z) → GCD(-(max(x, y), min(x, y)), s(min(x, y)), z)
GCD(s(x), s(y), z) → -1(max(x, y), min(x, y))
GCD(s(x), s(y), z) → MAX(x, y)
GCD(s(x), s(y), z) → MIN(x, y)
GCD(x, s(y), s(z)) → GCD(x, -(max(y, z), min(y, z)), s(min(y, z)))
GCD(x, s(y), s(z)) → -1(max(y, z), min(y, z))
GCD(x, s(y), s(z)) → MAX(y, z)
GCD(x, s(y), s(z)) → MIN(y, z)
GCD(s(x), y, s(z)) → GCD(-(max(x, z), min(x, z)), y, s(min(x, z)))
GCD(s(x), y, s(z)) → -1(max(x, z), min(x, z))
GCD(s(x), y, s(z)) → MAX(x, z)
GCD(s(x), y, s(z)) → MIN(x, z)
The TRS R consists of the following rules:
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), z) → gcd(-(max(x, y), min(x, y)), s(min(x, y)), z)
gcd(x, s(y), s(z)) → gcd(x, -(max(y, z), min(y, z)), s(min(y, z)))
gcd(s(x), y, s(z)) → gcd(-(max(x, z), min(x, z)), y, s(min(x, z)))
gcd(x, 0, 0) → x
gcd(0, y, 0) → y
gcd(0, 0, z) → z
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 4 SCCs with 9 less nodes.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
-1(s(x), s(y)) → -1(x, y)
The TRS R consists of the following rules:
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), z) → gcd(-(max(x, y), min(x, y)), s(min(x, y)), z)
gcd(x, s(y), s(z)) → gcd(x, -(max(y, z), min(y, z)), s(min(y, z)))
gcd(s(x), y, s(z)) → gcd(-(max(x, z), min(x, z)), y, s(min(x, z)))
gcd(x, 0, 0) → x
gcd(0, y, 0) → y
gcd(0, 0, z) → z
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAX(s(x), s(y)) → MAX(x, y)
The TRS R consists of the following rules:
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), z) → gcd(-(max(x, y), min(x, y)), s(min(x, y)), z)
gcd(x, s(y), s(z)) → gcd(x, -(max(y, z), min(y, z)), s(min(y, z)))
gcd(s(x), y, s(z)) → gcd(-(max(x, z), min(x, z)), y, s(min(x, z)))
gcd(x, 0, 0) → x
gcd(0, y, 0) → y
gcd(0, 0, z) → z
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MIN(s(x), s(y)) → MIN(x, y)
The TRS R consists of the following rules:
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), z) → gcd(-(max(x, y), min(x, y)), s(min(x, y)), z)
gcd(x, s(y), s(z)) → gcd(x, -(max(y, z), min(y, z)), s(min(y, z)))
gcd(s(x), y, s(z)) → gcd(-(max(x, z), min(x, z)), y, s(min(x, z)))
gcd(x, 0, 0) → x
gcd(0, y, 0) → y
gcd(0, 0, z) → z
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(x, s(y), s(z)) → GCD(x, -(max(y, z), min(y, z)), s(min(y, z)))
GCD(s(x), s(y), z) → GCD(-(max(x, y), min(x, y)), s(min(x, y)), z)
GCD(s(x), y, s(z)) → GCD(-(max(x, z), min(x, z)), y, s(min(x, z)))
The TRS R consists of the following rules:
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), z) → gcd(-(max(x, y), min(x, y)), s(min(x, y)), z)
gcd(x, s(y), s(z)) → gcd(x, -(max(y, z), min(y, z)), s(min(y, z)))
gcd(s(x), y, s(z)) → gcd(-(max(x, z), min(x, z)), y, s(min(x, z)))
gcd(x, 0, 0) → x
gcd(0, y, 0) → y
gcd(0, 0, z) → z
Q is empty.
We have to consider all minimal (P,Q,R)-chains.