YES
(VAR y x z)
(RULES 
div(0,y) -> 0
div(x,y) -> quot(x,y,y)
quot(0,s(y),z) -> 0
quot(s(x),s(y),z) -> quot(x,y,z)
quot(x,0,s(z)) -> s(div(x,s(z)))
)

Proving termination of rewriting for IJCAR_1:

-> Dependency pairs:
nF_div(x,y) -> nF_quot(x,y,y)
nF_quot(s(x),s(y),z) -> nF_quot(x,y,z)
nF_quot(x,0,s(z)) -> nF_div(x,s(z))

-> Proof of termination for IJCAR_1_1:
-> -> Dependency pairs in cycle:
nF_div(x,y) -> nF_quot(x,y,y)
nF_quot(x,0,s(z)) -> nF_div(x,s(z))
nF_quot(s(x),s(y),z) -> nF_quot(x,y,z)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_div(x,y) -> nF_quot(x,y,y)
nF_quot(x,0,s(z)) -> nF_div(x,s(z))

There are no usable rules.

Polynomial Interpretation:

[div](X1,X2) = 0
[0] = 1
[quot](X1,X2,X3) = 0
[s](X) = 0
[nF_div](X1,X2) = X2
[nF_quot](X1,X2,X3) = X2

TIME: 5.4796e-2


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.