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