TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (15812ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 14 remains open; application of the following processors failed [DependencyGraph (5ms), PolynomialLinearRange4iUR (13ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (17ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (16ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (12ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (11ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (22ms), DependencyGraph (5ms)].
 | – Problem 3 was processed with processor SubtermCriterion (4ms).
 |    | – Problem 15 remains open; application of the following processors failed [DependencyGraph (6ms), PolynomialLinearRange4iUR (7ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (11ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (10ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (6ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (11ms), DependencyGraph (5ms)].
 | – Problem 4 was processed with processor SubtermCriterion (2ms).
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 16 was processed with processor PolynomialLinearRange4iUR (78ms).
 | – Problem 8 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 17 was processed with processor PolynomialLinearRange4iUR (86ms).
 |    |    | – Problem 19 was processed with processor PolynomialLinearRange4iUR (80ms).
 | – Problem 9 was processed with processor SubtermCriterion (1ms).
 | – Problem 10 was processed with processor SubtermCriterion (1ms).
 | – Problem 11 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (2274ms), PolynomialLinearRange4iUR (1687ms), DependencyGraph (2220ms), PolynomialLinearRange4iUR (2000ms), DependencyGraph (2211ms), PolynomialLinearRange4iUR (2501ms), DependencyGraph (2288ms), PolynomialLinearRange4iUR (2500ms), DependencyGraph (2211ms), PolynomialLinearRange4iUR (2500ms), DependencyGraph (2366ms), PolynomialLinearRange4iUR (2503ms), DependencyGraph (2211ms), PolynomialLinearRange4iUR (3333ms), DependencyGraph (2254ms), PolynomialLinearRange8NegiUR (timeout)].
 | – Problem 12 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 18 was processed with processor PolynomialLinearRange4iUR (108ms).
 |    |    | – Problem 20 was processed with processor PolynomialLinearRange4iUR (40ms).
 |    |    |    | – Problem 21 was processed with processor PolynomialLinearRange4iUR (78ms).
 |    |    |    |    | – Problem 22 was processed with processor PolynomialLinearRange4iUR (29ms).
 |    |    |    |    |    | – Problem 23 was processed with processor PolynomialLinearRange4iUR (31ms).
 |    |    |    |    |    |    | – Problem 24 was processed with processor PolynomialLinearRange4iUR (19ms).
 | – Problem 13 was processed with processor SubtermCriterion (2ms).

The following open problems remain:

Open Dependency Pair Problem 11

Dependency Pairs

active#(isNat(s(N))) → mark#(isNat(N))mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))
mark#(take(X1, X2)) → mark#(X1)mark#(isNat(X)) → active#(isNat(X))
mark#(uTake2(X1, X2, X3, X4)) → active#(uTake2(mark(X1), X2, X3, X4))mark#(tt) → active#(tt)
mark#(uLength(X1, X2)) → active#(uLength(mark(X1), X2))mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))
mark#(and(X1, X2)) → mark#(X2)active#(isNatList(take(N, IL))) → mark#(and(isNat(N), isNatIList(IL)))
active#(isNat(length(L))) → mark#(isNatList(L))active#(length(cons(N, L))) → mark#(uLength(and(isNat(N), isNatList(L)), L))
active#(isNatList(nil)) → mark#(tt)mark#(nil) → active#(nil)
mark#(uTake1(X)) → active#(uTake1(mark(X)))mark#(and(X1, X2)) → active#(and(mark(X1), mark(X2)))
mark#(length(X)) → mark#(X)active#(take(s(M), cons(N, IL))) → mark#(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active#(isNatList(cons(N, L))) → mark#(and(isNat(N), isNatList(L)))active#(isNatIList(zeros)) → mark#(tt)
mark#(s(X)) → mark#(X)mark#(zeros) → active#(zeros)
mark#(uLength(X1, X2)) → mark#(X1)mark#(isNatIList(X)) → active#(isNatIList(X))
active#(isNatIList(cons(N, IL))) → mark#(and(isNat(N), isNatIList(IL)))mark#(0) → active#(0)
mark#(s(X)) → active#(s(mark(X)))active#(and(tt, T)) → mark#(T)
active#(isNat(0)) → mark#(tt)mark#(cons(X1, X2)) → mark#(X1)
active#(uTake1(tt)) → mark#(nil)mark#(uTake2(X1, X2, X3, X4)) → mark#(X1)
active#(isNatIList(IL)) → mark#(isNatList(IL))active#(uLength(tt, L)) → mark#(s(length(L)))
active#(uTake2(tt, M, N, IL)) → mark#(cons(N, take(M, IL)))mark#(uTake1(X)) → mark#(X)
mark#(and(X1, X2)) → mark#(X1)mark#(take(X1, X2)) → mark#(X2)
active#(zeros) → mark#(cons(0, zeros))active#(take(0, IL)) → mark#(uTake1(isNatIList(IL)))
mark#(length(X)) → active#(length(mark(X)))mark#(isNatList(X)) → active#(isNatList(X))

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, cons, nil

Open Dependency Pair Problem 14

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, nil, cons

Open Dependency Pair Problem 15

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, nil, cons

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

active#(isNat(s(N))) → mark#(isNat(N))active#(take(s(M), cons(N, IL))) → and#(isNat(M), and(isNat(N), isNatIList(IL)))
uTake1#(mark(X)) → uTake1#(X)mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))
active#(uTake2(tt, M, N, IL)) → cons#(N, take(M, IL))active#(isNatList(take(N, IL))) → mark#(and(isNat(N), isNatIList(IL)))
active#(length(cons(N, L))) → mark#(uLength(and(isNat(N), isNatList(L)), L))uTake2#(mark(X1), X2, X3, X4) → uTake2#(X1, X2, X3, X4)
uTake2#(X1, X2, X3, mark(X4)) → uTake2#(X1, X2, X3, X4)isNat#(active(X)) → isNat#(X)
mark#(s(X)) → mark#(X)uLength#(X1, mark(X2)) → uLength#(X1, X2)
uTake2#(active(X1), X2, X3, X4) → uTake2#(X1, X2, X3, X4)mark#(uTake2(X1, X2, X3, X4)) → uTake2#(mark(X1), X2, X3, X4)
length#(mark(X)) → length#(X)uLength#(active(X1), X2) → uLength#(X1, X2)
active#(and(tt, T)) → mark#(T)active#(length(cons(N, L))) → and#(isNat(N), isNatList(L))
mark#(cons(X1, X2)) → mark#(X1)active#(uLength(tt, L)) → mark#(s(length(L)))
and#(mark(X1), X2) → and#(X1, X2)active#(uTake2(tt, M, N, IL)) → mark#(cons(N, take(M, IL)))
mark#(and(X1, X2)) → mark#(X1)active#(take(s(M), cons(N, IL))) → isNat#(M)
uTake2#(X1, active(X2), X3, X4) → uTake2#(X1, X2, X3, X4)active#(isNatIList(cons(N, IL))) → and#(isNat(N), isNatIList(IL))
active#(take(s(M), cons(N, IL))) → uTake2#(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)mark#(uTake1(X)) → uTake1#(mark(X))
cons#(mark(X1), X2) → cons#(X1, X2)mark#(tt) → active#(tt)
active#(take(s(M), cons(N, IL))) → isNat#(N)active#(isNat(length(L))) → mark#(isNatList(L))
mark#(uTake1(X)) → active#(uTake1(mark(X)))active#(isNatList(take(N, IL))) → isNatIList#(IL)
uTake2#(X1, X2, active(X3), X4) → uTake2#(X1, X2, X3, X4)mark#(length(X)) → mark#(X)
active#(isNatIList(IL)) → isNatList#(IL)active#(take(s(M), cons(N, IL))) → mark#(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
cons#(X1, mark(X2)) → cons#(X1, X2)mark#(zeros) → active#(zeros)
active#(uTake2(tt, M, N, IL)) → take#(M, IL)mark#(0) → active#(0)
mark#(s(X)) → active#(s(mark(X)))uLength#(mark(X1), X2) → uLength#(X1, X2)
active#(uTake1(tt)) → mark#(nil)mark#(uTake2(X1, X2, X3, X4)) → mark#(X1)
cons#(active(X1), X2) → cons#(X1, X2)active#(isNatList(cons(N, L))) → isNat#(N)
mark#(isNatList(X)) → isNatList#(X)isNatList#(mark(X)) → isNatList#(X)
active#(zeros) → cons#(0, zeros)uTake2#(X1, mark(X2), X3, X4) → uTake2#(X1, X2, X3, X4)
mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))mark#(take(X1, X2)) → mark#(X1)
active#(take(s(M), cons(N, IL))) → isNatIList#(IL)mark#(uLength(X1, X2)) → active#(uLength(mark(X1), X2))
mark#(and(X1, X2)) → mark#(X2)mark#(s(X)) → s#(mark(X))
length#(active(X)) → length#(X)mark#(uLength(X1, X2)) → uLength#(mark(X1), X2)
active#(isNat(s(N))) → isNat#(N)active#(isNatIList(cons(N, IL))) → isNat#(N)
mark#(uLength(X1, X2)) → mark#(X1)mark#(isNatIList(X)) → active#(isNatIList(X))
active#(isNatIList(cons(N, IL))) → mark#(and(isNat(N), isNatIList(IL)))isNatList#(active(X)) → isNatList#(X)
active#(length(cons(N, L))) → uLength#(and(isNat(N), isNatList(L)), L)active#(isNatIList(cons(N, IL))) → isNatIList#(IL)
active#(isNat(0)) → mark#(tt)isNatIList#(active(X)) → isNatIList#(X)
active#(uLength(tt, L)) → length#(L)take#(X1, mark(X2)) → take#(X1, X2)
mark#(isNatIList(X)) → isNatIList#(X)isNatIList#(mark(X)) → isNatIList#(X)
mark#(uTake1(X)) → mark#(X)uTake1#(active(X)) → uTake1#(X)
cons#(X1, active(X2)) → cons#(X1, X2)active#(isNatList(take(N, IL))) → isNat#(N)
active#(isNatList(cons(N, L))) → and#(isNat(N), isNatList(L))active#(isNatList(cons(N, L))) → isNatList#(L)
active#(take(0, IL)) → mark#(uTake1(isNatIList(IL)))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)mark#(uTake2(X1, X2, X3, X4)) → active#(uTake2(mark(X1), X2, X3, X4))
active#(isNat(length(L))) → isNatList#(L)mark#(isNat(X)) → isNat#(X)
isNat#(mark(X)) → isNat#(X)active#(length(cons(N, L))) → isNatList#(L)
active#(isNatList(nil)) → mark#(tt)uLength#(X1, active(X2)) → uLength#(X1, X2)
active#(take(s(M), cons(N, IL))) → and#(isNat(N), isNatIList(IL))mark#(nil) → active#(nil)
mark#(and(X1, X2)) → active#(and(mark(X1), mark(X2)))take#(X1, active(X2)) → take#(X1, X2)
active#(length(cons(N, L))) → isNat#(N)active#(isNatList(cons(N, L))) → mark#(and(isNat(N), isNatList(L)))
active#(isNatIList(zeros)) → mark#(tt)mark#(cons(X1, X2)) → cons#(mark(X1), X2)
active#(take(0, IL)) → uTake1#(isNatIList(IL))and#(X1, mark(X2)) → and#(X1, X2)
mark#(length(X)) → length#(mark(X))active#(isNatList(take(N, IL))) → and#(isNat(N), isNatIList(IL))
active#(isNatIList(IL)) → mark#(isNatList(IL))uTake2#(X1, X2, mark(X3), X4) → uTake2#(X1, X2, X3, X4)
mark#(take(X1, X2)) → take#(mark(X1), mark(X2))s#(mark(X)) → s#(X)
uTake2#(X1, X2, X3, active(X4)) → uTake2#(X1, X2, X3, X4)active#(uLength(tt, L)) → s#(length(L))
mark#(and(X1, X2)) → and#(mark(X1), mark(X2))mark#(take(X1, X2)) → mark#(X2)
active#(zeros) → mark#(cons(0, zeros))s#(active(X)) → s#(X)
mark#(length(X)) → active#(length(mark(X)))mark#(isNatList(X)) → active#(isNatList(X))
active#(take(0, IL)) → isNatIList#(IL)take#(active(X1), X2) → take#(X1, X2)

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, nil, cons

Strategy

The following SCCs where found

uTake2#(mark(X1), X2, X3, X4) → uTake2#(X1, X2, X3, X4)uTake2#(X1, mark(X2), X3, X4) → uTake2#(X1, X2, X3, X4)
uTake2#(active(X1), X2, X3, X4) → uTake2#(X1, X2, X3, X4)uTake2#(X1, X2, X3, active(X4)) → uTake2#(X1, X2, X3, X4)
uTake2#(X1, X2, active(X3), X4) → uTake2#(X1, X2, X3, X4)uTake2#(X1, active(X2), X3, X4) → uTake2#(X1, X2, X3, X4)
uTake2#(X1, X2, X3, mark(X4)) → uTake2#(X1, X2, X3, X4)uTake2#(X1, X2, mark(X3), X4) → uTake2#(X1, X2, X3, X4)
length#(mark(X)) → length#(X)length#(active(X)) → length#(X)
isNatIList#(active(X)) → isNatIList#(X)isNatIList#(mark(X)) → isNatIList#(X)
uLength#(X1, mark(X2)) → uLength#(X1, X2)uLength#(X1, active(X2)) → uLength#(X1, X2)
uLength#(mark(X1), X2) → uLength#(X1, X2)uLength#(active(X1), X2) → uLength#(X1, X2)
mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))active#(isNat(s(N))) → mark#(isNat(N))
mark#(isNat(X)) → active#(isNat(X))mark#(take(X1, X2)) → mark#(X1)
mark#(tt) → active#(tt)mark#(uTake2(X1, X2, X3, X4)) → active#(uTake2(mark(X1), X2, X3, X4))
mark#(uLength(X1, X2)) → active#(uLength(mark(X1), X2))mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))
mark#(and(X1, X2)) → mark#(X2)active#(isNatList(take(N, IL))) → mark#(and(isNat(N), isNatIList(IL)))
active#(isNat(length(L))) → mark#(isNatList(L))active#(isNatList(nil)) → mark#(tt)
active#(length(cons(N, L))) → mark#(uLength(and(isNat(N), isNatList(L)), L))mark#(uTake1(X)) → active#(uTake1(mark(X)))
mark#(nil) → active#(nil)mark#(and(X1, X2)) → active#(and(mark(X1), mark(X2)))
active#(isNatList(cons(N, L))) → mark#(and(isNat(N), isNatList(L)))active#(take(s(M), cons(N, IL))) → mark#(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
mark#(length(X)) → mark#(X)mark#(s(X)) → mark#(X)
active#(isNatIList(zeros)) → mark#(tt)mark#(uLength(X1, X2)) → mark#(X1)
mark#(zeros) → active#(zeros)mark#(isNatIList(X)) → active#(isNatIList(X))
active#(isNatIList(cons(N, IL))) → mark#(and(isNat(N), isNatIList(IL)))mark#(0) → active#(0)
mark#(s(X)) → active#(s(mark(X)))active#(and(tt, T)) → mark#(T)
active#(isNat(0)) → mark#(tt)active#(uTake1(tt)) → mark#(nil)
mark#(cons(X1, X2)) → mark#(X1)active#(isNatIList(IL)) → mark#(isNatList(IL))
mark#(uTake2(X1, X2, X3, X4)) → mark#(X1)active#(uLength(tt, L)) → mark#(s(length(L)))
active#(uTake2(tt, M, N, IL)) → mark#(cons(N, take(M, IL)))mark#(uTake1(X)) → mark#(X)
mark#(and(X1, X2)) → mark#(X1)mark#(take(X1, X2)) → mark#(X2)
active#(zeros) → mark#(cons(0, zeros))mark#(isNatList(X)) → active#(isNatList(X))
mark#(length(X)) → active#(length(mark(X)))active#(take(0, IL)) → mark#(uTake1(isNatIList(IL)))
isNatList#(mark(X)) → isNatList#(X)isNatList#(active(X)) → isNatList#(X)
uTake1#(active(X)) → uTake1#(X)uTake1#(mark(X)) → uTake1#(X)
s#(mark(X)) → s#(X)s#(active(X)) → s#(X)
cons#(X1, active(X2)) → cons#(X1, X2)cons#(mark(X1), X2) → cons#(X1, X2)
cons#(X1, mark(X2)) → cons#(X1, X2)cons#(active(X1), X2) → cons#(X1, X2)
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)
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

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(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

uTake1#(active(X)) → uTake1#(X)uTake1#(mark(X)) → uTake1#(X)

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

uTake1#(active(X)) → uTake1#(X)uTake1#(mark(X)) → uTake1#(X)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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 7: 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(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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 16: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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, active(X2)) → take#(X1, X2)take#(X1, mark(X2)) → take#(X1, X2)

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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 17: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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 19: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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)

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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 12: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 18: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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:

uTake2#(X1, active(X2), X3, X4) → uTake2#(X1, X2, X3, X4)

Problem 20: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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:

uTake2#(X1, mark(X2), X3, X4) → uTake2#(X1, X2, X3, X4)

Problem 21: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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:

uTake2#(X1, X2, X3, mark(X4)) → uTake2#(X1, X2, X3, X4)

Problem 22: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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:

uTake2#(X1, X2, X3, active(X4)) → uTake2#(X1, X2, X3, X4)

Problem 23: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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:

uTake2#(X1, X2, mark(X3), X4) → uTake2#(X1, X2, X3, X4)

Problem 24: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

uTake2#(X1, X2, active(X3), X4) → uTake2#(X1, X2, X3, X4)

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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:

uTake2#(X1, X2, active(X3), X4) → uTake2#(X1, X2, X3, X4)

Problem 13: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(and(tt, T)) → mark(T)active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0)) → mark(tt)active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0, zeros))active(take(0, IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))mark(and(X1, X2)) → active(and(mark(X1), mark(X2)))
mark(tt) → active(tt)mark(isNatIList(X)) → active(isNatIList(X))
mark(isNatList(X)) → active(isNatList(X))mark(isNat(X)) → active(isNat(X))
mark(0) → active(0)mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(nil) → active(nil)
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))mark(uTake1(X)) → active(uTake1(mark(X)))
mark(uTake2(X1, X2, X3, X4)) → active(uTake2(mark(X1), X2, X3, X4))mark(uLength(X1, X2)) → active(uLength(mark(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)
isNatIList(mark(X)) → isNatIList(X)isNatIList(active(X)) → isNatIList(X)
isNatList(mark(X)) → isNatList(X)isNatList(active(X)) → isNatList(X)
isNat(mark(X)) → isNat(X)isNat(active(X)) → isNat(X)
s(mark(X)) → s(X)s(active(X)) → s(X)
length(mark(X)) → length(X)length(active(X)) → length(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)
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)
uTake1(mark(X)) → uTake1(X)uTake1(active(X)) → uTake1(X)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)uLength(X1, mark(X2)) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)uLength(X1, active(X2)) → uLength(X1, X2)

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, mark, and, uTake1, isNat, uTake2, 0, isNatList, s, tt, zeros, take, length, active, 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)