TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (16177ms).
 | – Problem 2 was processed with processor SubtermCriterion (5ms).
 | – Problem 3 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 14 remains open; application of the following processors failed [DependencyGraph (6ms), PolynomialLinearRange4iUR (14ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (17ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (5ms), PolynomialLinearRange8NegiUR (1ms), DependencyGraph (5ms)].
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor SubtermCriterion (2ms).
 | – Problem 6 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 15 remains open; application of the following processors failed [DependencyGraph (33ms), PolynomialLinearRange4iUR (4ms), DependencyGraph (35ms), PolynomialLinearRange4iUR (3ms), DependencyGraph (34ms), PolynomialLinearRange4iUR (5ms), DependencyGraph (33ms), PolynomialLinearRange8NegiUR (1ms), DependencyGraph (33ms)].
 | – Problem 7 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 16 was processed with processor PolynomialLinearRange4iUR (98ms).
 | – Problem 8 was processed with processor SubtermCriterion (1ms).
 | – Problem 9 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (2190ms), PolynomialLinearRange4iUR (1701ms), DependencyGraph (2269ms), PolynomialLinearRange4iUR (2007ms), DependencyGraph (2203ms), PolynomialLinearRange4iUR (3333ms), DependencyGraph (2199ms), PolynomialLinearRange8NegiUR (10000ms), DependencyGraph (2277ms), ReductionPairSAT (timeout)].
 | – Problem 10 was processed with processor SubtermCriterion (4ms).
 | – Problem 11 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 17 was processed with processor PolynomialLinearRange4iUR (79ms).
 |    |    | – Problem 19 was processed with processor PolynomialLinearRange4iUR (56ms).
 | – Problem 12 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 18 was processed with processor PolynomialLinearRange4iUR (41ms).
 |    |    | – Problem 20 was processed with processor PolynomialLinearRange4iUR (21ms).
 | – Problem 13 was processed with processor SubtermCriterion (1ms).

The following open problems remain:

Open Dependency Pair Problem 9

Dependency Pairs

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

Open Dependency Pair Problem 14

Dependency Pairs

U11#(X1, active(X2)) → U11#(X1, X2)U11#(X1, mark(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Open Dependency Pair Problem 15

Dependency Pairs

U31#(X1, active(X2), X3, X4) → U31#(X1, X2, X3, X4)U31#(X1, X2, active(X3), X4) → U31#(X1, X2, X3, X4)
U31#(X1, mark(X2), X3, X4) → U31#(X1, X2, X3, X4)U31#(X1, X2, X3, mark(X4)) → U31#(X1, X2, X3, X4)
U31#(X1, X2, mark(X3), X4) → U31#(X1, X2, X3, X4)U31#(X1, X2, X3, active(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

Strategy

The following SCCs where found

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

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

isNat#(active(X)) → isNat#(X)isNat#(mark(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNat#(active(X)) → isNat#(X)isNat#(mark(X)) → isNat#(X)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

U11#(X1, active(X2)) → U11#(X1, X2)U11#(active(X1), X2) → U11#(X1, X2)
U11#(mark(X1), X2) → U11#(X1, X2)U11#(X1, mark(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

s#(mark(X)) → s#(X)s#(active(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

s#(mark(X)) → s#(X)s#(active(X)) → s#(X)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

U21#(mark(X)) → U21#(X)U21#(active(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U21#(mark(X)) → U21#(X)U21#(active(X)) → U21#(X)

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

U31#(X1, active(X2), X3, X4) → U31#(X1, X2, X3, X4)U31#(X1, X2, active(X3), X4) → U31#(X1, X2, X3, X4)
U31#(X1, mark(X2), X3, X4) → U31#(X1, X2, X3, X4)U31#(mark(X1), X2, X3, X4) → U31#(X1, X2, X3, X4)
U31#(X1, X2, X3, mark(X4)) → U31#(X1, X2, X3, X4)U31#(active(X1), X2, X3, X4) → U31#(X1, X2, X3, X4)
U31#(X1, X2, mark(X3), X4) → U31#(X1, X2, X3, X4)U31#(X1, X2, X3, active(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

and#(active(X1), X2) → and#(X1, X2)and#(X1, active(X2)) → and#(X1, X2)
and#(mark(X1), X2) → and#(X1, X2)and#(X1, mark(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 16: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

and#(X1, active(X2)) → and#(X1, X2)and#(X1, mark(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, 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:

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

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

isNatIList#(active(X)) → isNatIList#(X)isNatIList#(mark(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatIList#(active(X)) → isNatIList#(X)isNatIList#(mark(X)) → isNatIList#(X)

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

isNatList#(mark(X)) → isNatList#(X)isNatList#(active(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatList#(mark(X)) → isNatList#(X)isNatList#(active(X)) → isNatList#(X)

Problem 11: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

take#(mark(X1), X2) → take#(X1, X2)take#(X1, active(X2)) → take#(X1, X2)
take#(X1, mark(X2)) → take#(X1, X2)take#(active(X1), 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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 17: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

take#(X1, active(X2)) → take#(X1, X2)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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, 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 19: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

take#(X1, active(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, 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, active(X2)) → take#(X1, X2)

Problem 12: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

cons#(X1, active(X2)) → cons#(X1, X2)cons#(mark(X1), X2) → cons#(X1, X2)
cons#(active(X1), X2) → cons#(X1, X2)cons#(X1, mark(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 18: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

cons#(X1, active(X2)) → cons#(X1, X2)cons#(X1, mark(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, 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:

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

Problem 20: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

cons#(X1, mark(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, 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:

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

Problem 13: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

length#(mark(X)) → length#(X)length#(active(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))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(U21(X)) → active(U21(mark(X)))
mark(nil) → active(nil)mark(U31(X1, X2, X3, X4)) → active(U31(mark(X1), X2, X3, X4))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X)) → U21(X)
U21(active(X)) → U21(X)U31(mark(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, mark(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, mark(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, mark(X4)) → U31(X1, X2, X3, X4)U31(active(X1), X2, X3, X4) → U31(X1, X2, X3, X4)
U31(X1, active(X2), X3, X4) → U31(X1, X2, X3, X4)U31(X1, X2, active(X3), X4) → U31(X1, X2, X3, X4)
U31(X1, X2, X3, active(X4)) → U31(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(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, U31, U21, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

length#(mark(X)) → length#(X)length#(active(X)) → length#(X)