YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (48ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (115ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4 (120ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4 (124ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4 (21ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

T(fst(X, Z)) → fst#(X, Z)T(add(x_1, x_2)) → T(x_2)
T(len(Z)) → len#(Z)T(add(x_1, x_2)) → T(x_1)
T(s(x_1)) → T(x_1)T(fst(x_1, x_2)) → T(x_2)
T(from(s(X))) → from#(s(X))T(fst(x_1, x_2)) → T(x_1)
T(add(X, Y)) → add#(X, Y)T(len(x_1)) → T(x_1)

Rewrite Rules

fst(0, Z) → nilfst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))len(nil) → 0
len(cons(X, Z)) → s(len(Z))

Original Signature

Termination of terms over the following signature is verified: fst, 0, s, from, len, add, nil, cons

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(from#) = μ(from) = μ(len) = μ(len#) = μ(cons) = {1}
μ(fst#) = μ(add) = μ(fst) = μ(add#) = {1, 2}

The following SCCs where found

T(add(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_1)
T(s(x_1)) → T(x_1)T(fst(x_1, x_2)) → T(x_2)
T(fst(x_1, x_2)) → T(x_1)T(len(x_1)) → T(x_1)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(add(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_1)
T(s(x_1)) → T(x_1)T(fst(x_1, x_2)) → T(x_2)
T(fst(x_1, x_2)) → T(x_1)T(len(x_1)) → T(x_1)

Rewrite Rules

fst(0, Z) → nilfst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))len(nil) → 0
len(cons(X, Z)) → s(len(Z))

Original Signature

Termination of terms over the following signature is verified: fst, 0, s, from, len, add, nil, cons

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(from#) = μ(from) = μ(len) = μ(len#) = μ(cons) = {1}
μ(fst#) = μ(add) = μ(fst) = μ(add#) = {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(x_1)) → T(x_1)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(add(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_1)
T(fst(x_1, x_2)) → T(x_2)T(fst(x_1, x_2)) → T(x_1)
T(len(x_1)) → T(x_1)

Rewrite Rules

fst(0, Z) → nilfst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))len(nil) → 0
len(cons(X, Z)) → s(len(Z))

Original Signature

Termination of terms over the following signature is verified: fst, 0, s, len, from, add, cons, nil

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(from#) = μ(from) = μ(len) = μ(len#) = μ(cons) = {1}
μ(fst#) = μ(add) = μ(fst) = μ(add#) = {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(len(x_1)) → T(x_1)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(add(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_1)
T(fst(x_1, x_2)) → T(x_2)T(fst(x_1, x_2)) → T(x_1)

Rewrite Rules

fst(0, Z) → nilfst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))len(nil) → 0
len(cons(X, Z)) → s(len(Z))

Original Signature

Termination of terms over the following signature is verified: fst, 0, s, from, len, add, nil, cons

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(from#) = μ(from) = μ(len) = μ(len#) = μ(cons) = {1}
μ(fst#) = μ(add) = μ(fst) = μ(add#) = {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(fst(x_1, x_2)) → T(x_2)T(fst(x_1, x_2)) → T(x_1)

Problem 5: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(add(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_1)

Rewrite Rules

fst(0, Z) → nilfst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))len(nil) → 0
len(cons(X, Z)) → s(len(Z))

Original Signature

Termination of terms over the following signature is verified: fst, 0, s, len, from, add, cons, nil

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(from#) = μ(from) = μ(len) = μ(len#) = μ(cons) = {1}
μ(fst#) = μ(add) = μ(fst) = μ(add#) = {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(add(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_1)