YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (10ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (223ms).
 |    | – Problem 3 was processed with processor DependencyGraph (1ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (152ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

a__tail#(cons(X, XS))mark#(XS)mark#(tail(X))mark#(X)
mark#(zeros)a__zeros#mark#(cons(X1, X2))mark#(X1)
mark#(tail(X))a__tail#(mark(X))

Rewrite Rules

a__zeroscons(0, zeros)a__tail(cons(X, XS))mark(XS)
mark(zeros)a__zerosmark(tail(X))a__tail(mark(X))
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
a__zeroszerosa__tail(X)tail(X)

Original Signature

Termination of terms over the following signature is verified: a__zeros, 0, zeros, mark, tail, cons, a__tail

Strategy


The following SCCs where found

a__tail#(cons(X, XS)) → mark#(XS)mark#(tail(X)) → mark#(X)
mark#(cons(X1, X2)) → mark#(X1)mark#(tail(X)) → a__tail#(mark(X))

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

a__tail#(cons(X, XS))mark#(XS)mark#(tail(X))mark#(X)
mark#(cons(X1, X2))mark#(X1)mark#(tail(X))a__tail#(mark(X))

Rewrite Rules

a__zeroscons(0, zeros)a__tail(cons(X, XS))mark(XS)
mark(zeros)a__zerosmark(tail(X))a__tail(mark(X))
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
a__zeroszerosa__tail(X)tail(X)

Original Signature

Termination of terms over the following signature is verified: a__zeros, 0, zeros, mark, tail, cons, a__tail

Strategy


Polynomial Interpretation

Improved Usable rules

mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
mark(tail(X))a__tail(mark(X))a__tail(X)tail(X)
a__zeroscons(0, zeros)a__zeroszeros
mark(zeros)a__zerosa__tail(cons(X, XS))mark(XS)

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

mark#(tail(X))mark#(X)mark#(tail(X))a__tail#(mark(X))

Problem 3: DependencyGraph



Dependency Pair Problem

Dependency Pairs

a__tail#(cons(X, XS))mark#(XS)mark#(cons(X1, X2))mark#(X1)

Rewrite Rules

a__zeroscons(0, zeros)a__tail(cons(X, XS))mark(XS)
mark(zeros)a__zerosmark(tail(X))a__tail(mark(X))
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
a__zeroszerosa__tail(X)tail(X)

Original Signature

Termination of terms over the following signature is verified: a__zeros, 0, zeros, mark, tail, a__tail, cons

Strategy


The following SCCs where found

mark#(cons(X1, X2)) → mark#(X1)

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(cons(X1, X2))mark#(X1)

Rewrite Rules

a__zeroscons(0, zeros)a__tail(cons(X, XS))mark(XS)
mark(zeros)a__zerosmark(tail(X))a__tail(mark(X))
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
a__zeroszerosa__tail(X)tail(X)

Original Signature

Termination of terms over the following signature is verified: a__zeros, 0, zeros, mark, tail, a__tail, cons

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#(cons(X1, X2))mark#(X1)