YES
The TRS could be proven terminating. The proof took 2147 ms.
The following DP Processors were used
Problem 1 was processed with processor PolynomialLinearRange4iUR (737ms).
| – Problem 2 was processed with processor PolynomialOrderingProcessor (764ms).
| | – Problem 3 was processed with processor DependencyGraph (1ms).
| | | – Problem 4 was processed with processor PolynomialOrderingProcessor (25ms).
Problem 1: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| 1#(1(x)) | → | 0#(x) | | 1#(0(x)) | → | 0#(0(0(1(x)))) |
| 1#(0(x)) | → | 1#(x) | | 0#(1(x)) | → | 1#(x) |
| 1#(1(x)) | → | 0#(0(x)) | | 1#(0(x)) | → | 0#(1(x)) |
| 1#(1(x)) | → | 0#(0(0(0(x)))) | | 1#(0(x)) | → | 0#(0(1(x))) |
| 1#(1(x)) | → | 0#(0(0(x))) | | 0#(0(x)) | → | 0#(x) |
Rewrite Rules
| 1(0(x)) | → | 0(0(0(1(x)))) | | 0(1(x)) | → | 1(x) |
| 1(1(x)) | → | 0(0(0(0(x)))) | | 0(0(x)) | → | 0(x) |
Original Signature
Termination of terms over the following signature is verified: 1, 0
Strategy
Polynomial Interpretation
- 0(x): x
- 0#(x): x
- 1(x): 2x + 1
- 1#(x): 2x + 1
Improved Usable rules
| 1(0(x)) | → | 0(0(0(1(x)))) | | 0(1(x)) | → | 1(x) |
| 0(0(x)) | → | 0(x) | | 1(1(x)) | → | 0(0(0(0(x)))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| 1#(1(x)) | → | 0#(x) | | 1#(1(x)) | → | 0#(0(x)) |
| 1#(1(x)) | → | 0#(0(0(0(x)))) | | 1#(1(x)) | → | 0#(0(0(x))) |
Problem 2: PolynomialOrderingProcessor
Dependency Pair Problem
Dependency Pairs
| 0#(1(x)) | → | 1#(x) | | 1#(0(x)) | → | 1#(x) |
| 1#(0(x)) | → | 0#(0(0(1(x)))) | | 1#(0(x)) | → | 0#(1(x)) |
| 1#(0(x)) | → | 0#(0(1(x))) | | 0#(0(x)) | → | 0#(x) |
Rewrite Rules
| 1(0(x)) | → | 0(0(0(1(x)))) | | 0(1(x)) | → | 1(x) |
| 1(1(x)) | → | 0(0(0(0(x)))) | | 0(0(x)) | → | 0(x) |
Original Signature
Termination of terms over the following signature is verified: 1, 0
Strategy
Polynomial Interpretation
- 0(x): x + 1
- 0#(x): x - 1
- 1(x): 4x + 1
- 1#(x): 4x - 1
Improved Usable rules
| 1(0(x)) | → | 0(0(0(1(x)))) | | 0(1(x)) | → | 1(x) |
| 0(0(x)) | → | 0(x) | | 1(1(x)) | → | 0(0(0(0(x)))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| 1#(0(x)) | → | 0#(0(0(1(x)))) | | 1#(0(x)) | → | 1#(x) |
| 1#(0(x)) | → | 0#(1(x)) | | 1#(0(x)) | → | 0#(0(1(x))) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| 0#(1(x)) | → | 1#(x) | | 0#(0(x)) | → | 0#(x) |
Rewrite Rules
| 1(0(x)) | → | 0(0(0(1(x)))) | | 0(1(x)) | → | 1(x) |
| 1(1(x)) | → | 0(0(0(0(x)))) | | 0(0(x)) | → | 0(x) |
Original Signature
Termination of terms over the following signature is verified: 1, 0
Strategy
The following SCCs where found
Problem 4: PolynomialOrderingProcessor
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| 1(0(x)) | → | 0(0(0(1(x)))) | | 0(1(x)) | → | 1(x) |
| 1(1(x)) | → | 0(0(0(0(x)))) | | 0(0(x)) | → | 0(x) |
Original Signature
Termination of terms over the following signature is verified: 1, 0
Strategy
Polynomial Interpretation
- 0(x): x + 1
- 0#(x): 4x - 2
- 1(x): -2
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed: