YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (881ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 |    | – Problem 11 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor PolynomialLinearRange4iUR (1482ms).
 |    | – Problem 13 was processed with processor PolynomialLinearRange4iUR (760ms).
 | – Problem 6 was processed with processor SubtermCriterion (0ms).
 |    | – Problem 12 was processed with processor SubtermCriterion (0ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 was processed with processor SubtermCriterion (0ms).
 | – Problem 9 was processed with processor SubtermCriterion (1ms).
 | – Problem 10 was processed with processor SubtermCriterion (0ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2)) → proper#(X1)top#(ok(X)) → top#(active(X))
add#(X1, mark(X2)) → add#(X1, X2)active#(len(X)) → active#(X)
cons#(ok(X1), ok(X2)) → cons#(X1, X2)from#(ok(X)) → from#(X)
proper#(fst(X1, X2)) → fst#(proper(X1), proper(X2))active#(fst(s(X), cons(Y, Z))) → fst#(X, Z)
active#(cons(X1, X2)) → cons#(active(X1), X2)active#(add(X1, X2)) → add#(active(X1), X2)
active#(len(cons(X, Z))) → len#(Z)top#(mark(X)) → proper#(X)
proper#(from(X)) → proper#(X)proper#(add(X1, X2)) → proper#(X2)
proper#(len(X)) → len#(proper(X))active#(fst(X1, X2)) → active#(X2)
top#(mark(X)) → top#(proper(X))proper#(cons(X1, X2)) → proper#(X2)
fst#(ok(X1), ok(X2)) → fst#(X1, X2)proper#(add(X1, X2)) → proper#(X1)
proper#(len(X)) → proper#(X)add#(mark(X1), X2) → add#(X1, X2)
fst#(X1, mark(X2)) → fst#(X1, X2)active#(from(X)) → s#(X)
proper#(s(X)) → proper#(X)active#(add(X1, X2)) → active#(X2)
active#(add(s(X), Y)) → add#(X, Y)len#(mark(X)) → len#(X)
active#(len(cons(X, Z))) → s#(len(Z))active#(cons(X1, X2)) → active#(X1)
proper#(add(X1, X2)) → add#(proper(X1), proper(X2))cons#(mark(X1), X2) → cons#(X1, X2)
active#(from(X)) → from#(active(X))active#(add(X1, X2)) → add#(X1, active(X2))
active#(len(X)) → len#(active(X))active#(fst(X1, X2)) → fst#(active(X1), X2)
add#(ok(X1), ok(X2)) → add#(X1, X2)from#(mark(X)) → from#(X)
top#(ok(X)) → active#(X)active#(add(s(X), Y)) → s#(add(X, Y))
active#(from(X)) → cons#(X, from(s(X)))proper#(from(X)) → from#(proper(X))
active#(add(X1, X2)) → active#(X1)active#(fst(X1, X2)) → fst#(X1, active(X2))
len#(ok(X)) → len#(X)proper#(fst(X1, X2)) → proper#(X1)
active#(from(X)) → active#(X)s#(ok(X)) → s#(X)
proper#(cons(X1, X2)) → cons#(proper(X1), proper(X2))proper#(s(X)) → s#(proper(X))
active#(fst(X1, X2)) → active#(X1)active#(fst(s(X), cons(Y, Z))) → cons#(Y, fst(X, Z))
fst#(mark(X1), X2) → fst#(X1, X2)proper#(fst(X1, X2)) → proper#(X2)
active#(from(X)) → from#(s(X))

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

The following SCCs where found

cons#(mark(X1), X2) → cons#(X1, X2)cons#(ok(X1), ok(X2)) → cons#(X1, X2)
len#(ok(X)) → len#(X)len#(mark(X)) → len#(X)
fst#(X1, mark(X2)) → fst#(X1, X2)fst#(ok(X1), ok(X2)) → fst#(X1, X2)
fst#(mark(X1), X2) → fst#(X1, X2)
active#(add(X1, X2)) → active#(X1)active#(add(X1, X2)) → active#(X2)
active#(fst(X1, X2)) → active#(X2)active#(from(X)) → active#(X)
active#(len(X)) → active#(X)active#(fst(X1, X2)) → active#(X1)
active#(cons(X1, X2)) → active#(X1)
add#(X1, mark(X2)) → add#(X1, X2)add#(mark(X1), X2) → add#(X1, X2)
add#(ok(X1), ok(X2)) → add#(X1, X2)
s#(ok(X)) → s#(X)
from#(mark(X)) → from#(X)from#(ok(X)) → from#(X)
top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))
proper#(s(X)) → proper#(X)proper#(cons(X1, X2)) → proper#(X1)
proper#(fst(X1, X2)) → proper#(X1)proper#(cons(X1, X2)) → proper#(X2)
proper#(add(X1, X2)) → proper#(X1)proper#(len(X)) → proper#(X)
proper#(from(X)) → proper#(X)proper#(fst(X1, X2)) → proper#(X2)
proper#(add(X1, X2)) → proper#(X2)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

len#(ok(X)) → len#(X)len#(mark(X)) → len#(X)

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

len#(ok(X)) → len#(X)len#(mark(X)) → len#(X)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

add#(X1, mark(X2)) → add#(X1, X2)add#(mark(X1), X2) → add#(X1, X2)
add#(ok(X1), ok(X2)) → add#(X1, X2)

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

add#(mark(X1), X2) → add#(X1, X2)add#(ok(X1), ok(X2)) → add#(X1, X2)

Problem 11: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

add#(X1, mark(X2)) → add#(X1, X2)

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

add#(X1, mark(X2)) → add#(X1, X2)

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

proper#(s(X)) → proper#(X)proper#(cons(X1, X2)) → proper#(X1)
proper#(fst(X1, X2)) → proper#(X1)proper#(cons(X1, X2)) → proper#(X2)
proper#(add(X1, X2)) → proper#(X1)proper#(len(X)) → proper#(X)
proper#(from(X)) → proper#(X)proper#(fst(X1, X2)) → proper#(X2)
proper#(add(X1, X2)) → proper#(X2)

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(s(X)) → proper#(X)proper#(cons(X1, X2)) → proper#(X1)
proper#(fst(X1, X2)) → proper#(X1)proper#(cons(X1, X2)) → proper#(X2)
proper#(add(X1, X2)) → proper#(X1)proper#(len(X)) → proper#(X)
proper#(from(X)) → proper#(X)proper#(fst(X1, X2)) → proper#(X2)
proper#(add(X1, X2)) → proper#(X2)

Problem 5: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Polynomial Interpretation

Improved Usable rules

fst(mark(X1), X2) → mark(fst(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
len(ok(X)) → ok(len(X))cons(mark(X1), X2) → mark(cons(X1, X2))
active(from(X)) → from(active(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
active(fst(X1, X2)) → fst(active(X1), X2)add(mark(X1), X2) → mark(add(X1, X2))
active(len(cons(X, Z))) → mark(s(len(Z)))active(add(X1, X2)) → add(active(X1), X2)
proper(s(X)) → s(proper(X))add(X1, mark(X2)) → mark(add(X1, X2))
active(from(X)) → mark(cons(X, from(s(X))))active(fst(0, Z)) → mark(nil)
s(ok(X)) → ok(s(X))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
active(add(s(X), Y)) → mark(s(add(X, Y)))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))len(mark(X)) → mark(len(X))
active(fst(X1, X2)) → fst(X1, active(X2))active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
from(mark(X)) → mark(from(X))fst(X1, mark(X2)) → mark(fst(X1, X2))
proper(len(X)) → len(proper(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
active(cons(X1, X2)) → cons(active(X1), X2)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)active(add(0, X)) → mark(X)
proper(0) → ok(0)active(len(X)) → len(active(X))
active(len(nil)) → mark(0)active(add(X1, X2)) → add(X1, active(X2))
proper(from(X)) → from(proper(X))

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

top#(mark(X)) → top#(proper(X))

Problem 13: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

top#(ok(X)) → top#(active(X))

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Polynomial Interpretation

Improved Usable rules

fst(ok(X1), ok(X2)) → ok(fst(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
len(ok(X)) → ok(len(X))cons(mark(X1), X2) → mark(cons(X1, X2))
active(from(X)) → from(active(X))active(fst(X1, X2)) → fst(active(X1), X2)
add(mark(X1), X2) → mark(add(X1, X2))active(len(cons(X, Z))) → mark(s(len(Z)))
active(add(X1, X2)) → add(active(X1), X2)add(X1, mark(X2)) → mark(add(X1, X2))
active(from(X)) → mark(cons(X, from(s(X))))active(fst(0, Z)) → mark(nil)
active(add(s(X), Y)) → mark(s(add(X, Y)))from(ok(X)) → ok(from(X))
len(mark(X)) → mark(len(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
active(fst(X1, X2)) → fst(X1, active(X2))active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
from(mark(X)) → mark(from(X))fst(X1, mark(X2)) → mark(fst(X1, X2))
add(ok(X1), ok(X2)) → ok(add(X1, X2))active(cons(X1, X2)) → cons(active(X1), X2)
active(add(0, X)) → mark(X)active(len(nil)) → mark(0)
active(len(X)) → len(active(X))active(add(X1, X2)) → add(X1, active(X2))

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

top#(ok(X)) → top#(active(X))

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

fst#(X1, mark(X2)) → fst#(X1, X2)fst#(ok(X1), ok(X2)) → fst#(X1, X2)
fst#(mark(X1), X2) → fst#(X1, X2)

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

fst#(ok(X1), ok(X2)) → fst#(X1, X2)fst#(mark(X1), X2) → fst#(X1, X2)

Problem 12: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

fst#(X1, mark(X2)) → fst#(X1, X2)

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

fst#(X1, mark(X2)) → fst#(X1, X2)

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

active#(add(X1, X2)) → active#(X1)active#(add(X1, X2)) → active#(X2)
active#(fst(X1, X2)) → active#(X2)active#(from(X)) → active#(X)
active#(len(X)) → active#(X)active#(fst(X1, X2)) → active#(X1)
active#(cons(X1, X2)) → active#(X1)

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(add(X1, X2)) → active#(X1)active#(add(X1, X2)) → active#(X2)
active#(fst(X1, X2)) → active#(X2)active#(from(X)) → active#(X)
active#(fst(X1, X2)) → active#(X1)active#(len(X)) → active#(X)
active#(cons(X1, X2)) → active#(X1)

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

cons#(mark(X1), X2) → cons#(X1, X2)cons#(ok(X1), ok(X2)) → cons#(X1, X2)

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

cons#(mark(X1), X2) → cons#(X1, X2)cons#(ok(X1), ok(X2)) → cons#(X1, X2)

Problem 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

s#(ok(X)) → s#(X)

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

s#(ok(X)) → s#(X)

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

from#(mark(X)) → from#(X)from#(ok(X)) → from#(X)

Rewrite Rules

active(fst(0, Z)) → mark(nil)active(fst(s(X), cons(Y, Z))) → mark(cons(Y, fst(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))active(len(nil)) → mark(0)
active(len(cons(X, Z))) → mark(s(len(Z)))active(cons(X1, X2)) → cons(active(X1), X2)
active(fst(X1, X2)) → fst(active(X1), X2)active(fst(X1, X2)) → fst(X1, active(X2))
active(from(X)) → from(active(X))active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))active(len(X)) → len(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))fst(mark(X1), X2) → mark(fst(X1, X2))
fst(X1, mark(X2)) → mark(fst(X1, X2))from(mark(X)) → mark(from(X))
add(mark(X1), X2) → mark(add(X1, X2))add(X1, mark(X2)) → mark(add(X1, X2))
len(mark(X)) → mark(len(X))proper(0) → ok(0)
proper(s(X)) → s(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(fst(X1, X2)) → fst(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(len(X)) → len(proper(X))s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))fst(ok(X1), ok(X2)) → ok(fst(X1, X2))
from(ok(X)) → ok(from(X))add(ok(X1), ok(X2)) → ok(add(X1, X2))
len(ok(X)) → ok(len(X))top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: mark, from, len, add, fst, 0, s, active, ok, proper, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

from#(mark(X)) → from#(X)from#(ok(X)) → from#(X)