Term Rewriting System R:
[x]
f(x) -> s(x)
f(s(s(x))) -> s(f(f(x)))
Innermost Termination of R to be shown.
TRS
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(s(s(x))) -> F(f(x))
F(s(s(x))) -> F(x)
Furthermore, R contains one SCC.
TRS
↳DPs
→DP Problem 1
↳Modular Removal of Rules
Dependency Pairs:
F(s(s(x))) -> F(x)
F(s(s(x))) -> F(f(x))
Rules:
f(x) -> s(x)
f(s(s(x))) -> s(f(f(x)))
Strategy:
innermost
We have the following set of usable rules:
f(s(s(x))) -> s(f(f(x)))
f(x) -> s(x)
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(s(x1)) | = 1 + x1 |
| POL(F(x1)) | = 1 + x1 |
| POL(f(x1)) | = 1 + x1 |
We have the following set D of usable symbols: {s, F, f}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:
F(s(s(x))) -> F(x)
F(s(s(x))) -> F(f(x))
No Rules can be deleted.
After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.
Innermost Termination of R successfully shown.
Duration:
0:01 minutes