YES
(VAR Y X)
(RULES 
plus(0,Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
min(X,0) -> X
min(s(X),s(Y)) -> min(X,Y)
min(min(X,Y),Z) -> min(X,plus(Y,Z))
quot(0,s(Y)) -> 0
quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
)

Proving termination of rewriting for quotminus:

-> Dependency pairs:
nF_plus(s(X),Y) -> nF_plus(X,Y)
nF_min(s(X),s(Y)) -> nF_min(X,Y)
nF_min(min(X,Y),Z) -> nF_min(X,plus(Y,Z))
nF_min(min(X,Y),Z) -> nF_plus(Y,Z)
nF_quot(s(X),s(Y)) -> nF_quot(min(X,Y),s(Y))
nF_quot(s(X),s(Y)) -> nF_min(X,Y)

-> Proof of termination for quotminus_1_1:
-> -> Dependency pairs in cycle:
nF_quot(s(X),s(Y)) -> nF_quot(min(X,Y),s(Y))

UsableRules:
plus(0,Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
min(X,0) -> X
min(s(X),s(Y)) -> min(X,Y)
min(min(X,Y),Z) -> min(X,plus(Y,Z))

Polynomial Interpretation:

[plus](X1,X2) = X1 + X2
[0] = 0
[s](X) = X + 1
[min](X1,X2) = X1
[Z] = 0
[quot](X1,X2) = 0
[nF_quot](X1,X2) = X1

TIME: 0.10421


-> Proof of termination for quotminus_1_2:
-> -> Dependency pairs in cycle:
nF_min(s(X),s(Y)) -> nF_min(X,Y)
nF_min(min(X,Y),Z) -> nF_min(X,plus(Y,Z))

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for quotminus_1_3:
-> -> Dependency pairs in cycle:
nF_plus(s(X),Y) -> nF_plus(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.