Term Rewriting System R:
[x, y]
f(x, f(a, y)) -> f(f(y, f(f(a, a), a)), x)
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(x, f(a, y)) -> F(f(y, f(f(a, a), a)), x)
F(x, f(a, y)) -> F(y, f(f(a, a), a))
F(x, f(a, y)) -> F(f(a, a), a)
F(x, f(a, y)) -> F(a, a)
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
Dependency Pair:
F(x, f(a, y)) -> F(f(y, f(f(a, a), a)), x)
Rule:
f(x, f(a, y)) -> f(f(y, f(f(a, a), a)), x)
Strategy:
innermost
As we are in the innermost case, we can delete all 1 non-usable-rules.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Semantic Labelling
Dependency Pair:
F(x, f(a, y)) -> F(f(y, f(f(a, a), a)), x)
Rule:
none
Strategy:
innermost
Using Semantic Labelling, the DP problem could be transformed. The following model was found:
| F(x0, x1) | = 1 |
| f(x0, x1) | = 1 + x1 |
| a | = 0 |
From the dependency graph we obtain 1 (labeled) SCCs which each result in correspondingDP problem.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳SemLab
...
→DP Problem 3
↳Modular Removal of Rules
Dependency Pair:
F00(x, f01(a, y)) -> F00(f11(y, f10(f00(a, a), a)), x)
Rule:
none
Strategy:
innermost
We have the following set of usable rules:
none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(f_11(x1, x2)) | = x1 + x2 |
| POL(F_00(x1, x2)) | = 1 + x1 + x2 |
| POL(f_00(x1, x2)) | = x1 + x2 |
| POL(f_10(x1, x2)) | = x1 + x2 |
| POL(f_01(x1, x2)) | = x1 + x2 |
| POL(a) | = 0 |
We have the following set D of usable symbols: {f11, F00, f00, f10, a}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
F00(x, f01(a, y)) -> F00(f11(y, f10(f00(a, a), a)), 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:00 minutes