YES
The TRS could be proven terminating. The proof took 4289 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (165ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (425ms).
| | – Problem 5 was processed with processor BackwardsNarrowing (4ms).
| | | – Problem 10 was processed with processor ForwardNarrowing (2ms).
| | | – Problem 11 was processed with processor BackwardsNarrowing (2ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (422ms).
| | – Problem 6 was processed with processor PolynomialLinearRange4 (200ms).
| | | – Problem 8 was processed with processor PolynomialLinearRange4 (8ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (278ms).
| | – Problem 7 was processed with processor PolynomialLinearRange4 (190ms).
| | | – Problem 9 was processed with processor BackwardsNarrowing (0ms).
| | | | – Problem 12 was processed with processor ForwardNarrowing (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| g_0#(f_1(f_0(g_0(x)))) | → | T(x) | | g_0#(f_1(f_0(g_0(x)))) | → | g_0#(x) |
| *top*_0#(f_0(f_1(f_0(g_0(x))))) | → | T(x) | | f_0#(f_1(f_0(g_0(x)))) | → | f_1#(x) |
| g_0#(f_0(f_1(f_0(g_0(x))))) | → | T(x) | | T(f_0(x)) | → | f_0#(x) |
| g_0#(g_1(b_0)) | → | f_0#(g_1(b_0)) | | T(f_0(g_1(b_0))) | → | f_0#(g_1(b_0)) |
| f_0#(f_0(f_1(f_0(g_0(x))))) | → | f_1#(f_0(x)) | | *top*_0#(g_1(b_0)) | → | f_0#(g_1(b_0)) |
| T(f_0(x_1)) | → | T(x_1) | | f_0#(f_1(f_0(g_1(x)))) | → | f_0#(x) |
| g_0#(f_0(f_1(f_0(g_0(x))))) | → | g_0#(f_0(x)) | | g_0#(f_0(f_1(f_0(g_0(x))))) | → | f_0#(x) |
| *top*_0#(f_1(f_0(g_0(x)))) | → | T(x) | | *top*_0#(f_1(f_0(g_0(x)))) | → | *top*_0#(x) |
| *top*_0#(f_0(f_1(f_0(g_0(x))))) | → | f_0#(x) | | f_1#(f_0(g_0(x))) | → | T(x) |
| *top*_0#(f_1(f_0(g_1(x)))) | → | T(x) | | *top*_0#(f_1(f_0(g_1(x)))) | → | *top*_0#(x) |
| g_0#(g_1(b_0)) | → | g_0#(f_0(g_1(b_0))) | | *top*_0#(f_0(f_1(f_0(g_0(x))))) | → | *top*_0#(f_0(x)) |
| f_0#(f_1(f_0(g_1(x)))) | → | T(x) | | f_0#(g_1(b_0)) | → | f_1#(f_0(g_1(b_0))) |
| *top*_0#(g_1(b_0)) | → | *top*_0#(f_0(g_1(b_0))) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, *top*_0, g_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0#) = μ(*top*_0) = μ(g_0) = μ(f_0#) = μ(*top*_0#) = {1}
The following SCCs where found
| *top*_0#(f_1(f_0(g_1(x)))) → *top*_0#(x) | *top*_0#(f_0(f_1(f_0(g_0(x))))) → *top*_0#(f_0(x)) |
| *top*_0#(f_1(f_0(g_0(x)))) → *top*_0#(x) | *top*_0#(g_1(b_0)) → *top*_0#(f_0(g_1(b_0))) |
| f_0#(f_1(f_0(g_1(x)))) → f_0#(x) | f_0#(f_0(f_1(f_0(g_0(x))))) → f_1#(f_0(x)) |
| f_0#(f_1(f_0(g_1(x)))) → T(x) | f_0#(f_1(f_0(g_0(x)))) → f_1#(x) |
| f_1#(f_0(g_0(x))) → T(x) | T(f_0(x)) → f_0#(x) |
| T(f_0(x_1)) → T(x_1) |
| g_0#(f_0(f_1(f_0(g_0(x))))) → g_0#(f_0(x)) | g_0#(f_1(f_0(g_0(x)))) → g_0#(x) |
| g_0#(g_1(b_0)) → g_0#(f_0(g_1(b_0))) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| g_0#(f_0(f_1(f_0(g_0(x))))) | → | g_0#(f_0(x)) | | g_0#(f_1(f_0(g_0(x)))) | → | g_0#(x) |
| g_0#(g_1(b_0)) | → | g_0#(f_0(g_1(b_0))) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, *top*_0, g_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0) = μ(*top*_0) = μ(g_0#) = μ(*top*_0#) = μ(f_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- b_0: 0
- f_0(x): x
- f_1(x): 2x
- g_0(x): x + 1
- g_0#(x): x
- g_1(x): 2x
Standard Usable rules
| *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) | | f_0(f_1(f_0(g_0(x)))) | → | f_1(x) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) | | g_0(f_1(f_0(g_1(x)))) | → | g_1(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) |
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| f_1(f_0(g_0(x))) | → | x | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| g_0#(f_0(f_1(f_0(g_0(x))))) | → | g_0#(f_0(x)) | | g_0#(f_1(f_0(g_0(x)))) | → | g_0#(x) |
Problem 5: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| g_0#(g_1(b_0)) | → | g_0#(f_0(g_1(b_0))) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, g_0, *top*_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0#) = μ(*top*_0) = μ(g_0) = μ(f_0#) = μ(*top*_0#) = {1}
The left-hand side of the rule g_0
#(g_1(b_0)) → g_0
#(f_0(g_1(b_0))) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| g_0#(f_1(f_0(g_0(g_1(b_0))))) | |
| g_0#(g_0(f_1(f_0(g_1(b_0))))) | |
Thus, the rule g_0
#(g_1(b_0)) → g_0
#(f_0(g_1(b_0))) is replaced by the following rules:
| g_0#(g_0(f_1(f_0(g_1(b_0))))) → g_0#(f_0(g_1(b_0))) | g_0#(f_1(f_0(g_0(g_1(b_0))))) → g_0#(f_0(g_1(b_0))) |
Problem 10: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g_0#(g_1(b_0)) | → | g_0#(f_1(f_0(g_1(b_0)))) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, *top*_0, g_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0) = μ(*top*_0) = μ(g_0#) = μ(*top*_0#) = μ(f_0#) = {1}
The right-hand side of the rule g_0
#(g_1(b_0)) → g_0
#(f_1(f_0(g_1(b_0)))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule g_0
#(g_1(b_0)) → g_0
#(f_1(f_0(g_1(b_0)))) is deleted.
Problem 11: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| g_0#(g_0(f_1(f_0(g_1(b_0))))) | → | g_0#(f_0(g_1(b_0))) | | g_0#(f_1(f_0(g_0(g_1(b_0))))) | → | g_0#(f_0(g_1(b_0))) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, *top*_0, g_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0) = μ(*top*_0) = μ(g_0#) = μ(*top*_0#) = μ(f_0#) = {1}
The left-hand side of the rule g_0
#(g_0(f_1(f_0(g_1(b_0))))) → g_0
#(f_0(g_1(b_0))) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| g_0#(f_1(f_0(g_0(g_0(f_1(f_0(g_1(b_0)))))))) | |
| g_0#(g_0(f_0(g_1(b_0)))) | |
| g_0#(g_0(f_0(f_0(f_1(f_0(g_0(g_1(b_0)))))))) | |
| g_0#(g_0(f_1(f_0(g_0(f_1(f_0(g_1(b_0)))))))) | |
| g_0#(g_0(f_0(f_1(f_0(g_0(f_0(g_1(b_0)))))))) | |
Thus, the rule g_0
#(g_0(f_1(f_0(g_1(b_0))))) → g_0
#(f_0(g_1(b_0))) is replaced by the following rules:
| g_0#(g_0(f_1(f_0(g_0(f_1(f_0(g_1(b_0)))))))) → g_0#(f_0(g_1(b_0))) | g_0#(g_0(f_0(f_0(f_1(f_0(g_0(g_1(b_0)))))))) → g_0#(f_0(g_1(b_0))) |
| g_0#(g_0(f_0(f_1(f_0(g_0(f_0(g_1(b_0)))))))) → g_0#(f_0(g_1(b_0))) | g_0#(g_0(f_0(g_1(b_0)))) → g_0#(f_0(g_1(b_0))) |
| g_0#(f_1(f_0(g_0(g_0(f_1(f_0(g_1(b_0)))))))) → g_0#(f_0(g_1(b_0))) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| f_0#(f_1(f_0(g_1(x)))) | → | f_0#(x) | | f_0#(f_0(f_1(f_0(g_0(x))))) | → | f_1#(f_0(x)) |
| f_0#(f_1(f_0(g_1(x)))) | → | T(x) | | f_0#(f_1(f_0(g_0(x)))) | → | f_1#(x) |
| f_1#(f_0(g_0(x))) | → | T(x) | | T(f_0(x)) | → | f_0#(x) |
| T(f_0(x_1)) | → | T(x_1) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, *top*_0, g_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0) = μ(*top*_0) = μ(g_0#) = μ(*top*_0#) = μ(f_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 1
- T(x): 2x
- b_0: 0
- f_0(x): x
- f_0#(x): 2x
- f_1(x): x
- f_1#(x): 2x
- g_0(x): 2x
- g_1(x): 2x + 1
Standard Usable rules
| *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) | | f_0(f_1(f_0(g_0(x)))) | → | f_1(x) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) | | g_0(f_1(f_0(g_1(x)))) | → | g_1(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) |
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| f_1(f_0(g_0(x))) | → | x | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f_0#(f_1(f_0(g_1(x)))) | → | f_0#(x) | | f_0#(f_1(f_0(g_1(x)))) | → | T(x) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| f_0#(f_0(f_1(f_0(g_0(x))))) | → | f_1#(f_0(x)) | | f_0#(f_1(f_0(g_0(x)))) | → | f_1#(x) |
| f_1#(f_0(g_0(x))) | → | T(x) | | T(f_0(x_1)) | → | T(x_1) |
| T(f_0(x)) | → | f_0#(x) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, g_0, *top*_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0#) = μ(*top*_0) = μ(g_0) = μ(f_0#) = μ(*top*_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 1
- T(x): x + 1
- b_0: 0
- f_0(x): x
- f_0#(x): x
- f_1(x): 2x
- f_1#(x): x + 1
- g_0(x): x + 1
- g_1(x): 2x
Standard Usable rules
| *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) | | f_0(f_1(f_0(g_0(x)))) | → | f_1(x) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) | | g_0(f_1(f_0(g_1(x)))) | → | g_1(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) |
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| f_1(f_0(g_0(x))) | → | x | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f_0#(f_0(f_1(f_0(g_0(x))))) | → | f_1#(f_0(x)) | | f_0#(f_1(f_0(g_0(x)))) | → | f_1#(x) |
| f_1#(f_0(g_0(x))) | → | T(x) | | T(f_0(x)) | → | f_0#(x) |
Problem 8: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, *top*_0, g_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0) = μ(*top*_0) = μ(g_0#) = μ(*top*_0#) = μ(f_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- T(x): x + 1
- b_0: 0
- f_0(x): x + 2
- f_1(x): 0
- g_0(x): 0
- g_1(x): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| *top*_0#(f_1(f_0(g_1(x)))) | → | *top*_0#(x) | | *top*_0#(f_0(f_1(f_0(g_0(x))))) | → | *top*_0#(f_0(x)) |
| *top*_0#(f_1(f_0(g_0(x)))) | → | *top*_0#(x) | | *top*_0#(g_1(b_0)) | → | *top*_0#(f_0(g_1(b_0))) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, *top*_0, g_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0) = μ(*top*_0) = μ(g_0#) = μ(*top*_0#) = μ(f_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 1
- *top*_0#(x): x
- b_0: 0
- f_0(x): x
- f_1(x): x
- g_0(x): x
- g_1(x): 2x + 2
Standard Usable rules
| *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) | | f_0(f_1(f_0(g_0(x)))) | → | f_1(x) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) | | g_0(f_1(f_0(g_1(x)))) | → | g_1(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) |
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| f_1(f_0(g_0(x))) | → | x | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| *top*_0#(f_1(f_0(g_1(x)))) | → | *top*_0#(x) |
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| *top*_0#(f_0(f_1(f_0(g_0(x))))) | → | *top*_0#(f_0(x)) | | *top*_0#(f_1(f_0(g_0(x)))) | → | *top*_0#(x) |
| *top*_0#(g_1(b_0)) | → | *top*_0#(f_0(g_1(b_0))) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, g_0, *top*_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0#) = μ(*top*_0) = μ(g_0) = μ(f_0#) = μ(*top*_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 1
- *top*_0#(x): 2x
- b_0: 0
- f_0(x): x
- f_1(x): x
- g_0(x): x + 1
- g_1(x): 2x
Standard Usable rules
| *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) | | f_0(f_1(f_0(g_0(x)))) | → | f_1(x) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) | | g_0(f_1(f_0(g_1(x)))) | → | g_1(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) |
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| f_1(f_0(g_0(x))) | → | x | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| *top*_0#(f_0(f_1(f_0(g_0(x))))) | → | *top*_0#(f_0(x)) | | *top*_0#(f_1(f_0(g_0(x)))) | → | *top*_0#(x) |
Problem 9: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| *top*_0#(g_1(b_0)) | → | *top*_0#(f_0(g_1(b_0))) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, *top*_0, g_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0) = μ(*top*_0) = μ(g_0#) = μ(*top*_0#) = μ(f_0#) = {1}
The left-hand side of the rule *top*_0
#(g_1(b_0)) → *top*_0
#(f_0(g_1(b_0))) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| *top*_0#(g_0(f_1(f_0(g_1(b_0))))) | |
| *top*_0#(f_1(f_0(g_0(g_1(b_0))))) | |
Thus, the rule *top*_0
#(g_1(b_0)) → *top*_0
#(f_0(g_1(b_0))) is replaced by the following rules:
| *top*_0#(g_0(f_1(f_0(g_1(b_0))))) → *top*_0#(f_0(g_1(b_0))) | *top*_0#(f_1(f_0(g_0(g_1(b_0))))) → *top*_0#(f_0(g_1(b_0))) |
Problem 12: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *top*_0#(g_1(b_0)) | → | *top*_0#(f_1(f_0(g_1(b_0)))) |
Rewrite Rules
| *top*_0(f_1(f_0(g_1(x)))) | → | *top*_0(x) | | f_0(f_1(f_0(g_1(x)))) | → | f_0(x) |
| g_0(f_1(f_0(g_1(x)))) | → | g_1(x) | | *top*_0(f_0(f_1(f_0(g_0(x))))) | → | *top*_0(f_0(x)) |
| f_0(f_0(f_1(f_0(g_0(x))))) | → | f_1(f_0(x)) | | g_0(f_0(f_1(f_0(g_0(x))))) | → | g_0(f_0(x)) |
| f_1(f_0(g_0(x))) | → | x | | *top*_0(f_1(f_0(g_0(x)))) | → | *top*_0(x) |
| f_0(f_1(f_0(g_0(x)))) | → | f_1(x) | | g_0(f_1(f_0(g_0(x)))) | → | g_0(x) |
| *top*_0(g_1(b_0)) | → | *top*_0(f_0(g_1(b_0))) | | f_0(g_1(b_0)) | → | f_1(f_0(g_1(b_0))) |
| g_0(g_1(b_0)) | → | g_0(f_0(g_1(b_0))) |
Original Signature
Termination of terms over the following signature is verified: f_0, g_0, *top*_0, g_1, b_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(g_0#) = μ(*top*_0) = μ(g_0) = μ(f_0#) = μ(*top*_0#) = {1}
The right-hand side of the rule *top*_0
#(g_1(b_0)) → *top*_0
#(f_1(f_0(g_1(b_0)))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule *top*_0
#(g_1(b_0)) → *top*_0
#(f_1(f_0(g_1(b_0)))) is deleted.