YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

fac#(s(x))p#(s(x))fac#(s(x))fac#(p(s(x)))

Rewrite Rules

p(s(x))xfac(0)s(0)
fac(s(x))times(s(x), fac(p(s(x))))

Original Signature

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

Strategy


The following SCCs where found

fac#(s(x)) → fac#(p(s(x)))

Problem 2: PolynomialOrderingProcessor



Dependency Pair Problem

Dependency Pairs

fac#(s(x))fac#(p(s(x)))

Rewrite Rules

p(s(x))xfac(0)s(0)
fac(s(x))times(s(x), fac(p(s(x))))

Original Signature

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

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:

fac#(s(x))fac#(p(s(x)))