YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (41ms).
 | – Problem 2 was processed with processor PolynomialOrderingProcessor (615ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor PolynomialOrderingProcessor (82ms).
 | – Problem 5 was processed with processor PolynomialOrderingProcessor (140ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

times#(s(x), y)plus#(y, times(p(s(x)), y))fac#(s(x), y)times#(s(x), y)
plus#(s(x), y)plus#(p(s(x)), y)times#(s(x), y)p#(s(x))
times#(s(x), y)times#(p(s(x)), y)fac#(s(x), y)p#(s(x))
factorial#(x)fac#(x, s(0))plus#(s(x), y)p#(s(x))
p#(s(s(x)))p#(s(x))fac#(s(x), y)fac#(p(s(x)), times(s(x), y))

Rewrite Rules

plus(0, x)xplus(s(x), y)s(plus(p(s(x)), y))
times(0, y)0times(s(x), y)plus(y, times(p(s(x)), y))
p(s(0))0p(s(s(x)))s(p(s(x)))
fac(0, x)xfac(s(x), y)fac(p(s(x)), times(s(x), y))
factorial(x)fac(x, s(0))

Original Signature

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

Strategy


The following SCCs where found

plus#(s(x), y) → plus#(p(s(x)), y)

times#(s(x), y) → times#(p(s(x)), y)

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

fac#(s(x), y) → fac#(p(s(x)), times(s(x), y))

Problem 2: PolynomialOrderingProcessor



Dependency Pair Problem

Dependency Pairs

fac#(s(x), y)fac#(p(s(x)), times(s(x), y))

Rewrite Rules

plus(0, x)xplus(s(x), y)s(plus(p(s(x)), y))
times(0, y)0times(s(x), y)plus(y, times(p(s(x)), y))
p(s(0))0p(s(s(x)))s(p(s(x)))
fac(0, x)xfac(s(x), y)fac(p(s(x)), times(s(x), y))
factorial(x)fac(x, s(0))

Original Signature

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

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), y)fac#(p(s(x)), times(s(x), y))

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

plus(0, x)xplus(s(x), y)s(plus(p(s(x)), y))
times(0, y)0times(s(x), y)plus(y, times(p(s(x)), y))
p(s(0))0p(s(s(x)))s(p(s(x)))
fac(0, x)xfac(s(x), y)fac(p(s(x)), times(s(x), y))
factorial(x)fac(x, s(0))

Original Signature

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

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: PolynomialOrderingProcessor



Dependency Pair Problem

Dependency Pairs

times#(s(x), y)times#(p(s(x)), y)

Rewrite Rules

plus(0, x)xplus(s(x), y)s(plus(p(s(x)), y))
times(0, y)0times(s(x), y)plus(y, times(p(s(x)), y))
p(s(0))0p(s(s(x)))s(p(s(x)))
fac(0, x)xfac(s(x), y)fac(p(s(x)), times(s(x), y))
factorial(x)fac(x, s(0))

Original Signature

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

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:

times#(s(x), y)times#(p(s(x)), y)

Problem 5: PolynomialOrderingProcessor



Dependency Pair Problem

Dependency Pairs

plus#(s(x), y)plus#(p(s(x)), y)

Rewrite Rules

plus(0, x)xplus(s(x), y)s(plus(p(s(x)), y))
times(0, y)0times(s(x), y)plus(y, times(p(s(x)), y))
p(s(0))0p(s(s(x)))s(p(s(x)))
fac(0, x)xfac(s(x), y)fac(p(s(x)), times(s(x), y))
factorial(x)fac(x, s(0))

Original Signature

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

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:

plus#(s(x), y)plus#(p(s(x)), y)