YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (4ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor PolynomialOrderingProcessor (158ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

fac(s(x)) → *(fac(p(s(x))), s(x))p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

Original Signature

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

Strategy

The following SCCs where found

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

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

fac(s(x)) → *(fac(p(s(x))), s(x))p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

Original Signature

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

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 3: PolynomialOrderingProcessor

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

fac(s(x)) → *(fac(p(s(x))), s(x))p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

Original Signature

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

Strategy

Polynomial Interpretation

Improved Usable rules

p(s(s(x))) → s(p(s(x)))p(s(0)) → 0

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)))