YES
(VAR y x z)
(RULES 
minus_active(0,y) -> 0
mark(0) -> 0
minus_active(s(x),s(y)) -> minus_active(x,y)
mark(s(x)) -> s(mark(x))
ge_active(x,0) -> true
mark(minus(x,y)) -> minus_active(x,y)
ge_active(0,s(y)) -> false
mark(ge(x,y)) -> ge_active(x,y)
ge_active(s(x),s(y)) -> ge_active(x,y)
mark(div(x,y)) -> div_active(mark(x),y)
div_active(0,s(y)) -> 0
mark(if(x,y,z)) -> if_active(mark(x),y,z)
div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
if_active(true,x,y) -> mark(x)
minus_active(x,y) -> minus(x,y)
if_active(false,x,y) -> mark(y)
ge_active(x,y) -> ge(x,y)
if_active(x,y,z) -> if(x,y,z)
div_active(x,y) -> div(x,y)
)

Proving termination of rewriting for JFP_Ex51:

-> Dependency pairs:
nF_minus_active(s(x),s(y)) -> nF_minus_active(x,y)
nF_mark(s(x)) -> nF_mark(x)
nF_mark(minus(x,y)) -> nF_minus_active(x,y)
nF_mark(ge(x,y)) -> nF_ge_active(x,y)
nF_ge_active(s(x),s(y)) -> nF_ge_active(x,y)
nF_mark(div(x,y)) -> nF_div_active(mark(x),y)
nF_mark(div(x,y)) -> nF_mark(x)
nF_mark(if(x,y,z)) -> nF_if_active(mark(x),y,z)
nF_mark(if(x,y,z)) -> nF_mark(x)
nF_div_active(s(x),s(y)) -> nF_if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
nF_div_active(s(x),s(y)) -> nF_ge_active(x,y)
nF_if_active(true,x,y) -> nF_mark(x)
nF_if_active(false,x,y) -> nF_mark(y)

-> Proof of termination for JFP_Ex51_1_1:
-> -> Dependency pairs in cycle:
nF_mark(s(x)) -> nF_mark(x)
nF_if_active(false,x,y) -> nF_mark(y)
nF_div_active(s(x),s(y)) -> nF_if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
nF_mark(div(x,y)) -> nF_div_active(mark(x),y)
nF_if_active(true,x,y) -> nF_mark(x)
nF_mark(if(x,y,z)) -> nF_if_active(mark(x),y,z)
nF_mark(if(x,y,z)) -> nF_mark(x)
nF_mark(div(x,y)) -> nF_mark(x)

UsableRules:
minus_active(0,y) -> 0
mark(0) -> 0
minus_active(s(x),s(y)) -> minus_active(x,y)
mark(s(x)) -> s(mark(x))
ge_active(x,0) -> true
mark(minus(x,y)) -> minus_active(x,y)
ge_active(0,s(y)) -> false
mark(ge(x,y)) -> ge_active(x,y)
ge_active(s(x),s(y)) -> ge_active(x,y)
mark(div(x,y)) -> div_active(mark(x),y)
div_active(0,s(y)) -> 0
mark(if(x,y,z)) -> if_active(mark(x),y,z)
div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
if_active(true,x,y) -> mark(x)
minus_active(x,y) -> minus(x,y)
if_active(false,x,y) -> mark(y)
ge_active(x,y) -> ge(x,y)
if_active(x,y,z) -> if(x,y,z)
div_active(x,y) -> div(x,y)

Polynomial Interpretation:

[minus_active](X1,X2) = X1
[0] = 0
[mark](X) = X
[s](X) = X
[ge_active](X1,X2) = 0
[true] = 0
[minus](X1,X2) = X1
[false] = 0
[ge](X1,X2) = 0
[div](X1,X2) = X1 + 1
[div_active](X1,X2) = X1 + 1
[if](X1,X2,X3) = X1 + X2 + X3
[if_active](X1,X2,X3) = X1 + X2 + X3
[nF_mark](X) = X
[nF_if_active](X1,X2,X3) = X2 + X3
[nF_div_active](X1,X2) = X1 + 1

TIME: 8.5591e-2

-> -> Dependency pairs in cycle:
nF_mark(s(x)) -> nF_mark(x)
nF_mark(if(x,y,z)) -> nF_mark(x)
nF_if_active(true,x,y) -> nF_mark(x)
nF_mark(if(x,y,z)) -> nF_if_active(mark(x),y,z)
nF_if_active(false,x,y) -> nF_mark(y)
nF_div_active(s(x),s(y)) -> nF_if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
nF_mark(div(x,y)) -> nF_div_active(mark(x),y)

UsableRules:
minus_active(0,y) -> 0
mark(0) -> 0
minus_active(s(x),s(y)) -> minus_active(x,y)
mark(s(x)) -> s(mark(x))
ge_active(x,0) -> true
mark(minus(x,y)) -> minus_active(x,y)
ge_active(0,s(y)) -> false
mark(ge(x,y)) -> ge_active(x,y)
ge_active(s(x),s(y)) -> ge_active(x,y)
mark(div(x,y)) -> div_active(mark(x),y)
div_active(0,s(y)) -> 0
mark(if(x,y,z)) -> if_active(mark(x),y,z)
div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
if_active(true,x,y) -> mark(x)
minus_active(x,y) -> minus(x,y)
if_active(false,x,y) -> mark(y)
ge_active(x,y) -> ge(x,y)
if_active(x,y,z) -> if(x,y,z)
div_active(x,y) -> div(x,y)

Polynomial Interpretation:

[minus_active](X1,X2) = 0
[0] = 0
[mark](X) = X + 1
[s](X) = X
[ge_active](X1,X2) = 0
[true] = 0
[minus](X1,X2) = 0
[false] = 0
[ge](X1,X2) = 0
[div](X1,X2) = 0
[div_active](X1,X2) = 1
[if](X1,X2,X3) = X1 + X2 + X3 + 1
[if_active](X1,X2,X3) = X1 + X2 + X3 + 1
[nF_mark](X) = X
[nF_if_active](X1,X2,X3) = X2 + X3
[nF_div_active](X1,X2) = 0

TIME: 7.2995e-2

-> -> Dependency pairs in cycle:
nF_mark(s(x)) -> nF_mark(x)
nF_if_active(false,x,y) -> nF_mark(y)
nF_div_active(s(x),s(y)) -> nF_if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
nF_mark(div(x,y)) -> nF_div_active(mark(x),y)
nF_if_active(true,x,y) -> nF_mark(x)
nF_mark(if(x,y,z)) -> nF_mark(x)

UsableRules:
minus_active(0,y) -> 0
mark(0) -> 0
minus_active(s(x),s(y)) -> minus_active(x,y)
mark(s(x)) -> s(mark(x))
ge_active(x,0) -> true
mark(minus(x,y)) -> minus_active(x,y)
ge_active(0,s(y)) -> false
mark(ge(x,y)) -> ge_active(x,y)
ge_active(s(x),s(y)) -> ge_active(x,y)
mark(div(x,y)) -> div_active(mark(x),y)
div_active(0,s(y)) -> 0
mark(if(x,y,z)) -> if_active(mark(x),y,z)
div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
if_active(true,x,y) -> mark(x)
minus_active(x,y) -> minus(x,y)
if_active(false,x,y) -> mark(y)
ge_active(x,y) -> ge(x,y)
if_active(x,y,z) -> if(x,y,z)
div_active(x,y) -> div(x,y)

Polynomial Interpretation:

[minus_active](X1,X2) = 1
[0] = 0
[mark](X) = X + 1
[s](X) = X
[ge_active](X1,X2) = 0
[true] = 0
[minus](X1,X2) = 1
[false] = 0
[ge](X1,X2) = 0
[div](X1,X2) = 0
[div_active](X1,X2) = 1
[if](X1,X2,X3) = X1 + X2 + X3 + 1
[if_active](X1,X2,X3) = X1 + X2 + X3 + 1
[nF_mark](X) = X
[nF_if_active](X1,X2,X3) = X2 + X3
[nF_div_active](X1,X2) = 0

TIME: 6.9018e-2

-> -> Dependency pairs in cycle:
nF_mark(s(x)) -> nF_mark(x)
nF_if_active(true,x,y) -> nF_mark(x)
nF_div_active(s(x),s(y)) -> nF_if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
nF_mark(div(x,y)) -> nF_div_active(mark(x),y)
nF_if_active(false,x,y) -> nF_mark(y)

UsableRules:
minus_active(0,y) -> 0
mark(0) -> 0
minus_active(s(x),s(y)) -> minus_active(x,y)
mark(s(x)) -> s(mark(x))
ge_active(x,0) -> true
mark(minus(x,y)) -> minus_active(x,y)
ge_active(0,s(y)) -> false
mark(ge(x,y)) -> ge_active(x,y)
ge_active(s(x),s(y)) -> ge_active(x,y)
mark(div(x,y)) -> div_active(mark(x),y)
div_active(0,s(y)) -> 0
mark(if(x,y,z)) -> if_active(mark(x),y,z)
div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
if_active(true,x,y) -> mark(x)
minus_active(x,y) -> minus(x,y)
if_active(false,x,y) -> mark(y)
ge_active(x,y) -> ge(x,y)
if_active(x,y,z) -> if(x,y,z)
div_active(x,y) -> div(x,y)

Polynomial Interpretation:

[minus_active](X1,X2) = 0
[0] = 0
[mark](X) = X
[s](X) = X + 1
[ge_active](X1,X2) = X2
[true] = 0
[minus](X1,X2) = 0
[false] = 0
[ge](X1,X2) = X2
[div](X1,X2) = X1 + X2
[div_active](X1,X2) = X1 + X2
[if](X1,X2,X3) = X2 + X3
[if_active](X1,X2,X3) = X2 + X3
[nF_mark](X) = X
[nF_if_active](X1,X2,X3) = X2 + X3
[nF_div_active](X1,X2) = X1 + X2

TIME: 7.252e-2

-> -> Dependency pairs in cycle:
nF_if_active(true,x,y) -> nF_mark(x)
nF_div_active(s(x),s(y)) -> nF_if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
nF_mark(div(x,y)) -> nF_div_active(mark(x),y)
nF_if_active(false,x,y) -> nF_mark(y)

UsableRules:
minus_active(0,y) -> 0
mark(0) -> 0
minus_active(s(x),s(y)) -> minus_active(x,y)
mark(s(x)) -> s(mark(x))
ge_active(x,0) -> true
mark(minus(x,y)) -> minus_active(x,y)
ge_active(0,s(y)) -> false
mark(ge(x,y)) -> ge_active(x,y)
ge_active(s(x),s(y)) -> ge_active(x,y)
mark(div(x,y)) -> div_active(mark(x),y)
div_active(0,s(y)) -> 0
mark(if(x,y,z)) -> if_active(mark(x),y,z)
div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
if_active(true,x,y) -> mark(x)
minus_active(x,y) -> minus(x,y)
if_active(false,x,y) -> mark(y)
ge_active(x,y) -> ge(x,y)
if_active(x,y,z) -> if(x,y,z)
div_active(x,y) -> div(x,y)

Polynomial Interpretation:

[minus_active](X1,X2) = 0
[0] = 0
[mark](X) = 1
[s](X) = 0
[ge_active](X1,X2) = 0
[true] = 0
[minus](X1,X2) = 0
[false] = 0
[ge](X1,X2) = 0
[div](X1,X2) = 1
[div_active](X1,X2) = 1
[if](X1,X2,X3) = 0
[if_active](X1,X2,X3) = 1
[nF_if_active](X1,X2,X3) = X2 + X3 + 1
[nF_div_active](X1,X2) = 1
[nF_mark](X) = X

TIME: 7.8365e-2

-> -> Dependency pairs in cycle:
nF_if_active(true,x,y) -> nF_mark(x)
nF_div_active(s(x),s(y)) -> nF_if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
nF_mark(div(x,y)) -> nF_div_active(mark(x),y)

UsableRules:
minus_active(0,y) -> 0
mark(0) -> 0
minus_active(s(x),s(y)) -> minus_active(x,y)
mark(s(x)) -> s(mark(x))
ge_active(x,0) -> true
mark(minus(x,y)) -> minus_active(x,y)
ge_active(0,s(y)) -> false
mark(ge(x,y)) -> ge_active(x,y)
ge_active(s(x),s(y)) -> ge_active(x,y)
mark(div(x,y)) -> div_active(mark(x),y)
div_active(0,s(y)) -> 0
mark(if(x,y,z)) -> if_active(mark(x),y,z)
div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
if_active(true,x,y) -> mark(x)
minus_active(x,y) -> minus(x,y)
if_active(false,x,y) -> mark(y)
ge_active(x,y) -> ge(x,y)
if_active(x,y,z) -> if(x,y,z)
div_active(x,y) -> div(x,y)

Polynomial Interpretation:

[minus_active](X1,X2) = 1
[0] = 1
[mark](X) = X
[s](X) = 1
[ge_active](X1,X2) = 0
[true] = 0
[minus](X1,X2) = 1
[false] = 0
[ge](X1,X2) = 0
[div](X1,X2) = X2 + 1
[div_active](X1,X2) = X2 + 1
[if](X1,X2,X3) = X2 + X3
[if_active](X1,X2,X3) = X2 + X3
[nF_if_active](X1,X2,X3) = X2
[nF_div_active](X1,X2) = X2
[nF_mark](X) = X

TIME: 7.1559e-2


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

Termination proved: Cycles verify subterm criterion.

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