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)