YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (5ms).
 | – Problem 2 was processed with processor PolynomialOrderingProcessor (118ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(s(x))p#(s(x))f#(s(x))f#(p(s(x)))

Rewrite Rules

f(s(x))s(s(f(p(s(x)))))f(0)0
p(s(x))x

Original Signature

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

Strategy


The following SCCs where found

f#(s(x)) → f#(p(s(x)))

Problem 2: PolynomialOrderingProcessor



Dependency Pair Problem

Dependency Pairs

f#(s(x))f#(p(s(x)))

Rewrite Rules

f(s(x))s(s(f(p(s(x)))))f(0)0
p(s(x))x

Original Signature

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

Strategy


Polynomial Interpretation

Improved Usable rules

p(s(x))x

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

f#(s(x))f#(p(s(x)))