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))
↳ QTRS
↳ DependencyPairsProof
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))
+1(0(x), 0(y)) → 01(+(x, y))
*1(j(x), y) → *1(x, y)
+1(j(x), 0(y)) → +1(x, y)
+1(0(x), j(y)) → +1(x, y)
*1(0(x), y) → 01(*(x, y))
+1(1(x), j(y)) → +1(x, y)
+1(j(x), 1(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(x, y)
OPP(j(x)) → OPP(x)
*1(1(x), y) → +1(0(*(x, y)), y)
+1(j(x), j(y)) → +1(x, y)
*1(1(x), y) → 01(*(x, y))
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
-1(x, y) → +1(x, opp(y))
+1(j(x), 1(y)) → 01(+(x, y))
+1(1(x), j(y)) → 01(+(x, y))
*1(0(x), y) → *1(x, y)
OPP(0(x)) → 01(opp(x))
OPP(0(x)) → OPP(x)
+1(+(x, y), z) → +1(y, z)
OPP(1(x)) → OPP(x)
*1(j(x), y) → -1(0(*(x, y)), y)
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(0(x), 1(y)) → +1(x, y)
-1(x, y) → OPP(y)
*1(*(x, y), z) → *1(y, z)
+1(+(x, y), z) → +1(x, +(y, z))
*1(*(x, y), z) → *1(x, *(y, z))
+1(j(x), j(y)) → +1(+(x, y), j(#))
*1(j(x), y) → 01(*(x, y))
*1(1(x), y) → *1(x, y)
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))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
+1(0(x), 0(y)) → 01(+(x, y))
*1(j(x), y) → *1(x, y)
+1(j(x), 0(y)) → +1(x, y)
+1(0(x), j(y)) → +1(x, y)
*1(0(x), y) → 01(*(x, y))
+1(1(x), j(y)) → +1(x, y)
+1(j(x), 1(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(x, y)
OPP(j(x)) → OPP(x)
*1(1(x), y) → +1(0(*(x, y)), y)
+1(j(x), j(y)) → +1(x, y)
*1(1(x), y) → 01(*(x, y))
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
-1(x, y) → +1(x, opp(y))
+1(j(x), 1(y)) → 01(+(x, y))
+1(1(x), j(y)) → 01(+(x, y))
*1(0(x), y) → *1(x, y)
OPP(0(x)) → 01(opp(x))
OPP(0(x)) → OPP(x)
+1(+(x, y), z) → +1(y, z)
OPP(1(x)) → OPP(x)
*1(j(x), y) → -1(0(*(x, y)), y)
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(0(x), 1(y)) → +1(x, y)
-1(x, y) → OPP(y)
*1(*(x, y), z) → *1(y, z)
+1(+(x, y), z) → +1(x, +(y, z))
*1(*(x, y), z) → *1(x, *(y, z))
+1(j(x), j(y)) → +1(+(x, y), j(#))
*1(j(x), y) → 01(*(x, y))
*1(1(x), y) → *1(x, y)
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))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
OPP(0(x)) → OPP(x)
OPP(j(x)) → OPP(x)
OPP(1(x)) → OPP(x)
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
OPP(0(x)) → OPP(x)
OPP(j(x)) → OPP(x)
OPP(1(x)) → OPP(x)
The value of delta used in the strict ordering is 16.
POL(1(x1)) = 4 + (3)x_1
POL(j(x1)) = 4 + (4)x_1
POL(0(x1)) = 4 + (4)x_1
POL(OPP(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
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))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
+1(0(x), j(y)) → +1(x, y)
+1(j(x), 0(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(y, z)
+1(1(x), 1(y)) → +1(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(j(x), j(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(j(x), j(y)) → +1(+(x, y), j(#))
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(0(x), j(y)) → +1(x, y)
+1(j(x), 0(y)) → +1(x, y)
+1(1(x), j(y)) → +1(x, y)
+1(j(x), 1(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(x, y)
+1(0(x), 1(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(j(x), j(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(j(x), j(y)) → +1(+(x, y), j(#))
Used ordering: Polynomial interpretation [25,35]:
+1(+(x, y), z) → +1(y, z)
+1(0(x), 0(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
The value of delta used in the strict ordering is 2.
POL(1(x1)) = 2 + x_1
POL(j(x1)) = 2 + x_1
POL(0(x1)) = x_1
POL(+1(x1, x2)) = x_1 + x_2
POL(+(x1, x2)) = x_1 + x_2
POL(#) = 0
+(#, x) → x
+(x, #) → x
0(#) → #
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
+1(0(x), 0(y)) → +1(x, y)
+1(+(x, y), z) → +1(y, z)
+1(+(x, y), z) → +1(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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(0(x), 0(y)) → +1(x, y)
Used ordering: Polynomial interpretation [25,35]:
+1(+(x, y), z) → +1(y, z)
+1(+(x, y), z) → +1(x, +(y, z))
The value of delta used in the strict ordering is 2.
POL(1(x1)) = 1
POL(j(x1)) = 3 + (4)x_1
POL(0(x1)) = 2 + (4)x_1
POL(+1(x1, x2)) = x_1
POL(+(x1, x2)) = (4)x_1 + (2)x_2
POL(#) = 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
+1(+(x, y), z) → +1(y, z)
+1(+(x, y), z) → +1(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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(+(x, y), z) → +1(y, z)
+1(+(x, y), z) → +1(x, +(y, z))
The value of delta used in the strict ordering is 8.
POL(1(x1)) = 0
POL(j(x1)) = 4 + x_1
POL(0(x1)) = 2
POL(+1(x1, x2)) = (2)x_1
POL(+(x1, x2)) = 4 + (4)x_1 + x_2
POL(#) = 1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
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))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
*1(j(x), y) → *1(x, y)
*1(*(x, y), z) → *1(y, z)
*1(*(x, y), z) → *1(x, *(y, z))
*1(0(x), y) → *1(x, y)
*1(1(x), y) → *1(x, y)
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
*1(j(x), y) → *1(x, y)
*1(*(x, y), z) → *1(y, z)
*1(*(x, y), z) → *1(x, *(y, z))
*1(0(x), y) → *1(x, y)
*1(1(x), y) → *1(x, y)
The value of delta used in the strict ordering is 1.
POL(1(x1)) = 4 + x_1
POL(j(x1)) = 2 + x_1
POL(*1(x1, x2)) = x_1
POL(opp(x1)) = 0
POL(-(x1, x2)) = 2 + (3)x_2
POL(*(x1, x2)) = 3 + (4)x_1 + (2)x_2
POL(0(x1)) = 1 + (4)x_1
POL(+(x1, x2)) = 2 + (3)x_1
POL(#) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
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))