YES
The TRS could be proven terminating. The proof took 157 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (12ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (123ms).
| | – Problem 3 was processed with processor DependencyGraph (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(f(X)) | → | c#(n__f(g(n__f(X)))) | | activate#(n__d(X)) | → | d#(X) |
| activate#(n__f(X)) | → | f#(X) | | h#(X) | → | c#(n__d(X)) |
| c#(X) | → | d#(activate(X)) | | c#(X) | → | activate#(X) |
Rewrite Rules
| f(f(X)) | → | c(n__f(g(n__f(X)))) | | c(X) | → | d(activate(X)) |
| h(X) | → | c(n__d(X)) | | f(X) | → | n__f(X) |
| d(X) | → | n__d(X) | | activate(n__f(X)) | → | f(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
Strategy
The following SCCs where found
| f#(f(X)) → c#(n__f(g(n__f(X)))) | activate#(n__f(X)) → f#(X) |
| c#(X) → activate#(X) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(f(X)) | → | c#(n__f(g(n__f(X)))) | | activate#(n__f(X)) | → | f#(X) |
| c#(X) | → | activate#(X) |
Rewrite Rules
| f(f(X)) | → | c(n__f(g(n__f(X)))) | | c(X) | → | d(activate(X)) |
| h(X) | → | c(n__d(X)) | | f(X) | → | n__f(X) |
| d(X) | → | n__d(X) | | activate(n__f(X)) | → | f(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
Strategy
Polynomial Interpretation
- activate(x): 0
- activate#(x): 2x
- c(x): 0
- c#(x): 2x
- d(x): 0
- f(x): 1
- f#(x): 2x
- g(x): 0
- h(x): 0
- n__d(x): 0
- n__f(x): 2x
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(f(X)) | → | c#(n__f(g(n__f(X)))) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| activate#(n__f(X)) | → | f#(X) | | c#(X) | → | activate#(X) |
Rewrite Rules
| f(f(X)) | → | c(n__f(g(n__f(X)))) | | c(X) | → | d(activate(X)) |
| h(X) | → | c(n__d(X)) | | f(X) | → | n__f(X) |
| d(X) | → | n__d(X) | | activate(n__f(X)) | → | f(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
Strategy
There are no SCCs!