The TRS could be proven terminating. The proof took 121 ms.
Problem 1 was processed with processor PolynomialLinearRange4iUR (97ms). | – Problem 2 was processed with processor DependencyGraph (1ms).
| if#(false, X, Y) | → | activate#(Y) | activate#(n__f(X)) | → | f#(X) | |
| f#(X) | → | if#(X, c, n__f(true)) |
| 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 |
Termination of terms over the following signature is verified: f, activate, c, if, true, false, n__f
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) |
| activate#(n__f(X)) | → | f#(X) | f#(X) | → | if#(X, c, n__f(true)) |
| 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 |
Termination of terms over the following signature is verified: activate, f, c, if, false, true, n__f