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