YES

The TRS could be proven terminating. The proof took 2353 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (750ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (792ms).
 |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (365ms).
 |    |    | – Problem 6 was processed with processor PolynomialLinearRange4iUR (157ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

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

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, opp, *, +, j, -

Strategy

The following SCCs where found

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

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

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

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, opp, *, +, j, -

Strategy

Polynomial Interpretation

Improved Usable rules

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

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

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

Problem 5: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

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

Original Signature

Termination of terms over the following signature is verified: #, 1, opp, 0, *, +, j, -

Strategy

Polynomial Interpretation

Improved Usable rules

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

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

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

Problem 6: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

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

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, opp, *, +, j, -

Strategy

Polynomial Interpretation

Improved Usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

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

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

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

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, opp, *, +, j, -

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

opp#(j(x)) → opp#(x)opp#(0(x)) → opp#(x)
opp#(1(x)) → opp#(x)

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

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, opp, *, +, j, -

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

opp#(j(x)) → opp#(x)opp#(0(x)) → opp#(x)
opp#(1(x)) → opp#(x)