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