Term Rewriting System R:
[x]
f(a, f(b, x)) -> f(a, f(a, f(a, x)))
f(b, f(a, x)) -> f(b, f(b, f(b, x)))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(a, f(b, x)) -> F(a, f(a, f(a, x)))
F(a, f(b, x)) -> F(a, f(a, x))
F(a, f(b, x)) -> F(a, x)
F(b, f(a, x)) -> F(b, f(b, f(b, x)))
F(b, f(a, x)) -> F(b, f(b, x))
F(b, f(a, x)) -> F(b, x)
Furthermore, R contains two SCCs.
R
↳DPs
→DP Problem 1
↳Modular Removal of Rules
→DP Problem 2
↳MRR
Dependency Pairs:
F(a, f(b, x)) -> F(a, x)
F(a, f(b, x)) -> F(a, f(a, x))
F(a, f(b, x)) -> F(a, f(a, f(a, x)))
Rules:
f(a, f(b, x)) -> f(a, f(a, f(a, x)))
f(b, f(a, x)) -> f(b, f(b, f(b, x)))
The original DP problem is in applicative form. Its DPs and usable rules are the following.
F(a, f(b, x)) -> F(a, x)
F(a, f(b, x)) -> F(a, f(a, x))
F(a, f(b, x)) -> F(a, f(a, f(a, x)))
f(a, f(b, x)) -> f(a, f(a, f(a, x)))
It is proper and hence, it can be A-transformed which results in the DP problem
A(b(x)) -> A(x)
A(b(x)) -> A(a(x))
A(b(x)) -> A(a(a(x)))
a(b(x)) -> a(a(a(x)))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(b(x1)) | = x1 |
| POL(a(x1)) | = x1 |
| POL(A(x1)) | = 1 + x1 |
We have the following set D of usable symbols: {a, A}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
A(b(x)) -> A(x)
A(b(x)) -> A(a(x))
A(b(x)) -> 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.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Modular Removal of Rules
Dependency Pairs:
F(b, f(a, x)) -> F(b, x)
F(b, f(a, x)) -> F(b, f(b, x))
F(b, f(a, x)) -> F(b, f(b, f(b, x)))
Rules:
f(a, f(b, x)) -> f(a, f(a, f(a, x)))
f(b, f(a, x)) -> f(b, f(b, f(b, x)))
The original DP problem is in applicative form. Its DPs and usable rules are the following.
F(b, f(a, x)) -> F(b, x)
F(b, f(a, x)) -> F(b, f(b, x))
F(b, f(a, x)) -> F(b, f(b, f(b, x)))
f(b, f(a, x)) -> f(b, f(b, f(b, x)))
It is proper and hence, it can be A-transformed which results in the DP problem
B(a(x)) -> B(x)
B(a(x)) -> B(b(x))
B(a(x)) -> B(b(b(x)))
b(a(x)) -> b(b(b(x)))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(B(x1)) | = 1 + x1 |
| POL(b(x1)) | = x1 |
| POL(a(x1)) | = x1 |
We have the following set D of usable symbols: {B, b}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
B(a(x)) -> B(x)
B(a(x)) -> B(b(x))
B(a(x)) -> B(b(b(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.
Termination of R successfully shown.
Duration:
0:00 minutes