YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (6ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (69ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4 (16ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

T(s(x_1))T(x_1)T(from(x_1))T(x_1)
2nd#(cons(X, cons(Y, Z)))T(Y)T(from(s(X)))from#(s(X))

Rewrite Rules

2nd(cons(X, cons(Y, Z)))Yfrom(X)cons(X, from(s(X)))

Original Signature

Termination of terms over the following signature is verified: 2nd, s, from, cons

Strategy

Context-sensitive strategy:
μ(T) = ∅
μ(2nd) = μ(from#) = μ(s) = μ(2nd#) = μ(from) = μ(cons) = {1}


The following SCCs where found

T(s(x_1)) → T(x_1)T(from(x_1)) → T(x_1)

Problem 2: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

T(s(x_1))T(x_1)T(from(x_1))T(x_1)

Rewrite Rules

2nd(cons(X, cons(Y, Z)))Yfrom(X)cons(X, from(s(X)))

Original Signature

Termination of terms over the following signature is verified: 2nd, s, from, cons

Strategy

Context-sensitive strategy:
μ(T) = ∅
μ(2nd) = μ(s) = μ(from#) = μ(from) = μ(2nd#) = μ(cons) = {1}


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:

T(s(x_1))T(x_1)

Problem 3: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

T(from(x_1))T(x_1)

Rewrite Rules

2nd(cons(X, cons(Y, Z)))Yfrom(X)cons(X, from(s(X)))

Original Signature

Termination of terms over the following signature is verified: 2nd, s, from, cons

Strategy

Context-sensitive strategy:
μ(T) = ∅
μ(2nd) = μ(from#) = μ(s) = μ(2nd#) = μ(from) = μ(cons) = {1}


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:

T(from(x_1))T(x_1)