0 QTRS
↳1 QTRSRRRProof (⇔, 266 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 58 ms)
↳4 QTRS
↳5 DependencyPairsProof (⇔, 68 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 QDP
↳10 QDPSizeChangeProof (⇔, 0 ms)
↳11 YES
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
↳15 QDP
↳16 QDPSizeChangeProof (⇔, 0 ms)
↳17 YES
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 QDPSizeChangeProof (⇔, 0 ms)
↳23 YES
↳24 QDP
↳25 MRRProof (⇔, 66 ms)
↳26 QDP
↳27 MRRProof (⇔, 59 ms)
↳28 QDP
↳29 MRRProof (⇔, 63 ms)
↳30 QDP
↳31 QDPOrderProof (⇔, 57 ms)
↳32 QDP
↳33 QDPOrderProof (⇔, 96 ms)
↳34 QDP
↳35 QDPOrderProof (⇔, 88 ms)
↳36 QDP
↳37 DependencyGraphProof (⇔, 0 ms)
↳38 QDP
↳39 QDPOrderProof (⇔, 90 ms)
↳40 QDP
↳41 Narrowing (⇔, 0 ms)
↳42 QDP
↳43 Narrowing (⇔, 4 ms)
↳44 QDP
↳45 DependencyGraphProof (⇔, 0 ms)
↳46 QDP
↳47 Narrowing (⇔, 0 ms)
↳48 QDP
↳49 DependencyGraphProof (⇔, 0 ms)
↳50 QDP
↳51 Narrowing (⇔, 0 ms)
↳52 QDP
↳53 DependencyGraphProof (⇔, 0 ms)
↳54 QDP
↳55 QDPOrderProof (⇔, 284 ms)
↳56 QDP
↳57 QDPOrderProof (⇔, 62 ms)
↳58 QDP
↳59 QDPOrderProof (⇔, 195 ms)
↳60 QDP
↳61 QDPOrderProof (⇔, 175 ms)
↳62 QDP
↳63 QDPOrderProof (⇔, 0 ms)
↳64 QDP
↳65 NonTerminationLoopProof (⇔, 149 ms)
↳66 NO
active(zeros) → mark(cons(0, zeros))
active(and(tt, X)) → mark(X)
active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(s(length(L)))
active(take(0, IL)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(active(x1)) = x1
POL(and(x1, x2)) = 1 + 2·x1 + x2
POL(cons(x1, x2)) = 2·x1 + x2
POL(length(x1)) = 2 + x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 2·x1 + 2·x2
POL(tt) = 0
POL(zeros) = 0
active(and(tt, X)) → mark(X)
active(length(nil)) → mark(0)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(0, IL)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(active(x1)) = x1
POL(and(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = 2·x1 + x2
POL(length(x1)) = 2·x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 1 + 2·x1 + 2·x2
POL(tt) = 0
POL(zeros) = 0
active(take(0, IL)) → mark(nil)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
ACTIVE(zeros) → MARK(cons(0, zeros))
ACTIVE(zeros) → CONS(0, zeros)
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
ACTIVE(length(cons(N, L))) → S(length(L))
ACTIVE(length(cons(N, L))) → LENGTH(L)
ACTIVE(take(s(M), cons(N, IL))) → MARK(cons(N, take(M, IL)))
ACTIVE(take(s(M), cons(N, IL))) → CONS(N, take(M, IL))
ACTIVE(take(s(M), cons(N, IL))) → TAKE(M, IL)
MARK(zeros) → ACTIVE(zeros)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(0) → ACTIVE(0)
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
MARK(and(X1, X2)) → AND(mark(X1), X2)
MARK(and(X1, X2)) → MARK(X1)
MARK(tt) → ACTIVE(tt)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(length(X)) → LENGTH(mark(X))
MARK(length(X)) → MARK(X)
MARK(nil) → ACTIVE(nil)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → S(mark(X))
MARK(s(X)) → MARK(X)
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
MARK(take(X1, X2)) → TAKE(mark(X1), mark(X2))
MARK(take(X1, X2)) → MARK(X1)
MARK(take(X1, X2)) → MARK(X2)
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)
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)
LENGTH(mark(X)) → LENGTH(X)
LENGTH(active(X)) → LENGTH(X)
S(mark(X)) → S(X)
S(active(X)) → S(X)
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)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
TAKE(X1, mark(X2)) → TAKE(X1, X2)
TAKE(mark(X1), X2) → TAKE(X1, X2)
TAKE(active(X1), X2) → TAKE(X1, X2)
TAKE(X1, active(X2)) → TAKE(X1, X2)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
From the DPs we obtained the following set of size-change graphs:
S(active(X)) → S(X)
S(mark(X)) → S(X)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
From the DPs we obtained the following set of size-change graphs:
LENGTH(active(X)) → LENGTH(X)
LENGTH(mark(X)) → LENGTH(X)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
From the DPs we obtained the following set of size-change graphs:
AND(X1, mark(X2)) → AND(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
From the DPs we obtained the following set of size-change graphs:
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
From the DPs we obtained the following set of size-change graphs:
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(take(s(M), cons(N, IL))) → MARK(cons(N, take(M, IL)))
MARK(and(X1, X2)) → MARK(X1)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(length(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
MARK(take(X1, X2)) → MARK(X1)
MARK(take(X1, X2)) → MARK(X2)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(and(X1, X2)) → MARK(X1)
POL(0) = 0
POL(ACTIVE(x1)) = 2·x1
POL(MARK(x1)) = 2·x1
POL(active(x1)) = x1
POL(and(x1, x2)) = 1 + x1 + 2·x2
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(length(x1)) = x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = 2·x1
POL(take(x1, x2)) = x1 + 2·x2
POL(tt) = 0
POL(zeros) = 0
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(take(s(M), cons(N, IL))) → MARK(cons(N, take(M, IL)))
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(length(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
MARK(take(X1, X2)) → MARK(X1)
MARK(take(X1, X2)) → MARK(X2)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(take(X1, X2)) → MARK(X1)
MARK(take(X1, X2)) → MARK(X2)
POL(0) = 0
POL(ACTIVE(x1)) = 2·x1
POL(MARK(x1)) = 2·x1
POL(active(x1)) = x1
POL(and(x1, x2)) = 2·x1 + 2·x2
POL(cons(x1, x2)) = 2·x1 + x2
POL(length(x1)) = x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 2 + x1 + x2
POL(tt) = 2
POL(zeros) = 0
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(take(s(M), cons(N, IL))) → MARK(cons(N, take(M, IL)))
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(length(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(length(X)) → MARK(X)
POL(0) = 0
POL(ACTIVE(x1)) = 2·x1
POL(MARK(x1)) = 2·x1
POL(active(x1)) = x1
POL(and(x1, x2)) = x1 + 2·x2
POL(cons(x1, x2)) = 2·x1 + x2
POL(length(x1)) = 1 + 2·x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = x1 + 2·x2
POL(tt) = 0
POL(zeros) = 0
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(take(s(M), cons(N, IL))) → MARK(cons(N, take(M, IL)))
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
MARK(s(X)) → ACTIVE(s(mark(X)))
POL(0) = 0
POL(ACTIVE(x1)) = x1
POL(MARK(x1)) = 1
POL(active(x1)) = 0
POL(and(x1, x2)) = 0
POL(cons(x1, x2)) = 0
POL(length(x1)) = 1
POL(mark(x1)) = 0
POL(nil) = 0
POL(s(x1)) = 0
POL(take(x1, x2)) = 1
POL(tt) = 0
POL(zeros) = 1
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
ACTIVE(take(s(M), cons(N, IL))) → MARK(cons(N, take(M, IL)))
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(s(X)) → MARK(X)
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(take(s(M), cons(N, IL))) → MARK(cons(N, take(M, IL)))
[ACTIVE1, MARK1, zeros, 0] > length
[ACTIVE1, MARK1, zeros, 0] > take1
ACTIVE1: [1]
length: multiset
MARK1: [1]
zeros: multiset
0: multiset
take1: multiset
and: []
tt: multiset
nil: multiset
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(s(X)) → MARK(X)
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(cons(X1, X2)) → MARK(X1)
ACTIVE(zeros) → MARK(cons(0, zeros))
[ACTIVE1, MARK1] > length > cons1
[ACTIVE1, MARK1] > zeros > 0 > cons1
[ACTIVE1, MARK1] > take > cons1
and > cons1
tt > cons1
nil > cons1
ACTIVE1: [1]
length: multiset
cons1: multiset
MARK1: [1]
zeros: multiset
0: multiset
take: multiset
and: multiset
tt: multiset
nil: multiset
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(zeros) → ACTIVE(zeros)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(s(X)) → MARK(X)
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
POL(0) = 0
POL(ACTIVE(x1)) = 0
POL(MARK(x1)) = x1
POL(active(x1)) = x1
POL(and(x1, x2)) = 0
POL(cons(x1, x2)) = 0
POL(length(x1)) = 0
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 1
POL(tt) = 0
POL(zeros) = 1
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(0)) → ACTIVE(length(active(0)))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(tt)) → ACTIVE(length(active(tt)))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(nil)) → ACTIVE(length(active(nil)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(0)) → ACTIVE(length(active(0)))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(tt)) → ACTIVE(length(active(tt)))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(nil)) → ACTIVE(length(active(nil)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(length(0)) → ACTIVE(length(0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(tt)) → ACTIVE(length(active(tt)))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(nil)) → ACTIVE(length(active(nil)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
MARK(length(0)) → ACTIVE(length(0))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(tt)) → ACTIVE(length(active(tt)))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(nil)) → ACTIVE(length(active(nil)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(length(tt)) → ACTIVE(length(tt))
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(nil)) → ACTIVE(length(active(nil)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
MARK(length(tt)) → ACTIVE(length(tt))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(nil)) → ACTIVE(length(active(nil)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(length(nil)) → ACTIVE(length(nil))
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
MARK(length(nil)) → ACTIVE(length(nil))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
POL( ACTIVE(x1) ) = x1
POL( MARK(x1) ) = 2x1
POL( s(x1) ) = x1
POL( length(x1) ) = x1
POL( active(x1) ) = x1
POL( mark(x1) ) = 2x1
POL( cons(x1, x2) ) = 2x2
POL( zeros ) = 0
POL( 0 ) = 0
POL( and(x1, x2) ) = 2x1 + 2x2 + 2
POL( take(x1, x2) ) = max{0, -2}
POL( tt ) = 2
POL( nil ) = 1
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
POL(MARK(x1)) = 1A + 1A · x1
POL(s(x1)) = -I + 0A · x1
POL(length(x1)) = -I + 0A · x1
POL(ACTIVE(x1)) = 1A + 0A · x1
POL(cons(x1, x2)) = 1A + 0A · x1 + 1A · x2
POL(zeros) = 0A
POL(active(x1)) = 1A + 0A · x1
POL(mark(x1)) = 1A + 0A · x1
POL(take(x1, x2)) = -I + -I · x1 + 0A · x2
POL(0) = 0A
POL(and(x1, x2)) = -I + 0A · x1 + -I · x2
POL(tt) = 4A
POL(nil) = 4A
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
POL( ACTIVE(x1) ) = x1 + 2
POL( MARK(x1) ) = 2x1
POL( s(x1) ) = x1
POL( length(x1) ) = x1 + 2
POL( active(x1) ) = x1
POL( mark(x1) ) = x1
POL( cons(x1, x2) ) = 2x2
POL( zeros ) = 0
POL( 0 ) = 2
POL( and(x1, x2) ) = 2
POL( take(x1, x2) ) = max{0, -2}
POL( tt ) = 1
POL( nil ) = 2
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(length(x0)) → ACTIVE(length(x0))
POL(MARK(x1)) = 3A + 1A · x1
POL(s(x1)) = -I + 0A · x1
POL(length(x1)) = -I + 0A · x1
POL(ACTIVE(x1)) = -I + 0A · x1
POL(cons(x1, x2)) = 3A + 0A · x1 + 1A · x2
POL(zeros) = 0A
POL(active(x1)) = 3A + 0A · x1
POL(mark(x1)) = 3A + 0A · x1
POL(take(x1, x2)) = -I + -I · x1 + 0A · x2
POL(0) = 0A
POL(and(x1, x2)) = 0A + 0A · x1 + -I · x2
POL(tt) = 0A
POL(nil) = 0A
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
MARK(s(X)) → MARK(X)
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
POL(0) = 0
POL(ACTIVE(x1)) = x1
POL(MARK(x1)) = 1
POL(active(x1)) = x1
POL(and(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = 1
POL(length(x1)) = x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = 0
POL(take(x1, x2)) = 1
POL(tt) = 0
POL(zeros) = 1
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
MARK(s(X)) → MARK(X)
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(take(x0, x1))) → ACTIVE(length(active(take(mark(x0), mark(x1)))))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(take(s(M), cons(N, IL))) → mark(cons(N, take(M, IL)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
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)
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)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
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)