YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(s(X), X)f#(X, a(X))f#(X, c(X))f#(s(X), X)

Rewrite Rules

f(s(X), X)f(X, a(X))f(X, c(X))f(s(X), X)
f(X, X)c(X)

Original Signature

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

Strategy


The following SCCs where found

f#(s(X), X) → f#(X, a(X))

f#(X, c(X)) → f#(s(X), X)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

f#(X, c(X))f#(s(X), X)

Rewrite Rules

f(s(X), X)f(X, a(X))f(X, c(X))f(s(X), X)
f(X, X)c(X)

Original Signature

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

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

f#(X, c(X))f#(s(X), X)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

f#(s(X), X)f#(X, a(X))

Rewrite Rules

f(s(X), X)f(X, a(X))f(X, c(X))f(s(X), X)
f(X, X)c(X)

Original Signature

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

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

f#(s(X), X)f#(X, a(X))