Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
    ↳5 QDP
        ↳6 QDPOrderProof (⇔)
        ↳7 QDP
        ↳8 QDPOrderProof (⇔)
        ↳9 QDP
        ↳10 QDPOrderProof (⇔)
        ↳11 QDP
        ↳12 PisEmptyProof (⇔)
        ↳13 TRUE
    ↳14 QDP
        ↳15 QDPOrderProof (⇔)
        ↳16 QDP
        ↳17 QDPOrderProof (⇔)
        ↳18 QDP
        ↳19 QDPOrderProof (⇔)
        ↳20 QDP
        ↳21 PisEmptyProof (⇔)
        ↳22 TRUE
    ↳23 QDP
        ↳24 QDPOrderProof (⇔)
        ↳25 QDP
        ↳26 QDPOrderProof (⇔)
        ↳27 QDP
        ↳28 QDPOrderProof (⇔)
        ↳29 QDP
        ↳30 QDPOrderProof (⇔)
        ↳31 QDP
        ↳32 QDPOrderProof (⇔)
        ↳33 QDP
        ↳34 PisEmptyProof (⇔)
        ↳35 TRUE

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following 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))

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+1(0(x), 0(y)) → 01(+(x, y))
+1(0(x), 0(y)) → +1(x, y)
+1(0(x), 1(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(0(x), j(y)) → +1(x, y)
+1(j(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(j(x), j(y)) → +1(+(x, y), j(#))
+1(j(x), j(y)) → +1(x, y)
+1(1(x), j(y)) → 01(+(x, y))
+1(1(x), j(y)) → +1(x, y)
+1(j(x), 1(y)) → 01(+(x, y))
+1(j(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)
OPP(0(x)) → 01(opp(x))
OPP(0(x)) → OPP(x)
OPP(1(x)) → OPP(x)
OPP(j(x)) → OPP(x)
-1(x, y) → +1(x, opp(y))
-1(x, y) → OPP(y)
*1(0(x), y) → 01(*(x, y))
*1(0(x), y) → *1(x, y)
*1(1(x), y) → +1(0(*(x, y)), y)
*1(1(x), y) → 01(*(x, y))
*1(1(x), y) → *1(x, y)
*1(j(x), y) → -1(0(*(x, y)), y)
*1(j(x), y) → 01(*(x, y))
*1(j(x), y) → *1(x, y)
*1(*(x, y), z) → *1(x, *(y, z))
*1(*(x, y), z) → *1(y, z)
*1(+(x, y), z) → +1(*(x, z), *(y, z))
*1(+(x, y), z) → *1(x, z)
*1(+(x, y), z) → *1(y, z)
*1(x, +(y, z)) → +1(*(x, y), *(x, z))
*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 13 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

OPP(1(x)) → OPP(x)
OPP(0(x)) → OPP(x)
OPP(j(x)) → OPP(x)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


OPP(j(x)) → OPP(x)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
OPP(x0, x1)  =  OPP(x0, x1)

Tags:
OPP has argument tags [0,0] and root tag 0

Comparison: MS
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(0(x1)) = x1   
POL(1(x1)) = x1   
POL(OPP(x1)) = 1   
POL(j(x1)) = 1 + x1   

The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

OPP(1(x)) → OPP(x)
OPP(0(x)) → OPP(x)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


OPP(0(x)) → OPP(x)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
OPP(x0, x1)  =  OPP(x1)

Tags:
OPP has argument tags [1,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(0(x1)) = 1 + x1   
POL(1(x1)) = x1   
POL(OPP(x1)) = 1   

The following usable rules [FROCOS05] were oriented: none

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

OPP(1(x)) → OPP(x)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


OPP(1(x)) → OPP(x)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
OPP(x0, x1)  =  OPP(x1)

Tags:
OPP has argument tags [1,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(1(x1)) = 1 + x1   
POL(OPP(x1)) = 1   

The following usable rules [FROCOS05] were oriented: none

(11) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(13) TRUE

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+1(0(x), 1(y)) → +1(x, y)
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(0(x), j(y)) → +1(x, y)
+1(j(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(j(x), j(y)) → +1(+(x, y), j(#))
+1(j(x), j(y)) → +1(x, y)
+1(1(x), j(y)) → +1(x, y)
+1(j(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(15) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


+1(0(x), 1(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(0(x), j(y)) → +1(x, y)
+1(j(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(j(x), j(y)) → +1(+(x, y), j(#))
+1(j(x), j(y)) → +1(x, y)
+1(1(x), j(y)) → +1(x, y)
+1(j(x), 1(y)) → +1(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+1(x0, x1, x2)  =  +1(x0, x2)

Tags:
+1 has argument tags [0,3,2] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 0   
POL(+(x1, x2)) = x1 + x2   
POL(+1(x1, x2)) = 1 + x1 + x2   
POL(0(x1)) = x1   
POL(1(x1)) = 1 + x1   
POL(j(x1)) = 1 + x1   

The following usable rules [FROCOS05] were oriented:

+(#, 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(#) → #

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+1(0(x), 0(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(17) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


+1(0(x), 0(y)) → +1(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+1(x0, x1, x2)  =  +1(x1)

Tags:
+1 has argument tags [0,2,3] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 0   
POL(+(x1, x2)) = x1 + x2   
POL(+1(x1, x2)) = x1 + x2   
POL(0(x1)) = 1 + x1   
POL(1(x1)) = 1 + x1   
POL(j(x1)) = 1 + x1   

The following usable rules [FROCOS05] were oriented:

+(#, 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(#) → #

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+1(x0, x1, x2)  =  +1(x1)

Tags:
+1 has argument tags [0,3,3] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 0   
POL(+(x1, x2)) = 1 + x1 + x2   
POL(+1(x1, x2)) = x2   
POL(0(x1)) = 1   
POL(1(x1)) = 0   
POL(j(x1)) = 0   

The following usable rules [FROCOS05] were oriented:

+(#, 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(#) → #

(20) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(22) TRUE

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

*1(1(x), y) → *1(x, y)
*1(0(x), y) → *1(x, y)
*1(j(x), y) → *1(x, y)
*1(*(x, y), z) → *1(x, *(y, z))
*1(*(x, y), z) → *1(y, z)
*1(+(x, y), z) → *1(x, z)
*1(+(x, y), z) → *1(y, z)
*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(24) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


*1(1(x), y) → *1(x, y)
*1(*(x, y), z) → *1(x, *(y, z))
*1(*(x, y), z) → *1(y, z)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
*1(x0, x1, x2)  =  *1(x1)

Tags:
*1 has argument tags [2,0,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 0   
POL(*(x1, x2)) = 1 + x1 + x2   
POL(*1(x1, x2)) = 1   
POL(+(x1, x2)) = x1 + x2   
POL(-(x1, x2)) = 0   
POL(0(x1)) = x1   
POL(1(x1)) = 1 + x1   
POL(j(x1)) = x1   
POL(opp(x1)) = 1   

The following usable rules [FROCOS05] were oriented: none

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

*1(0(x), y) → *1(x, y)
*1(j(x), y) → *1(x, y)
*1(+(x, y), z) → *1(x, z)
*1(+(x, y), z) → *1(y, z)
*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


*1(0(x), y) → *1(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
*1(x0, x1, x2)  =  *1(x1)

Tags:
*1 has argument tags [0,1,2] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(*1(x1, x2)) = 1   
POL(+(x1, x2)) = x1 + x2   
POL(0(x1)) = 1 + x1   
POL(j(x1)) = x1   

The following usable rules [FROCOS05] were oriented: none

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

*1(j(x), y) → *1(x, y)
*1(+(x, y), z) → *1(x, z)
*1(+(x, y), z) → *1(y, z)
*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(28) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


*1(j(x), y) → *1(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
*1(x0, x1, x2)  =  *1(x1)

Tags:
*1 has argument tags [3,2,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(*1(x1, x2)) = 1   
POL(+(x1, x2)) = x1 + x2   
POL(j(x1)) = 1 + x1   

The following usable rules [FROCOS05] were oriented: none

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

*1(+(x, y), z) → *1(x, z)
*1(+(x, y), z) → *1(y, z)
*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(30) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


*1(+(x, y), z) → *1(x, z)
*1(+(x, y), z) → *1(y, z)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
*1(x0, x1, x2)  =  *1(x1)

Tags:
*1 has argument tags [2,2,2] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(*1(x1, x2)) = x1 + x2   
POL(+(x1, x2)) = 1 + x1 + x2   

The following usable rules [FROCOS05] were oriented: none

(31) Obligation:

Q DP problem:
The TRS P consists of the following rules:

*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(32) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
*1(x0, x1, x2)  =  *1(x2)

Tags:
*1 has argument tags [0,2,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(*1(x1, x2)) = x1   
POL(+(x1, x2)) = 1 + x1 + x2   

The following usable rules [FROCOS05] were oriented: none

(33) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(34) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(35) TRUE