(VAR Y X)
(STRATEGY CONTEXTSENSITIVE 
  (minus)
  (0)
  (s 1)
  (geq)
  (true)
  (false)
  (div 1)
  (if 1)
)
(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 orthogonal, thus termination of innermost context-sensitive rewriting is equivalent to termination of context-sensitive rewriting.

Proving termination of context-sensitive 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_if(true,X,Y) -> X
nF_if(false,X,Y) -> Y

-> Proof of termination for Ex49_GM04_1_1:
-> -> Dependency pairs in cycle:
nF_div(s(X),s(Y)) -> nF_if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)
nF_if(false,X,Y) -> Y
nF_if(true,X,Y) -> X

Usable 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

Polynomial Interpretation:

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

TIME: 3.892e-3


-> 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 CSDG + base ordering
Upper bound for coeffs: 2
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.