The TRS could be proven terminating. The proof took 165 ms.
Problem 1 was processed with processor PolynomialLinearRange4 (126ms). | – Problem 2 was processed with processor DependencyGraph (1ms).
| if#(false, X, Y) | → | T(Y) | f#(X) | → | if#(X, c, f(true)) | |
| T(f(true)) | → | f#(true) |
| f(X) | → | if(X, c, f(true)) | if(true, X, Y) | → | X | |
| if(false, X, Y) | → | Y |
Termination of terms over the following signature is verified: f, c, if, true, false
Context-sensitive strategy:
μ(T) = μ(c) = μ(false) = μ(true) = ∅
μ(f) = μ(f#) = {1}
μ(if) = μ(if#) = {1, 2}
| if(false, X, Y) | → | Y | if(true, X, Y) | → | X | |
| f(X) | → | if(X, c, f(true)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(f(true)) | → | f#(true) |
| if#(false, X, Y) | → | T(Y) | f#(X) | → | if#(X, c, f(true)) |
| f(X) | → | if(X, c, f(true)) | if(true, X, Y) | → | X | |
| if(false, X, Y) | → | Y |
Termination of terms over the following signature is verified: f, c, if, false, true
Context-sensitive strategy:
μ(T) = μ(c) = μ(true) = μ(false) = ∅
μ(f) = μ(f#) = {1}
μ(if) = μ(if#) = {1, 2}