YES
(VAR X Y)
(RULES 
f(X) -> if(X,c,n__f(n__true))
if(true,X,Y) -> X
if(false,X,Y) -> activate(Y)
f(X) -> n__f(X)
true -> n__true
activate(n__f(X)) -> f(activate(X))
activate(n__true) -> true
activate(X) -> X
)

Proving termination of rewriting for Ex5_Zan97_FR:

-> Dependency pairs:
nF_f(X) -> nF_if(X,c,n__f(n__true))
nF_if(false,X,Y) -> nF_activate(Y)
nF_activate(n__f(X)) -> nF_f(activate(X))
nF_activate(n__f(X)) -> nF_activate(X)
nF_activate(n__true) -> nF_true

-> Proof of termination for Ex5_Zan97_FR_1:
-> -> Dependency pairs in cycle:
nF_f(X) -> nF_if(X,c,n__f(n__true))
nF_activate(n__f(X)) -> nF_f(activate(X))
nF_activate(n__f(X)) -> nF_activate(X)
nF_if(false,X,Y) -> nF_activate(Y)

UsableRules:
f(X) -> if(X,c,n__f(n__true))
if(true,X,Y) -> X
if(false,X,Y) -> activate(Y)
f(X) -> n__f(X)
true -> n__true
activate(n__f(X)) -> f(activate(X))
activate(n__true) -> true
activate(X) -> X

Polynomial Interpretation:

[f](X) = X
[if](X1,X2,X3) = X2 + X3
[c] = 0
[n__f](X) = X
[n__true] = 0
[true] = 0
[false] = 1
[activate](X) = X
[nF_f](X) = X
[nF_activate](X) = X
[nF_if](X1,X2,X3) = X1 + X3

TIME: 5.529499999999998e-2

-> -> Dependency pairs in cycle:
nF_activate(n__f(X)) -> nF_activate(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.