Term Rewriting System R:
[x]
w(r(x)) -> r(w(x))
b(r(x)) -> r(b(x))
b(w(x)) -> w(b(x))
Innermost Termination of R to be shown.
TRS
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
W(r(x)) -> W(x)
B(r(x)) -> B(x)
B(w(x)) -> W(b(x))
B(w(x)) -> B(x)
Furthermore, R contains three SCCs.
TRS
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
Dependency Pair:
W(r(x)) -> W(x)
Rules:
w(r(x)) -> r(w(x))
b(r(x)) -> r(b(x))
b(w(x)) -> w(b(x))
Strategy:
innermost
As we are in the innermost case, we can delete all 3 non-usable-rules.
TRS
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳Modular Removal of Rules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
Dependency Pair:
W(r(x)) -> W(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(W(x1)) | = x1 |
| POL(r(x1)) | = x1 |
We have the following set D of usable symbols: {W}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
W(r(x)) -> W(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.
TRS
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
Dependency Pair:
B(r(x)) -> B(x)
Rules:
w(r(x)) -> r(w(x))
b(r(x)) -> r(b(x))
b(w(x)) -> w(b(x))
Strategy:
innermost
As we are in the innermost case, we can delete all 3 non-usable-rules.
TRS
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 5
↳Modular Removal of Rules
→DP Problem 3
↳UsableRules
Dependency Pair:
B(r(x)) -> B(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(B(x1)) | = x1 |
| POL(r(x1)) | = x1 |
We have the following set D of usable symbols: {B}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
B(r(x)) -> 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.
TRS
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
Dependency Pair:
B(w(x)) -> B(x)
Rules:
w(r(x)) -> r(w(x))
b(r(x)) -> r(b(x))
b(w(x)) -> w(b(x))
Strategy:
innermost
As we are in the innermost case, we can delete all 3 non-usable-rules.
TRS
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 6
↳Modular Removal of Rules
Dependency Pair:
B(w(x)) -> B(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(B(x1)) | = x1 |
| POL(w(x1)) | = x1 |
We have the following set D of usable symbols: {B}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
B(w(x)) -> 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.
Innermost Termination of R successfully shown.
Duration:
0:01 minutes