Term Rewriting System R:
[x, y, z]
0(#) -> #
+(#, x) -> x
+(x, #) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(1(x), j(y)) -> 0(+(x, y))
+(j(x), 1(y)) -> 0(+(x, y))
+(+(x, y), z) -> +(x, +(y, z))
opp(#) -> #
opp(0(x)) -> 0(opp(x))
opp(1(x)) -> j(opp(x))
opp(j(x)) -> 1(opp(x))
-(x, y) -> +(x, opp(y))
*(#, x) -> #
*(0(x), y) -> 0(*(x, y))
*(1(x), y) -> +(0(*(x, y)), y)
*(j(x), y) -> -(0(*(x, y)), y)
*(*(x, y), z) -> *(x, *(y, z))
*(+(x, y), z) -> +(*(x, z), *(y, z))
*(x, +(y, z)) -> +(*(x, y), *(x, z))

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

+'(0(x), 0(y)) -> 0'(+(x, y))
+'(0(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)
+'(1(x), 0(y)) -> +'(x, y)
+'(0(x), j(y)) -> +'(x, y)
+'(j(x), 0(y)) -> +'(x, y)
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(1(x), 1(y)) -> +'(x, y)
+'(j(x), j(y)) -> +'(+(x, y), j(#))
+'(j(x), j(y)) -> +'(x, y)
+'(1(x), j(y)) -> 0'(+(x, y))
+'(1(x), j(y)) -> +'(x, y)
+'(j(x), 1(y)) -> 0'(+(x, y))
+'(j(x), 1(y)) -> +'(x, y)
+'(+(x, y), z) -> +'(x, +(y, z))
+'(+(x, y), z) -> +'(y, z)
OPP(0(x)) -> 0'(opp(x))
OPP(0(x)) -> OPP(x)
OPP(1(x)) -> OPP(x)
OPP(j(x)) -> OPP(x)
-'(x, y) -> +'(x, opp(y))
-'(x, y) -> OPP(y)
*'(0(x), y) -> 0'(*(x, y))
*'(0(x), y) -> *'(x, y)
*'(1(x), y) -> +'(0(*(x, y)), y)
*'(1(x), y) -> 0'(*(x, y))
*'(1(x), y) -> *'(x, y)
*'(j(x), y) -> -'(0(*(x, y)), y)
*'(j(x), y) -> 0'(*(x, y))
*'(j(x), y) -> *'(x, y)
*'(*(x, y), z) -> *'(x, *(y, z))
*'(*(x, y), z) -> *'(y, z)
*'(+(x, y), z) -> +'(*(x, z), *(y, z))
*'(+(x, y), z) -> *'(x, z)
*'(+(x, y), z) -> *'(y, z)
*'(x, +(y, z)) -> +'(*(x, y), *(x, z))
*'(x, +(y, z)) -> *'(x, y)
*'(x, +(y, z)) -> *'(x, z)

Furthermore, R contains three SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Modular Removal of Rules
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP


Dependency Pairs:

+'(+(x, y), z) -> +'(y, z)
+'(+(x, y), z) -> +'(x, +(y, z))
+'(j(x), 1(y)) -> +'(x, y)
+'(1(x), j(y)) -> +'(x, y)
+'(j(x), j(y)) -> +'(x, y)
+'(j(x), j(y)) -> +'(+(x, y), j(#))
+'(1(x), 1(y)) -> +'(x, y)
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(j(x), 0(y)) -> +'(x, y)
+'(0(x), j(y)) -> +'(x, y)
+'(1(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)
+'(0(x), 0(y)) -> +'(x, y)


Rules:


0(#) -> #
+(#, x) -> x
+(x, #) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(1(x), j(y)) -> 0(+(x, y))
+(j(x), 1(y)) -> 0(+(x, y))
+(+(x, y), z) -> +(x, +(y, z))
opp(#) -> #
opp(0(x)) -> 0(opp(x))
opp(1(x)) -> j(opp(x))
opp(j(x)) -> 1(opp(x))
-(x, y) -> +(x, opp(y))
*(#, x) -> #
*(0(x), y) -> 0(*(x, y))
*(1(x), y) -> +(0(*(x, y)), y)
*(j(x), y) -> -(0(*(x, y)), y)
*(*(x, y), z) -> *(x, *(y, z))
*(+(x, y), z) -> +(*(x, z), *(y, z))
*(x, +(y, z)) -> +(*(x, y), *(x, z))





We have the following set of usable rules:

+(#, x) -> x
+(x, #) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(1(x), j(y)) -> 0(+(x, y))
+(j(x), 1(y)) -> 0(+(x, y))
+(+(x, y), z) -> +(x, +(y, z))
0(#) -> #
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(#)=  0  
  POL(0(x1))=  x1  
  POL(1(x1))=  x1  
  POL(j(x1))=  x1  
  POL(+(x1, x2))=  x1 + x2  
  POL(+'(x1, x2))=  1 + x1 + x2  

We have the following set D of usable symbols: {#, 0, 1, j, +, +'}
No Dependency Pairs can be deleted.
12 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
         ↳SCP
       →DP Problem 3
         ↳SCP


Dependency Pairs:

+'(+(x, y), z) -> +'(y, z)
+'(+(x, y), z) -> +'(x, +(y, z))
+'(j(x), 1(y)) -> +'(x, y)
+'(1(x), j(y)) -> +'(x, y)
+'(j(x), j(y)) -> +'(x, y)
+'(j(x), j(y)) -> +'(+(x, y), j(#))
+'(1(x), 1(y)) -> +'(x, y)
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(j(x), 0(y)) -> +'(x, y)
+'(0(x), j(y)) -> +'(x, y)
+'(1(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)
+'(0(x), 0(y)) -> +'(x, y)


Rules:


+(#, x) -> x
+(x, #) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(1(x), j(y)) -> 0(+(x, y))
+(j(x), 1(y)) -> 0(+(x, y))
+(+(x, y), z) -> +(x, +(y, z))
0(#) -> #





We have the following set of usable rules:

+(#, x) -> x
+(x, #) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(1(x), j(y)) -> 0(+(x, y))
+(j(x), 1(y)) -> 0(+(x, y))
+(+(x, y), z) -> +(x, +(y, z))
0(#) -> #
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(#)=  0  
  POL(0(x1))=  x1  
  POL(1(x1))=  1 + x1  
  POL(j(x1))=  1 + x1  
  POL(+(x1, x2))=  x1 + x2  
  POL(+'(x1, x2))=  1 + x1 + x2  

We have the following set D of usable symbols: {#, 0, 1, j, +, +'}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

+'(j(x), 1(y)) -> +'(x, y)
+'(1(x), j(y)) -> +'(x, y)
+'(j(x), j(y)) -> +'(x, y)
+'(j(x), j(y)) -> +'(+(x, y), j(#))
+'(1(x), 1(y)) -> +'(x, y)
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(j(x), 0(y)) -> +'(x, y)
+'(0(x), j(y)) -> +'(x, y)
+'(1(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

+(1(x), j(y)) -> 0(+(x, y))
+(j(x), 1(y)) -> 0(+(x, y))


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
         ↳SCP
       →DP Problem 3
         ↳SCP


Dependency Pairs:

+'(+(x, y), z) -> +'(y, z)
+'(+(x, y), z) -> +'(x, +(y, z))
+'(0(x), 0(y)) -> +'(x, y)


Rules:


+(#, x) -> x
+(x, #) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(+(x, y), z) -> +(x, +(y, z))
0(#) -> #





We have the following set of usable rules:

+(#, x) -> x
+(x, #) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(+(x, y), z) -> +(x, +(y, z))
0(#) -> #
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(#)=  0  
  POL(0(x1))=  1 + x1  
  POL(1(x1))=  x1  
  POL(j(x1))=  x1  
  POL(+(x1, x2))=  x1 + x2  
  POL(+'(x1, x2))=  1 + x1 + x2  

We have the following set D of usable symbols: {#, 0, 1, j, +, +'}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

+'(0(x), 0(y)) -> +'(x, y)

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
0(#) -> #


The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 4
             ↳MRR
             ...
               →DP Problem 6
                 ↳Size-Change Principle
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP


Dependency Pairs:

+'(+(x, y), z) -> +'(y, z)
+'(+(x, y), z) -> +'(x, +(y, z))


Rules:


+(#, x) -> x
+(x, #) -> x
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(+(x, y), z) -> +(x, +(y, z))





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

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

DP: empty set
Oriented Rules: none

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


We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
       →DP Problem 2
         ↳Size-Change Principle
       →DP Problem 3
         ↳SCP


Dependency Pairs:

OPP(j(x)) -> OPP(x)
OPP(1(x)) -> OPP(x)
OPP(0(x)) -> OPP(x)


Rules:


0(#) -> #
+(#, x) -> x
+(x, #) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(1(x), j(y)) -> 0(+(x, y))
+(j(x), 1(y)) -> 0(+(x, y))
+(+(x, y), z) -> +(x, +(y, z))
opp(#) -> #
opp(0(x)) -> 0(opp(x))
opp(1(x)) -> j(opp(x))
opp(j(x)) -> 1(opp(x))
-(x, y) -> +(x, opp(y))
*(#, x) -> #
*(0(x), y) -> 0(*(x, y))
*(1(x), y) -> +(0(*(x, y)), y)
*(j(x), y) -> -(0(*(x, y)), y)
*(*(x, y), z) -> *(x, *(y, z))
*(+(x, y), z) -> +(*(x, z), *(y, z))
*(x, +(y, z)) -> +(*(x, y), *(x, z))





We number the DPs as follows:
  1. OPP(j(x)) -> OPP(x)
  2. OPP(1(x)) -> OPP(x)
  3. OPP(0(x)) -> OPP(x)
and get the following Size-Change Graph(s):
{3, 2, 1} , {3, 2, 1}
1>1

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

DP: empty set
Oriented Rules: none

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

with Argument Filtering System:
0(x1) -> 0(x1)
1(x1) -> 1(x1)
j(x1) -> j(x1)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳Size-Change Principle


Dependency Pairs:

*'(x, +(y, z)) -> *'(x, z)
*'(x, +(y, z)) -> *'(x, y)
*'(+(x, y), z) -> *'(y, z)
*'(+(x, y), z) -> *'(x, z)
*'(*(x, y), z) -> *'(y, z)
*'(*(x, y), z) -> *'(x, *(y, z))
*'(j(x), y) -> *'(x, y)
*'(1(x), y) -> *'(x, y)
*'(0(x), y) -> *'(x, y)


Rules:


0(#) -> #
+(#, x) -> x
+(x, #) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(1(x), j(y)) -> 0(+(x, y))
+(j(x), 1(y)) -> 0(+(x, y))
+(+(x, y), z) -> +(x, +(y, z))
opp(#) -> #
opp(0(x)) -> 0(opp(x))
opp(1(x)) -> j(opp(x))
opp(j(x)) -> 1(opp(x))
-(x, y) -> +(x, opp(y))
*(#, x) -> #
*(0(x), y) -> 0(*(x, y))
*(1(x), y) -> +(0(*(x, y)), y)
*(j(x), y) -> -(0(*(x, y)), y)
*(*(x, y), z) -> *(x, *(y, z))
*(+(x, y), z) -> +(*(x, z), *(y, z))
*(x, +(y, z)) -> +(*(x, y), *(x, z))





We number the DPs as follows:
  1. *'(x, +(y, z)) -> *'(x, z)
  2. *'(x, +(y, z)) -> *'(x, y)
  3. *'(+(x, y), z) -> *'(y, z)
  4. *'(+(x, y), z) -> *'(x, z)
  5. *'(*(x, y), z) -> *'(y, z)
  6. *'(*(x, y), z) -> *'(x, *(y, z))
  7. *'(j(x), y) -> *'(x, y)
  8. *'(1(x), y) -> *'(x, y)
  9. *'(0(x), y) -> *'(x, y)
and get the following Size-Change Graph(s):
{9, 8, 7, 6, 5, 4, 3, 2, 1} , {9, 8, 7, 6, 5, 4, 3, 2, 1}
1=1
2>2
{9, 8, 7, 6, 5, 4, 3, 2, 1} , {9, 8, 7, 6, 5, 4, 3, 2, 1}
1>1
2=2
{9, 8, 7, 6, 5, 4, 3, 2, 1} , {9, 8, 7, 6, 5, 4, 3, 2, 1}
1>1

which lead(s) to this/these maximal multigraph(s):
{9, 8, 7, 6, 5, 4, 3, 2, 1} , {9, 8, 7, 6, 5, 4, 3, 2, 1}
1>1
{9, 8, 7, 6, 5, 4, 3, 2, 1} , {9, 8, 7, 6, 5, 4, 3, 2, 1}
1>1
2=2
{9, 8, 7, 6, 5, 4, 3, 2, 1} , {9, 8, 7, 6, 5, 4, 3, 2, 1}
1=1
2>2
{9, 8, 7, 6, 5, 4, 3, 2, 1} , {9, 8, 7, 6, 5, 4, 3, 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:
0(x1) -> 0(x1)
1(x1) -> 1(x1)
j(x1) -> j(x1)
+(x1, x2) -> +(x1, x2)

We obtain no new DP problems.

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