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

Innermost 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
         ↳Usable Rules (Innermost)
       →DP Problem 2
         ↳UsableRules
       →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))


Strategy:

innermost




As we are in the innermost case, we can delete all 12 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 4
             ↳Modular Removal of Rules
       →DP Problem 2
         ↳UsableRules
       →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(#) -> #
+(0(x), 1(y)) -> 1(+(x, y))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(1(x), j(y)) -> 0(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(x, #) -> x
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(0(x), 0(y)) -> 0(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(j(x), 1(y)) -> 0(+(x, y))
+(#, x) -> x
+(+(x, y), z) -> +(x, +(y, z))


Strategy:

innermost




We have the following set of usable rules:

0(#) -> #
+(0(x), 1(y)) -> 1(+(x, y))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(1(x), j(y)) -> 0(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(x, #) -> x
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(0(x), 0(y)) -> 0(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(j(x), 1(y)) -> 0(+(x, y))
+(#, x) -> x
+(+(x, y), z) -> +(x, +(y, z))
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
         ↳UsableRules
           →DP Problem 4
             ↳MRR
             ...
               →DP Problem 5
                 ↳Modular Removal of Rules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳SCP


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




We have the following set of usable rules:

+(x, #) -> x
0(#) -> #
+(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
+(0(x), 0(y)) -> 0(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(j(x), j(y)) -> 1(+(+(x, y), j(#)))
+(0(x), j(y)) -> j(+(x, y))
+(#, x) -> x
+(1(x), 0(y)) -> 1(+(x, y))
+(+(x, y), z) -> +(x, +(y, z))
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(#) -> #
+(0(x), 0(y)) -> 0(+(x, y))
+(j(x), 0(y)) -> j(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(0(x), j(y)) -> j(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))


The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 4
             ↳MRR
             ...
               →DP Problem 6
                 ↳Dependency Graph
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳SCP


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




Using the Dependency Graph the DP problem was split into 1 DP problems.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 4
             ↳MRR
             ...
               →DP Problem 7
                 ↳Usable Rules (Innermost)
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳SCP


Dependency Pair:

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


Rules:


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


Strategy:

innermost




As we are in the innermost case, we can delete all 5 non-usable-rules.


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


Dependency Pair:

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


Rule:

none


Strategy:

innermost




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

which lead(s) to this/these maximal multigraph(s):
{1} , {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:
+(x1, x2) -> +(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳Usable Rules (Innermost)
       →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))


Strategy:

innermost




As we are in the innermost case, we can delete all 25 non-usable-rules.


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


Dependency Pairs:

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


Rule:

none


Strategy:

innermost




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):
{1, 2, 3} , {1, 2, 3}
1>1

which lead(s) to this/these maximal multigraph(s):
{1, 2, 3} , {1, 2, 3}
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
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳Size-Change Principle


Dependency Pairs:

*'(+(x, y), z) -> *'(y, z)
*'(+(x, y), z) -> *'(x, z)
*'(x, +(y, z)) -> *'(x, z)
*'(*(x, y), z) -> *'(y, z)
*'(x, +(y, z)) -> *'(x, y)
*'(*(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))


Strategy:

innermost




We number the DPs as follows:
  1. *'(+(x, y), z) -> *'(y, z)
  2. *'(+(x, y), z) -> *'(x, z)
  3. *'(x, +(y, z)) -> *'(x, z)
  4. *'(*(x, y), z) -> *'(y, z)
  5. *'(x, +(y, z)) -> *'(x, y)
  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):
{1} , {1}
1>1
2=2
{2} , {2}
1>1
2=2
{3} , {3}
1=1
2>2
{4} , {4}
1>1
2=2
{5} , {5}
1=1
2>2
{6} , {6}
1>1
{9, 8, 7} , {9, 8, 7}
1>1
2=2

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

We obtain no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:04 minutes