Termination w.r.t. Q of the given QTRS could not be shown:

0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
  ↳5 QDP
    ↳6 QDPOrderProof (⇔)
    ↳7 QDP
    ↳8 QDPOrderProof (⇔)
    ↳9 QDP
    ↳10 PisEmptyProof (⇔)
    ↳11 TRUE
  ↳12 QDP
    ↳13 QDPOrderProof (⇔)
    ↳14 QDP
    ↳15 QDPOrderProof (⇔)
    ↳16 QDP
    ↳17 QDPOrderProof (⇔)
    ↳18 QDP
    ↳19 QDPOrderProof (⇔)
    ↳20 QDP
    ↳21 QDPOrderProof (⇔)
    ↳22 QDP
    ↳23 QDPOrderProof (⇔)
    ↳24 QDP
    ↳25 PisEmptyProof (⇔)
    ↳26 TRUE
  ↳27 QDP
    ↳28 QDPOrderProof (⇔)
    ↳29 QDP
    ↳30 QDPOrderProof (⇔)
    ↳31 QDP
    ↳32 PisEmptyProof (⇔)
    ↳33 TRUE
  ↳34 QDP
    ↳35 QDPOrderProof (⇔)
    ↳36 QDP
    ↳37 QDPOrderProof (⇔)
    ↳38 QDP
    ↳39 PisEmptyProof (⇔)
    ↳40 TRUE
  ↳41 QDP
    ↳42 QDPOrderProof (⇔)
    ↳43 QDP
    ↳44 QDPOrderProof (⇔)
    ↳45 QDP
    ↳46 PisEmptyProof (⇔)
    ↳47 TRUE
  ↳48 QDP
    ↳49 QDPOrderProof (⇔)
    ↳50 QDP
    ↳51 QDPOrderProof (⇔)
    ↳52 QDP
    ↳53 PisEmptyProof (⇔)
    ↳54 TRUE
  ↳55 QDP
    ↳56 QDPOrderProof (⇔)
    ↳57 QDP
    ↳58 QDPOrderProof (⇔)
    ↳59 QDP
    ↳60 PisEmptyProof (⇔)
    ↳61 TRUE
  ↳62 QDP
    ↳63 QDPOrderProof (⇔)
    ↳64 QDP
    ↳65 QDPOrderProof (⇔)
    ↳66 QDP
    ↳67 PisEmptyProof (⇔)
    ↳68 TRUE
  ↳69 QDP
    ↳70 QDPOrderProof (⇔)
    ↳71 QDP
    ↳72 QDPOrderProof (⇔)
    ↳73 QDP
    ↳74 PisEmptyProof (⇔)
    ↳75 TRUE
  ↳76 QDP
    ↳77 QDPOrderProof (⇔)
    ↳78 QDP
    ↳79 QDPOrderProof (⇔)
    ↳80 QDP
    ↳81 PisEmptyProof (⇔)
    ↳82 TRUE
  ↳83 QDP
    ↳84 QDPOrderProof (⇔)
    ↳85 QDP
    ↳86 QDPOrderProof (⇔)
    ↳87 QDP
    ↳88 PisEmptyProof (⇔)
    ↳89 TRUE
  ↳90 QDP
    ↳91 QDPOrderProof (⇔)
    ↳92 QDP
    ↳93 QDPOrderProof (⇔)
    ↳94 QDP
    ↳95 QDPOrderProof (⇔)
    ↳96 QDP

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(and(tt, T)) → MARK(T)
ACTIVE(isNatIList(IL)) → MARK(isNatList(IL))
ACTIVE(isNatIList(IL)) → ISNATLIST(IL)
ACTIVE(isNat(0)) → MARK(tt)
ACTIVE(isNat(s(N))) → MARK(isNat(N))
ACTIVE(isNat(s(N))) → ISNAT(N)
ACTIVE(isNat(length(L))) → MARK(isNatList(L))
ACTIVE(isNat(length(L))) → ISNATLIST(L)
ACTIVE(isNatIList(zeros)) → MARK(tt)
ACTIVE(isNatIList(cons(N, IL))) → MARK(and(isNat(N), isNatIList(IL)))
ACTIVE(isNatIList(cons(N, IL))) → AND(isNat(N), isNatIList(IL))
ACTIVE(isNatIList(cons(N, IL))) → ISNAT(N)
ACTIVE(isNatIList(cons(N, IL))) → ISNATILIST(IL)
ACTIVE(isNatList(nil)) → MARK(tt)
ACTIVE(isNatList(cons(N, L))) → MARK(and(isNat(N), isNatList(L)))
ACTIVE(isNatList(cons(N, L))) → AND(isNat(N), isNatList(L))
ACTIVE(isNatList(cons(N, L))) → ISNAT(N)
ACTIVE(isNatList(cons(N, L))) → ISNATLIST(L)
ACTIVE(isNatList(take(N, IL))) → MARK(and(isNat(N), isNatIList(IL)))
ACTIVE(isNatList(take(N, IL))) → AND(isNat(N), isNatIList(IL))
ACTIVE(isNatList(take(N, IL))) → ISNAT(N)
ACTIVE(isNatList(take(N, IL))) → ISNATILIST(IL)
ACTIVE(zeros) → MARK(cons(0, zeros))
ACTIVE(zeros) → CONS(0, zeros)
ACTIVE(take(0, IL)) → MARK(uTake1(isNatIList(IL)))
ACTIVE(take(0, IL)) → UTAKE1(isNatIList(IL))
ACTIVE(take(0, IL)) → ISNATILIST(IL)
ACTIVE(uTake1(tt)) → MARK(nil)
ACTIVE(take(s(M), cons(N, IL))) → MARK(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
ACTIVE(take(s(M), cons(N, IL))) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
ACTIVE(take(s(M), cons(N, IL))) → AND(isNat(M), and(isNat(N), isNatIList(IL)))
ACTIVE(take(s(M), cons(N, IL))) → ISNAT(M)
ACTIVE(take(s(M), cons(N, IL))) → AND(isNat(N), isNatIList(IL))
ACTIVE(take(s(M), cons(N, IL))) → ISNAT(N)
ACTIVE(take(s(M), cons(N, IL))) → ISNATILIST(IL)
ACTIVE(uTake2(tt, M, N, IL)) → MARK(cons(N, take(M, IL)))
ACTIVE(uTake2(tt, M, N, IL)) → CONS(N, take(M, IL))
ACTIVE(uTake2(tt, M, N, IL)) → TAKE(M, IL)
ACTIVE(length(cons(N, L))) → MARK(uLength(and(isNat(N), isNatList(L)), L))
ACTIVE(length(cons(N, L))) → ULENGTH(and(isNat(N), isNatList(L)), L)
ACTIVE(length(cons(N, L))) → AND(isNat(N), isNatList(L))
ACTIVE(length(cons(N, L))) → ISNAT(N)
ACTIVE(length(cons(N, L))) → ISNATLIST(L)
ACTIVE(uLength(tt, L)) → MARK(s(length(L)))
ACTIVE(uLength(tt, L)) → S(length(L))
ACTIVE(uLength(tt, L)) → LENGTH(L)
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), mark(X2)))
MARK(and(X1, X2)) → AND(mark(X1), mark(X2))
MARK(and(X1, X2)) → MARK(X1)
MARK(and(X1, X2)) → MARK(X2)
MARK(tt) → ACTIVE(tt)
MARK(isNatIList(X)) → ACTIVE(isNatIList(X))
MARK(isNatList(X)) → ACTIVE(isNatList(X))
MARK(isNat(X)) → ACTIVE(isNat(X))
MARK(0) → ACTIVE(0)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → S(mark(X))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(length(X)) → LENGTH(mark(X))
MARK(length(X)) → MARK(X)
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(nil) → ACTIVE(nil)
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)
MARK(uTake1(X)) → ACTIVE(uTake1(mark(X)))
MARK(uTake1(X)) → UTAKE1(mark(X))
MARK(uTake1(X)) → MARK(X)
MARK(uTake2(X1, X2, X3, X4)) → ACTIVE(uTake2(mark(X1), X2, X3, X4))
MARK(uTake2(X1, X2, X3, X4)) → UTAKE2(mark(X1), X2, X3, X4)
MARK(uTake2(X1, X2, X3, X4)) → MARK(X1)
MARK(uLength(X1, X2)) → ACTIVE(uLength(mark(X1), X2))
MARK(uLength(X1, X2)) → ULENGTH(mark(X1), X2)
MARK(uLength(X1, X2)) → MARK(X1)
AND(mark(X1), X2) → AND(X1, X2)
AND(X1, mark(X2)) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)
ISNATILIST(mark(X)) → ISNATILIST(X)
ISNATILIST(active(X)) → ISNATILIST(X)
ISNATLIST(mark(X)) → ISNATLIST(X)
ISNATLIST(active(X)) → ISNATLIST(X)
ISNAT(mark(X)) → ISNAT(X)
ISNAT(active(X)) → ISNAT(X)
S(mark(X)) → S(X)
S(active(X)) → S(X)
LENGTH(mark(X)) → LENGTH(X)
LENGTH(active(X)) → LENGTH(X)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
TAKE(mark(X1), X2) → TAKE(X1, X2)
TAKE(X1, mark(X2)) → TAKE(X1, X2)
TAKE(active(X1), X2) → TAKE(X1, X2)
TAKE(X1, active(X2)) → TAKE(X1, X2)
UTAKE1(mark(X)) → UTAKE1(X)
UTAKE1(active(X)) → UTAKE1(X)
UTAKE2(mark(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, mark(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, mark(X3), X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, X3, mark(X4)) → UTAKE2(X1, X2, X3, X4)
UTAKE2(active(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, active(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, active(X3), X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, X3, active(X4)) → UTAKE2(X1, X2, X3, X4)
ULENGTH(mark(X1), X2) → ULENGTH(X1, X2)
ULENGTH(X1, mark(X2)) → ULENGTH(X1, X2)
ULENGTH(active(X1), X2) → ULENGTH(X1, X2)
ULENGTH(X1, active(X2)) → ULENGTH(X1, X2)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 12 SCCs with 44 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ULENGTH(X1, mark(X2)) → ULENGTH(X1, X2)
ULENGTH(mark(X1), X2) → ULENGTH(X1, X2)
ULENGTH(active(X1), X2) → ULENGTH(X1, X2)
ULENGTH(X1, active(X2)) → ULENGTH(X1, X2)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ULENGTH(X1, mark(X2)) → ULENGTH(X1, X2)
ULENGTH(mark(X1), X2) → ULENGTH(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ULENGTH(x1, x2)  =  ULENGTH(x1, x2)
mark(x1)  =  mark(x1)
active(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[ULENGTH2, mark1]

Status:
ULENGTH2: [2,1]
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ULENGTH(active(X1), X2) → ULENGTH(X1, X2)
ULENGTH(X1, active(X2)) → ULENGTH(X1, X2)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ULENGTH(active(X1), X2) → ULENGTH(X1, X2)
ULENGTH(X1, active(X2)) → ULENGTH(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Quasi-Precedence:
[ULENGTH2, active1]

Status:
active1: [1]
ULENGTH2: [2,1]


The following usable rules [FROCOS05] were oriented: none

(9) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(11) TRUE

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UTAKE2(X1, mark(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(mark(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, mark(X3), X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, X3, mark(X4)) → UTAKE2(X1, X2, X3, X4)
UTAKE2(active(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, active(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, active(X3), X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, X3, active(X4)) → UTAKE2(X1, X2, X3, X4)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


UTAKE2(X1, X2, mark(X3), X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, X3, mark(X4)) → UTAKE2(X1, X2, X3, X4)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
UTAKE2(x1, x2, x3, x4)  =  UTAKE2(x3, x4)
mark(x1)  =  mark(x1)
active(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
UTAKE22: [2,1]
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UTAKE2(X1, mark(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(mark(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(active(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, active(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, active(X3), X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, X3, active(X4)) → UTAKE2(X1, X2, X3, X4)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(15) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


UTAKE2(X1, X2, active(X3), X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, X2, X3, active(X4)) → UTAKE2(X1, X2, X3, X4)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
UTAKE2(x1, x2, x3, x4)  =  UTAKE2(x3, x4)
mark(x1)  =  mark
active(x1)  =  active(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active1: [1]
UTAKE22: [2,1]
mark: []


The following usable rules [FROCOS05] were oriented: none

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UTAKE2(X1, mark(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(mark(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(active(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(X1, active(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(17) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


UTAKE2(X1, active(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
UTAKE2(x1, x2, x3, x4)  =  UTAKE2(x2)
mark(x1)  =  x1
active(x1)  =  active(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
active1 > UTAKE21

Status:
active1: [1]
UTAKE21: [1]


The following usable rules [FROCOS05] were oriented: none

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UTAKE2(X1, mark(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(mark(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(active(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


UTAKE2(X1, mark(X2), X3, X4) → UTAKE2(X1, X2, X3, X4)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
UTAKE2(x1, x2, x3, x4)  =  UTAKE2(x2, x4)
mark(x1)  =  mark(x1)
active(x1)  =  active

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active: []
UTAKE22: [1,2]
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UTAKE2(mark(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
UTAKE2(active(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


UTAKE2(active(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
UTAKE2(x1, x2, x3, x4)  =  UTAKE2(x1, x2)
mark(x1)  =  x1
active(x1)  =  active(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
[UTAKE22, active1]

Status:
active1: [1]
UTAKE22: [1,2]


The following usable rules [FROCOS05] were oriented: none

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UTAKE2(mark(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


UTAKE2(mark(X1), X2, X3, X4) → UTAKE2(X1, X2, X3, X4)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
UTAKE2(x1, x2, x3, x4)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(24) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(26) TRUE

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UTAKE1(active(X)) → UTAKE1(X)
UTAKE1(mark(X)) → UTAKE1(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(28) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


UTAKE1(active(X)) → UTAKE1(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
UTAKE1(x1)  =  UTAKE1(x1)
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[UTAKE11, active1]

Status:
active1: [1]
UTAKE11: [1]


The following usable rules [FROCOS05] were oriented: none

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UTAKE1(mark(X)) → UTAKE1(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(30) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


UTAKE1(mark(X)) → UTAKE1(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
UTAKE1(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(31) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(32) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(33) TRUE

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(35) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


TAKE(X1, mark(X2)) → TAKE(X1, X2)
TAKE(mark(X1), X2) → TAKE(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
TAKE(x1, x2)  =  TAKE(x1, x2)
mark(x1)  =  mark(x1)
active(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[TAKE2, mark1]

Status:
TAKE2: [2,1]
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TAKE(active(X1), X2) → TAKE(X1, X2)
TAKE(X1, active(X2)) → TAKE(X1, X2)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(37) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


TAKE(active(X1), X2) → TAKE(X1, X2)
TAKE(X1, active(X2)) → TAKE(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Quasi-Precedence:
[TAKE2, active1]

Status:
active1: [1]
TAKE2: [2,1]


The following usable rules [FROCOS05] were oriented: none

(38) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(39) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(40) TRUE

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(42) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CONS(x1, x2)  =  CONS(x1, x2)
mark(x1)  =  mark(x1)
active(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[CONS2, mark1]

Status:
CONS2: [2,1]
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(44) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Quasi-Precedence:
[CONS2, active1]

Status:
active1: [1]
CONS2: [2,1]


The following usable rules [FROCOS05] were oriented: none

(45) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(46) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(47) TRUE

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LENGTH(active(X)) → LENGTH(X)
LENGTH(mark(X)) → LENGTH(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(49) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


LENGTH(active(X)) → LENGTH(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
LENGTH(x1)  =  LENGTH(x1)
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[LENGTH1, active1]

Status:
active1: [1]
LENGTH1: [1]


The following usable rules [FROCOS05] were oriented: none

(50) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LENGTH(mark(X)) → LENGTH(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(51) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


LENGTH(mark(X)) → LENGTH(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
LENGTH(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(52) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(53) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(54) TRUE

(55) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(active(X)) → S(X)
S(mark(X)) → S(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(56) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


S(active(X)) → S(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
S(x1)  =  S(x1)
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[S1, active1]

Status:
active1: [1]
S1: [1]


The following usable rules [FROCOS05] were oriented: none

(57) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(mark(X)) → S(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(58) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


S(mark(X)) → S(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
S(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(59) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(60) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(61) TRUE

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNAT(active(X)) → ISNAT(X)
ISNAT(mark(X)) → ISNAT(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(63) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNAT(active(X)) → ISNAT(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNAT(x1)  =  ISNAT(x1)
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[ISNAT1, active1]

Status:
active1: [1]
ISNAT1: [1]


The following usable rules [FROCOS05] were oriented: none

(64) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNAT(mark(X)) → ISNAT(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(65) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNAT(mark(X)) → ISNAT(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNAT(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(66) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(67) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(68) TRUE

(69) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(active(X)) → ISNATLIST(X)
ISNATLIST(mark(X)) → ISNATLIST(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(70) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATLIST(active(X)) → ISNATLIST(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNATLIST(x1)  =  ISNATLIST(x1)
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[ISNATLIST1, active1]

Status:
active1: [1]
ISNATLIST1: [1]


The following usable rules [FROCOS05] were oriented: none

(71) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(mark(X)) → ISNATLIST(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(72) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATLIST(mark(X)) → ISNATLIST(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNATLIST(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(73) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(74) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(75) TRUE

(76) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(active(X)) → ISNATILIST(X)
ISNATILIST(mark(X)) → ISNATILIST(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(77) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATILIST(active(X)) → ISNATILIST(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNATILIST(x1)  =  ISNATILIST(x1)
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[ISNATILIST1, active1]

Status:
active1: [1]
ISNATILIST1: [1]


The following usable rules [FROCOS05] were oriented: none

(78) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(mark(X)) → ISNATILIST(X)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(79) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATILIST(mark(X)) → ISNATILIST(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNATILIST(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(80) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(81) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(82) TRUE

(83) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(84) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


AND(X1, mark(X2)) → AND(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
AND(x1, x2)  =  AND(x1, x2)
mark(x1)  =  mark(x1)
active(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[AND2, mark1]

Status:
AND2: [2,1]
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(85) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(86) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Quasi-Precedence:
[AND2, active1]

Status:
active1: [1]
AND2: [2,1]


The following usable rules [FROCOS05] were oriented: none

(87) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(88) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(89) TRUE

(90) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(91) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  MARK
and(x1, x2)  =  and
ACTIVE(x1)  =  x1
mark(x1)  =  mark(x1)
tt  =  tt
isNatIList(x1)  =  isNatIList
isNatList(x1)  =  isNatList
isNat(x1)  =  isNat
s(x1)  =  s
length(x1)  =  length
cons(x1, x2)  =  cons
zeros  =  zeros
0  =  0
take(x1, x2)  =  take
uTake1(x1)  =  uTake1
uTake2(x1, x2, x3, x4)  =  uTake2
uLength(x1, x2)  =  uLength
active(x1)  =  active
nil  =  nil

Lexicographic path order with status [LPO].
Quasi-Precedence:
[mark1, tt, active] > [MARK, and, isNatIList, isNatList, isNat, s, length, zeros, 0, take, uTake1, uTake2, uLength] > cons
[mark1, tt, active] > nil

Status:
active: []
MARK: []
isNatList: []
mark1: [1]
isNatIList: []
s: []
length: []
0: []
take: []
uTake1: []
isNat: []
tt: []
cons: []
zeros: []
and: []
uLength: []
uTake2: []
nil: []


The following usable rules [FROCOS05] were oriented:

take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
uTake1(active(X)) → uTake1(X)
uTake1(mark(X)) → uTake1(X)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)
uLength(X1, active(X2)) → uLength(X1, X2)
uLength(X1, mark(X2)) → uLength(X1, X2)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)
and(X1, mark(X2)) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)

(92) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(93) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(s(X)) → ACTIVE(s(mark(X)))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  MARK
and(x1, x2)  =  and
ACTIVE(x1)  =  x1
mark(x1)  =  x1
tt  =  tt
isNatIList(x1)  =  isNatIList
isNatList(x1)  =  isNatList
isNat(x1)  =  isNat
s(x1)  =  s
length(x1)  =  length
cons(x1, x2)  =  cons(x1, x2)
zeros  =  zeros
0  =  0
take(x1, x2)  =  take
uTake1(x1)  =  uTake1
uTake2(x1, x2, x3, x4)  =  uTake2
uLength(x1, x2)  =  uLength
active(x1)  =  active(x1)
nil  =  nil

Lexicographic path order with status [LPO].
Quasi-Precedence:
[MARK, and, isNatIList, isNatList, isNat, length, zeros, take, uTake1, uTake2, uLength] > [tt, 0, active1, nil] > s > cons2

Status:
MARK: []
isNatList: []
isNatIList: []
s: []
length: []
0: []
take: []
uTake1: []
isNat: []
cons2: [2,1]
active1: [1]
tt: []
zeros: []
and: []
uLength: []
uTake2: []
nil: []


The following usable rules [FROCOS05] were oriented:

take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
uTake1(active(X)) → uTake1(X)
uTake1(mark(X)) → uTake1(X)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)
uLength(X1, active(X2)) → uLength(X1, X2)
uLength(X1, mark(X2)) → uLength(X1, X2)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)
and(X1, mark(X2)) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)

(94) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(95) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(uTake1(X)) → ACTIVE(uTake1(mark(X)))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  MARK
and(x1, x2)  =  and
ACTIVE(x1)  =  x1
mark(x1)  =  x1
tt  =  tt
isNatIList(x1)  =  isNatIList
isNatList(x1)  =  isNatList
isNat(x1)  =  isNat
s(x1)  =  s
length(x1)  =  length
cons(x1, x2)  =  cons(x1, x2)
zeros  =  zeros
0  =  0
take(x1, x2)  =  take
uTake1(x1)  =  uTake1
uTake2(x1, x2, x3, x4)  =  uTake2
uLength(x1, x2)  =  uLength
active(x1)  =  active(x1)
nil  =  nil

Lexicographic path order with status [LPO].
Quasi-Precedence:
tt > nil > active1 > cons2 > [MARK, and, isNatIList, isNatList, isNat, length, zeros, take, uTake2, uLength] > [0, uTake1]
s > active1 > cons2 > [MARK, and, isNatIList, isNatList, isNat, length, zeros, take, uTake2, uLength] > [0, uTake1]

Status:
MARK: []
isNatList: []
isNatIList: []
s: []
length: []
0: []
take: []
uTake1: []
isNat: []
cons2: [1,2]
active1: [1]
tt: []
zeros: []
and: []
uLength: []
uTake2: []
nil: []


The following usable rules [FROCOS05] were oriented:

take(X1, mark(X2)) → take(X1, X2)
take(mark(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
uTake1(active(X)) → uTake1(X)
uTake1(mark(X)) → uTake1(X)
uTake2(active(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, active(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(mark(X1), X2, X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, X3, mark(X4)) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, mark(X3), X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, mark(X2), X3, X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, active(X3), X4) → uTake2(X1, X2, X3, X4)
uTake2(X1, X2, X3, active(X4)) → uTake2(X1, X2, X3, X4)
uLength(mark(X1), X2) → uLength(X1, X2)
uLength(active(X1), X2) → uLength(X1, X2)
uLength(X1, active(X2)) → uLength(X1, X2)
uLength(X1, mark(X2)) → uLength(X1, X2)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)
and(X1, mark(X2)) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)

(96) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.