(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R 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(nil) → 0
gcd(cons(x, nil)) → x
gcd(cons(0, y)) → gcd(y)
gcd(cons(x, cons(y, z))) → gcd(cons(-(x, y), cons(y, z)))
The relative TRS consists of the following S rules:
gcd(cons(x, cons(y, z))) → gcd(cons(max(x, y), cons(min(x, y), z)))
(1) RelTRSLoopFinderProof (COMPLETE transformation)
The following loop was found:
---------- Loop: ----------
gcd(cons(x, cons(y, z))) → gcd(cons(-(x, y), cons(y, z))) with rule gcd(cons(x', cons(y', z'))) → gcd(cons(-(x', y'), cons(y', z'))) at position [] and matcher [x' / x, y' / y, z' / z]
Now an instance of the first term with Matcher [x / -(x, y)] occurs in the last term at position [].
Context: []
Therefore, the relative TRS problem does not terminate.
(2) NO