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