Termination w.r.t. Q proof of /tmp/tmpAtYcE0/ExSec4_2_DLMMU04

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 PisEmptyProof (⇔)

    ↳9 TRUE

  ↳10 QDP

    ↳11 QDPOrderProof (⇔)

    ↳12 QDP

    ↳13 PisEmptyProof (⇔)

    ↳14 TRUE

  ↳15 QDP

    ↳16 QDPOrderProof (⇔)

    ↳17 QDP

    ↳18 PisEmptyProof (⇔)

    ↳19 TRUE

  ↳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 PisEmptyProof (⇔)

    ↳38 TRUE

  ↳39 QDP

    ↳40 QDPOrderProof (⇔)

    ↳41 QDP

    ↳42 PisEmptyProof (⇔)

    ↳43 TRUE

  ↳44 QDP

    ↳45 QDPOrderProof (⇔)

    ↳46 QDP

    ↳47 QDPOrderProof (⇔)

    ↳48 QDP

    ↳49 PisEmptyProof (⇔)

    ↳50 TRUE

  ↳51 QDP

    ↳52 QDPOrderProof (⇔)

    ↳53 QDP

    ↳54 PisEmptyProof (⇔)

    ↳55 TRUE

  ↳56 QDP

    ↳57 QDPOrderProof (⇔)

    ↳58 QDP

    ↳59 QDPOrderProof (⇔)

    ↳60 QDP

    ↳61 PisEmptyProof (⇔)

    ↳62 TRUE

  ↳63 QDP

    ↳64 QDPOrderProof (⇔)

    ↳65 QDP

    ↳66 QDPOrderProof (⇔)

    ↳67 QDP

    ↳68 PisEmptyProof (⇔)

    ↳69 TRUE

  ↳70 QDP

    ↳71 QDPOrderProof (⇔)

    ↳72 QDP

    ↳73 PisEmptyProof (⇔)

    ↳74 TRUE

  ↳75 QDP

    ↳76 QDPOrderProof (⇔)

    ↳77 QDP

    ↳78 QDPOrderProof (⇔)

    ↳79 QDP

    ↳80 PisEmptyProof (⇔)

    ↳81 TRUE

  ↳82 QDP

(0) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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(natsFrom(N)) → MARK(cons(N, natsFrom(s(N))))
ACTIVE(natsFrom(N)) → CONS(N, natsFrom(s(N)))
ACTIVE(natsFrom(N)) → NATSFROM(s(N))
ACTIVE(natsFrom(N)) → S(N)
ACTIVE(fst(pair(XS, YS))) → MARK(XS)
ACTIVE(snd(pair(XS, YS))) → MARK(YS)
ACTIVE(splitAt(0, XS)) → MARK(pair(nil, XS))
ACTIVE(splitAt(0, XS)) → PAIR(nil, XS)
ACTIVE(splitAt(s(N), cons(X, XS))) → MARK(u(splitAt(N, XS), N, X, XS))
ACTIVE(splitAt(s(N), cons(X, XS))) → U(splitAt(N, XS), N, X, XS)
ACTIVE(splitAt(s(N), cons(X, XS))) → SPLITAT(N, XS)
ACTIVE(u(pair(YS, ZS), N, X, XS)) → MARK(pair(cons(X, YS), ZS))
ACTIVE(u(pair(YS, ZS), N, X, XS)) → PAIR(cons(X, YS), ZS)
ACTIVE(u(pair(YS, ZS), N, X, XS)) → CONS(X, YS)
ACTIVE(head(cons(N, XS))) → MARK(N)
ACTIVE(tail(cons(N, XS))) → MARK(XS)
ACTIVE(sel(N, XS)) → MARK(head(afterNth(N, XS)))
ACTIVE(sel(N, XS)) → HEAD(afterNth(N, XS))
ACTIVE(sel(N, XS)) → AFTERNTH(N, XS)
ACTIVE(take(N, XS)) → MARK(fst(splitAt(N, XS)))
ACTIVE(take(N, XS)) → FST(splitAt(N, XS))
ACTIVE(take(N, XS)) → SPLITAT(N, XS)
ACTIVE(afterNth(N, XS)) → MARK(snd(splitAt(N, XS)))
ACTIVE(afterNth(N, XS)) → SND(splitAt(N, XS))
ACTIVE(afterNth(N, XS)) → SPLITAT(N, XS)
MARK(natsFrom(X)) → ACTIVE(natsFrom(mark(X)))
MARK(natsFrom(X)) → NATSFROM(mark(X))
MARK(natsFrom(X)) → MARK(X)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → S(mark(X))
MARK(s(X)) → MARK(X)
MARK(fst(X)) → ACTIVE(fst(mark(X)))
MARK(fst(X)) → FST(mark(X))
MARK(fst(X)) → MARK(X)
MARK(pair(X1, X2)) → ACTIVE(pair(mark(X1), mark(X2)))
MARK(pair(X1, X2)) → PAIR(mark(X1), mark(X2))
MARK(pair(X1, X2)) → MARK(X1)
MARK(pair(X1, X2)) → MARK(X2)
MARK(snd(X)) → ACTIVE(snd(mark(X)))
MARK(snd(X)) → SND(mark(X))
MARK(snd(X)) → MARK(X)
MARK(splitAt(X1, X2)) → ACTIVE(splitAt(mark(X1), mark(X2)))
MARK(splitAt(X1, X2)) → SPLITAT(mark(X1), mark(X2))
MARK(splitAt(X1, X2)) → MARK(X1)
MARK(splitAt(X1, X2)) → MARK(X2)
MARK(0) → ACTIVE(0)
MARK(nil) → ACTIVE(nil)
MARK(u(X1, X2, X3, X4)) → ACTIVE(u(mark(X1), X2, X3, X4))
MARK(u(X1, X2, X3, X4)) → U(mark(X1), X2, X3, X4)
MARK(u(X1, X2, X3, X4)) → MARK(X1)
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(head(X)) → HEAD(mark(X))
MARK(head(X)) → MARK(X)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
MARK(tail(X)) → TAIL(mark(X))
MARK(tail(X)) → MARK(X)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
MARK(sel(X1, X2)) → SEL(mark(X1), mark(X2))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(X1, X2)) → MARK(X2)
MARK(afterNth(X1, X2)) → ACTIVE(afterNth(mark(X1), mark(X2)))
MARK(afterNth(X1, X2)) → AFTERNTH(mark(X1), mark(X2))
MARK(afterNth(X1, X2)) → MARK(X1)
MARK(afterNth(X1, X2)) → MARK(X2)
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)
NATSFROM(mark(X)) → NATSFROM(X)
NATSFROM(active(X)) → NATSFROM(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)
S(mark(X)) → S(X)
S(active(X)) → S(X)
FST(mark(X)) → FST(X)
FST(active(X)) → FST(X)
PAIR(mark(X1), X2) → PAIR(X1, X2)
PAIR(X1, mark(X2)) → PAIR(X1, X2)
PAIR(active(X1), X2) → PAIR(X1, X2)
PAIR(X1, active(X2)) → PAIR(X1, X2)
SND(mark(X)) → SND(X)
SND(active(X)) → SND(X)
SPLITAT(mark(X1), X2) → SPLITAT(X1, X2)
SPLITAT(X1, mark(X2)) → SPLITAT(X1, X2)
SPLITAT(active(X1), X2) → SPLITAT(X1, X2)
SPLITAT(X1, active(X2)) → SPLITAT(X1, X2)
U(mark(X1), X2, X3, X4) → U(X1, X2, X3, X4)
U(X1, mark(X2), X3, X4) → U(X1, X2, X3, X4)
U(X1, X2, mark(X3), X4) → U(X1, X2, X3, X4)
U(X1, X2, X3, mark(X4)) → U(X1, X2, X3, X4)
U(active(X1), X2, X3, X4) → U(X1, X2, X3, X4)
U(X1, active(X2), X3, X4) → U(X1, X2, X3, X4)
U(X1, X2, active(X3), X4) → U(X1, X2, X3, X4)
U(X1, X2, X3, active(X4)) → U(X1, X2, X3, X4)
HEAD(mark(X)) → HEAD(X)
HEAD(active(X)) → HEAD(X)
TAIL(mark(X)) → TAIL(X)
TAIL(active(X)) → TAIL(X)
SEL(mark(X1), X2) → SEL(X1, X2)
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(active(X1), X2) → SEL(X1, X2)
SEL(X1, active(X2)) → SEL(X1, X2)
AFTERNTH(mark(X1), X2) → AFTERNTH(X1, X2)
AFTERNTH(X1, mark(X2)) → AFTERNTH(X1, X2)
AFTERNTH(active(X1), X2) → AFTERNTH(X1, X2)
AFTERNTH(X1, active(X2)) → AFTERNTH(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)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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 14 SCCs with 29 less nodes.

(4) Complex Obligation (AND)

(5) 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(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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.

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 remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > TAKE₂
active₁ > TAKE₂

Status:

TAKE₂: [1,2]
mark₁: [1]
active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(8) PisEmptyProof (EQUIVALENT transformation)

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

(9) TRUE

(10) Obligation:

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

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

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > AFTERNTH₂
active₁ > AFTERNTH₂

Status:

AFTERNTH₂: [1,2]
mark₁: [1]
active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(12) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(13) PisEmptyProof (EQUIVALENT transformation)

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

(14) TRUE

(15) Obligation:

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

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

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > SEL₂
active₁ > SEL₂

Status:

SEL₂: [1,2]
mark₁: [1]
active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(17) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(18) PisEmptyProof (EQUIVALENT transformation)

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

(19) TRUE

(20) Obligation:

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

TAIL(active(X)) → TAIL(X)
TAIL(mark(X)) → TAIL(X)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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.

TAIL(active(X)) → TAIL(X)

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

Lexicographic path order with status [LPO].
Precedence:

trivial

Status:

active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(22) Obligation:

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

TAIL(mark(X)) → TAIL(X)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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.

TAIL(mark(X)) → TAIL(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > TAIL₁

Status:

TAIL₁: [1]
mark₁: [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(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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:

HEAD(active(X)) → HEAD(X)
HEAD(mark(X)) → HEAD(X)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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.

HEAD(active(X)) → HEAD(X)

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

Lexicographic path order with status [LPO].
Precedence:

trivial

Status:

active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(29) Obligation:

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

HEAD(mark(X)) → HEAD(X)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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.

HEAD(mark(X)) → HEAD(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > HEAD₁

Status:

HEAD₁: [1]
mark₁: [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(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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:

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

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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.

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

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > U₄
active₁ > U₄

Status:

U₄: [3,4,2,1]
mark₁: [1]
active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(36) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(37) PisEmptyProof (EQUIVALENT transformation)

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

(38) TRUE

(39) Obligation:

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

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

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > SPLITAT₂
active₁ > SPLITAT₂

Status:

SPLITAT₂: [1,2]
mark₁: [1]
active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(41) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(42) PisEmptyProof (EQUIVALENT transformation)

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

(43) TRUE

(44) Obligation:

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

SND(active(X)) → SND(X)
SND(mark(X)) → SND(X)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(45) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

SND(active(X)) → SND(X)

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

Lexicographic path order with status [LPO].
Precedence:

trivial

Status:

active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(46) Obligation:

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

SND(mark(X)) → SND(X)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(47) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

SND(mark(X)) → SND(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > SND₁

Status:

SND₁: [1]
mark₁: [1]

The following usable rules [FROCOS05] were oriented: none

(48) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(49) PisEmptyProof (EQUIVALENT transformation)

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

(50) TRUE

(51) Obligation:

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

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

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(52) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > PAIR₂
active₁ > PAIR₂

Status:

PAIR₂: [1,2]
mark₁: [1]
active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(53) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(54) PisEmptyProof (EQUIVALENT transformation)

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

(55) TRUE

(56) Obligation:

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

FST(active(X)) → FST(X)
FST(mark(X)) → FST(X)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(57) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

FST(active(X)) → FST(X)

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

Lexicographic path order with status [LPO].
Precedence:

trivial

Status:

active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(58) Obligation:

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

FST(mark(X)) → FST(X)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(59) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

FST(mark(X)) → FST(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > FST₁

Status:

FST₁: [1]
mark₁: [1]

The following usable rules [FROCOS05] were oriented: none

(60) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(61) PisEmptyProof (EQUIVALENT transformation)

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

(62) TRUE

(63) 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(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(64) 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) = x1
active(x1) = active(x1)
mark(x1) = x1

Lexicographic path order with status [LPO].
Precedence:

trivial

Status:

active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(65) 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(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(66) 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: Lexicographic path order with status [LPO].
Precedence:

mark₁ > S₁

Status:

S₁: [1]
mark₁: [1]

The following usable rules [FROCOS05] were oriented: none

(67) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(68) PisEmptyProof (EQUIVALENT transformation)

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

(69) TRUE

(70) 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(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(71) 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)
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].
Precedence:

mark₁ > CONS₂
active₁ > CONS₂

Status:

CONS₂: [1,2]
mark₁: [1]
active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(72) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(73) PisEmptyProof (EQUIVALENT transformation)

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

(74) TRUE

(75) Obligation:

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

NATSFROM(active(X)) → NATSFROM(X)
NATSFROM(mark(X)) → NATSFROM(X)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(76) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

NATSFROM(active(X)) → NATSFROM(X)

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

Lexicographic path order with status [LPO].
Precedence:

trivial

Status:

active₁: [1]

The following usable rules [FROCOS05] were oriented: none

(77) Obligation:

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

NATSFROM(mark(X)) → NATSFROM(X)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(78) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

NATSFROM(mark(X)) → NATSFROM(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Precedence:

mark₁ > NATSFROM₁

Status:

NATSFROM₁: [1]
mark₁: [1]

The following usable rules [FROCOS05] were oriented: none

(79) Obligation:

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

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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

(80) PisEmptyProof (EQUIVALENT transformation)

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

(81) TRUE

(82) Obligation:

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

MARK(natsFrom(X)) → ACTIVE(natsFrom(mark(X)))
ACTIVE(natsFrom(N)) → MARK(cons(N, natsFrom(s(N))))
MARK(natsFrom(X)) → MARK(X)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(fst(pair(XS, YS))) → MARK(XS)
MARK(cons(X1, X2)) → MARK(X1)
MARK(s(X)) → ACTIVE(s(mark(X)))
ACTIVE(snd(pair(XS, YS))) → MARK(YS)
MARK(s(X)) → MARK(X)
MARK(fst(X)) → ACTIVE(fst(mark(X)))
ACTIVE(splitAt(0, XS)) → MARK(pair(nil, XS))
MARK(fst(X)) → MARK(X)
MARK(pair(X1, X2)) → ACTIVE(pair(mark(X1), mark(X2)))
ACTIVE(splitAt(s(N), cons(X, XS))) → MARK(u(splitAt(N, XS), N, X, XS))
MARK(pair(X1, X2)) → MARK(X1)
MARK(pair(X1, X2)) → MARK(X2)
MARK(snd(X)) → ACTIVE(snd(mark(X)))
ACTIVE(u(pair(YS, ZS), N, X, XS)) → MARK(pair(cons(X, YS), ZS))
MARK(snd(X)) → MARK(X)
MARK(splitAt(X1, X2)) → ACTIVE(splitAt(mark(X1), mark(X2)))
ACTIVE(head(cons(N, XS))) → MARK(N)
MARK(splitAt(X1, X2)) → MARK(X1)
MARK(splitAt(X1, X2)) → MARK(X2)
MARK(u(X1, X2, X3, X4)) → ACTIVE(u(mark(X1), X2, X3, X4))
ACTIVE(tail(cons(N, XS))) → MARK(XS)
MARK(u(X1, X2, X3, X4)) → MARK(X1)
MARK(head(X)) → ACTIVE(head(mark(X)))
ACTIVE(sel(N, XS)) → MARK(head(afterNth(N, XS)))
MARK(head(X)) → MARK(X)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
ACTIVE(take(N, XS)) → MARK(fst(splitAt(N, XS)))
MARK(tail(X)) → MARK(X)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
ACTIVE(afterNth(N, XS)) → MARK(snd(splitAt(N, XS)))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(X1, X2)) → MARK(X2)
MARK(afterNth(X1, X2)) → ACTIVE(afterNth(mark(X1), mark(X2)))
MARK(afterNth(X1, X2)) → MARK(X1)
MARK(afterNth(X1, X2)) → MARK(X2)
MARK(take(X1, X2)) → ACTIVE(take(mark(X1), mark(X2)))
MARK(take(X1, X2)) → MARK(X1)
MARK(take(X1, X2)) → MARK(X2)

The TRS R consists of the following rules:

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))
active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)
active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))
mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)
natsFrom(active(X)) → natsFrom(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)
s(mark(X)) → s(X)
s(active(X)) → s(X)
fst(mark(X)) → fst(X)
fst(active(X)) → fst(X)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
snd(mark(X)) → snd(X)
snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)
splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)
splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)
u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)
u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)
afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)
afterNth(X1, active(X2)) → afterNth(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)

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