Term Rewriting System R:
[x, y]
O(0) -> 0
+(0, x) -> x
+(x, 0) -> x
+(O(x), O(y)) -> O(+(x, y))
+(O(x), I(y)) -> I(+(x, y))
+(I(x), O(y)) -> I(+(x, y))
+(I(x), I(y)) -> O(+(+(x, y), I(0)))
*(0, x) -> 0
*(x, 0) -> 0
*(O(x), y) -> O(*(x, y))
*(I(x), y) -> +(O(*(x, y)), y)
-(x, 0) -> x
-(0, x) -> 0
-(O(x), O(y)) -> O(-(x, y))
-(O(x), I(y)) -> I(-(-(x, y), I(1)))
-(I(x), O(y)) -> I(-(x, y))
-(I(x), I(y)) -> O(-(x, y))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
+'(O(x), O(y)) -> O'(+(x, y))
+'(O(x), O(y)) -> +'(x, y)
+'(O(x), I(y)) -> +'(x, y)
+'(I(x), O(y)) -> +'(x, y)
+'(I(x), I(y)) -> O'(+(+(x, y), I(0)))
+'(I(x), I(y)) -> +'(+(x, y), I(0))
+'(I(x), I(y)) -> +'(x, y)
*'(O(x), y) -> O'(*(x, y))
*'(O(x), y) -> *'(x, y)
*'(I(x), y) -> +'(O(*(x, y)), y)
*'(I(x), y) -> O'(*(x, y))
*'(I(x), y) -> *'(x, y)
-'(O(x), O(y)) -> O'(-(x, y))
-'(O(x), O(y)) -> -'(x, y)
-'(O(x), I(y)) -> -'(-(x, y), I(1))
-'(O(x), I(y)) -> -'(x, y)
-'(I(x), O(y)) -> -'(x, y)
-'(I(x), I(y)) -> O'(-(x, y))
-'(I(x), I(y)) -> -'(x, y)
Furthermore, R contains three SCCs.
R
↳DPs
→DP Problem 1
↳Modular Removal of Rules
→DP Problem 2
↳MRR
→DP Problem 3
↳SCP
Dependency Pairs:
+'(I(x), I(y)) -> +'(x, y)
+'(I(x), I(y)) -> +'(+(x, y), I(0))
+'(I(x), O(y)) -> +'(x, y)
+'(O(x), I(y)) -> +'(x, y)
+'(O(x), O(y)) -> +'(x, y)
Rules:
O(0) -> 0
+(0, x) -> x
+(x, 0) -> x
+(O(x), O(y)) -> O(+(x, y))
+(O(x), I(y)) -> I(+(x, y))
+(I(x), O(y)) -> I(+(x, y))
+(I(x), I(y)) -> O(+(+(x, y), I(0)))
*(0, x) -> 0
*(x, 0) -> 0
*(O(x), y) -> O(*(x, y))
*(I(x), y) -> +(O(*(x, y)), y)
-(x, 0) -> x
-(0, x) -> 0
-(O(x), O(y)) -> O(-(x, y))
-(O(x), I(y)) -> I(-(-(x, y), I(1)))
-(I(x), O(y)) -> I(-(x, y))
-(I(x), I(y)) -> O(-(x, y))
We have the following set of usable rules:
+(0, x) -> x
+(x, 0) -> x
+(O(x), O(y)) -> O(+(x, y))
+(O(x), I(y)) -> I(+(x, y))
+(I(x), O(y)) -> I(+(x, y))
+(I(x), I(y)) -> O(+(+(x, y), I(0)))
O(0) -> 0
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(I(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(0) | = 0_{ }^{ } |
_{ }^{ }POL(O(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(+(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(+'(x_{1}, x_{2})) | = 1 + x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {I, 0, O, +, +'}
No Dependency Pairs can be deleted.
10 non usable rules have been deleted.
The result of this processor delivers one new DP problem.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 4
↳Modular Removal of Rules
→DP Problem 2
↳MRR
→DP Problem 3
↳SCP
Dependency Pairs:
+'(I(x), I(y)) -> +'(x, y)
+'(I(x), I(y)) -> +'(+(x, y), I(0))
+'(I(x), O(y)) -> +'(x, y)
+'(O(x), I(y)) -> +'(x, y)
+'(O(x), O(y)) -> +'(x, y)
Rules:
+(0, x) -> x
+(x, 0) -> x
+(O(x), O(y)) -> O(+(x, y))
+(O(x), I(y)) -> I(+(x, y))
+(I(x), O(y)) -> I(+(x, y))
+(I(x), I(y)) -> O(+(+(x, y), I(0)))
O(0) -> 0
We have the following set of usable rules:
+(0, x) -> x
+(x, 0) -> x
+(O(x), O(y)) -> O(+(x, y))
+(O(x), I(y)) -> I(+(x, y))
+(I(x), O(y)) -> I(+(x, y))
+(I(x), I(y)) -> O(+(+(x, y), I(0)))
O(0) -> 0
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(I(x_{1})) | = 1 + x_{1}_{ }^{ } |
_{ }^{ }POL(0) | = 0_{ }^{ } |
_{ }^{ }POL(O(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(+(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(+'(x_{1}, x_{2})) | = 1 + x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {I, 0, O, +, +'}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:
+'(I(x), I(y)) -> +'(x, y)
+'(I(x), I(y)) -> +'(+(x, y), I(0))
+'(I(x), O(y)) -> +'(x, y)
+'(O(x), I(y)) -> +'(x, y)
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:
+(I(x), I(y)) -> O(+(+(x, y), I(0)))
The result of this processor delivers one new DP problem.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 4
↳MRR
...
→DP Problem 5
↳Modular Removal of Rules
→DP Problem 2
↳MRR
→DP Problem 3
↳SCP
Dependency Pair:
+'(O(x), O(y)) -> +'(x, y)
Rules:
+(0, x) -> x
+(x, 0) -> x
+(O(x), O(y)) -> O(+(x, y))
+(O(x), I(y)) -> I(+(x, y))
+(I(x), O(y)) -> I(+(x, y))
O(0) -> 0
We have the following set of usable rules:
none
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(O(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(+'(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {+'}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
+'(O(x), O(y)) -> +'(x, y)
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
→DP Problem 3
↳SCP
Dependency Pairs:
-'(I(x), I(y)) -> -'(x, y)
-'(I(x), O(y)) -> -'(x, y)
-'(O(x), I(y)) -> -'(x, y)
-'(O(x), I(y)) -> -'(-(x, y), I(1))
-'(O(x), O(y)) -> -'(x, y)
Rules:
O(0) -> 0
+(0, x) -> x
+(x, 0) -> x
+(O(x), O(y)) -> O(+(x, y))
+(O(x), I(y)) -> I(+(x, y))
+(I(x), O(y)) -> I(+(x, y))
+(I(x), I(y)) -> O(+(+(x, y), I(0)))
*(0, x) -> 0
*(x, 0) -> 0
*(O(x), y) -> O(*(x, y))
*(I(x), y) -> +(O(*(x, y)), y)
-(x, 0) -> x
-(0, x) -> 0
-(O(x), O(y)) -> O(-(x, y))
-(O(x), I(y)) -> I(-(-(x, y), I(1)))
-(I(x), O(y)) -> I(-(x, y))
-(I(x), I(y)) -> O(-(x, y))
We have the following set of usable rules:
-(x, 0) -> x
-(0, x) -> 0
-(O(x), O(y)) -> O(-(x, y))
-(O(x), I(y)) -> I(-(-(x, y), I(1)))
-(I(x), O(y)) -> I(-(x, y))
-(I(x), I(y)) -> O(-(x, y))
O(0) -> 0
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(I(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(-'(x_{1}, x_{2})) | = 1 + x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(0) | = 0_{ }^{ } |
_{ }^{ }POL(1) | = 0_{ }^{ } |
_{ }^{ }POL(O(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(-(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {I, -', 0, 1, O, -}
No Dependency Pairs can be deleted.
10 non usable rules have been deleted.
The result of this processor delivers one new DP problem.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳MRR
→DP Problem 6
↳Modular Removal of Rules
→DP Problem 3
↳SCP
Dependency Pairs:
-'(I(x), I(y)) -> -'(x, y)
-'(I(x), O(y)) -> -'(x, y)
-'(O(x), I(y)) -> -'(x, y)
-'(O(x), I(y)) -> -'(-(x, y), I(1))
-'(O(x), O(y)) -> -'(x, y)
Rules:
-(x, 0) -> x
-(0, x) -> 0
-(O(x), O(y)) -> O(-(x, y))
-(O(x), I(y)) -> I(-(-(x, y), I(1)))
-(I(x), O(y)) -> I(-(x, y))
-(I(x), I(y)) -> O(-(x, y))
O(0) -> 0
We have the following set of usable rules:
-(x, 0) -> x
-(0, x) -> 0
-(O(x), O(y)) -> O(-(x, y))
-(O(x), I(y)) -> I(-(-(x, y), I(1)))
-(I(x), O(y)) -> I(-(x, y))
-(I(x), I(y)) -> O(-(x, y))
O(0) -> 0
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(I(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(-'(x_{1}, x_{2})) | = 1 + x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(0) | = 1_{ }^{ } |
_{ }^{ }POL(1) | = 0_{ }^{ } |
_{ }^{ }POL(O(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(-(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {I, -', 0, 1, O, -}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:
-(x, 0) -> x
The result of this processor delivers one new DP problem.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳MRR
→DP Problem 6
↳MRR
...
→DP Problem 7
↳Modular Removal of Rules
→DP Problem 3
↳SCP
Dependency Pairs:
-'(I(x), I(y)) -> -'(x, y)
-'(I(x), O(y)) -> -'(x, y)
-'(O(x), I(y)) -> -'(x, y)
-'(O(x), I(y)) -> -'(-(x, y), I(1))
-'(O(x), O(y)) -> -'(x, y)
Rules:
-(0, x) -> 0
-(O(x), O(y)) -> O(-(x, y))
-(O(x), I(y)) -> I(-(-(x, y), I(1)))
-(I(x), O(y)) -> I(-(x, y))
-(I(x), I(y)) -> O(-(x, y))
O(0) -> 0
We have the following set of usable rules:
-(0, x) -> 0
-(O(x), O(y)) -> O(-(x, y))
-(O(x), I(y)) -> I(-(-(x, y), I(1)))
-(I(x), O(y)) -> I(-(x, y))
-(I(x), I(y)) -> O(-(x, y))
O(0) -> 0
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(I(x_{1})) | = 1 + x_{1}_{ }^{ } |
_{ }^{ }POL(-'(x_{1}, x_{2})) | = 1 + x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(0) | = 0_{ }^{ } |
_{ }^{ }POL(1) | = 0_{ }^{ } |
_{ }^{ }POL(O(x_{1})) | = 1 + x_{1}_{ }^{ } |
_{ }^{ }POL(-(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {I, -', 0, 1, O, -}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:
-'(I(x), I(y)) -> -'(x, y)
-'(I(x), O(y)) -> -'(x, y)
-'(O(x), I(y)) -> -'(x, y)
-'(O(x), I(y)) -> -'(-(x, y), I(1))
-'(O(x), O(y)) -> -'(x, y)
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
↳MRR
→DP Problem 3
↳Size-Change Principle
Dependency Pairs:
*'(I(x), y) -> *'(x, y)
*'(O(x), y) -> *'(x, y)
Rules:
O(0) -> 0
+(0, x) -> x
+(x, 0) -> x
+(O(x), O(y)) -> O(+(x, y))
+(O(x), I(y)) -> I(+(x, y))
+(I(x), O(y)) -> I(+(x, y))
+(I(x), I(y)) -> O(+(+(x, y), I(0)))
*(0, x) -> 0
*(x, 0) -> 0
*(O(x), y) -> O(*(x, y))
*(I(x), y) -> +(O(*(x, y)), y)
-(x, 0) -> x
-(0, x) -> 0
-(O(x), O(y)) -> O(-(x, y))
-(O(x), I(y)) -> I(-(-(x, y), I(1)))
-(I(x), O(y)) -> I(-(x, y))
-(I(x), I(y)) -> O(-(x, y))
We number the DPs as follows:
- *'(I(x), y) -> *'(x, y)
- *'(O(x), y) -> *'(x, y)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
D_{P}: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
I(x_{1}) -> I(x_{1})
O(x_{1}) -> O(x_{1})
We obtain no new DP problems.
Termination of R successfully shown.
Duration:
0:01 minutes