YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (7ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (65ms).
 |    | – Problem 4 was processed with processor DependencyGraph (0ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4 (35ms).
 |    | – Problem 5 was processed with processor PolynomialLinearRange4 (9ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

T(s(x_1)) → T(x_1)T(from(x_1)) → T(x_1)
length1#(X) → length#(X)length#(cons(X, Y)) → length1#(Y)
T(from(s(X))) → from#(s(X))

Rewrite Rules

from(X) → cons(X, from(s(X)))length(nil) → 0
length(cons(X, Y)) → s(length1(Y))length1(X) → length(X)

Original Signature

Termination of terms over the following signature is verified: 0, s, length, from, length1, cons, nil

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(length#) = μ(length) = μ(length1) = μ(length1#) = μ(nil) = ∅
μ(from#) = μ(s) = μ(from) = μ(cons) = {1}

The following SCCs where found

T(s(x_1)) → T(x_1)T(from(x_1)) → T(x_1)
length1#(X) → length#(X)length#(cons(X, Y)) → length1#(Y)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

length1#(X) → length#(X)length#(cons(X, Y)) → length1#(Y)

Rewrite Rules

from(X) → cons(X, from(s(X)))length(nil) → 0
length(cons(X, Y)) → s(length1(Y))length1(X) → length(X)

Original Signature

Termination of terms over the following signature is verified: 0, s, length, from, length1, cons, nil

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(length#) = μ(length) = μ(length1) = μ(length1#) = μ(nil) = ∅
μ(s) = μ(from#) = μ(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:

length1#(X) → length#(X)

Problem 4: DependencyGraph

Dependency Pair Problem

Dependency Pairs

length#(cons(X, Y)) → length1#(Y)

Rewrite Rules

from(X) → cons(X, from(s(X)))length(nil) → 0
length(cons(X, Y)) → s(length1(Y))length1(X) → length(X)

Original Signature

Termination of terms over the following signature is verified: 0, s, length, length1, from, nil, cons

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(length#) = μ(length) = μ(length1) = μ(length1#) = μ(nil) = ∅
μ(from#) = μ(s) = μ(from) = μ(cons) = {1}

There are no SCCs!

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

from(X) → cons(X, from(s(X)))length(nil) → 0
length(cons(X, Y)) → s(length1(Y))length1(X) → length(X)

Original Signature

Termination of terms over the following signature is verified: 0, s, length, from, length1, cons, nil

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(length#) = μ(length) = μ(length1) = μ(length1#) = μ(nil) = ∅
μ(s) = μ(from#) = μ(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(s(x_1)) → T(x_1)

Problem 5: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

from(X) → cons(X, from(s(X)))length(nil) → 0
length(cons(X, Y)) → s(length1(Y))length1(X) → length(X)

Original Signature

Termination of terms over the following signature is verified: 0, s, length, length1, from, nil, cons

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(length#) = μ(length) = μ(length1) = μ(length1#) = μ(nil) = ∅
μ(from#) = μ(s) = μ(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)