YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (57ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 was processed with processor PolynomialLinearRange4iUR (647ms).
 |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (418ms).
 |    |    | – Problem 6 was processed with processor DependencyGraph (1ms).
 |    |    |    | – Problem 7 was processed with processor PolynomialLinearRange4iUR (38ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Strategy


The following SCCs where found

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

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

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

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

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Strategy


Polynomial Interpretation

Improved Usable rules

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

Rewrite Rules

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

Strategy


The following SCCs where found

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

Problem 7: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

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:

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