Term Rewriting System R:
[x]
f(s(x)) -> s(s(f(p(s(x)))))
f(0) -> 0
p(s(x)) -> x
Innermost Termination of R to be shown.
TRS
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
f(0) -> 0
where the Polynomial interpretation:
| POL(0) | = 1 |
| POL(s(x1)) | = x1 |
| POL(f(x1)) | = 2·x1 |
| POL(p(x1)) | = x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳RRRPolo
→TRS2
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(s(x)) -> F(p(s(x)))
F(s(x)) -> P(s(x))
Furthermore, R contains one SCC.
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
Dependency Pair:
F(s(x)) -> F(p(s(x)))
Rules:
f(s(x)) -> s(s(f(p(s(x)))))
p(s(x)) -> x
Strategy:
innermost
As we are in the innermost case, we can delete all 1 non-usable-rules.
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
...
→DP Problem 2
↳Modular Removal of Rules
Dependency Pair:
F(s(x)) -> F(p(s(x)))
Rule:
p(s(x)) -> x
Strategy:
innermost
We have the following set of usable rules:
p(s(x)) -> 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(p(x1)) | = x1 |
We have the following set D of usable symbols: {s, F, p}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:
p(s(x)) -> x
The result of this processor delivers one new DP problem.
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
...
→DP Problem 3
↳Dependency Graph
Dependency Pair:
F(s(x)) -> F(p(s(x)))
Rule:
none
Strategy:
innermost
Using the Dependency Graph resulted in no new DP problems.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes