YES

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

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (103ms).

Problem 1: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

p#(m, s(n), 0) → p#(0, n, m)p#(m, n, s(r)) → p#(m, r, n)

Rewrite Rules

p(m, n, s(r)) → p(m, r, n)p(m, s(n), 0) → p(0, n, m)
p(m, 0, 0) → m

Original Signature

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

Strategy

Polynomial Interpretation

There are no usable rules

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

p#(m, s(n), 0) → p#(0, n, m)p#(m, n, s(r)) → p#(m, r, n)