YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (716ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (417ms).
 |    | – Problem 8 was processed with processor PolynomialLinearRange4iUR (176ms).
 |    |    | – Problem 9 was processed with processor PolynomialLinearRange4iUR (120ms).
 |    |    |    | – Problem 10 was processed with processor PolynomialLinearRange4iUR (122ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (36ms).
 |    | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 | – Problem 6 was processed with processor SubtermCriterion (22ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Original Signature

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

Strategy


The following SCCs where found

sum#(app(l1, l2)) → sum#(l1)sum#(cons(x, l)) → sum#(l)
sum#(app(l1, l2)) → sum#(l2)

app#(cons(x, l1), l2) → app#(l1, l2)

prod#(cons(x, l)) → prod#(l)prod#(app(l1, l2)) → prod#(l1)
prod#(app(l1, l2)) → prod#(l2)

+#(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))

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

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

Original Signature

Termination of terms over the following signature is verified: #, app, 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 8: 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))
*(x, +(y, z))+(*(x, y), *(x, z))app(nil, l)l
app(cons(x, l1), l2)cons(x, app(l1, l2))sum(nil)0(#)
sum(cons(x, l))+(x, sum(l))sum(app(l1, l2))+(sum(l1), sum(l2))
prod(nil)1(#)prod(cons(x, l))*(x, prod(l))
prod(app(l1, l2))*(prod(l1), prod(l2))

Original Signature

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

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 9: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Original Signature

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

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

Original Signature

Termination of terms over the following signature is verified: app, #, 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 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

prod#(cons(x, l))prod#(l)prod#(app(l1, l2))prod#(l1)
prod#(app(l1, l2))prod#(l2)

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

Original Signature

Termination of terms over the following signature is verified: #, app, 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)prod#(app(l1, l2))prod#(l1)
prod#(app(l1, l2))prod#(l2)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Original Signature

Termination of terms over the following signature is verified: #, app, 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)

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

Original Signature

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

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



Dependency Pair Problem

Dependency Pairs

app#(cons(x, l1), l2)app#(l1, l2)

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

Original Signature

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

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

app#(cons(x, l1), l2)app#(l1, l2)

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

sum#(app(l1, l2))sum#(l1)sum#(cons(x, l))sum#(l)
sum#(app(l1, l2))sum#(l2)

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

Original Signature

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

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

sum#(app(l1, l2))sum#(l1)sum#(cons(x, l))sum#(l)
sum#(app(l1, l2))sum#(l2)