YES
(VAR X Y)
(RULES 
minus(X,s(Y)) -> pred(minus(X,Y))
minus(X,0) -> X
pred(s(X)) -> X
le(s(X),s(Y)) -> le(X,Y)
le(s(X),0) -> false
le(0,Y) -> true
gcd(0,Y) -> 0
gcd(s(X),0) -> s(X)
gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
if(true,s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
if(false,s(X),s(Y)) -> gcd(minus(Y,X),s(X))
)

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_minus(X,s(Y)) -> nF_pred(minus(X,Y))
nF_minus(X,s(Y)) -> nF_minus(X,Y)
nF_le(s(X),s(Y)) -> nF_le(X,Y)
nF_gcd(s(X),s(Y)) -> nF_if(le(Y,X),s(X),s(Y))
nF_gcd(s(X),s(Y)) -> nF_le(Y,X)
nF_if(true,s(X),s(Y)) -> nF_gcd(minus(X,Y),s(Y))
nF_if(true,s(X),s(Y)) -> nF_minus(X,Y)
nF_if(false,s(X),s(Y)) -> nF_gcd(minus(Y,X),s(X))
nF_if(false,s(X),s(Y)) -> nF_minus(Y,X)

-> Proof of termination for gcd_1_1:
-> -> Dependency pairs in cycle:
nF_gcd(s(X),s(Y)) -> nF_if(le(Y,X),s(X),s(Y))
nF_if(false,s(X),s(Y)) -> nF_gcd(minus(Y,X),s(X))
nF_if(true,s(X),s(Y)) -> nF_gcd(minus(X,Y),s(Y))

UsableRules:
minus(X,s(Y)) -> pred(minus(X,Y))
minus(X,0) -> X
pred(s(X)) -> X
le(s(X),s(Y)) -> le(X,Y)
le(s(X),0) -> false
le(0,Y) -> true

Polynomial Interpretation:

[minus](X1,X2) = X1
[s](X) = X + 1
[pred](X) = X
[0] = 1
[le](X1,X2) = X1
[false] = 0
[true] = 0
[gcd](X1,X2) = 0
[if](X1,X2,X3) = 0
[nF_gcd](X1,X2) = X1 + X2
[nF_if](X1,X2,X3) = X2 + X3

TIME: 6.5526e-2

-> -> Dependency pairs in cycle:
nF_gcd(s(X),s(Y)) -> nF_if(le(Y,X),s(X),s(Y))
nF_if(false,s(X),s(Y)) -> nF_gcd(minus(Y,X),s(X))

UsableRules:
minus(X,s(Y)) -> pred(minus(X,Y))
minus(X,0) -> X
pred(s(X)) -> X
le(s(X),s(Y)) -> le(X,Y)
le(s(X),0) -> false
le(0,Y) -> true

Polynomial Interpretation:

[minus](X1,X2) = X1
[s](X) = X + 1
[pred](X) = X
[0] = 0
[le](X1,X2) = 1
[false] = 1
[true] = 0
[gcd](X1,X2) = 0
[if](X1,X2,X3) = 0
[nF_gcd](X1,X2) = X1 + X2 + 1
[nF_if](X1,X2,X3) = X1 + X2 + X3

TIME: 6.1671e-2


-> Proof of termination for gcd_1_2:
-> -> Dependency pairs in cycle:
nF_le(s(X),s(Y)) -> nF_le(X,Y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for gcd_1_3:
-> -> Dependency pairs in cycle:
nF_minus(X,s(Y)) -> nF_minus(X,Y)

Termination proved: Cycles verify subterm criterion.

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



Termination was proved succesfully.