YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (16ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (609ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(g(x), g(y))p#(f(g(x), s(y)))f#(g(x), g(y))f#(g(x), s(y))
f#(g(x), g(y))f#(p(f(g(x), s(y))), g(s(p(x))))f#(g(x), g(y))g#(s(p(x)))
f#(g(x), g(y))g#(x)g#(s(p(x)))p#(x)
p#(0)g#(0)f#(g(x), g(y))p#(x)

Rewrite Rules

f(g(x), g(y))f(p(f(g(x), s(y))), g(s(p(x))))p(0)g(0)
g(s(p(x)))p(x)

Original Signature

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

Strategy


The following SCCs where found

f#(g(x), g(y)) → f#(p(f(g(x), s(y))), g(s(p(x))))

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

f#(g(x), g(y))f#(p(f(g(x), s(y))), g(s(p(x))))

Rewrite Rules

f(g(x), g(y))f(p(f(g(x), s(y))), g(s(p(x))))p(0)g(0)
g(s(p(x)))p(x)

Original Signature

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

Strategy


Polynomial Interpretation

Improved Usable rules

p(0)g(0)g(s(p(x)))p(x)
f(g(x), g(y))f(p(f(g(x), s(y))), g(s(p(x))))

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

f#(g(x), g(y))f#(p(f(g(x), s(y))), g(s(p(x))))