YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (263ms).
 | – Problem 2 was processed with processor SubtermCriterion (3ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4iUR (506ms).
 |    | – Problem 6 was processed with processor PolynomialLinearRange4iUR (210ms).
 |    |    | – Problem 7 was processed with processor PolynomialLinearRange4iUR (113ms).
 |    |    |    | – Problem 8 was processed with processor PolynomialLinearRange4iUR (141ms).
 | – Problem 4 was processed with processor SubtermCriterion (2ms).
 | – Problem 5 was processed with processor SubtermCriterion (2ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

+#(0(x), 1(y))+#(x, y)+#(1(x), 1(y))0#(+(+(x, y), 1(#)))
*#(*(x, y), z)*#(y, z)*#(*(x, y), z)*#(x, *(y, z))
+#(0(x), 0(y))+#(x, y)sum#(cons(x, l))sum#(l)
+#(+(x, y), z)+#(y, z)*#(0(x), y)0#(*(x, y))
prod#(cons(x, l))*#(x, prod(l))sum#(cons(x, l))+#(x, sum(l))
+#(1(x), 1(y))+#(+(x, y), 1(#))+#(+(x, y), z)+#(x, +(y, z))
*#(1(x), y)+#(0(*(x, y)), y)+#(0(x), 0(y))0#(+(x, y))
prod#(cons(x, l))prod#(l)*#(1(x), y)*#(x, y)
sum#(nil)0#(#)*#(1(x), y)0#(*(x, y))
+#(1(x), 1(y))+#(x, y)*#(0(x), 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))
+(1(x), 1(y))0(+(+(x, y), 1(#)))+(+(x, y), z)+(x, +(y, z))
*(#, x)#*(0(x), y)0(*(x, y))
*(1(x), y)+(0(*(x, y)), y)*(*(x, y), z)*(x, *(y, z))
sum(nil)0(#)sum(cons(x, l))+(x, sum(l))
prod(nil)1(#)prod(cons(x, l))*(x, prod(l))

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, *, +, sum, nil, cons, prod

Strategy


The following SCCs where found

prod#(cons(x, l)) → prod#(l)

sum#(cons(x, l)) → sum#(l)

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

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

sum#(cons(x, l))sum#(l)

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))
+(1(x), 1(y))0(+(+(x, y), 1(#)))+(+(x, y), z)+(x, +(y, z))
*(#, x)#*(0(x), y)0(*(x, y))
*(1(x), y)+(0(*(x, y)), y)*(*(x, y), z)*(x, *(y, z))
sum(nil)0(#)sum(cons(x, l))+(x, sum(l))
prod(nil)1(#)prod(cons(x, l))*(x, prod(l))

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, *, +, sum, nil, cons, prod

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

sum#(cons(x, l))sum#(l)

Problem 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

+#(0(x), 1(y))+#(x, y)+#(0(x), 0(y))+#(x, y)
+#(+(x, y), z)+#(y, z)+#(1(x), 1(y))+#(x, y)
+#(1(x), 1(y))+#(+(x, y), 1(#))+#(1(x), 0(y))+#(x, y)
+#(+(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))
+(1(x), 1(y))0(+(+(x, y), 1(#)))+(+(x, y), z)+(x, +(y, z))
*(#, x)#*(0(x), y)0(*(x, y))
*(1(x), y)+(0(*(x, y)), y)*(*(x, y), z)*(x, *(y, z))
sum(nil)0(#)sum(cons(x, l))+(x, sum(l))
prod(nil)1(#)prod(cons(x, l))*(x, prod(l))

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, *, +, sum, nil, cons, prod

Strategy


Polynomial Interpretation

Improved Usable rules

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

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

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

Problem 6: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

+#(0(x), 0(y))+#(x, y)+#(+(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))
+(1(x), 1(y))0(+(+(x, y), 1(#)))+(+(x, y), z)+(x, +(y, z))
*(#, x)#*(0(x), y)0(*(x, y))
*(1(x), y)+(0(*(x, y)), y)*(*(x, y), z)*(x, *(y, z))
sum(nil)0(#)sum(cons(x, l))+(x, sum(l))
prod(nil)1(#)prod(cons(x, l))*(x, prod(l))

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, *, sum, +, prod, cons, nil

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:

+#(0(x), 0(y))+#(x, y)

Problem 7: 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))
+(1(x), 1(y))0(+(+(x, y), 1(#)))+(+(x, y), z)+(x, +(y, z))
*(#, x)#*(0(x), y)0(*(x, y))
*(1(x), y)+(0(*(x, y)), y)*(*(x, y), z)*(x, *(y, z))
sum(nil)0(#)sum(cons(x, l))+(x, sum(l))
prod(nil)1(#)prod(cons(x, l))*(x, prod(l))

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, *, +, sum, nil, cons, prod

Strategy


Polynomial Interpretation

Improved Usable rules

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

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 8: 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))
+(1(x), 1(y))0(+(+(x, y), 1(#)))+(+(x, y), z)+(x, +(y, z))
*(#, x)#*(0(x), y)0(*(x, y))
*(1(x), y)+(0(*(x, y)), y)*(*(x, y), z)*(x, *(y, z))
sum(nil)0(#)sum(cons(x, l))+(x, sum(l))
prod(nil)1(#)prod(cons(x, l))*(x, prod(l))

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, *, sum, +, prod, cons, nil

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 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

prod#(cons(x, l))prod#(l)

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))
+(1(x), 1(y))0(+(+(x, y), 1(#)))+(+(x, y), z)+(x, +(y, z))
*(#, x)#*(0(x), y)0(*(x, y))
*(1(x), y)+(0(*(x, y)), y)*(*(x, y), z)*(x, *(y, z))
sum(nil)0(#)sum(cons(x, l))+(x, sum(l))
prod(nil)1(#)prod(cons(x, l))*(x, prod(l))

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, *, +, sum, nil, cons, prod

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

prod#(cons(x, l))prod#(l)

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

*#(1(x), y)*#(x, y)*#(*(x, y), z)*#(x, *(y, z))
*#(*(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))
+(1(x), 1(y))0(+(+(x, y), 1(#)))+(+(x, y), z)+(x, +(y, z))
*(#, x)#*(0(x), y)0(*(x, y))
*(1(x), y)+(0(*(x, y)), y)*(*(x, y), z)*(x, *(y, z))
sum(nil)0(#)sum(cons(x, l))+(x, sum(l))
prod(nil)1(#)prod(cons(x, l))*(x, prod(l))

Original Signature

Termination of terms over the following signature is verified: #, 1, 0, *, +, sum, nil, cons, prod

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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