Term Rewriting System R:
[x, y, z]
f(0, 1, x) -> f(g(x), g(x), x)
f(g(x), y, z) -> g(f(x, y, z))
f(x, g(y), z) -> g(f(x, y, z))
f(x, y, g(z)) -> g(f(x, y, z))
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(0, 1, x) -> F(g(x), g(x), x)
F(g(x), y, z) -> F(x, y, z)
F(x, g(y), z) -> F(x, y, z)
F(x, y, g(z)) -> F(x, y, z)
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
Dependency Pairs:
F(x, y, g(z)) -> F(x, y, z)
F(x, g(y), z) -> F(x, y, z)
F(g(x), y, z) -> F(x, y, z)
F(0, 1, x) -> F(g(x), g(x), x)
Rules:
f(0, 1, x) -> f(g(x), g(x), x)
f(g(x), y, z) -> g(f(x, y, z))
f(x, g(y), z) -> g(f(x, y, z))
f(x, y, g(z)) -> g(f(x, y, z))
Strategy:
innermost
As we are in the innermost case, we can delete all 4 non-usable-rules.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Negative Polynomial Order
Dependency Pairs:
F(x, y, g(z)) -> F(x, y, z)
F(x, g(y), z) -> F(x, y, z)
F(g(x), y, z) -> F(x, y, z)
F(0, 1, x) -> F(g(x), g(x), x)
Rule:
none
Strategy:
innermost
The following Dependency Pair can be strictly oriented using the given order.
F(x, y, g(z)) -> F(x, y, z)
There are no usable rules (regarding the implicit AFS).
Used ordering:
Polynomial Order with Interpretation:
POL( F(x1, ..., x3) ) = x3
POL( g(x1) ) = x1 + 1
This results in one new DP problem.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 3
↳Semantic Labelling
Dependency Pairs:
F(x, g(y), z) -> F(x, y, z)
F(g(x), y, z) -> F(x, y, z)
F(0, 1, x) -> F(g(x), g(x), x)
Rule:
none
Strategy:
innermost
Using Semantic Labelling, the DP problem could be transformed. The following model was found:
| F(x0, x1, x2) | = x2 |
| 0 | = 0 |
| 1 | = 1 |
| g(x0) | = x0 |
From the dependency graph we obtain 8 (labeled) SCCs which each result in correspondingDP problem.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 4
↳Modular Removal of Rules
Dependency Pairs:
F011(g0(x), y, z) -> F011(x, y, z)
F011(x, g1(y), z) -> F011(x, y, z)
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(g_1(x1)) | = x1 |
| POL(F_011(x1, x2, x3)) | = x1 + x2 + x3 |
| POL(g_0(x1)) | = x1 |
We have the following set D of usable symbols: {F011}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
F011(g0(x), y, z) -> F011(x, y, z)
F011(x, g1(y), z) -> F011(x, y, z)
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
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 5
↳Modular Removal of Rules
Dependency Pairs:
F111(g1(x), y, z) -> F111(x, y, z)
F111(x, g1(y), z) -> F111(x, y, z)
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_111(x1, x2, x3)) | = x1 + x2 + x3 |
| POL(g_1(x1)) | = x1 |
We have the following set D of usable symbols: {F111}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
F111(g1(x), y, z) -> F111(x, y, z)
F111(x, g1(y), z) -> F111(x, y, z)
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
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 6
↳Modular Removal of Rules
Dependency Pairs:
F101(g1(x), y, z) -> F101(x, y, z)
F101(x, g0(y), z) -> F101(x, y, z)
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(g_1(x1)) | = x1 |
| POL(F_101(x1, x2, x3)) | = x1 + x2 + x3 |
| POL(g_0(x1)) | = x1 |
We have the following set D of usable symbols: {F101}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
F101(g1(x), y, z) -> F101(x, y, z)
F101(x, g0(y), z) -> F101(x, y, z)
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
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 7
↳Modular Removal of Rules
Dependency Pairs:
F110(g1(x), y, z) -> F110(x, y, z)
F110(x, g1(y), z) -> F110(x, y, z)
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(g_1(x1)) | = x1 |
| POL(F_110(x1, x2, x3)) | = x1 + x2 + x3 |
We have the following set D of usable symbols: {F110}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
F110(g1(x), y, z) -> F110(x, y, z)
F110(x, g1(y), z) -> F110(x, y, z)
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
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 8
↳Modular Removal of Rules
Dependency Pairs:
F001(g0(x), y, z) -> F001(x, y, z)
F001(x, g0(y), z) -> F001(x, y, z)
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_001(x1, x2, x3)) | = x1 + x2 + x3 |
| POL(g_0(x1)) | = x1 |
We have the following set D of usable symbols: {F001}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
F001(g0(x), y, z) -> F001(x, y, z)
F001(x, g0(y), z) -> F001(x, y, z)
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
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 9
↳Modular Removal of Rules
Dependency Pairs:
F100(g1(x), y, z) -> F100(x, y, z)
F100(x, g0(y), z) -> F100(x, y, z)
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_100(x1, x2, x3)) | = x1 + x2 + x3 |
| POL(g_1(x1)) | = x1 |
| POL(g_0(x1)) | = x1 |
We have the following set D of usable symbols: {F100}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
F100(g1(x), y, z) -> F100(x, y, z)
F100(x, g0(y), z) -> F100(x, y, z)
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
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 10
↳Modular Removal of Rules
Dependency Pairs:
F000(g0(x), y, z) -> F000(x, y, z)
F000(x, g0(y), z) -> F000(x, y, z)
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_000(x1, x2, x3)) | = x1 + x2 + x3 |
| POL(g_0(x1)) | = x1 |
We have the following set D of usable symbols: {F000}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
F000(g0(x), y, z) -> F000(x, y, z)
F000(x, g0(y), z) -> F000(x, y, z)
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
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 11
↳Modular Removal of Rules
Dependency Pairs:
F010(g0(x), y, z) -> F010(x, y, z)
F010(x, g1(y), z) -> F010(x, y, z)
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_010(x1, x2, x3)) | = x1 + x2 + x3 |
| POL(g_1(x1)) | = x1 |
| POL(g_0(x1)) | = x1 |
We have the following set D of usable symbols: {F010}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
F010(g0(x), y, z) -> F010(x, y, z)
F010(x, g1(y), z) -> F010(x, y, z)
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:02 minutes