YES

The TRS could be proven terminating. The proof took 121 ms.

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (97ms).
 | – Problem 2 was processed with processor DependencyGraph (1ms).

Problem 1: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

if#(false, X, Y)activate#(Y)activate#(n__f(X))f#(X)
f#(X)if#(X, c, n__f(true))

Rewrite Rules

f(X)if(X, c, n__f(true))if(true, X, Y)X
if(false, X, Y)activate(Y)f(X)n__f(X)
activate(n__f(X))f(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: f, activate, c, if, true, false, n__f

Strategy


Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

if#(false, X, Y)activate#(Y)

Problem 2: DependencyGraph



Dependency Pair Problem

Dependency Pairs

activate#(n__f(X))f#(X)f#(X)if#(X, c, n__f(true))

Rewrite Rules

f(X)if(X, c, n__f(true))if(true, X, Y)X
if(false, X, Y)activate(Y)f(X)n__f(X)
activate(n__f(X))f(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, f, c, if, false, true, n__f

Strategy


There are no SCCs!