YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (5ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (141ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

quot#(s(x), s(y))minus#(x, y)quot#(s(x), s(y))quot#(minus(x, y), s(y))
minus#(s(x), s(y))minus#(x, y)

Rewrite Rules

minus(x, 0)xminus(s(x), s(y))minus(x, y)
quot(0, s(y))0quot(s(x), s(y))s(quot(minus(x, y), s(y)))

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, quot

Strategy


The following SCCs where found

quot#(s(x), s(y)) → quot#(minus(x, y), s(y))

minus#(s(x), s(y)) → minus#(x, y)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

quot#(s(x), s(y))quot#(minus(x, y), s(y))

Rewrite Rules

minus(x, 0)xminus(s(x), s(y))minus(x, y)
quot(0, s(y))0quot(s(x), s(y))s(quot(minus(x, y), s(y)))

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, quot

Strategy


Polynomial Interpretation

Improved Usable rules

minus(s(x), s(y))minus(x, y)minus(x, 0)x

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

quot#(s(x), s(y))quot#(minus(x, y), s(y))

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

minus#(s(x), s(y))minus#(x, y)

Rewrite Rules

minus(x, 0)xminus(s(x), s(y))minus(x, y)
quot(0, s(y))0quot(s(x), s(y))s(quot(minus(x, y), s(y)))

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, quot

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

minus#(s(x), s(y))minus#(x, y)