YES
The TRS could be proven terminating. The proof took 1696 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (60ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor PolynomialOrderingProcessor (170ms).
| – Problem 4 was processed with processor SubtermCriterion (0ms).
| – Problem 5 was processed with processor PolynomialOrderingProcessor (649ms).
| – Problem 6 was processed with processor PolynomialOrderingProcessor (119ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| towerIter#(s(x), y, z) | → | towerIter#(p(s(x)), y, exp(y, z)) | | times#(s(x), y) | → | plus#(y, times(p(s(x)), y)) |
| exp#(x, s(y)) | → | exp#(x, y) | | plus#(s(x), y) | → | plus#(p(s(x)), y) |
| times#(s(x), y) | → | p#(s(x)) | | tower#(x, y) | → | towerIter#(x, y, s(0)) |
| towerIter#(s(x), y, z) | → | p#(s(x)) | | towerIter#(s(x), y, z) | → | exp#(y, z) |
| times#(s(x), y) | → | times#(p(s(x)), y) | | plus#(s(x), y) | → | p#(s(x)) |
| exp#(x, s(y)) | → | times#(x, exp(x, y)) | | p#(s(s(x))) | → | p#(s(x)) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(p(s(x)), y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(p(s(x)), y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| tower(x, y) | → | towerIter(x, y, s(0)) | | towerIter(0, y, z) | → | z |
| towerIter(s(x), y, z) | → | towerIter(p(s(x)), y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, 0, s, times, p, towerIter
Strategy
The following SCCs where found
| towerIter#(s(x), y, z) → towerIter#(p(s(x)), y, exp(y, z)) |
| exp#(x, s(y)) → exp#(x, y) |
| plus#(s(x), y) → plus#(p(s(x)), y) |
| times#(s(x), y) → times#(p(s(x)), y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| exp#(x, s(y)) | → | exp#(x, y) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(p(s(x)), y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(p(s(x)), y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| tower(x, y) | → | towerIter(x, y, s(0)) | | towerIter(0, y, z) | → | z |
| towerIter(s(x), y, z) | → | towerIter(p(s(x)), y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, 0, s, times, p, towerIter
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| exp#(x, s(y)) | → | exp#(x, y) |
Problem 3: PolynomialOrderingProcessor
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(p(s(x)), y) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(p(s(x)), y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(p(s(x)), y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| tower(x, y) | → | towerIter(x, y, s(0)) | | towerIter(0, y, z) | → | z |
| towerIter(s(x), y, z) | → | towerIter(p(s(x)), y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, 0, s, times, p, towerIter
Strategy
Polynomial Interpretation
- 0: 1
- exp(x,y): -2
- p(x): x - 2
- plus(x,y): -2
- plus#(x,y): y + 2x - 2
- s(x): x + 2
- times(x,y): -2
- tower(x,y): -2
- towerIter(x,y,z): -2
Improved Usable rules
| p(s(s(x))) | → | s(p(s(x))) | | p(s(0)) | → | 0 |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| plus#(s(x), y) | → | plus#(p(s(x)), y) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(p(s(x)), y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(p(s(x)), y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| tower(x, y) | → | towerIter(x, y, s(0)) | | towerIter(0, y, z) | → | z |
| towerIter(s(x), y, z) | → | towerIter(p(s(x)), y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, 0, s, times, p, towerIter
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 5: PolynomialOrderingProcessor
Dependency Pair Problem
Dependency Pairs
| towerIter#(s(x), y, z) | → | towerIter#(p(s(x)), y, exp(y, z)) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(p(s(x)), y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(p(s(x)), y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| tower(x, y) | → | towerIter(x, y, s(0)) | | towerIter(0, y, z) | → | z |
| towerIter(s(x), y, z) | → | towerIter(p(s(x)), y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, 0, s, times, p, towerIter
Strategy
Polynomial Interpretation
- 0: 2
- exp(x,y): -2
- p(x): x - 1
- plus(x,y): -1
- s(x): x + 2
- times(x,y): -1
- tower(x,y): -2
- towerIter(x,y,z): -2
- towerIter#(x,y,z): y + x - 1
Improved Usable rules
| p(s(s(x))) | → | s(p(s(x))) | | p(s(0)) | → | 0 |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| towerIter#(s(x), y, z) | → | towerIter#(p(s(x)), y, exp(y, z)) |
Problem 6: PolynomialOrderingProcessor
Dependency Pair Problem
Dependency Pairs
| times#(s(x), y) | → | times#(p(s(x)), y) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(p(s(x)), y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(p(s(x)), y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| tower(x, y) | → | towerIter(x, y, s(0)) | | towerIter(0, y, z) | → | z |
| towerIter(s(x), y, z) | → | towerIter(p(s(x)), y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, 0, s, times, p, towerIter
Strategy
Polynomial Interpretation
- 0: 1
- exp(x,y): -2
- p(x): x - 2
- plus(x,y): -2
- s(x): 3x + 1
- times(x,y): -2
- times#(x,y): y + 4x - 2
- tower(x,y): -2
- towerIter(x,y,z): -2
Improved Usable rules
| p(s(s(x))) | → | s(p(s(x))) | | p(s(0)) | → | 0 |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| times#(s(x), y) | → | times#(p(s(x)), y) |