YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(p(X))a__p#(mark(X))mark#(p(X))mark#(X)
mark#(cons(X1, X2))mark#(X1)mark#(f(X))a__f#(mark(X))
mark#(s(X))mark#(X)mark#(f(X))mark#(X)
a__f#(s(0))a__p#(s(0))a__f#(s(0))a__f#(a__p(s(0)))

Rewrite Rules

a__f(0)cons(0, f(s(0)))a__f(s(0))a__f(a__p(s(0)))
a__p(s(0))0mark(f(X))a__f(mark(X))
mark(p(X))a__p(mark(X))mark(0)0
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__f(X)f(X)a__p(X)p(X)

Original Signature

Termination of terms over the following signature is verified: f, 0, s, a__p, p, mark, a__f, cons

Strategy


The following SCCs where found

mark#(p(X)) → mark#(X)mark#(cons(X1, X2)) → mark#(X1)
mark#(s(X)) → mark#(X)mark#(f(X)) → mark#(X)

a__f#(s(0)) → a__f#(a__p(s(0)))

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

mark#(p(X))mark#(X)mark#(cons(X1, X2))mark#(X1)
mark#(s(X))mark#(X)mark#(f(X))mark#(X)

Rewrite Rules

a__f(0)cons(0, f(s(0)))a__f(s(0))a__f(a__p(s(0)))
a__p(s(0))0mark(f(X))a__f(mark(X))
mark(p(X))a__p(mark(X))mark(0)0
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__f(X)f(X)a__p(X)p(X)

Original Signature

Termination of terms over the following signature is verified: f, 0, s, a__p, p, mark, a__f, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

mark#(p(X))mark#(X)mark#(cons(X1, X2))mark#(X1)
mark#(s(X))mark#(X)mark#(f(X))mark#(X)

Problem 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

a__f#(s(0))a__f#(a__p(s(0)))

Rewrite Rules

a__f(0)cons(0, f(s(0)))a__f(s(0))a__f(a__p(s(0)))
a__p(s(0))0mark(f(X))a__f(mark(X))
mark(p(X))a__p(mark(X))mark(0)0
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__f(X)f(X)a__p(X)p(X)

Original Signature

Termination of terms over the following signature is verified: f, 0, s, a__p, p, mark, a__f, cons

Strategy


Polynomial Interpretation

Improved Usable rules

a__p(X)p(X)a__p(s(0))0

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

a__f#(s(0))a__f#(a__p(s(0)))