YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (3ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (125ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4iUR (52ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

g#(c(x, s(y))) → g#(c(s(x), y))f#(c(s(x), y)) → f#(c(x, s(y)))

Rewrite Rules

f(c(s(x), y)) → f(c(x, s(y)))g(c(x, s(y))) → g(c(s(x), y))

Original Signature

Termination of terms over the following signature is verified: f, g, s, c

Strategy

The following SCCs where found

g#(c(x, s(y))) → g#(c(s(x), y))
f#(c(s(x), y)) → f#(c(x, s(y)))

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

g#(c(x, s(y))) → g#(c(s(x), y))

Rewrite Rules

f(c(s(x), y)) → f(c(x, s(y)))g(c(x, s(y))) → g(c(s(x), y))

Original Signature

Termination of terms over the following signature is verified: f, g, s, c

Strategy

Polynomial Interpretation

There are no usable rules

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

g#(c(x, s(y))) → g#(c(s(x), y))

Problem 3: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

f#(c(s(x), y)) → f#(c(x, s(y)))

Rewrite Rules

f(c(s(x), y)) → f(c(x, s(y)))g(c(x, s(y))) → g(c(s(x), y))

Original Signature

Termination of terms over the following signature is verified: f, g, s, c

Strategy

Polynomial Interpretation

There are no usable rules

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

f#(c(s(x), y)) → f#(c(x, s(y)))