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