YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (79ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (277ms).
 |    | – Problem 5 was processed with processor DependencyGraph (9ms).
 |    |    | – Problem 6 was processed with processor PolynomialLinearRange4iUR (202ms).
 |    |    |    | – Problem 7 was processed with processor DependencyGraph (23ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(c)mark(f(g(c)))active(f(g(X)))mark(g(X))
mark(c)active(c)mark(f(X))active(f(X))
mark(g(X))active(g(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, c, active, mark

Strategy


The following SCCs where found

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

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

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

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(c)mark(f(g(c)))active(f(g(X)))mark(g(X))
mark(c)active(c)mark(f(X))active(f(X))
mark(g(X))active(g(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, c, 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#(c)mark#(f(g(c)))

Problem 5: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(c)mark(f(g(c)))active(f(g(X)))mark(g(X))
mark(c)active(c)mark(f(X))active(f(X))
mark(g(X))active(g(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, c, active, mark

Strategy


The following SCCs where found

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

Problem 6: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(c)mark(f(g(c)))active(f(g(X)))mark(g(X))
mark(c)active(c)mark(f(X))active(f(X))
mark(g(X))active(g(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, c, 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:

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

Problem 7: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(c)mark(f(g(c)))active(f(g(X)))mark(g(X))
mark(c)active(c)mark(f(X))active(f(X))
mark(g(X))active(g(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, c, active, mark

Strategy


There are no SCCs!

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(c)mark(f(g(c)))active(f(g(X)))mark(g(X))
mark(c)active(c)mark(f(X))active(f(X))
mark(g(X))active(g(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, c, 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)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(c)mark(f(g(c)))active(f(g(X)))mark(g(X))
mark(c)active(c)mark(f(X))active(f(X))
mark(g(X))active(g(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, c, 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)