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

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

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:

+¹(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)

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

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

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

(6) Obligation:

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

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

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

(7) Obligation:

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

*¹(1(x), y) → *¹(x, y)
*¹(0(x), y) → *¹(x, y)
*¹(j(x), y) → *¹(x, y)
*¹(*(x, y), z) → *¹(x, *(y, z))
*¹(*(x, y), z) → *¹(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))

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