MAYBE

The TRS could not be proven terminating. The proof attempt took 1784 ms.

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (0ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (0ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4iUR (0ms).
 |    |    | – Problem 4 remains open; application of the following processors failed [DependencyGraph (1ms), PolynomialLinearRange4iUR (43ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (224ms), DependencyGraph (0ms), ReductionPairSAT (568ms), DependencyGraph (1ms), SizeChangePrinciple (52ms)].

The following open problems remain:



Open Dependency Pair Problem 4

Dependency Pairs

*#(x, +(y, f(z)))*#(g(x, z), +(y, y))

Rewrite Rules

*(*(x, y), z)*(x, *(y, z))*(+(x, y), z)+(*(x, z), *(y, z))
*(x, +(y, f(z)))*(g(x, z), +(y, y))

Original Signature

Termination of terms over the following signature is verified: f, g, *, +


Problem 1: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

*#(+(x, y), z)*#(x, z)*#(*(x, y), z)*#(x, *(y, z))
*#(*(x, y), z)*#(y, z)*#(+(x, y), z)*#(y, z)
*#(x, +(y, f(z)))*#(g(x, z), +(y, y))

Rewrite Rules

*(*(x, y), z)*(x, *(y, z))*(+(x, y), z)+(*(x, z), *(y, z))
*(x, +(y, f(z)))*(g(x, z), +(y, y))

Original Signature

Termination of terms over the following signature is verified: f, g, *, +

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

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

*#(*(x, y), z)*#(y, z)*#(*(x, y), z)*#(x, *(y, z))
*#(x, +(y, f(z)))*#(g(x, z), +(y, y))

Rewrite Rules

*(*(x, y), z)*(x, *(y, z))*(+(x, y), z)+(*(x, z), *(y, z))
*(x, +(y, f(z)))*(g(x, z), +(y, y))

Original Signature

Termination of terms over the following signature is verified: f, g, *, +

Strategy


Polynomial Interpretation

Improved Usable rules

*(+(x, y), z)+(*(x, z), *(y, z))*(x, +(y, f(z)))*(g(x, z), +(y, y))
*(*(x, y), z)*(x, *(y, z))

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



Dependency Pair Problem

Dependency Pairs

*#(*(x, y), z)*#(x, *(y, z))*#(x, +(y, f(z)))*#(g(x, z), +(y, y))

Rewrite Rules

*(*(x, y), z)*(x, *(y, z))*(+(x, y), z)+(*(x, z), *(y, z))
*(x, +(y, f(z)))*(g(x, z), +(y, y))

Original Signature

Termination of terms over the following signature is verified: f, g, *, +

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