YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (58ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4iUR (593ms).
 |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (501ms).
 |    |    | – Problem 6 was processed with processor DependencyGraph (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

g#(mark(X))g#(X)mark#(g(X))g#(mark(X))
mark#(g(X))mark#(X)mark#(a)active#(a)
f#(active(X))f#(X)mark#(f(X))active#(f(X))
g#(active(X))g#(X)active#(f(f(a)))mark#(f(g(f(a))))
active#(f(f(a)))f#(g(f(a)))active#(f(f(a)))f#(a)
active#(f(f(a)))g#(f(a))mark#(g(X))active#(g(mark(X)))
f#(mark(X))f#(X)mark#(f(X))f#(X)

Rewrite Rules

active(f(f(a)))mark(f(g(f(a))))mark(f(X))active(f(X))
mark(a)active(a)mark(g(X))active(g(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
g(mark(X))g(X)g(active(X))g(X)

Original Signature

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

Strategy


The following SCCs where found

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

f#(active(X)) → f#(X)f#(mark(X)) → f#(X)

g#(active(X)) → g#(X)g#(mark(X)) → g#(X)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

g#(active(X))g#(X)g#(mark(X))g#(X)

Rewrite Rules

active(f(f(a)))mark(f(g(f(a))))mark(f(X))active(f(X))
mark(a)active(a)mark(g(X))active(g(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
g(mark(X))g(X)g(active(X))g(X)

Original Signature

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

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

g#(active(X))g#(X)g#(mark(X))g#(X)

Problem 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

active#(f(f(a)))mark#(f(g(f(a))))mark#(g(X))mark#(X)
mark#(g(X))active#(g(mark(X)))mark#(f(X))active#(f(X))

Rewrite Rules

active(f(f(a)))mark(f(g(f(a))))mark(f(X))active(f(X))
mark(a)active(a)mark(g(X))active(g(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
g(mark(X))g(X)g(active(X))g(X)

Original Signature

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

Strategy


Polynomial Interpretation

Improved Usable rules

g(active(X))g(X)mark(a)active(a)
active(f(f(a)))mark(f(g(f(a))))f(active(X))f(X)
mark(g(X))active(g(mark(X)))g(mark(X))g(X)
f(mark(X))f(X)mark(f(X))active(f(X))

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

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

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

active#(f(f(a)))mark#(f(g(f(a))))mark#(g(X))active#(g(mark(X)))
mark#(f(X))active#(f(X))

Rewrite Rules

active(f(f(a)))mark(f(g(f(a))))mark(f(X))active(f(X))
mark(a)active(a)mark(g(X))active(g(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
g(mark(X))g(X)g(active(X))g(X)

Original Signature

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

Strategy


Polynomial Interpretation

Improved Usable rules

g(active(X))g(X)f(active(X))f(X)
g(mark(X))g(X)f(mark(X))f(X)

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

active#(f(f(a)))mark#(f(g(f(a))))

Problem 6: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(f(f(a)))mark(f(g(f(a))))mark(f(X))active(f(X))
mark(a)active(a)mark(g(X))active(g(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
g(mark(X))g(X)g(active(X))g(X)

Original Signature

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

Strategy


There are no SCCs!

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

f#(active(X))f#(X)f#(mark(X))f#(X)

Rewrite Rules

active(f(f(a)))mark(f(g(f(a))))mark(f(X))active(f(X))
mark(a)active(a)mark(g(X))active(g(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
g(mark(X))g(X)g(active(X))g(X)

Original Signature

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

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

f#(active(X))f#(X)f#(mark(X))f#(X)