YES
The TRS could be proven terminating. The proof took 645 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (9ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (205ms).
| | – Problem 3 was processed with processor PolynomialLinearRange4iUR (137ms).
| | | – Problem 4 was processed with processor DependencyGraph (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if#(false, X, Y) | → | activate#(Y) | | activate#(n__f(X)) | → | f#(activate(X)) |
| f#(X) | → | if#(X, c, n__f(n__true)) | | activate#(n__f(X)) | → | activate#(X) |
| activate#(n__true) | → | true# |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: f, activate, c, if, true, false, n__true, n__f
Strategy
The following SCCs where found
| if#(false, X, Y) → activate#(Y) | activate#(n__f(X)) → f#(activate(X)) |
| f#(X) → if#(X, c, n__f(n__true)) | activate#(n__f(X)) → activate#(X) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| if#(false, X, Y) | → | activate#(Y) | | activate#(n__f(X)) | → | f#(activate(X)) |
| f#(X) | → | if#(X, c, n__f(n__true)) | | activate#(n__f(X)) | → | activate#(X) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: f, activate, c, if, true, false, n__true, n__f
Strategy
Polynomial Interpretation
- activate(x): 0
- activate#(x): x + 1
- c: 0
- f(x): 3x + 3
- f#(x): 2
- false: 1
- if(x,y,z): z
- if#(x,y,z): z + 3y + 1
- n__f(x): 2x + 1
- n__true: 0
- true: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| activate#(n__f(X)) | → | activate#(X) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| activate#(n__f(X)) | → | f#(activate(X)) | | if#(false, X, Y) | → | activate#(Y) |
| f#(X) | → | if#(X, c, n__f(n__true)) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: activate, f, c, if, false, true, n__true, n__f
Strategy
Polynomial Interpretation
- activate(x): 2x
- activate#(x): x
- c: 0
- f(x): 3x
- f#(x): x
- false: 2
- if(x,y,z): 2z + 2y
- if#(x,y,z): 2z + x
- n__f(x): 3x
- n__true: 0
- true: 0
Improved Usable rules
| activate(X) | → | X | | f(X) | → | if(X, c, n__f(n__true)) |
| if(false, X, Y) | → | activate(Y) | | activate(n__f(X)) | → | f(activate(X)) |
| f(X) | → | n__f(X) | | if(true, X, Y) | → | X |
| true | → | n__true | | activate(n__true) | → | true |
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 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| activate#(n__f(X)) | → | f#(activate(X)) | | f#(X) | → | if#(X, c, n__f(n__true)) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: f, activate, c, if, true, false, n__true, n__f
Strategy
There are no SCCs!