YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(g(X))mark#(X)mark#(f(X))a__f#(mark(X))
mark#(f(X))mark#(X)

Rewrite Rules

a__f(f(a))c(f(g(f(a))))mark(f(X))a__f(mark(X))
mark(a)amark(c(X))c(X)
mark(g(X))g(mark(X))a__f(X)f(X)

Original Signature

Termination of terms over the following signature is verified: f, g, c, a, mark, a__f

Strategy


The following SCCs where found

mark#(g(X)) → mark#(X)mark#(f(X)) → mark#(X)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

mark#(g(X))mark#(X)mark#(f(X))mark#(X)

Rewrite Rules

a__f(f(a))c(f(g(f(a))))mark(f(X))a__f(mark(X))
mark(a)amark(c(X))c(X)
mark(g(X))g(mark(X))a__f(X)f(X)

Original Signature

Termination of terms over the following signature is verified: f, g, c, a, mark, a__f

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

mark#(g(X))mark#(X)mark#(f(X))mark#(X)