TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (2079ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (2ms).
 | – Problem 5 was processed with processor SubtermCriterion (3ms).
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 12 was processed with processor ReductionPairSAT (69ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 was processed with processor SubtermCriterion (0ms).
 | – Problem 9 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (6ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (13ms), ReductionPairSAT (6326ms), DependencyGraph (22ms), ReductionPairSAT (6216ms), DependencyGraph (4ms), SizeChangePrinciple (timeout)].
 | – Problem 10 was processed with processor SubtermCriterion (1ms).
 | – Problem 11 was processed with processor SubtermCriterion (1ms).

The following open problems remain:

Open Dependency Pair Problem 9

Dependency Pairs

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

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, top, nil, cons

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2)) → proper#(X1)top#(ok(X)) → top#(active(X))
dbls#(ok(X)) → dbls#(X)active#(dbl(s(X))) → s#(dbl(X))
cons#(ok(X1), ok(X2)) → cons#(X1, X2)active#(dbls(cons(X, Y))) → cons#(dbl(X), dbls(Y))
dbls#(mark(X)) → dbls#(X)from#(ok(X)) → from#(X)
active#(sel(X1, X2)) → active#(X2)indx#(ok(X1), ok(X2)) → indx#(X1, X2)
active#(dbl(s(X))) → dbl#(X)top#(mark(X)) → proper#(X)
proper#(indx(X1, X2)) → proper#(X1)proper#(from(X)) → proper#(X)
indx#(mark(X1), X2) → indx#(X1, X2)active#(sel(s(X), cons(Y, Z))) → sel#(X, Z)
top#(mark(X)) → top#(proper(X))proper#(cons(X1, X2)) → proper#(X2)
active#(dbl(s(X))) → s#(s(dbl(X)))sel#(X1, mark(X2)) → sel#(X1, X2)
active#(indx(cons(X, Y), Z)) → cons#(sel(X, Z), indx(Y, Z))active#(from(X)) → s#(X)
proper#(s(X)) → proper#(X)sel#(ok(X1), ok(X2)) → sel#(X1, X2)
active#(dbls(X)) → active#(X)active#(dbls(X)) → dbls#(active(X))
sel#(mark(X1), X2) → sel#(X1, X2)active#(dbls(cons(X, Y))) → dbls#(Y)
proper#(indx(X1, X2)) → proper#(X2)active#(indx(cons(X, Y), Z)) → indx#(Y, Z)
top#(ok(X)) → active#(X)proper#(sel(X1, X2)) → sel#(proper(X1), proper(X2))
active#(sel(X1, X2)) → active#(X1)active#(indx(cons(X, Y), Z)) → sel#(X, Z)
active#(dbl(X)) → active#(X)active#(from(X)) → cons#(X, from(s(X)))
proper#(from(X)) → from#(proper(X))proper#(sel(X1, X2)) → proper#(X2)
active#(dbls(cons(X, Y))) → dbl#(X)proper#(indx(X1, X2)) → indx#(proper(X1), proper(X2))
proper#(dbls(X)) → dbls#(proper(X))active#(sel(X1, X2)) → sel#(X1, active(X2))
active#(sel(X1, X2)) → sel#(active(X1), X2)active#(indx(X1, X2)) → active#(X1)
proper#(dbl(X)) → proper#(X)dbl#(mark(X)) → dbl#(X)
active#(dbl(X)) → dbl#(active(X))s#(ok(X)) → s#(X)
dbl#(ok(X)) → dbl#(X)proper#(sel(X1, X2)) → proper#(X1)
proper#(cons(X1, X2)) → cons#(proper(X1), proper(X2))proper#(dbl(X)) → dbl#(proper(X))
proper#(dbls(X)) → proper#(X)proper#(s(X)) → s#(proper(X))
active#(indx(X1, X2)) → indx#(active(X1), X2)active#(from(X)) → from#(s(X))

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, cons, top, nil

Strategy

The following SCCs where found

sel#(mark(X1), X2) → sel#(X1, X2)sel#(ok(X1), ok(X2)) → sel#(X1, X2)
sel#(X1, mark(X2)) → sel#(X1, X2)
proper#(sel(X1, X2)) → proper#(X1)proper#(s(X)) → proper#(X)
proper#(cons(X1, X2)) → proper#(X1)proper#(cons(X1, X2)) → proper#(X2)
proper#(dbl(X)) → proper#(X)proper#(dbls(X)) → proper#(X)
proper#(indx(X1, X2)) → proper#(X2)proper#(sel(X1, X2)) → proper#(X2)
proper#(indx(X1, X2)) → proper#(X1)proper#(from(X)) → proper#(X)
dbl#(ok(X)) → dbl#(X)dbl#(mark(X)) → dbl#(X)
cons#(ok(X1), ok(X2)) → cons#(X1, X2)
active#(sel(X1, X2)) → active#(X2)active#(indx(X1, X2)) → active#(X1)
active#(sel(X1, X2)) → active#(X1)active#(dbls(X)) → active#(X)
active#(dbl(X)) → active#(X)
dbls#(ok(X)) → dbls#(X)dbls#(mark(X)) → dbls#(X)
indx#(ok(X1), ok(X2)) → indx#(X1, X2)indx#(mark(X1), X2) → indx#(X1, X2)
s#(ok(X)) → s#(X)
from#(ok(X)) → from#(X)
top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, cons, top, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, cons, top, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

proper#(sel(X1, X2)) → proper#(X1)proper#(s(X)) → proper#(X)
proper#(cons(X1, X2)) → proper#(X1)proper#(cons(X1, X2)) → proper#(X2)
proper#(dbl(X)) → proper#(X)proper#(dbls(X)) → proper#(X)
proper#(indx(X1, X2)) → proper#(X2)proper#(sel(X1, X2)) → proper#(X2)
proper#(indx(X1, X2)) → proper#(X1)proper#(from(X)) → proper#(X)

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, cons, top, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(sel(X1, X2)) → proper#(X1)proper#(s(X)) → proper#(X)
proper#(cons(X1, X2)) → proper#(X1)proper#(cons(X1, X2)) → proper#(X2)
proper#(dbl(X)) → proper#(X)proper#(dbls(X)) → proper#(X)
proper#(indx(X1, X2)) → proper#(X2)proper#(sel(X1, X2)) → proper#(X2)
proper#(indx(X1, X2)) → proper#(X1)proper#(from(X)) → proper#(X)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

active#(sel(X1, X2)) → active#(X2)active#(indx(X1, X2)) → active#(X1)
active#(sel(X1, X2)) → active#(X1)active#(dbls(X)) → active#(X)
active#(dbl(X)) → active#(X)

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, cons, top, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(sel(X1, X2)) → active#(X2)active#(indx(X1, X2)) → active#(X1)
active#(sel(X1, X2)) → active#(X1)active#(dbls(X)) → active#(X)
active#(dbl(X)) → active#(X)

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, cons, top, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 12: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, nil, cons, top

Strategy

Function Precedence

mark < dbl = sel# = from = dbls = 0 = s = indx = active = ok = proper = sel = top = cons = nil

Argument Filtering

mark: 1
dbl: all arguments are removed from dbl
sel#: collapses to 2
from: collapses to 1
dbls: collapses to 1
0: all arguments are removed from 0
s: collapses to 1
indx: collapses to 1
active: collapses to 1
ok: collapses to 1
proper: all arguments are removed from proper
sel: 1 2
top: collapses to 1
cons: collapses to 1
nil: all arguments are removed from nil

Status

mark: multiset
dbl: multiset
0: multiset
proper: multiset
sel: lexicographic with permutation 1 → 2 2 → 1
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

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

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, cons, top, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

dbls#(ok(X)) → dbls#(X)dbls#(mark(X)) → dbls#(X)

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, cons, top, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

dbls#(ok(X)) → dbls#(X)dbls#(mark(X)) → dbls#(X)

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

dbl#(ok(X)) → dbl#(X)dbl#(mark(X)) → dbl#(X)

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, cons, top, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

dbl#(ok(X)) → dbl#(X)dbl#(mark(X)) → dbl#(X)

Problem 11: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(dbl(0)) → mark(0)active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))active(indx(X1, X2)) → indx(active(X1), X2)
dbl(mark(X)) → mark(dbl(X))dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))proper(from(X)) → from(proper(X))
dbl(ok(X)) → ok(dbl(X))s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(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, dbl, from, dbls, 0, s, indx, active, ok, proper, sel, cons, top, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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