YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (3ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (79ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(s(0))f#(p(s(0)))T(f(s(0)))f#(s(0))
f#(s(0))p#(s(0))

Rewrite Rules

f(0)cons(0, f(s(0)))f(s(0))f(p(s(0)))
p(s(0))0

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = ∅
μ(f) = μ(f#) = μ(p#) = μ(s) = μ(p) = μ(cons) = {1}


The following SCCs where found

f#(s(0)) → f#(p(s(0)))

Problem 2: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

f#(s(0))f#(p(s(0)))

Rewrite Rules

f(0)cons(0, f(s(0)))f(s(0))f(p(s(0)))
p(s(0))0

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = ∅
μ(f) = μ(f#) = μ(p#) = μ(s) = μ(p) = μ(cons) = {1}


Polynomial Interpretation

Standard Usable rules

p(s(0))0

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

f#(s(0))f#(p(s(0)))