TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60001 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (1189ms).
 | – Problem 2 was processed with processor SubtermCriterion (4ms).
 | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (3805ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (3208ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (30037ms), DependencyGraph (timeout), ReductionPairSAT (4828ms), DependencyGraph (4ms), SizeChangePrinciple (timeout)].
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 11 was processed with processor PolynomialLinearRange4iUR (45ms).
 | – Problem 6 was processed with processor SubtermCriterion (0ms).
 | – Problem 7 was processed with processor SubtermCriterion (0ms).
 | – Problem 8 was processed with processor SubtermCriterion (1ms).
 | – Problem 9 was processed with processor SubtermCriterion (1ms).
 | – Problem 10 was processed with processor SubtermCriterion (3ms).

The following open problems remain:

Open Dependency Pair Problem 3

Dependency Pairs

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

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, top, eq, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

take#(mark(X1), X2) → take#(X1, X2)proper#(cons(X1, X2)) → proper#(X1)
proper#(length(X)) → length#(proper(X))top#(ok(X)) → top#(active(X))
proper#(inf(X)) → proper#(X)cons#(ok(X1), ok(X2)) → cons#(X1, X2)
active#(eq(s(X), s(Y))) → eq#(X, Y)top#(ok(X)) → active#(X)
active#(take(X1, X2)) → take#(active(X1), X2)active#(inf(X)) → s#(X)
inf#(ok(X)) → inf#(X)active#(inf(X)) → active#(X)
proper#(take(X1, X2)) → proper#(X1)active#(take(s(X), cons(Y, L))) → take#(X, L)
length#(ok(X)) → length#(X)take#(ok(X1), ok(X2)) → take#(X1, X2)
top#(mark(X)) → proper#(X)length#(mark(X)) → length#(X)
top#(mark(X)) → top#(proper(X))active#(inf(X)) → inf#(s(X))
active#(length(X)) → length#(active(X))proper#(cons(X1, X2)) → proper#(X2)
active#(length(cons(X, L))) → s#(length(L))active#(take(X1, X2)) → active#(X2)
active#(length(X)) → active#(X)active#(take(X1, X2)) → active#(X1)
proper#(take(X1, X2)) → proper#(X2)proper#(eq(X1, X2)) → eq#(proper(X1), proper(X2))
take#(X1, mark(X2)) → take#(X1, X2)active#(length(cons(X, L))) → length#(L)
proper#(eq(X1, X2)) → proper#(X2)s#(ok(X)) → s#(X)
active#(take(s(X), cons(Y, L))) → cons#(Y, take(X, L))proper#(s(X)) → proper#(X)
proper#(length(X)) → proper#(X)proper#(cons(X1, X2)) → cons#(proper(X1), proper(X2))
active#(inf(X)) → inf#(active(X))active#(take(X1, X2)) → take#(X1, active(X2))
proper#(s(X)) → s#(proper(X))proper#(eq(X1, X2)) → proper#(X1)
proper#(take(X1, X2)) → take#(proper(X1), proper(X2))active#(inf(X)) → cons#(X, inf(s(X)))
proper#(inf(X)) → inf#(proper(X))eq#(ok(X1), ok(X2)) → eq#(X1, X2)
inf#(mark(X)) → inf#(X)

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, nil, cons, top, eq

Strategy

The following SCCs where found

length#(mark(X)) → length#(X)length#(ok(X)) → length#(X)
inf#(ok(X)) → inf#(X)inf#(mark(X)) → inf#(X)
eq#(ok(X1), ok(X2)) → eq#(X1, X2)
cons#(ok(X1), ok(X2)) → cons#(X1, X2)
take#(mark(X1), X2) → take#(X1, X2)take#(X1, mark(X2)) → take#(X1, X2)
take#(ok(X1), ok(X2)) → take#(X1, X2)
proper#(length(X)) → proper#(X)proper#(s(X)) → proper#(X)
proper#(cons(X1, X2)) → proper#(X1)proper#(cons(X1, X2)) → proper#(X2)
proper#(take(X1, X2)) → proper#(X1)proper#(eq(X1, X2)) → proper#(X1)
proper#(take(X1, X2)) → proper#(X2)proper#(inf(X)) → proper#(X)
proper#(eq(X1, X2)) → proper#(X2)
s#(ok(X)) → s#(X)
top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))
active#(inf(X)) → active#(X)active#(take(X1, X2)) → active#(X2)
active#(take(X1, X2)) → active#(X1)active#(length(X)) → active#(X)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, nil, cons, top, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

length#(mark(X)) → length#(X)length#(ok(X)) → length#(X)

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, nil, cons, top, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

length#(mark(X)) → length#(X)length#(ok(X)) → length#(X)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, nil, cons, top, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 11: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, eq, top, nil, cons

Strategy

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:

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

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

inf#(ok(X)) → inf#(X)inf#(mark(X)) → inf#(X)

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, nil, cons, top, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

inf#(ok(X)) → inf#(X)inf#(mark(X)) → inf#(X)

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

eq#(ok(X1), ok(X2)) → eq#(X1, X2)

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, nil, cons, top, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

eq#(ok(X1), ok(X2)) → eq#(X1, X2)

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, nil, cons, top, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

active#(inf(X)) → active#(X)active#(take(X1, X2)) → active#(X2)
active#(take(X1, X2)) → active#(X1)active#(length(X)) → active#(X)

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, nil, cons, top, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(inf(X)) → active#(X)active#(take(X1, X2)) → active#(X2)
active#(length(X)) → active#(X)active#(take(X1, X2)) → active#(X1)

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

proper#(length(X)) → proper#(X)proper#(s(X)) → proper#(X)
proper#(cons(X1, X2)) → proper#(X1)proper#(cons(X1, X2)) → proper#(X2)
proper#(take(X1, X2)) → proper#(X1)proper#(eq(X1, X2)) → proper#(X1)
proper#(take(X1, X2)) → proper#(X2)proper#(inf(X)) → proper#(X)
proper#(eq(X1, X2)) → proper#(X2)

Rewrite Rules

active(eq(0, 0)) → mark(true)active(eq(s(X), s(Y))) → mark(eq(X, Y))
active(eq(X, Y)) → mark(false)active(inf(X)) → mark(cons(X, inf(s(X))))
active(take(0, X)) → mark(nil)active(take(s(X), cons(Y, L))) → mark(cons(Y, take(X, L)))
active(length(nil)) → mark(0)active(length(cons(X, L))) → mark(s(length(L)))
active(inf(X)) → inf(active(X))active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))active(length(X)) → length(active(X))
inf(mark(X)) → mark(inf(X))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))length(mark(X)) → mark(length(X))
proper(eq(X1, X2)) → eq(proper(X1), proper(X2))proper(0) → ok(0)
proper(true) → ok(true)proper(s(X)) → s(proper(X))
proper(false) → ok(false)proper(inf(X)) → inf(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(nil) → ok(nil)proper(length(X)) → length(proper(X))
eq(ok(X1), ok(X2)) → ok(eq(X1, X2))s(ok(X)) → ok(s(X))
inf(ok(X)) → ok(inf(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))length(ok(X)) → ok(length(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, length, active, false, ok, proper, nil, cons, top, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(s(X)) → proper#(X)proper#(length(X)) → proper#(X)
proper#(cons(X1, X2)) → proper#(X1)proper#(cons(X1, X2)) → proper#(X2)
proper#(take(X1, X2)) → proper#(X1)proper#(eq(X1, X2)) → proper#(X1)
proper#(take(X1, X2)) → proper#(X2)proper#(inf(X)) → proper#(X)
proper#(eq(X1, X2)) → proper#(X2)