YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (73ms).
 | – Problem 2 was processed with processor SubtermCriterion (12ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

minus#(p(x))s#(minus(x))*#(p(x), y)minus#(y)
*#(p(x), y)+#(*(x, y), minus(y))+#(p(x), y)+#(x, y)
+#(s(x), y)s#(+(x, y))+#(s(x), y)+#(x, y)
minus#(p(x))minus#(x)*#(s(x), y)*#(x, y)
*#(s(x), y)+#(*(x, y), y)+#(p(x), y)p#(+(x, y))
minus#(s(x))minus#(x)*#(p(x), y)*#(x, y)
minus#(s(x))p#(minus(x))

Rewrite Rules

p(s(x))xs(p(x))x
+(0, y)y+(s(x), y)s(+(x, y))
+(p(x), y)p(+(x, y))minus(0)0
minus(s(x))p(minus(x))minus(p(x))s(minus(x))
*(0, y)0*(s(x), y)+(*(x, y), y)
*(p(x), y)+(*(x, y), minus(y))

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, p, *, +

Strategy


The following SCCs where found

+#(p(x), y) → +#(x, y)+#(s(x), y) → +#(x, y)

minus#(p(x)) → minus#(x)minus#(s(x)) → minus#(x)

*#(s(x), y) → *#(x, y)*#(p(x), y) → *#(x, y)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

*#(s(x), y)*#(x, y)*#(p(x), y)*#(x, y)

Rewrite Rules

p(s(x))xs(p(x))x
+(0, y)y+(s(x), y)s(+(x, y))
+(p(x), y)p(+(x, y))minus(0)0
minus(s(x))p(minus(x))minus(p(x))s(minus(x))
*(0, y)0*(s(x), y)+(*(x, y), y)
*(p(x), y)+(*(x, y), minus(y))

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, p, *, +

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

*#(s(x), y)*#(x, y)*#(p(x), y)*#(x, y)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

minus#(p(x))minus#(x)minus#(s(x))minus#(x)

Rewrite Rules

p(s(x))xs(p(x))x
+(0, y)y+(s(x), y)s(+(x, y))
+(p(x), y)p(+(x, y))minus(0)0
minus(s(x))p(minus(x))minus(p(x))s(minus(x))
*(0, y)0*(s(x), y)+(*(x, y), y)
*(p(x), y)+(*(x, y), minus(y))

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, p, *, +

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

minus#(p(x))minus#(x)minus#(s(x))minus#(x)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

+#(p(x), y)+#(x, y)+#(s(x), y)+#(x, y)

Rewrite Rules

p(s(x))xs(p(x))x
+(0, y)y+(s(x), y)s(+(x, y))
+(p(x), y)p(+(x, y))minus(0)0
minus(s(x))p(minus(x))minus(p(x))s(minus(x))
*(0, y)0*(s(x), y)+(*(x, y), y)
*(p(x), y)+(*(x, y), minus(y))

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, p, *, +

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

+#(p(x), y)+#(x, y)+#(s(x), y)+#(x, y)