YES
(VAR X Y Z)
(RULES 
div(X,e) -> i(X)
i(div(X,Y)) -> div(Y,X)
div(div(X,Y),Z) -> div(Y,div(i(X),Z))
)

Proving termination of rewriting for lescanne:

-> Dependency pairs:
nF_div(X,e) -> nF_i(X)
nF_i(div(X,Y)) -> nF_div(Y,X)
nF_div(div(X,Y),Z) -> nF_div(Y,div(i(X),Z))
nF_div(div(X,Y),Z) -> nF_div(i(X),Z)
nF_div(div(X,Y),Z) -> nF_i(X)

-> Proof of termination for lescanne_1:
-> -> Dependency pairs in cycle:
nF_div(X,e) -> nF_i(X)
nF_div(div(X,Y),Z) -> nF_div(i(X),Z)
nF_div(div(X,Y),Z) -> nF_div(Y,div(i(X),Z))
nF_i(div(X,Y)) -> nF_div(Y,X)
nF_div(div(X,Y),Z) -> nF_i(X)

UsableRules:
div(X,e) -> i(X)
i(div(X,Y)) -> div(Y,X)
div(div(X,Y),Z) -> div(Y,div(i(X),Z))

Polynomial Interpretation:

[div](X1,X2) = X1 + X2 + 1
[e] = 0
[i](X) = X
[nF_div](X1,X2) = X1
[nF_i](X) = X

TIME: 4.0845e-2

-> -> Dependency pairs in cycle:
nF_div(X,e) -> nF_i(X)
nF_i(div(X,Y)) -> nF_div(Y,X)
nF_div(div(X,Y),Z) -> nF_div(Y,div(i(X),Z))
nF_div(div(X,Y),Z) -> nF_div(i(X),Z)

UsableRules:
div(X,e) -> i(X)
i(div(X,Y)) -> div(Y,X)
div(div(X,Y),Z) -> div(Y,div(i(X),Z))

Polynomial Interpretation:

[div](X1,X2) = X1 + X2 + 1
[e] = 1
[i](X) = X
[nF_div](X1,X2) = X1 + X2
[nF_i](X) = X

TIME: 3.8641e-2

-> -> Dependency pairs in cycle:
nF_div(X,e) -> nF_i(X)
nF_div(div(X,Y),Z) -> nF_div(Y,div(i(X),Z))
nF_i(div(X,Y)) -> nF_div(Y,X)

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.