TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (9370ms).
 | – Problem 2 was processed with processor SubtermCriterion (3ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – 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 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 16 was processed with processor PolynomialLinearRange4iUR (104ms).
 | – Problem 9 was processed with processor SubtermCriterion (3ms).
 | – Problem 10 was processed with processor SubtermCriterion (2ms).
 | – Problem 11 was processed with processor SubtermCriterion (1ms).
 | – Problem 12 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (5039ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (8026ms), DependencyGraph (5ms), PolynomialLinearRange8NegiUR (30000ms), ReductionPairSAT (timeout)].
 | – Problem 13 was processed with processor SubtermCriterion (4ms).
 | – Problem 14 was processed with processor SubtermCriterion (3ms).
 | – Problem 15 was processed with processor SubtermCriterion (2ms).

The following open problems remain:

Open Dependency Pair Problem 12

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, proper, U31, U21, top, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2)) → proper#(X1)proper#(length(X)) → length#(proper(X))
proper#(U11(X1, X2)) → proper#(X1)active#(U21(X)) → U21#(active(X))
U11#(mark(X1), X2) → U11#(X1, X2)active#(take(X1, X2)) → take#(active(X1), X2)
proper#(U11(X1, X2)) → proper#(X2)active#(isNat(length(V1))) → isNatList#(V1)
active#(U11(tt, L)) → s#(length(L))top#(mark(X)) → proper#(X)
length#(mark(X)) → length#(X)active#(take(X1, X2)) → active#(X2)
active#(length(X)) → active#(X)active#(U31(tt, IL, M, N)) → take#(M, IL)
isNat#(ok(X)) → isNat#(X)and#(mark(X1), X2) → and#(X1, X2)
proper#(U31(X1, X2, X3, X4)) → U31#(proper(X1), proper(X2), proper(X3), proper(X4))active#(isNatIList(cons(V1, V2))) → isNat#(V1)
isNatIList#(ok(X)) → isNatIList#(X)active#(take(s(M), cons(N, IL))) → isNat#(M)
proper#(U21(X)) → U21#(proper(X))cons#(mark(X1), X2) → cons#(X1, X2)
active#(take(s(M), cons(N, IL))) → isNat#(N)active#(isNatIList(cons(V1, V2))) → and#(isNat(V1), isNatIList(V2))
top#(ok(X)) → active#(X)active#(and(X1, X2)) → and#(active(X1), X2)
U31#(mark(X1), X2, X3, X4) → U31#(X1, X2, X3, X4)proper#(isNatList(X)) → proper#(X)
active#(U31(tt, IL, M, N)) → cons#(N, take(M, IL))proper#(isNat(X)) → isNat#(proper(X))
take#(ok(X1), ok(X2)) → take#(X1, X2)proper#(U21(X)) → proper#(X)
active#(isNat(s(V1))) → isNat#(V1)active#(take(s(M), cons(N, IL))) → and#(isNat(M), isNat(N))
active#(U31(X1, X2, X3, X4)) → U31#(active(X1), X2, X3, X4)proper#(isNat(X)) → proper#(X)
active#(isNatIList(cons(V1, V2))) → isNatIList#(V2)active#(isNatList(cons(V1, V2))) → and#(isNat(V1), isNatList(V2))
active#(take(s(M), cons(N, IL))) → and#(isNatIList(IL), and(isNat(M), isNat(N)))active#(take(s(M), cons(N, IL))) → U31#(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
active#(U11(X1, X2)) → U11#(active(X1), X2)active#(s(X)) → s#(active(X))
s#(ok(X)) → s#(X)active#(isNatList(take(V1, V2))) → and#(isNat(V1), isNatIList(V2))
proper#(length(X)) → proper#(X)active#(take(X1, X2)) → take#(X1, active(X2))
proper#(s(X)) → s#(proper(X))active#(zeros) → cons#(0, zeros)
top#(ok(X)) → top#(active(X))active#(take(s(M), cons(N, IL))) → isNatIList#(IL)
U11#(ok(X1), ok(X2)) → U11#(X1, X2)proper#(isNatIList(X)) → isNatIList#(proper(X))
cons#(ok(X1), ok(X2)) → cons#(X1, X2)proper#(U11(X1, X2)) → U11#(proper(X1), proper(X2))
active#(U31(X1, X2, X3, X4)) → active#(X1)proper#(U31(X1, X2, X3, X4)) → proper#(X4)
proper#(and(X1, X2)) → and#(proper(X1), proper(X2))active#(cons(X1, X2)) → cons#(active(X1), X2)
active#(length(cons(N, L))) → U11#(and(isNatList(L), isNat(N)), L)proper#(and(X1, X2)) → proper#(X2)
length#(ok(X)) → length#(X)active#(isNatList(cons(V1, V2))) → isNatList#(V2)
active#(U11(X1, X2)) → active#(X1)U21#(ok(X)) → U21#(X)
proper#(U31(X1, X2, X3, X4)) → proper#(X2)top#(mark(X)) → top#(proper(X))
proper#(cons(X1, X2)) → proper#(X2)proper#(U31(X1, X2, X3, X4)) → proper#(X3)
proper#(isNatIList(X)) → proper#(X)take#(X1, mark(X2)) → take#(X1, X2)
isNatList#(ok(X)) → isNatList#(X)active#(U11(tt, L)) → length#(L)
proper#(s(X)) → proper#(X)proper#(isNatList(X)) → isNatList#(proper(X))
proper#(take(X1, X2)) → take#(proper(X1), proper(X2))active#(isNatList(cons(V1, V2))) → isNat#(V1)
active#(cons(X1, X2)) → active#(X1)take#(mark(X1), X2) → take#(X1, X2)
and#(ok(X1), ok(X2)) → and#(X1, X2)proper#(and(X1, X2)) → proper#(X1)
active#(U21(X)) → active#(X)active#(length(cons(N, L))) → isNatList#(L)
proper#(take(X1, X2)) → proper#(X1)U31#(ok(X1), ok(X2), ok(X3), ok(X4)) → U31#(X1, X2, X3, X4)
active#(isNatList(take(V1, V2))) → isNat#(V1)active#(length(cons(N, L))) → isNat#(N)
active#(length(X)) → length#(active(X))U21#(mark(X)) → U21#(X)
active#(length(cons(N, L))) → and#(isNatList(L), isNat(N))active#(take(X1, X2)) → active#(X1)
proper#(take(X1, X2)) → proper#(X2)active#(isNatIList(V)) → isNatList#(V)
active#(isNatList(take(V1, V2))) → isNatIList#(V2)active#(take(0, IL)) → U21#(isNatIList(IL))
s#(mark(X)) → s#(X)proper#(cons(X1, X2)) → cons#(proper(X1), proper(X2))
active#(s(X)) → active#(X)proper#(U31(X1, X2, X3, X4)) → proper#(X1)
active#(and(X1, X2)) → active#(X1)active#(take(0, IL)) → isNatIList#(IL)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

The following SCCs where found

proper#(isNat(X)) → proper#(X)proper#(cons(X1, X2)) → proper#(X1)
proper#(U31(X1, X2, X3, X4)) → proper#(X2)proper#(U11(X1, X2)) → proper#(X1)
proper#(cons(X1, X2)) → proper#(X2)proper#(isNatIList(X)) → proper#(X)
proper#(U31(X1, X2, X3, X4)) → proper#(X3)proper#(take(X1, X2)) → proper#(X2)
proper#(and(X1, X2)) → proper#(X1)proper#(U31(X1, X2, X3, X4)) → proper#(X4)
proper#(s(X)) → proper#(X)proper#(length(X)) → proper#(X)
proper#(U11(X1, X2)) → proper#(X2)proper#(and(X1, X2)) → proper#(X2)
proper#(take(X1, X2)) → proper#(X1)proper#(U31(X1, X2, X3, X4)) → proper#(X1)
proper#(isNatList(X)) → proper#(X)proper#(U21(X)) → proper#(X)
U31#(ok(X1), ok(X2), ok(X3), ok(X4)) → U31#(X1, X2, X3, X4)U31#(mark(X1), X2, X3, X4) → U31#(X1, X2, X3, X4)
isNat#(ok(X)) → isNat#(X)
take#(mark(X1), X2) → take#(X1, X2)take#(X1, mark(X2)) → take#(X1, X2)
take#(ok(X1), ok(X2)) → take#(X1, X2)
U21#(ok(X)) → U21#(X)U21#(mark(X)) → U21#(X)
isNatList#(ok(X)) → isNatList#(X)
s#(mark(X)) → s#(X)s#(ok(X)) → s#(X)
isNatIList#(ok(X)) → isNatIList#(X)
cons#(mark(X1), X2) → cons#(X1, X2)cons#(ok(X1), ok(X2)) → cons#(X1, X2)
length#(mark(X)) → length#(X)length#(ok(X)) → length#(X)
active#(s(X)) → active#(X)active#(take(X1, X2)) → active#(X2)
active#(take(X1, X2)) → active#(X1)active#(length(X)) → active#(X)
active#(and(X1, X2)) → active#(X1)active#(U31(X1, X2, X3, X4)) → active#(X1)
active#(U11(X1, X2)) → active#(X1)active#(U21(X)) → active#(X)
active#(cons(X1, X2)) → active#(X1)
U11#(ok(X1), ok(X2)) → U11#(X1, X2)U11#(mark(X1), X2) → U11#(X1, X2)
and#(ok(X1), ok(X2)) → and#(X1, X2)and#(mark(X1), X2) → and#(X1, X2)
top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2)) → proper#(X1)proper#(isNat(X)) → proper#(X)
proper#(U31(X1, X2, X3, X4)) → proper#(X2)proper#(cons(X1, X2)) → proper#(X2)
proper#(U11(X1, X2)) → proper#(X1)proper#(U31(X1, X2, X3, X4)) → proper#(X3)
proper#(isNatIList(X)) → proper#(X)proper#(take(X1, X2)) → proper#(X2)
proper#(and(X1, X2)) → proper#(X1)proper#(U31(X1, X2, X3, X4)) → proper#(X4)
proper#(length(X)) → proper#(X)proper#(s(X)) → proper#(X)
proper#(U11(X1, X2)) → proper#(X2)proper#(and(X1, X2)) → proper#(X2)
proper#(take(X1, X2)) → proper#(X1)proper#(U31(X1, X2, X3, X4)) → proper#(X1)
proper#(isNatList(X)) → proper#(X)proper#(U21(X)) → proper#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(cons(X1, X2)) → proper#(X1)proper#(isNat(X)) → proper#(X)
proper#(U31(X1, X2, X3, X4)) → proper#(X2)proper#(cons(X1, X2)) → proper#(X2)
proper#(U11(X1, X2)) → proper#(X1)proper#(isNatIList(X)) → proper#(X)
proper#(U31(X1, X2, X3, X4)) → proper#(X3)proper#(take(X1, X2)) → proper#(X2)
proper#(and(X1, X2)) → proper#(X1)proper#(U31(X1, X2, X3, X4)) → proper#(X4)
proper#(length(X)) → proper#(X)proper#(s(X)) → proper#(X)
proper#(U11(X1, X2)) → proper#(X2)proper#(and(X1, X2)) → proper#(X2)
proper#(take(X1, X2)) → proper#(X1)proper#(U31(X1, X2, X3, X4)) → proper#(X1)
proper#(isNatList(X)) → proper#(X)proper#(U21(X)) → proper#(X)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

U31#(ok(X1), ok(X2), ok(X3), ok(X4)) → U31#(X1, X2, X3, X4)U31#(mark(X1), X2, X3, X4) → U31#(X1, X2, X3, X4)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U31#(ok(X1), ok(X2), ok(X3), ok(X4)) → U31#(X1, X2, X3, X4)U31#(mark(X1), X2, X3, X4) → U31#(X1, X2, X3, X4)

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

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 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

active#(s(X)) → active#(X)active#(take(X1, X2)) → active#(X2)
active#(take(X1, X2)) → active#(X1)active#(length(X)) → active#(X)
active#(and(X1, X2)) → active#(X1)active#(U31(X1, X2, X3, X4)) → active#(X1)
active#(U11(X1, X2)) → active#(X1)active#(U21(X)) → active#(X)
active#(cons(X1, X2)) → active#(X1)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(s(X)) → active#(X)active#(take(X1, X2)) → active#(X2)
active#(length(X)) → active#(X)active#(take(X1, X2)) → active#(X1)
active#(and(X1, X2)) → active#(X1)active#(U31(X1, X2, X3, X4)) → active#(X1)
active#(U11(X1, X2)) → active#(X1)active#(U21(X)) → active#(X)
active#(cons(X1, X2)) → active#(X1)

Problem 8: 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(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

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 16: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, proper, U31, U21, top, cons, nil

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 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

U21#(ok(X)) → U21#(X)U21#(mark(X)) → U21#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U21#(ok(X)) → U21#(X)U21#(mark(X)) → U21#(X)

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

isNatList#(ok(X)) → isNatList#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatList#(ok(X)) → isNatList#(X)

Problem 11: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

isNatIList#(ok(X)) → isNatIList#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatIList#(ok(X)) → isNatIList#(X)

Problem 13: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

isNat#(ok(X)) → isNat#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNat#(ok(X)) → isNat#(X)

Problem 14: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, 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 15: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(s(length(L)))
active(U21(tt)) → mark(nil)active(U31(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(and(tt, X)) → mark(X)active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))active(isNatList(take(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(take(0, IL)) → mark(U21(isNatIList(IL)))active(take(s(M), cons(N, IL))) → mark(U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N))
active(cons(X1, X2)) → cons(active(X1), X2)active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))active(length(X)) → length(active(X))
active(U21(X)) → U21(active(X))active(U31(X1, X2, X3, X4)) → U31(active(X1), X2, X3, X4)
active(take(X1, X2)) → take(active(X1), X2)active(take(X1, X2)) → take(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U21(mark(X)) → mark(U21(X))
U31(mark(X1), X2, X3, X4) → mark(U31(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U21(X)) → U21(proper(X))
proper(nil) → ok(nil)proper(U31(X1, X2, X3, X4)) → U31(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))U21(ok(X)) → ok(U21(X))
U31(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U31(X1, X2, X3, X4))take(ok(X1), ok(X2)) → ok(take(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIList, mark, and, isNat, 0, isNatList, s, zeros, tt, take, length, active, U11, ok, U31, proper, U21, nil, cons, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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