YES
The TRS could be proven terminating. The proof took 100 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (5ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (75ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(b) | → | a# | | f#(b) | → | f#(a) |
| a# | → | b# | | a# | → | U21#(b) |
Rewrite Rules
| b | → | c | | f(b) | → | f(a) |
| a | → | U21(b) | | U21(c) | → | c |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(b#) = μ(a#) = ∅
μ(f) = μ(f#) = μ(U21#) = μ(U21) = {1}
The following SCCs where found
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| b | → | c | | f(b) | → | f(a) |
| a | → | U21(b) | | U21(c) | → | c |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(b#) = μ(a#) = ∅
μ(f) = μ(f#) = μ(U21#) = μ(U21) = {1}
Polynomial Interpretation
- U21(x): 1
- a: 1
- b: 2
- c: 1
- f(x): 0
- f#(x): x
Standard Usable rules
| U21(c) | → | c | | b | → | c |
| a | → | U21(b) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed: