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)

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)

Furthermore, R contains two SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Modular Removal of Rules
       →DP Problem 2
         ↳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)





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 CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(I(x1))=  x1  
  POL(0)=  0  
  POL(O(x1))=  x1  
  POL(+(x1, x2))=  x1 + x2  
  POL(+'(x1, x2))=  1 + x1 + x2  

We have the following set D of usable symbols: {I, 0, O, +, +'}
No Dependency Pairs can be deleted.
4 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 3
             ↳Modular Removal of Rules
       →DP Problem 2
         ↳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 CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(I(x1))=  1 + x1  
  POL(0)=  0  
  POL(O(x1))=  x1  
  POL(+(x1, x2))=  x1 + x2  
  POL(+'(x1, x2))=  1 + x1 + x2  

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 3
             ↳MRR
             ...
               →DP Problem 4
                 ↳Modular Removal of Rules
       →DP Problem 2
         ↳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 CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(O(x1))=  x1  
  POL(+'(x1, x2))=  x1 + x2  

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
         ↳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)





We number the DPs as follows:
  1. *'(I(x), y) -> *'(x, y)
  2. *'(O(x), y) -> *'(x, y)
and get the following Size-Change Graph(s):
{2, 1} , {2, 1}
1>1
2=2

which lead(s) to this/these maximal multigraph(s):
{2, 1} , {2, 1}
1>1
2=2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
I(x1) -> I(x1)
O(x1) -> O(x1)

We obtain no new DP problems.

Termination of R successfully shown.
Duration:
0:00 minutes