YES
(VAR x y)
(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),0) -> s(x)
gcd(0,s(x)) -> s(x)
gcd(s(x),s(y)) -> gcd(-(max(x,y),min(x,y)),s(min(x,y)))
)

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for gcd:

-> Dependency pairs:
nF_min(s(x),s(y)) -> nF_min(x,y)
nF_max(s(x),s(y)) -> nF_max(x,y)
nF_-(s(x),s(y)) -> nF_-(x,y)
nF_gcd(s(x),s(y)) -> nF_gcd(-(max(x,y),min(x,y)),s(min(x,y)))
nF_gcd(s(x),s(y)) -> nF_-(max(x,y),min(x,y))
nF_gcd(s(x),s(y)) -> nF_max(x,y)
nF_gcd(s(x),s(y)) -> nF_min(x,y)

-> Proof of termination for gcd_1_1:
-> -> Dependency pairs in cycle:
nF_gcd(s(x),s(y)) -> nF_gcd(-(max(x,y),min(x,y)),s(min(x,y)))

UsableRules:
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)

Polynomial Interpretation:

[min](X1,X2) = X1
[0] = 0
[s](X) = 2.X + 1
[max](X1,X2) = X1 + X2
[-](X1,X2) = X1
[gcd](X1,X2) = 0
[nF_gcd](X1,X2) = 2.X1 + X2

TIME: 6.746e-3


-> Proof of termination for gcd_1_2:
-> -> Dependency pairs in cycle:
nF_-(s(x),s(y)) -> nF_-(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for gcd_1_3:
-> -> Dependency pairs in cycle:
nF_max(s(x),s(y)) -> nF_max(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for gcd_1_4:
-> -> Dependency pairs in cycle:
nF_min(s(x),s(y)) -> nF_min(x,y)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 2
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.