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