YES
(VAR Y X)
(RULES 
minus(0,Y) -> 0
minus(s(X),s(Y)) -> minus(X,Y)
geq(X,0) -> true
geq(0,s(Y)) -> false
geq(s(X),s(Y)) -> geq(X,Y)
div(0,s(Y)) -> 0
div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)
if(true,X,Y) -> X
if(false,X,Y) -> 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 Ex49_GM04:

-> Dependency pairs:
nF_minus(s(X),s(Y)) -> nF_minus(X,Y)
nF_geq(s(X),s(Y)) -> nF_geq(X,Y)
nF_div(s(X),s(Y)) -> nF_if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)
nF_div(s(X),s(Y)) -> nF_geq(X,Y)
nF_div(s(X),s(Y)) -> nF_div(minus(X,Y),s(Y))
nF_div(s(X),s(Y)) -> nF_minus(X,Y)

-> Proof of termination for Ex49_GM04_1_1:
-> -> Dependency pairs in cycle:
nF_div(s(X),s(Y)) -> nF_div(minus(X,Y),s(Y))

UsableRules:
minus(0,Y) -> 0
minus(s(X),s(Y)) -> minus(X,Y)

Polynomial Interpretation:

[minus](X1,X2) = X1
[0] = 1
[s](X) = X + 1
[geq](X1,X2) = 0
[true] = 0
[false] = 0
[div](X1,X2) = 0
[if](X1,X2,X3) = 0
[nF_div](X1,X2) = X1

TIME: 4.4204e-2


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

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex49_GM04_1_3:
-> -> Dependency pairs in cycle:
nF_minus(s(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.