YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (25ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (71ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4 (24ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

from_3#(x)T(x)from_4#(x)T(x)
T(from_1(s_0(x)))from_1#(s_0(x))from_2#(x)from_1#(s_0(x))
from_4#(x)from_2#(s_0(x))from_2#(x)T(x)
T(from_1(x_1))T(x_1)from_3#(x)from_2#(s_0(x))
T(s_0(x_1))T(x_1)from_1#(x)cons_1#(x, from_1(s_0(x)))

Rewrite Rules

from_2(x)cons_0(x, from_1(s_0(x)))from_3(x)cons_0(x, from_2(s_0(x)))
from_4(x)cons_0(x, from_2(s_0(x)))from_1(x)cons_1(x, from_1(s_0(x)))
cons_1(s_0(s_0(x)), xs)nil_0

Original Signature

Termination of terms over the following signature is verified: cons_1, cons_0, nil_0, from_2, from_1, s_0, from_4, from_3

Strategy

Context-sensitive strategy:
μ(from_2#) = μ(from_1#) = μ(cons_1#) = μ(cons_1) = μ(from_2) = μ(from_1) = μ(from_4) = μ(from_3) = μ(T) = μ(nil_0) = μ(from_4#) = μ(from_3#) = ∅
μ(s_0) = {1}
μ(cons_0) = {1, 2}


The following SCCs where found

T(from_1(x_1)) → T(x_1)T(s_0(x_1)) → T(x_1)

Problem 2: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

T(from_1(x_1))T(x_1)T(s_0(x_1))T(x_1)

Rewrite Rules

from_2(x)cons_0(x, from_1(s_0(x)))from_3(x)cons_0(x, from_2(s_0(x)))
from_4(x)cons_0(x, from_2(s_0(x)))from_1(x)cons_1(x, from_1(s_0(x)))
cons_1(s_0(s_0(x)), xs)nil_0

Original Signature

Termination of terms over the following signature is verified: cons_1, cons_0, nil_0, from_2, from_1, s_0, from_4, from_3

Strategy

Context-sensitive strategy:
μ(from_2#) = μ(from_1#) = μ(cons_1#) = μ(cons_1) = μ(from_2) = μ(from_1) = μ(from_4) = μ(from_3) = μ(T) = μ(nil_0) = μ(from_4#) = μ(from_3#) = ∅
μ(s_0) = {1}
μ(cons_0) = {1, 2}


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_1(x_1))T(x_1)

Problem 3: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

T(s_0(x_1))T(x_1)

Rewrite Rules

from_2(x)cons_0(x, from_1(s_0(x)))from_3(x)cons_0(x, from_2(s_0(x)))
from_4(x)cons_0(x, from_2(s_0(x)))from_1(x)cons_1(x, from_1(s_0(x)))
cons_1(s_0(s_0(x)), xs)nil_0

Original Signature

Termination of terms over the following signature is verified: cons_1, cons_0, nil_0, from_2, from_1, from_4, s_0, from_3

Strategy

Context-sensitive strategy:
μ(from_2#) = μ(from_1#) = μ(cons_1#) = μ(cons_1) = μ(from_2) = μ(from_1) = μ(from_4) = μ(from_3) = μ(T) = μ(nil_0) = μ(from_4#) = μ(from_3#) = ∅
μ(s_0) = {1}
μ(cons_0) = {1, 2}


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_0(x_1))T(x_1)