YES

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

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (719ms).
 | – Problem 2 was processed with processor DependencyGraph (5ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4iUR (242ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (48ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (53ms).

Problem 1: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

a__from#(X)mark#(X)mark#(first(X1, X2))mark#(X2)
mark#(from(X))a__from#(mark(X))a__first#(s(X), cons(Y, Z))mark#(Y)
mark#(first(X1, X2))a__first#(mark(X1), mark(X2))mark#(from(X))mark#(X)
mark#(cons(X1, X2))mark#(X1)mark#(first(X1, X2))mark#(X1)
mark#(s(X))mark#(X)

Rewrite Rules

a__first(0, X)nila__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))
a__from(X)cons(mark(X), from(s(X)))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(0)0
mark(nil)nilmark(s(X))s(mark(X))
mark(cons(X1, X2))cons(mark(X1), X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: 0, s, mark, from, a__first, first, a__from, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

mark(cons(X1, X2))cons(mark(X1), X2)a__first(X1, X2)first(X1, X2)
mark(0)0a__from(X)from(X)
mark(s(X))s(mark(X))a__from(X)cons(mark(X), from(s(X)))
mark(from(X))a__from(mark(X))mark(nil)nil
mark(first(X1, X2))a__first(mark(X1), mark(X2))a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))
a__first(0, X)nil

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

mark#(from(X))a__from#(mark(X))mark#(from(X))mark#(X)

Problem 2: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(first(X1, X2))mark#(X2)a__from#(X)mark#(X)
mark#(first(X1, X2))a__first#(mark(X1), mark(X2))a__first#(s(X), cons(Y, Z))mark#(Y)
mark#(cons(X1, X2))mark#(X1)mark#(first(X1, X2))mark#(X1)
mark#(s(X))mark#(X)

Rewrite Rules

a__first(0, X)nila__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))
a__from(X)cons(mark(X), from(s(X)))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(0)0
mark(nil)nilmark(s(X))s(mark(X))
mark(cons(X1, X2))cons(mark(X1), X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: 0, s, mark, from, first, a__first, a__from, cons, nil

Strategy


The following SCCs where found

mark#(first(X1, X2)) → mark#(X2)mark#(first(X1, X2)) → a__first#(mark(X1), mark(X2))
a__first#(s(X), cons(Y, Z)) → mark#(Y)mark#(cons(X1, X2)) → mark#(X1)
mark#(first(X1, X2)) → mark#(X1)mark#(s(X)) → mark#(X)

Problem 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(first(X1, X2))mark#(X2)mark#(first(X1, X2))a__first#(mark(X1), mark(X2))
a__first#(s(X), cons(Y, Z))mark#(Y)mark#(cons(X1, X2))mark#(X1)
mark#(first(X1, X2))mark#(X1)mark#(s(X))mark#(X)

Rewrite Rules

a__first(0, X)nila__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))
a__from(X)cons(mark(X), from(s(X)))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(0)0
mark(nil)nilmark(s(X))s(mark(X))
mark(cons(X1, X2))cons(mark(X1), X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: 0, s, mark, from, first, a__first, a__from, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

mark(cons(X1, X2))cons(mark(X1), X2)a__first(X1, X2)first(X1, X2)
mark(0)0a__from(X)from(X)
mark(s(X))s(mark(X))a__from(X)cons(mark(X), from(s(X)))
mark(from(X))a__from(mark(X))mark(nil)nil
mark(first(X1, X2))a__first(mark(X1), mark(X2))a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))
a__first(0, X)nil

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

mark#(first(X1, X2))mark#(X2)a__first#(s(X), cons(Y, Z))mark#(Y)
mark#(first(X1, X2))a__first#(mark(X1), mark(X2))mark#(first(X1, X2))mark#(X1)

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

a__first(0, X)nila__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))
a__from(X)cons(mark(X), from(s(X)))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(0)0
mark(nil)nilmark(s(X))s(mark(X))
mark(cons(X1, X2))cons(mark(X1), X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: 0, s, mark, from, a__first, first, a__from, nil, 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)

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(s(X))mark#(X)

Rewrite Rules

a__first(0, X)nila__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))
a__from(X)cons(mark(X), from(s(X)))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(0)0
mark(nil)nilmark(s(X))s(mark(X))
mark(cons(X1, X2))cons(mark(X1), X2)a__first(X1, X2)first(X1, X2)
a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: 0, s, mark, from, first, a__first, a__from, cons, nil

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#(s(X))mark#(X)