YES
(VAR x y)
(RULES 
-(x,0) -> x
-(0,s(y)) -> 0
-(s(x),s(y)) -> -(x,y)
lt(x,0) -> false
lt(0,s(y)) -> true
lt(s(x),s(y)) -> lt(x,y)
if(true,x,y) -> x
if(false,x,y) -> y
div(x,0) -> 0
div(0,y) -> 0
div(s(x),s(y)) -> if(lt(x,y),0,s(div(-(x,y),s(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 t014:

-> Dependency pairs:
nF_-(s(x),s(y)) -> nF_-(x,y)
nF_lt(s(x),s(y)) -> nF_lt(x,y)
nF_div(s(x),s(y)) -> nF_if(lt(x,y),0,s(div(-(x,y),s(y))))
nF_div(s(x),s(y)) -> nF_lt(x,y)
nF_div(s(x),s(y)) -> nF_div(-(x,y),s(y))
nF_div(s(x),s(y)) -> nF_-(x,y)

-> Proof of termination for t014_1_1:
-> -> Dependency pairs in cycle:
nF_div(s(x),s(y)) -> nF_div(-(x,y),s(y))

UsableRules:
-(x,0) -> x
-(0,s(y)) -> 0
-(s(x),s(y)) -> -(x,y)

Polynomial Interpretation:

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

TIME: 3.9316e-2


-> Proof of termination for t014_1_2:
-> -> Dependency pairs in cycle:
nF_lt(s(x),s(y)) -> nF_lt(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for t014_1_3:
-> -> Dependency pairs in cycle:
nF_-(s(x),s(y)) -> nF_-(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.