YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (490ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (32ms).
 |    | – Problem 5 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 was processed with processor PolynomialLinearRange4iUR (785ms).
 |    | – Problem 6 was processed with processor PolynomialLinearRange4iUR (257ms).
 |    |    | – Problem 7 was processed with processor PolynomialLinearRange4iUR (155ms).

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

Original Signature

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

Strategy

The following SCCs where found

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

Problem 2: 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))*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, 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)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

*#(x, +(y, z)) → *#(x, z)*#(+(x, y), z) → *#(x, z)
*#(1(x), y) → *#(x, y)*#(*(x, y), z) → *#(y, z)
*#(*(x, y), z) → *#(x, *(y, z))*#(j(x), y) → *#(x, y)
*#(x, +(y, z)) → *#(x, y)*#(+(x, y), z) → *#(y, z)
*#(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))*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, 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:

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

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

*#(x, +(y, z)) → *#(x, z)*#(x, +(y, z)) → *#(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))*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))

Original Signature

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

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: 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))*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, 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 6: 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))*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, 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 7: 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))*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, 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))