TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (10581ms).
 | – Problem 2 was processed with processor SubtermCriterion (4ms).
 |    | – Problem 12 remains open; application of the following processors failed [DependencyGraph (6ms), PolynomialLinearRange4iUR (13ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (11ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (19ms), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (24ms), DependencyGraph (5ms)].
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 13 remains open; application of the following processors failed [DependencyGraph (37ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (38ms), PolynomialLinearRange4iUR (6ms), DependencyGraph (38ms), PolynomialLinearRange4iUR (8ms), DependencyGraph (36ms), PolynomialLinearRange8NegiUR (33ms), DependencyGraph (37ms)].
 | – Problem 4 was processed with processor SubtermCriterion (2ms).
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 14 remains open; application of the following processors failed [DependencyGraph (6ms), PolynomialLinearRange4iUR (5ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (16ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (5ms), PolynomialLinearRange8NegiUR (6ms), DependencyGraph (5ms)].
 | – Problem 6 remains open; application of the following processors failed [SubtermCriterion (4ms), DependencyGraph (1308ms), PolynomialLinearRange4iUR (1250ms), DependencyGraph (1374ms), PolynomialLinearRange4iUR (1250ms), DependencyGraph (1411ms), PolynomialLinearRange4iUR (1666ms), DependencyGraph (1377ms), PolynomialLinearRange8NegiUR (5000ms), DependencyGraph (1370ms), ReductionPairSAT (timeout)].
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 15 remains open; application of the following processors failed [DependencyGraph (36ms), PolynomialLinearRange4iUR (28ms), DependencyGraph (38ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (38ms), PolynomialLinearRange4iUR (4ms), DependencyGraph (37ms), PolynomialLinearRange8NegiUR (22ms), DependencyGraph (36ms)].
 | – Problem 9 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 16 was processed with processor PolynomialLinearRange4iUR (73ms).
 |    |    | – Problem 20 was processed with processor PolynomialLinearRange4iUR (41ms).
 |    |    |    | – Problem 22 remains open; application of the following processors failed [DependencyGraph (17ms), PolynomialLinearRange4iUR (1ms), DependencyGraph (60ms), PolynomialLinearRange8NegiUR (21ms), DependencyGraph (17ms)].
 | – Problem 10 was processed with processor SubtermCriterion (4ms).
 |    | – Problem 17 was processed with processor PolynomialLinearRange4iUR (130ms).
 |    |    | – Problem 19 was processed with processor PolynomialLinearRange4iUR (42ms).
 | – Problem 11 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 18 was processed with processor PolynomialLinearRange4iUR (38ms).
 |    |    | – Problem 21 was processed with processor PolynomialLinearRange4iUR (40ms).

The following open problems remain:

Open Dependency Pair Problem 6

Dependency Pairs

mark#(U11(X1, X2)) → mark#(X1)mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))
mark#(take(X1, X2)) → mark#(X1)mark#(tt) → active#(tt)
active#(length(nil)) → mark#(0)mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))
active#(take(0, IL)) → mark#(nil)mark#(nil) → active#(nil)
mark#(length(X)) → mark#(X)active#(U21(tt, IL, M, N)) → mark#(U22(tt, IL, M, N))
mark#(s(X)) → mark#(X)active#(length(cons(N, L))) → mark#(U11(tt, L))
mark#(U11(X1, X2)) → active#(U11(mark(X1), X2))mark#(zeros) → active#(zeros)
active#(take(s(M), cons(N, IL))) → mark#(U21(tt, IL, M, N))mark#(U12(X1, X2)) → mark#(X1)
mark#(0) → active#(0)mark#(s(X)) → active#(s(mark(X)))
mark#(U21(X1, X2, X3, X4)) → mark#(X1)active#(U23(tt, IL, M, N)) → mark#(cons(N, take(M, IL)))
mark#(U22(X1, X2, X3, X4)) → mark#(X1)mark#(cons(X1, X2)) → mark#(X1)
mark#(U21(X1, X2, X3, X4)) → active#(U21(mark(X1), X2, X3, X4))mark#(U23(X1, X2, X3, X4)) → active#(U23(mark(X1), X2, X3, X4))
active#(U22(tt, IL, M, N)) → mark#(U23(tt, IL, M, N))mark#(U23(X1, X2, X3, X4)) → mark#(X1)
active#(U11(tt, L)) → mark#(U12(tt, L))mark#(take(X1, X2)) → mark#(X2)
mark#(U12(X1, X2)) → active#(U12(mark(X1), X2))active#(U12(tt, L)) → mark#(s(length(L)))
active#(zeros) → mark#(cons(0, zeros))mark#(U22(X1, X2, X3, X4)) → active#(U22(mark(X1), X2, X3, X4))
mark#(length(X)) → active#(length(mark(X)))

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, nil, cons, U22

Open Dependency Pair Problem 22

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Open Dependency Pair Problem 12

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Open Dependency Pair Problem 13

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Open Dependency Pair Problem 14

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Open Dependency Pair Problem 15

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))mark#(U11(X1, X2)) → mark#(X1)
mark#(take(X1, X2)) → mark#(X1)U12#(active(X1), X2) → U12#(X1, X2)
U23#(active(X1), X2, X3, X4) → U23#(X1, X2, X3, X4)U23#(X1, active(X2), X3, X4) → U23#(X1, X2, X3, X4)
U22#(X1, X2, X3, mark(X4)) → U22#(X1, X2, X3, X4)mark#(U22(X1, X2, X3, X4)) → U22#(mark(X1), X2, X3, X4)
U21#(X1, X2, mark(X3), X4) → U21#(X1, X2, X3, X4)active#(length(nil)) → mark#(0)
mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))U11#(mark(X1), X2) → U11#(X1, X2)
active#(U23(tt, IL, M, N)) → cons#(N, take(M, IL))mark#(s(X)) → s#(mark(X))
U23#(X1, X2, X3, active(X4)) → U23#(X1, X2, X3, X4)length#(active(X)) → length#(X)
active#(U11(tt, L)) → U12#(tt, L)U22#(X1, X2, X3, active(X4)) → U22#(X1, X2, X3, X4)
U12#(mark(X1), X2) → U12#(X1, X2)mark#(s(X)) → mark#(X)
active#(length(cons(N, L))) → mark#(U11(tt, L))mark#(U11(X1, X2)) → active#(U11(mark(X1), X2))
mark#(U12(X1, X2)) → mark#(X1)length#(mark(X)) → length#(X)
U11#(active(X1), X2) → U11#(X1, X2)active#(length(cons(N, L))) → U11#(tt, L)
mark#(cons(X1, X2)) → mark#(X1)active#(U23(tt, IL, M, N)) → mark#(cons(N, take(M, IL)))
U23#(X1, mark(X2), X3, X4) → U23#(X1, X2, X3, X4)U22#(X1, X2, mark(X3), X4) → U22#(X1, X2, X3, X4)
take#(X1, mark(X2)) → take#(X1, X2)active#(U21(tt, IL, M, N)) → U22#(tt, IL, M, N)
mark#(U21(X1, X2, X3, X4)) → U21#(mark(X1), X2, X3, X4)U22#(X1, active(X2), X3, X4) → U22#(X1, X2, X3, X4)
U11#(X1, mark(X2)) → U11#(X1, X2)U11#(X1, active(X2)) → U11#(X1, X2)
cons#(X1, active(X2)) → cons#(X1, X2)mark#(U23(X1, X2, X3, X4)) → mark#(X1)
U23#(mark(X1), X2, X3, X4) → U23#(X1, X2, X3, X4)U22#(mark(X1), X2, X3, X4) → U22#(X1, X2, X3, X4)
U23#(X1, X2, active(X3), X4) → U23#(X1, X2, X3, X4)U22#(X1, mark(X2), X3, X4) → U22#(X1, X2, X3, X4)
take#(mark(X1), X2) → take#(X1, X2)U23#(X1, X2, X3, mark(X4)) → U23#(X1, X2, X3, X4)
U12#(X1, active(X2)) → U12#(X1, X2)mark#(U23(X1, X2, X3, X4)) → U23#(mark(X1), X2, X3, X4)
cons#(mark(X1), X2) → cons#(X1, X2)mark#(tt) → active#(tt)
U21#(X1, mark(X2), X3, X4) → U21#(X1, X2, X3, X4)active#(take(0, IL)) → mark#(nil)
U21#(mark(X1), X2, X3, X4) → U21#(X1, X2, X3, X4)mark#(nil) → active#(nil)
active#(U23(tt, IL, M, N)) → take#(M, IL)U21#(X1, active(X2), X3, X4) → U21#(X1, X2, X3, X4)
take#(X1, active(X2)) → take#(X1, X2)mark#(U11(X1, X2)) → U11#(mark(X1), X2)
mark#(length(X)) → mark#(X)active#(U21(tt, IL, M, N)) → mark#(U22(tt, IL, M, N))
U23#(X1, X2, mark(X3), X4) → U23#(X1, X2, X3, X4)active#(U22(tt, IL, M, N)) → U23#(tt, IL, M, N)
cons#(X1, mark(X2)) → cons#(X1, X2)mark#(zeros) → active#(zeros)
mark#(cons(X1, X2)) → cons#(mark(X1), X2)active#(take(s(M), cons(N, IL))) → mark#(U21(tt, IL, M, N))
U12#(X1, mark(X2)) → U12#(X1, X2)mark#(length(X)) → length#(mark(X))
mark#(0) → active#(0)mark#(s(X)) → active#(s(mark(X)))
mark#(U21(X1, X2, X3, X4)) → mark#(X1)active#(U12(tt, L)) → length#(L)
mark#(U22(X1, X2, X3, X4)) → mark#(X1)U22#(X1, X2, active(X3), X4) → U22#(X1, X2, X3, X4)
cons#(active(X1), X2) → cons#(X1, X2)mark#(U21(X1, X2, X3, X4)) → active#(U21(mark(X1), X2, X3, X4))
mark#(U23(X1, X2, X3, X4)) → active#(U23(mark(X1), X2, X3, X4))mark#(take(X1, X2)) → take#(mark(X1), mark(X2))
U21#(active(X1), X2, X3, X4) → U21#(X1, X2, X3, X4)U22#(active(X1), X2, X3, X4) → U22#(X1, X2, X3, X4)
mark#(U12(X1, X2)) → U12#(mark(X1), X2)active#(U22(tt, IL, M, N)) → mark#(U23(tt, IL, M, N))
active#(U12(tt, L)) → s#(length(L))s#(mark(X)) → s#(X)
U21#(X1, X2, X3, mark(X4)) → U21#(X1, X2, X3, X4)U21#(X1, X2, active(X3), X4) → U21#(X1, X2, X3, X4)
U21#(X1, X2, X3, active(X4)) → U21#(X1, X2, X3, X4)active#(take(s(M), cons(N, IL))) → U21#(tt, IL, M, N)
active#(U11(tt, L)) → mark#(U12(tt, L))active#(zeros) → cons#(0, zeros)
mark#(U12(X1, X2)) → active#(U12(mark(X1), X2))active#(U12(tt, L)) → mark#(s(length(L)))
mark#(take(X1, X2)) → mark#(X2)active#(zeros) → mark#(cons(0, zeros))
s#(active(X)) → s#(X)mark#(U22(X1, X2, X3, X4)) → active#(U22(mark(X1), X2, X3, X4))
mark#(length(X)) → active#(length(mark(X)))take#(active(X1), X2) → take#(X1, X2)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Strategy

The following SCCs where found

U11#(X1, active(X2)) → U11#(X1, X2)U11#(active(X1), X2) → U11#(X1, X2)
U11#(mark(X1), X2) → U11#(X1, X2)U11#(X1, mark(X2)) → U11#(X1, X2)
length#(mark(X)) → length#(X)length#(active(X)) → length#(X)
U23#(X1, X2, X3, active(X4)) → U23#(X1, X2, X3, X4)U23#(X1, X2, X3, mark(X4)) → U23#(X1, X2, X3, X4)
U23#(active(X1), X2, X3, X4) → U23#(X1, X2, X3, X4)U23#(X1, active(X2), X3, X4) → U23#(X1, X2, X3, X4)
U23#(mark(X1), X2, X3, X4) → U23#(X1, X2, X3, X4)U23#(X1, X2, active(X3), X4) → U23#(X1, X2, X3, X4)
U23#(X1, X2, mark(X3), X4) → U23#(X1, X2, X3, X4)U23#(X1, mark(X2), X3, X4) → U23#(X1, X2, X3, X4)
mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))mark#(U11(X1, X2)) → mark#(X1)
mark#(take(X1, X2)) → mark#(X1)mark#(tt) → active#(tt)
active#(length(nil)) → mark#(0)mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))
active#(take(0, IL)) → mark#(nil)mark#(nil) → active#(nil)
mark#(length(X)) → mark#(X)active#(U21(tt, IL, M, N)) → mark#(U22(tt, IL, M, N))
active#(length(cons(N, L))) → mark#(U11(tt, L))mark#(s(X)) → mark#(X)
mark#(zeros) → active#(zeros)mark#(U11(X1, X2)) → active#(U11(mark(X1), X2))
active#(take(s(M), cons(N, IL))) → mark#(U21(tt, IL, M, N))mark#(U12(X1, X2)) → mark#(X1)
mark#(0) → active#(0)mark#(s(X)) → active#(s(mark(X)))
mark#(U21(X1, X2, X3, X4)) → mark#(X1)mark#(cons(X1, X2)) → mark#(X1)
mark#(U22(X1, X2, X3, X4)) → mark#(X1)active#(U23(tt, IL, M, N)) → mark#(cons(N, take(M, IL)))
mark#(U21(X1, X2, X3, X4)) → active#(U21(mark(X1), X2, X3, X4))mark#(U23(X1, X2, X3, X4)) → active#(U23(mark(X1), X2, X3, X4))
active#(U22(tt, IL, M, N)) → mark#(U23(tt, IL, M, N))mark#(U23(X1, X2, X3, X4)) → mark#(X1)
active#(U11(tt, L)) → mark#(U12(tt, L))active#(U12(tt, L)) → mark#(s(length(L)))
mark#(U12(X1, X2)) → active#(U12(mark(X1), X2))mark#(take(X1, X2)) → mark#(X2)
active#(zeros) → mark#(cons(0, zeros))mark#(U22(X1, X2, X3, X4)) → active#(U22(mark(X1), X2, X3, X4))
mark#(length(X)) → active#(length(mark(X)))
U12#(active(X1), X2) → U12#(X1, X2)U12#(X1, active(X2)) → U12#(X1, X2)
U12#(mark(X1), X2) → U12#(X1, X2)U12#(X1, mark(X2)) → U12#(X1, X2)
U22#(X1, X2, X3, mark(X4)) → U22#(X1, X2, X3, X4)U22#(mark(X1), X2, X3, X4) → U22#(X1, X2, X3, X4)
U22#(X1, X2, X3, active(X4)) → U22#(X1, X2, X3, X4)U22#(X1, X2, active(X3), X4) → U22#(X1, X2, X3, X4)
U22#(X1, X2, mark(X3), X4) → U22#(X1, X2, X3, X4)U22#(X1, mark(X2), X3, X4) → U22#(X1, X2, X3, X4)
U22#(X1, active(X2), X3, X4) → U22#(X1, X2, X3, X4)U22#(active(X1), X2, X3, X4) → U22#(X1, X2, X3, X4)
cons#(X1, active(X2)) → cons#(X1, X2)cons#(mark(X1), X2) → cons#(X1, X2)
cons#(active(X1), X2) → cons#(X1, X2)cons#(X1, mark(X2)) → cons#(X1, X2)
s#(mark(X)) → s#(X)s#(active(X)) → s#(X)
U21#(X1, X2, X3, mark(X4)) → U21#(X1, X2, X3, X4)U21#(X1, X2, active(X3), X4) → U21#(X1, X2, X3, X4)
U21#(X1, X2, X3, active(X4)) → U21#(X1, X2, X3, X4)U21#(X1, active(X2), X3, X4) → U21#(X1, X2, X3, X4)
U21#(X1, X2, mark(X3), X4) → U21#(X1, X2, X3, X4)U21#(X1, mark(X2), X3, X4) → U21#(X1, X2, X3, X4)
U21#(active(X1), X2, X3, X4) → U21#(X1, X2, X3, X4)U21#(mark(X1), X2, X3, X4) → U21#(X1, X2, X3, X4)
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

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

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

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

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

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

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

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 16: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, nil, cons, U22

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:

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

Problem 20: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, 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:

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

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 17: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, nil, cons, U22

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:

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

Problem 19: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, 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:

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

Problem 11: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 18: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, nil, cons, U22

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:

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

Problem 21: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt, L)) → mark(U12(tt, L))
active(U12(tt, L)) → mark(s(length(L)))active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N))
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N))active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(length(nil)) → mark(0)active(length(cons(N, L))) → mark(U11(tt, L))
active(take(0, IL)) → mark(nil)active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N))
mark(zeros) → active(zeros)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)mark(U12(X1, X2)) → active(U12(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(length(X)) → active(length(mark(X)))
mark(U21(X1, X2, X3, X4)) → active(U21(mark(X1), X2, X3, X4))mark(U22(X1, X2, X3, X4)) → active(U22(mark(X1), X2, X3, X4))
mark(U23(X1, X2, X3, X4)) → active(U23(mark(X1), X2, X3, X4))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)U12(mark(X1), X2) → U12(X1, X2)
U12(X1, mark(X2)) → U12(X1, X2)U12(active(X1), X2) → U12(X1, X2)
U12(X1, active(X2)) → U12(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)length(mark(X)) → length(X)
length(active(X)) → length(X)U21(mark(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, mark(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, mark(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, mark(X4)) → U21(X1, X2, X3, X4)U21(active(X1), X2, X3, X4) → U21(X1, X2, X3, X4)
U21(X1, active(X2), X3, X4) → U21(X1, X2, X3, X4)U21(X1, X2, active(X3), X4) → U21(X1, X2, X3, X4)
U21(X1, X2, X3, active(X4)) → U21(X1, X2, X3, X4)U22(mark(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, mark(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, mark(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, mark(X4)) → U22(X1, X2, X3, X4)U22(active(X1), X2, X3, X4) → U22(X1, X2, X3, X4)
U22(X1, active(X2), X3, X4) → U22(X1, X2, X3, X4)U22(X1, X2, active(X3), X4) → U22(X1, X2, X3, X4)
U22(X1, X2, X3, active(X4)) → U22(X1, X2, X3, X4)U23(mark(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, mark(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, mark(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, mark(X4)) → U23(X1, X2, X3, X4)U23(active(X1), X2, X3, X4) → U23(X1, X2, X3, X4)
U23(X1, active(X2), X3, X4) → U23(X1, X2, X3, X4)U23(X1, X2, active(X3), X4) → U23(X1, X2, X3, X4)
U23(X1, X2, X3, active(X4)) → U23(X1, X2, X3, X4)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: mark, 0, s, zeros, tt, take, length, active, U11, U12, U23, U21, U22, 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:

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