The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
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)))
active(natsFrom(X)) → natsFrom(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))
active(fst(X)) → fst(active(X))
active(pair(X1, X2)) → pair(active(X1), X2)
active(pair(X1, X2)) → pair(X1, active(X2))
active(snd(X)) → snd(active(X))
active(splitAt(X1, X2)) → splitAt(active(X1), X2)
active(splitAt(X1, X2)) → splitAt(X1, active(X2))
active(u(X1, X2, X3, X4)) → u(active(X1), X2, X3, X4)
active(head(X)) → head(active(X))
active(tail(X)) → tail(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(afterNth(X1, X2)) → afterNth(active(X1), X2)
active(afterNth(X1, X2)) → afterNth(X1, active(X2))
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
natsFrom(mark(X)) → mark(natsFrom(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
s(mark(X)) → mark(s(X))
fst(mark(X)) → mark(fst(X))
pair(mark(X1), X2) → mark(pair(X1, X2))
pair(X1, mark(X2)) → mark(pair(X1, X2))
snd(mark(X)) → mark(snd(X))
splitAt(mark(X1), X2) → mark(splitAt(X1, X2))
splitAt(X1, mark(X2)) → mark(splitAt(X1, X2))
u(mark(X1), X2, X3, X4) → mark(u(X1, X2, X3, X4))
head(mark(X)) → mark(head(X))
tail(mark(X)) → mark(tail(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
afterNth(mark(X1), X2) → mark(afterNth(X1, X2))
afterNth(X1, mark(X2)) → mark(afterNth(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
proper(natsFrom(X)) → natsFrom(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))
proper(fst(X)) → fst(proper(X))
proper(pair(X1, X2)) → pair(proper(X1), proper(X2))
proper(snd(X)) → snd(proper(X))
proper(splitAt(X1, X2)) → splitAt(proper(X1), proper(X2))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(u(X1, X2, X3, X4)) → u(proper(X1), proper(X2), proper(X3), proper(X4))
proper(head(X)) → head(proper(X))
proper(tail(X)) → tail(proper(X))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(afterNth(X1, X2)) → afterNth(proper(X1), proper(X2))
proper(take(X1, X2)) → take(proper(X1), proper(X2))
natsFrom(ok(X)) → ok(natsFrom(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
s(ok(X)) → ok(s(X))
fst(ok(X)) → ok(fst(X))
pair(ok(X1), ok(X2)) → ok(pair(X1, X2))
snd(ok(X)) → ok(snd(X))
splitAt(ok(X1), ok(X2)) → ok(splitAt(X1, X2))
u(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(u(X1, X2, X3, X4))
head(ok(X)) → ok(head(X))
tail(ok(X)) → ok(tail(X))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
afterNth(ok(X1), ok(X2)) → ok(afterNth(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(natsFrom(z0)) → mark(cons(z0, natsFrom(s(z0))))
active(fst(pair(z0, z1))) → mark(z0)
active(snd(pair(z0, z1))) → mark(z1)
active(splitAt(0, z0)) → mark(pair(nil, z0))
active(splitAt(s(z0), cons(z1, z2))) → mark(u(splitAt(z0, z2), z0, z1, z2))
active(u(pair(z0, z1), z2, z3, z4)) → mark(pair(cons(z3, z0), z1))
active(head(cons(z0, z1))) → mark(z0)
active(tail(cons(z0, z1))) → mark(z1)
active(sel(z0, z1)) → mark(head(afterNth(z0, z1)))
active(take(z0, z1)) → mark(fst(splitAt(z0, z1)))
active(afterNth(z0, z1)) → mark(snd(splitAt(z0, z1)))
active(natsFrom(z0)) → natsFrom(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(fst(z0)) → fst(active(z0))
active(pair(z0, z1)) → pair(active(z0), z1)
active(pair(z0, z1)) → pair(z0, active(z1))
active(snd(z0)) → snd(active(z0))
active(splitAt(z0, z1)) → splitAt(active(z0), z1)
active(splitAt(z0, z1)) → splitAt(z0, active(z1))
active(u(z0, z1, z2, z3)) → u(active(z0), z1, z2, z3)
active(head(z0)) → head(active(z0))
active(tail(z0)) → tail(active(z0))
active(sel(z0, z1)) → sel(active(z0), z1)
active(sel(z0, z1)) → sel(z0, active(z1))
active(afterNth(z0, z1)) → afterNth(active(z0), z1)
active(afterNth(z0, z1)) → afterNth(z0, active(z1))
active(take(z0, z1)) → take(active(z0), z1)
active(take(z0, z1)) → take(z0, active(z1))
natsFrom(mark(z0)) → mark(natsFrom(z0))
natsFrom(ok(z0)) → ok(natsFrom(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
fst(mark(z0)) → mark(fst(z0))
fst(ok(z0)) → ok(fst(z0))
pair(mark(z0), z1) → mark(pair(z0, z1))
pair(z0, mark(z1)) → mark(pair(z0, z1))
pair(ok(z0), ok(z1)) → ok(pair(z0, z1))
snd(mark(z0)) → mark(snd(z0))
snd(ok(z0)) → ok(snd(z0))
splitAt(mark(z0), z1) → mark(splitAt(z0, z1))
splitAt(z0, mark(z1)) → mark(splitAt(z0, z1))
splitAt(ok(z0), ok(z1)) → ok(splitAt(z0, z1))
u(mark(z0), z1, z2, z3) → mark(u(z0, z1, z2, z3))
u(ok(z0), ok(z1), ok(z2), ok(z3)) → ok(u(z0, z1, z2, z3))
head(mark(z0)) → mark(head(z0))
head(ok(z0)) → ok(head(z0))
tail(mark(z0)) → mark(tail(z0))
tail(ok(z0)) → ok(tail(z0))
sel(mark(z0), z1) → mark(sel(z0, z1))
sel(z0, mark(z1)) → mark(sel(z0, z1))
sel(ok(z0), ok(z1)) → ok(sel(z0, z1))
afterNth(mark(z0), z1) → mark(afterNth(z0, z1))
afterNth(z0, mark(z1)) → mark(afterNth(z0, z1))
afterNth(ok(z0), ok(z1)) → ok(afterNth(z0, z1))
take(mark(z0), z1) → mark(take(z0, z1))
take(z0, mark(z1)) → mark(take(z0, z1))
take(ok(z0), ok(z1)) → ok(take(z0, z1))
proper(natsFrom(z0)) → natsFrom(proper(z0))
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(fst(z0)) → fst(proper(z0))
proper(pair(z0, z1)) → pair(proper(z0), proper(z1))
proper(snd(z0)) → snd(proper(z0))
proper(splitAt(z0, z1)) → splitAt(proper(z0), proper(z1))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(u(z0, z1, z2, z3)) → u(proper(z0), proper(z1), proper(z2), proper(z3))
proper(head(z0)) → head(proper(z0))
proper(tail(z0)) → tail(proper(z0))
proper(sel(z0, z1)) → sel(proper(z0), proper(z1))
proper(afterNth(z0, z1)) → afterNth(proper(z0), proper(z1))
proper(take(z0, z1)) → take(proper(z0), proper(z1))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(natsFrom(z0)) → c(CONS(z0, natsFrom(s(z0))), NATSFROM(s(z0)), S(z0))
ACTIVE(fst(pair(z0, z1))) → c1
ACTIVE(snd(pair(z0, z1))) → c2
ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c4(U(splitAt(z0, z2), z0, z1, z2), SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c5(PAIR(cons(z3, z0), z1), CONS(z3, z0))
ACTIVE(head(cons(z0, z1))) → c6
ACTIVE(tail(cons(z0, z1))) → c7
ACTIVE(sel(z0, z1)) → c8(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(0) → c67
PROPER(nil) → c68
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))

S tuples:

ACTIVE(natsFrom(z0)) → c(CONS(z0, natsFrom(s(z0))), NATSFROM(s(z0)), S(z0))
ACTIVE(fst(pair(z0, z1))) → c1
ACTIVE(snd(pair(z0, z1))) → c2
ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c4(U(splitAt(z0, z2), z0, z1, z2), SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c5(PAIR(cons(z3, z0), z1), CONS(z3, z0))
ACTIVE(head(cons(z0, z1))) → c6
ACTIVE(tail(cons(z0, z1))) → c7
ACTIVE(sel(z0, z1)) → c8(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(0) → c67
PROPER(nil) → c68
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))

K tuples:none
Defined Rule Symbols:

active, natsFrom, cons, s, fst, pair, snd, splitAt, u, head, tail, sel, afterNth, take, proper, top

Defined Pair Symbols:

ACTIVE, NATSFROM, CONS, S, FST, PAIR, SND, SPLITAT, U, HEAD, TAIL, SEL, AFTERNTH, TAKE, PROPER, TOP

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67, c68, c69, c70, c71, c72, c73, c74, c75, c76

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 6 trailing nodes:

PROPER(nil) → c68
ACTIVE(fst(pair(z0, z1))) → c1
PROPER(0) → c67
ACTIVE(snd(pair(z0, z1))) → c2
ACTIVE(head(cons(z0, z1))) → c6
ACTIVE(tail(cons(z0, z1))) → c7

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(natsFrom(z0)) → mark(cons(z0, natsFrom(s(z0))))
active(fst(pair(z0, z1))) → mark(z0)
active(snd(pair(z0, z1))) → mark(z1)
active(splitAt(0, z0)) → mark(pair(nil, z0))
active(splitAt(s(z0), cons(z1, z2))) → mark(u(splitAt(z0, z2), z0, z1, z2))
active(u(pair(z0, z1), z2, z3, z4)) → mark(pair(cons(z3, z0), z1))
active(head(cons(z0, z1))) → mark(z0)
active(tail(cons(z0, z1))) → mark(z1)
active(sel(z0, z1)) → mark(head(afterNth(z0, z1)))
active(take(z0, z1)) → mark(fst(splitAt(z0, z1)))
active(afterNth(z0, z1)) → mark(snd(splitAt(z0, z1)))
active(natsFrom(z0)) → natsFrom(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(fst(z0)) → fst(active(z0))
active(pair(z0, z1)) → pair(active(z0), z1)
active(pair(z0, z1)) → pair(z0, active(z1))
active(snd(z0)) → snd(active(z0))
active(splitAt(z0, z1)) → splitAt(active(z0), z1)
active(splitAt(z0, z1)) → splitAt(z0, active(z1))
active(u(z0, z1, z2, z3)) → u(active(z0), z1, z2, z3)
active(head(z0)) → head(active(z0))
active(tail(z0)) → tail(active(z0))
active(sel(z0, z1)) → sel(active(z0), z1)
active(sel(z0, z1)) → sel(z0, active(z1))
active(afterNth(z0, z1)) → afterNth(active(z0), z1)
active(afterNth(z0, z1)) → afterNth(z0, active(z1))
active(take(z0, z1)) → take(active(z0), z1)
active(take(z0, z1)) → take(z0, active(z1))
natsFrom(mark(z0)) → mark(natsFrom(z0))
natsFrom(ok(z0)) → ok(natsFrom(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
fst(mark(z0)) → mark(fst(z0))
fst(ok(z0)) → ok(fst(z0))
pair(mark(z0), z1) → mark(pair(z0, z1))
pair(z0, mark(z1)) → mark(pair(z0, z1))
pair(ok(z0), ok(z1)) → ok(pair(z0, z1))
snd(mark(z0)) → mark(snd(z0))
snd(ok(z0)) → ok(snd(z0))
splitAt(mark(z0), z1) → mark(splitAt(z0, z1))
splitAt(z0, mark(z1)) → mark(splitAt(z0, z1))
splitAt(ok(z0), ok(z1)) → ok(splitAt(z0, z1))
u(mark(z0), z1, z2, z3) → mark(u(z0, z1, z2, z3))
u(ok(z0), ok(z1), ok(z2), ok(z3)) → ok(u(z0, z1, z2, z3))
head(mark(z0)) → mark(head(z0))
head(ok(z0)) → ok(head(z0))
tail(mark(z0)) → mark(tail(z0))
tail(ok(z0)) → ok(tail(z0))
sel(mark(z0), z1) → mark(sel(z0, z1))
sel(z0, mark(z1)) → mark(sel(z0, z1))
sel(ok(z0), ok(z1)) → ok(sel(z0, z1))
afterNth(mark(z0), z1) → mark(afterNth(z0, z1))
afterNth(z0, mark(z1)) → mark(afterNth(z0, z1))
afterNth(ok(z0), ok(z1)) → ok(afterNth(z0, z1))
take(mark(z0), z1) → mark(take(z0, z1))
take(z0, mark(z1)) → mark(take(z0, z1))
take(ok(z0), ok(z1)) → ok(take(z0, z1))
proper(natsFrom(z0)) → natsFrom(proper(z0))
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(fst(z0)) → fst(proper(z0))
proper(pair(z0, z1)) → pair(proper(z0), proper(z1))
proper(snd(z0)) → snd(proper(z0))
proper(splitAt(z0, z1)) → splitAt(proper(z0), proper(z1))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(u(z0, z1, z2, z3)) → u(proper(z0), proper(z1), proper(z2), proper(z3))
proper(head(z0)) → head(proper(z0))
proper(tail(z0)) → tail(proper(z0))
proper(sel(z0, z1)) → sel(proper(z0), proper(z1))
proper(afterNth(z0, z1)) → afterNth(proper(z0), proper(z1))
proper(take(z0, z1)) → take(proper(z0), proper(z1))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(natsFrom(z0)) → c(CONS(z0, natsFrom(s(z0))), NATSFROM(s(z0)), S(z0))
ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c4(U(splitAt(z0, z2), z0, z1, z2), SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c5(PAIR(cons(z3, z0), z1), CONS(z3, z0))
ACTIVE(sel(z0, z1)) → c8(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))

S tuples:

ACTIVE(natsFrom(z0)) → c(CONS(z0, natsFrom(s(z0))), NATSFROM(s(z0)), S(z0))
ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c4(U(splitAt(z0, z2), z0, z1, z2), SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c5(PAIR(cons(z3, z0), z1), CONS(z3, z0))
ACTIVE(sel(z0, z1)) → c8(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))

K tuples:none
Defined Rule Symbols:

active, natsFrom, cons, s, fst, pair, snd, splitAt, u, head, tail, sel, afterNth, take, proper, top

Defined Pair Symbols:

ACTIVE, NATSFROM, CONS, S, FST, PAIR, SND, SPLITAT, U, HEAD, TAIL, SEL, AFTERNTH, TAKE, PROPER, TOP

Compound Symbols:

c, c3, c4, c5, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c69, c70, c71, c72, c73, c74, c75, c76

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 5 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(natsFrom(z0)) → mark(cons(z0, natsFrom(s(z0))))
active(fst(pair(z0, z1))) → mark(z0)
active(snd(pair(z0, z1))) → mark(z1)
active(splitAt(0, z0)) → mark(pair(nil, z0))
active(splitAt(s(z0), cons(z1, z2))) → mark(u(splitAt(z0, z2), z0, z1, z2))
active(u(pair(z0, z1), z2, z3, z4)) → mark(pair(cons(z3, z0), z1))
active(head(cons(z0, z1))) → mark(z0)
active(tail(cons(z0, z1))) → mark(z1)
active(sel(z0, z1)) → mark(head(afterNth(z0, z1)))
active(take(z0, z1)) → mark(fst(splitAt(z0, z1)))
active(afterNth(z0, z1)) → mark(snd(splitAt(z0, z1)))
active(natsFrom(z0)) → natsFrom(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(fst(z0)) → fst(active(z0))
active(pair(z0, z1)) → pair(active(z0), z1)
active(pair(z0, z1)) → pair(z0, active(z1))
active(snd(z0)) → snd(active(z0))
active(splitAt(z0, z1)) → splitAt(active(z0), z1)
active(splitAt(z0, z1)) → splitAt(z0, active(z1))
active(u(z0, z1, z2, z3)) → u(active(z0), z1, z2, z3)
active(head(z0)) → head(active(z0))
active(tail(z0)) → tail(active(z0))
active(sel(z0, z1)) → sel(active(z0), z1)
active(sel(z0, z1)) → sel(z0, active(z1))
active(afterNth(z0, z1)) → afterNth(active(z0), z1)
active(afterNth(z0, z1)) → afterNth(z0, active(z1))
active(take(z0, z1)) → take(active(z0), z1)
active(take(z0, z1)) → take(z0, active(z1))
natsFrom(mark(z0)) → mark(natsFrom(z0))
natsFrom(ok(z0)) → ok(natsFrom(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
fst(mark(z0)) → mark(fst(z0))
fst(ok(z0)) → ok(fst(z0))
pair(mark(z0), z1) → mark(pair(z0, z1))
pair(z0, mark(z1)) → mark(pair(z0, z1))
pair(ok(z0), ok(z1)) → ok(pair(z0, z1))
snd(mark(z0)) → mark(snd(z0))
snd(ok(z0)) → ok(snd(z0))
splitAt(mark(z0), z1) → mark(splitAt(z0, z1))
splitAt(z0, mark(z1)) → mark(splitAt(z0, z1))
splitAt(ok(z0), ok(z1)) → ok(splitAt(z0, z1))
u(mark(z0), z1, z2, z3) → mark(u(z0, z1, z2, z3))
u(ok(z0), ok(z1), ok(z2), ok(z3)) → ok(u(z0, z1, z2, z3))
head(mark(z0)) → mark(head(z0))
head(ok(z0)) → ok(head(z0))
tail(mark(z0)) → mark(tail(z0))
tail(ok(z0)) → ok(tail(z0))
sel(mark(z0), z1) → mark(sel(z0, z1))
sel(z0, mark(z1)) → mark(sel(z0, z1))
sel(ok(z0), ok(z1)) → ok(sel(z0, z1))
afterNth(mark(z0), z1) → mark(afterNth(z0, z1))
afterNth(z0, mark(z1)) → mark(afterNth(z0, z1))
afterNth(ok(z0), ok(z1)) → ok(afterNth(z0, z1))
take(mark(z0), z1) → mark(take(z0, z1))
take(z0, mark(z1)) → mark(take(z0, z1))
take(ok(z0), ok(z1)) → ok(take(z0, z1))
proper(natsFrom(z0)) → natsFrom(proper(z0))
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(fst(z0)) → fst(proper(z0))
proper(pair(z0, z1)) → pair(proper(z0), proper(z1))
proper(snd(z0)) → snd(proper(z0))
proper(splitAt(z0, z1)) → splitAt(proper(z0), proper(z1))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(u(z0, z1, z2, z3)) → u(proper(z0), proper(z1), proper(z2), proper(z3))
proper(head(z0)) → head(proper(z0))
proper(tail(z0)) → tail(proper(z0))
proper(sel(z0, z1)) → sel(proper(z0), proper(z1))
proper(afterNth(z0, z1)) → afterNth(proper(z0), proper(z1))
proper(take(z0, z1)) → take(proper(z0), proper(z1))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c4(U(splitAt(z0, z2), z0, z1, z2), SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c5(PAIR(cons(z3, z0), z1), CONS(z3, z0))
ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))

S tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c4(U(splitAt(z0, z2), z0, z1, z2), SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c5(PAIR(cons(z3, z0), z1), CONS(z3, z0))
ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))

K tuples:none
Defined Rule Symbols:

active, natsFrom, cons, s, fst, pair, snd, splitAt, u, head, tail, sel, afterNth, take, proper, top

Defined Pair Symbols:

ACTIVE, NATSFROM, CONS, S, FST, PAIR, SND, SPLITAT, U, HEAD, TAIL, SEL, AFTERNTH, TAKE, PROPER, TOP

Compound Symbols:

c3, c4, c5, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c69, c70, c71, c72, c73, c74, c75, c76, c, c8, c9, c10

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(natsFrom(z0)) → mark(cons(z0, natsFrom(s(z0))))
active(fst(pair(z0, z1))) → mark(z0)
active(snd(pair(z0, z1))) → mark(z1)
active(splitAt(0, z0)) → mark(pair(nil, z0))
active(splitAt(s(z0), cons(z1, z2))) → mark(u(splitAt(z0, z2), z0, z1, z2))
active(u(pair(z0, z1), z2, z3, z4)) → mark(pair(cons(z3, z0), z1))
active(head(cons(z0, z1))) → mark(z0)
active(tail(cons(z0, z1))) → mark(z1)
active(sel(z0, z1)) → mark(head(afterNth(z0, z1)))
active(take(z0, z1)) → mark(fst(splitAt(z0, z1)))
active(afterNth(z0, z1)) → mark(snd(splitAt(z0, z1)))
active(natsFrom(z0)) → natsFrom(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(fst(z0)) → fst(active(z0))
active(pair(z0, z1)) → pair(active(z0), z1)
active(pair(z0, z1)) → pair(z0, active(z1))
active(snd(z0)) → snd(active(z0))
active(splitAt(z0, z1)) → splitAt(active(z0), z1)
active(splitAt(z0, z1)) → splitAt(z0, active(z1))
active(u(z0, z1, z2, z3)) → u(active(z0), z1, z2, z3)
active(head(z0)) → head(active(z0))
active(tail(z0)) → tail(active(z0))
active(sel(z0, z1)) → sel(active(z0), z1)
active(sel(z0, z1)) → sel(z0, active(z1))
active(afterNth(z0, z1)) → afterNth(active(z0), z1)
active(afterNth(z0, z1)) → afterNth(z0, active(z1))
active(take(z0, z1)) → take(active(z0), z1)
active(take(z0, z1)) → take(z0, active(z1))
natsFrom(mark(z0)) → mark(natsFrom(z0))
natsFrom(ok(z0)) → ok(natsFrom(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
fst(mark(z0)) → mark(fst(z0))
fst(ok(z0)) → ok(fst(z0))
pair(mark(z0), z1) → mark(pair(z0, z1))
pair(z0, mark(z1)) → mark(pair(z0, z1))
pair(ok(z0), ok(z1)) → ok(pair(z0, z1))
snd(mark(z0)) → mark(snd(z0))
snd(ok(z0)) → ok(snd(z0))
splitAt(mark(z0), z1) → mark(splitAt(z0, z1))
splitAt(z0, mark(z1)) → mark(splitAt(z0, z1))
splitAt(ok(z0), ok(z1)) → ok(splitAt(z0, z1))
u(mark(z0), z1, z2, z3) → mark(u(z0, z1, z2, z3))
u(ok(z0), ok(z1), ok(z2), ok(z3)) → ok(u(z0, z1, z2, z3))
head(mark(z0)) → mark(head(z0))
head(ok(z0)) → ok(head(z0))
tail(mark(z0)) → mark(tail(z0))
tail(ok(z0)) → ok(tail(z0))
sel(mark(z0), z1) → mark(sel(z0, z1))
sel(z0, mark(z1)) → mark(sel(z0, z1))
sel(ok(z0), ok(z1)) → ok(sel(z0, z1))
afterNth(mark(z0), z1) → mark(afterNth(z0, z1))
afterNth(z0, mark(z1)) → mark(afterNth(z0, z1))
afterNth(ok(z0), ok(z1)) → ok(afterNth(z0, z1))
take(mark(z0), z1) → mark(take(z0, z1))
take(z0, mark(z1)) → mark(take(z0, z1))
take(ok(z0), ok(z1)) → ok(take(z0, z1))
proper(natsFrom(z0)) → natsFrom(proper(z0))
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(fst(z0)) → fst(proper(z0))
proper(pair(z0, z1)) → pair(proper(z0), proper(z1))
proper(snd(z0)) → snd(proper(z0))
proper(splitAt(z0, z1)) → splitAt(proper(z0), proper(z1))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(u(z0, z1, z2, z3)) → u(proper(z0), proper(z1), proper(z2), proper(z3))
proper(head(z0)) → head(proper(z0))
proper(tail(z0)) → tail(proper(z0))
proper(sel(z0, z1)) → sel(proper(z0), proper(z1))
proper(afterNth(z0, z1)) → afterNth(proper(z0), proper(z1))
proper(take(z0, z1)) → take(proper(z0), proper(z1))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))

S tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))

K tuples:none
Defined Rule Symbols:

active, natsFrom, cons, s, fst, pair, snd, splitAt, u, head, tail, sel, afterNth, take, proper, top

Defined Pair Symbols:

ACTIVE, NATSFROM, CONS, S, FST, PAIR, SND, SPLITAT, U, HEAD, TAIL, SEL, AFTERNTH, TAKE, PROPER, TOP

Compound Symbols:

c3, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c69, c70, c71, c72, c73, c74, c75, c76, c, c8, c9, c10, c1

(9) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(natsFrom(z0)) → mark(cons(z0, natsFrom(s(z0))))
active(fst(pair(z0, z1))) → mark(z0)
active(snd(pair(z0, z1))) → mark(z1)
active(splitAt(0, z0)) → mark(pair(nil, z0))
active(splitAt(s(z0), cons(z1, z2))) → mark(u(splitAt(z0, z2), z0, z1, z2))
active(u(pair(z0, z1), z2, z3, z4)) → mark(pair(cons(z3, z0), z1))
active(head(cons(z0, z1))) → mark(z0)
active(tail(cons(z0, z1))) → mark(z1)
active(sel(z0, z1)) → mark(head(afterNth(z0, z1)))
active(take(z0, z1)) → mark(fst(splitAt(z0, z1)))
active(afterNth(z0, z1)) → mark(snd(splitAt(z0, z1)))
active(natsFrom(z0)) → natsFrom(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(fst(z0)) → fst(active(z0))
active(pair(z0, z1)) → pair(active(z0), z1)
active(pair(z0, z1)) → pair(z0, active(z1))
active(snd(z0)) → snd(active(z0))
active(splitAt(z0, z1)) → splitAt(active(z0), z1)
active(splitAt(z0, z1)) → splitAt(z0, active(z1))
active(u(z0, z1, z2, z3)) → u(active(z0), z1, z2, z3)
active(head(z0)) → head(active(z0))
active(tail(z0)) → tail(active(z0))
active(sel(z0, z1)) → sel(active(z0), z1)
active(sel(z0, z1)) → sel(z0, active(z1))
active(afterNth(z0, z1)) → afterNth(active(z0), z1)
active(afterNth(z0, z1)) → afterNth(z0, active(z1))
active(take(z0, z1)) → take(active(z0), z1)
active(take(z0, z1)) → take(z0, active(z1))
u(mark(z0), z1, z2, z3) → mark(u(z0, z1, z2, z3))
u(ok(z0), ok(z1), ok(z2), ok(z3)) → ok(u(z0, z1, z2, z3))
splitAt(z0, mark(z1)) → mark(splitAt(z0, z1))
splitAt(mark(z0), z1) → mark(splitAt(z0, z1))
splitAt(ok(z0), ok(z1)) → ok(splitAt(z0, z1))
pair(mark(z0), z1) → mark(pair(z0, z1))
pair(ok(z0), ok(z1)) → ok(pair(z0, z1))
pair(z0, mark(z1)) → mark(pair(z0, z1))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
natsFrom(mark(z0)) → mark(natsFrom(z0))
natsFrom(ok(z0)) → ok(natsFrom(z0))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
fst(mark(z0)) → mark(fst(z0))
fst(ok(z0)) → ok(fst(z0))
snd(mark(z0)) → mark(snd(z0))
snd(ok(z0)) → ok(snd(z0))
head(mark(z0)) → mark(head(z0))
head(ok(z0)) → ok(head(z0))
tail(mark(z0)) → mark(tail(z0))
tail(ok(z0)) → ok(tail(z0))
sel(mark(z0), z1) → mark(sel(z0, z1))
sel(ok(z0), ok(z1)) → ok(sel(z0, z1))
sel(z0, mark(z1)) → mark(sel(z0, z1))
afterNth(mark(z0), z1) → mark(afterNth(z0, z1))
afterNth(ok(z0), ok(z1)) → ok(afterNth(z0, z1))
afterNth(z0, mark(z1)) → mark(afterNth(z0, z1))
take(mark(z0), z1) → mark(take(z0, z1))
take(ok(z0), ok(z1)) → ok(take(z0, z1))
take(z0, mark(z1)) → mark(take(z0, z1))
proper(natsFrom(z0)) → natsFrom(proper(z0))
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(fst(z0)) → fst(proper(z0))
proper(pair(z0, z1)) → pair(proper(z0), proper(z1))
proper(snd(z0)) → snd(proper(z0))
proper(splitAt(z0, z1)) → splitAt(proper(z0), proper(z1))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(u(z0, z1, z2, z3)) → u(proper(z0), proper(z1), proper(z2), proper(z3))
proper(head(z0)) → head(proper(z0))
proper(tail(z0)) → tail(proper(z0))
proper(sel(z0, z1)) → sel(proper(z0), proper(z1))
proper(afterNth(z0, z1)) → afterNth(proper(z0), proper(z1))
proper(take(z0, z1)) → take(proper(z0), proper(z1))

Tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))

S tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))

K tuples:none
Defined Rule Symbols:

active, u, splitAt, pair, cons, natsFrom, s, fst, snd, head, tail, sel, afterNth, take, proper

Defined Pair Symbols:

ACTIVE, NATSFROM, CONS, S, FST, PAIR, SND, SPLITAT, U, HEAD, TAIL, SEL, AFTERNTH, TAKE, PROPER, TOP

Compound Symbols:

c3, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c69, c70, c71, c72, c73, c74, c75, c76, c, c8, c9, c10, c1

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(natsFrom(z0)) → c11(NATSFROM(active(z0)), ACTIVE(z0)) by

ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(fst(pair(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(natsFrom(snd(pair(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(natsFrom(splitAt(0, z0))) → c11(NATSFROM(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(natsFrom(splitAt(s(z0), cons(z1, z2)))) → c11(NATSFROM(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(natsFrom(u(pair(z0, z1), z2, z3, z4))) → c11(NATSFROM(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(natsFrom(head(cons(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(natsFrom(tail(cons(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(cons(z0, z1))) → c11(NATSFROM(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(natsFrom(s(z0))) → c11(NATSFROM(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(natsFrom(fst(z0))) → c11(NATSFROM(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(snd(z0))) → c11(NATSFROM(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(u(z0, z1, z2, z3))) → c11(NATSFROM(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(natsFrom(head(z0))) → c11(NATSFROM(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(natsFrom(tail(z0))) → c11(NATSFROM(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(z0, active(z1))), ACTIVE(take(z0, z1)))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(natsFrom(z0)) → mark(cons(z0, natsFrom(s(z0))))
active(fst(pair(z0, z1))) → mark(z0)
active(snd(pair(z0, z1))) → mark(z1)
active(splitAt(0, z0)) → mark(pair(nil, z0))
active(splitAt(s(z0), cons(z1, z2))) → mark(u(splitAt(z0, z2), z0, z1, z2))
active(u(pair(z0, z1), z2, z3, z4)) → mark(pair(cons(z3, z0), z1))
active(head(cons(z0, z1))) → mark(z0)
active(tail(cons(z0, z1))) → mark(z1)
active(sel(z0, z1)) → mark(head(afterNth(z0, z1)))
active(take(z0, z1)) → mark(fst(splitAt(z0, z1)))
active(afterNth(z0, z1)) → mark(snd(splitAt(z0, z1)))
active(natsFrom(z0)) → natsFrom(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(fst(z0)) → fst(active(z0))
active(pair(z0, z1)) → pair(active(z0), z1)
active(pair(z0, z1)) → pair(z0, active(z1))
active(snd(z0)) → snd(active(z0))
active(splitAt(z0, z1)) → splitAt(active(z0), z1)
active(splitAt(z0, z1)) → splitAt(z0, active(z1))
active(u(z0, z1, z2, z3)) → u(active(z0), z1, z2, z3)
active(head(z0)) → head(active(z0))
active(tail(z0)) → tail(active(z0))
active(sel(z0, z1)) → sel(active(z0), z1)
active(sel(z0, z1)) → sel(z0, active(z1))
active(afterNth(z0, z1)) → afterNth(active(z0), z1)
active(afterNth(z0, z1)) → afterNth(z0, active(z1))
active(take(z0, z1)) → take(active(z0), z1)
active(take(z0, z1)) → take(z0, active(z1))
u(mark(z0), z1, z2, z3) → mark(u(z0, z1, z2, z3))
u(ok(z0), ok(z1), ok(z2), ok(z3)) → ok(u(z0, z1, z2, z3))
splitAt(z0, mark(z1)) → mark(splitAt(z0, z1))
splitAt(mark(z0), z1) → mark(splitAt(z0, z1))
splitAt(ok(z0), ok(z1)) → ok(splitAt(z0, z1))
pair(mark(z0), z1) → mark(pair(z0, z1))
pair(ok(z0), ok(z1)) → ok(pair(z0, z1))
pair(z0, mark(z1)) → mark(pair(z0, z1))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
natsFrom(mark(z0)) → mark(natsFrom(z0))
natsFrom(ok(z0)) → ok(natsFrom(z0))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
fst(mark(z0)) → mark(fst(z0))
fst(ok(z0)) → ok(fst(z0))
snd(mark(z0)) → mark(snd(z0))
snd(ok(z0)) → ok(snd(z0))
head(mark(z0)) → mark(head(z0))
head(ok(z0)) → ok(head(z0))
tail(mark(z0)) → mark(tail(z0))
tail(ok(z0)) → ok(tail(z0))
sel(mark(z0), z1) → mark(sel(z0, z1))
sel(ok(z0), ok(z1)) → ok(sel(z0, z1))
sel(z0, mark(z1)) → mark(sel(z0, z1))
afterNth(mark(z0), z1) → mark(afterNth(z0, z1))
afterNth(ok(z0), ok(z1)) → ok(afterNth(z0, z1))
afterNth(z0, mark(z1)) → mark(afterNth(z0, z1))
take(mark(z0), z1) → mark(take(z0, z1))
take(ok(z0), ok(z1)) → ok(take(z0, z1))
take(z0, mark(z1)) → mark(take(z0, z1))
proper(natsFrom(z0)) → natsFrom(proper(z0))
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(fst(z0)) → fst(proper(z0))
proper(pair(z0, z1)) → pair(proper(z0), proper(z1))
proper(snd(z0)) → snd(proper(z0))
proper(splitAt(z0, z1)) → splitAt(proper(z0), proper(z1))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(u(z0, z1, z2, z3)) → u(proper(z0), proper(z1), proper(z2), proper(z3))
proper(head(z0)) → head(proper(z0))
proper(tail(z0)) → tail(proper(z0))
proper(sel(z0, z1)) → sel(proper(z0), proper(z1))
proper(afterNth(z0, z1)) → afterNth(proper(z0), proper(z1))
proper(take(z0, z1)) → take(proper(z0), proper(z1))

Tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(fst(pair(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(natsFrom(snd(pair(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(natsFrom(splitAt(0, z0))) → c11(NATSFROM(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(natsFrom(splitAt(s(z0), cons(z1, z2)))) → c11(NATSFROM(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(natsFrom(u(pair(z0, z1), z2, z3, z4))) → c11(NATSFROM(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(natsFrom(head(cons(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(natsFrom(tail(cons(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(cons(z0, z1))) → c11(NATSFROM(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(natsFrom(s(z0))) → c11(NATSFROM(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(natsFrom(fst(z0))) → c11(NATSFROM(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(snd(z0))) → c11(NATSFROM(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(u(z0, z1, z2, z3))) → c11(NATSFROM(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(natsFrom(head(z0))) → c11(NATSFROM(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(natsFrom(tail(z0))) → c11(NATSFROM(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(z0, active(z1))), ACTIVE(take(z0, z1)))

S tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(fst(pair(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(natsFrom(snd(pair(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(natsFrom(splitAt(0, z0))) → c11(NATSFROM(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(natsFrom(splitAt(s(z0), cons(z1, z2)))) → c11(NATSFROM(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(natsFrom(u(pair(z0, z1), z2, z3, z4))) → c11(NATSFROM(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(natsFrom(head(cons(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(natsFrom(tail(cons(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(cons(z0, z1))) → c11(NATSFROM(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(natsFrom(s(z0))) → c11(NATSFROM(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(natsFrom(fst(z0))) → c11(NATSFROM(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(snd(z0))) → c11(NATSFROM(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(u(z0, z1, z2, z3))) → c11(NATSFROM(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(natsFrom(head(z0))) → c11(NATSFROM(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(natsFrom(tail(z0))) → c11(NATSFROM(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(z0, active(z1))), ACTIVE(take(z0, z1)))

K tuples:none
Defined Rule Symbols:

active, u, splitAt, pair, cons, natsFrom, s, fst, snd, head, tail, sel, afterNth, take, proper

Defined Pair Symbols:

ACTIVE, NATSFROM, CONS, S, FST, PAIR, SND, SPLITAT, U, HEAD, TAIL, SEL, AFTERNTH, TAKE, PROPER, TOP

Compound Symbols:

c3, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c69, c70, c71, c72, c73, c74, c75, c76, c, c8, c9, c10, c1, c11

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(cons(z0, z1)) → c12(CONS(active(z0), z1), ACTIVE(z0)) by

ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(mark(cons(z0, natsFrom(s(z0)))), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(fst(pair(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(fst(pair(z0, z1))))
ACTIVE(cons(snd(pair(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(snd(pair(z0, z1))))
ACTIVE(cons(splitAt(0, z0), x1)) → c12(CONS(mark(pair(nil, z0)), x1), ACTIVE(splitAt(0, z0)))
ACTIVE(cons(splitAt(s(z0), cons(z1, z2)), x1)) → c12(CONS(mark(u(splitAt(z0, z2), z0, z1, z2)), x1), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(cons(u(pair(z0, z1), z2, z3, z4), x1)) → c12(CONS(mark(pair(cons(z3, z0), z1)), x1), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(cons(head(cons(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(head(cons(z0, z1))))
ACTIVE(cons(tail(cons(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(tail(cons(z0, z1))))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(mark(head(afterNth(z0, z1))), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(mark(fst(splitAt(z0, z1))), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(mark(snd(splitAt(z0, z1))), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(natsFrom(active(z0)), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c12(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c12(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(fst(z0), x1)) → c12(CONS(fst(active(z0)), x1), ACTIVE(fst(z0)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(active(z0), z1), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(z0, active(z1)), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(snd(z0), x1)) → c12(CONS(snd(active(z0)), x1), ACTIVE(snd(z0)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(active(z0), z1), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(z0, active(z1)), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(u(z0, z1, z2, z3), x1)) → c12(CONS(u(active(z0), z1, z2, z3), x1), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(cons(head(z0), x1)) → c12(CONS(head(active(z0)), x1), ACTIVE(head(z0)))
ACTIVE(cons(tail(z0), x1)) → c12(CONS(tail(active(z0)), x1), ACTIVE(tail(z0)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(active(z0), z1), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(z0, active(z1)), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(active(z0), z1), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(z0, active(z1)), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(active(z0), z1), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(z0, active(z1)), x1), ACTIVE(take(z0, z1)))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(natsFrom(z0)) → mark(cons(z0, natsFrom(s(z0))))
active(fst(pair(z0, z1))) → mark(z0)
active(snd(pair(z0, z1))) → mark(z1)
active(splitAt(0, z0)) → mark(pair(nil, z0))
active(splitAt(s(z0), cons(z1, z2))) → mark(u(splitAt(z0, z2), z0, z1, z2))
active(u(pair(z0, z1), z2, z3, z4)) → mark(pair(cons(z3, z0), z1))
active(head(cons(z0, z1))) → mark(z0)
active(tail(cons(z0, z1))) → mark(z1)
active(sel(z0, z1)) → mark(head(afterNth(z0, z1)))
active(take(z0, z1)) → mark(fst(splitAt(z0, z1)))
active(afterNth(z0, z1)) → mark(snd(splitAt(z0, z1)))
active(natsFrom(z0)) → natsFrom(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(fst(z0)) → fst(active(z0))
active(pair(z0, z1)) → pair(active(z0), z1)
active(pair(z0, z1)) → pair(z0, active(z1))
active(snd(z0)) → snd(active(z0))
active(splitAt(z0, z1)) → splitAt(active(z0), z1)
active(splitAt(z0, z1)) → splitAt(z0, active(z1))
active(u(z0, z1, z2, z3)) → u(active(z0), z1, z2, z3)
active(head(z0)) → head(active(z0))
active(tail(z0)) → tail(active(z0))
active(sel(z0, z1)) → sel(active(z0), z1)
active(sel(z0, z1)) → sel(z0, active(z1))
active(afterNth(z0, z1)) → afterNth(active(z0), z1)
active(afterNth(z0, z1)) → afterNth(z0, active(z1))
active(take(z0, z1)) → take(active(z0), z1)
active(take(z0, z1)) → take(z0, active(z1))
u(mark(z0), z1, z2, z3) → mark(u(z0, z1, z2, z3))
u(ok(z0), ok(z1), ok(z2), ok(z3)) → ok(u(z0, z1, z2, z3))
splitAt(z0, mark(z1)) → mark(splitAt(z0, z1))
splitAt(mark(z0), z1) → mark(splitAt(z0, z1))
splitAt(ok(z0), ok(z1)) → ok(splitAt(z0, z1))
pair(mark(z0), z1) → mark(pair(z0, z1))
pair(ok(z0), ok(z1)) → ok(pair(z0, z1))
pair(z0, mark(z1)) → mark(pair(z0, z1))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
natsFrom(mark(z0)) → mark(natsFrom(z0))
natsFrom(ok(z0)) → ok(natsFrom(z0))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
fst(mark(z0)) → mark(fst(z0))
fst(ok(z0)) → ok(fst(z0))
snd(mark(z0)) → mark(snd(z0))
snd(ok(z0)) → ok(snd(z0))
head(mark(z0)) → mark(head(z0))
head(ok(z0)) → ok(head(z0))
tail(mark(z0)) → mark(tail(z0))
tail(ok(z0)) → ok(tail(z0))
sel(mark(z0), z1) → mark(sel(z0, z1))
sel(ok(z0), ok(z1)) → ok(sel(z0, z1))
sel(z0, mark(z1)) → mark(sel(z0, z1))
afterNth(mark(z0), z1) → mark(afterNth(z0, z1))
afterNth(ok(z0), ok(z1)) → ok(afterNth(z0, z1))
afterNth(z0, mark(z1)) → mark(afterNth(z0, z1))
take(mark(z0), z1) → mark(take(z0, z1))
take(ok(z0), ok(z1)) → ok(take(z0, z1))
take(z0, mark(z1)) → mark(take(z0, z1))
proper(natsFrom(z0)) → natsFrom(proper(z0))
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(fst(z0)) → fst(proper(z0))
proper(pair(z0, z1)) → pair(proper(z0), proper(z1))
proper(snd(z0)) → snd(proper(z0))
proper(splitAt(z0, z1)) → splitAt(proper(z0), proper(z1))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(u(z0, z1, z2, z3)) → u(proper(z0), proper(z1), proper(z2), proper(z3))
proper(head(z0)) → head(proper(z0))
proper(tail(z0)) → tail(proper(z0))
proper(sel(z0, z1)) → sel(proper(z0), proper(z1))
proper(afterNth(z0, z1)) → afterNth(proper(z0), proper(z1))
proper(take(z0, z1)) → take(proper(z0), proper(z1))

Tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(fst(pair(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(natsFrom(snd(pair(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(natsFrom(splitAt(0, z0))) → c11(NATSFROM(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(natsFrom(splitAt(s(z0), cons(z1, z2)))) → c11(NATSFROM(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(natsFrom(u(pair(z0, z1), z2, z3, z4))) → c11(NATSFROM(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(natsFrom(head(cons(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(natsFrom(tail(cons(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(cons(z0, z1))) → c11(NATSFROM(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(natsFrom(s(z0))) → c11(NATSFROM(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(natsFrom(fst(z0))) → c11(NATSFROM(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(snd(z0))) → c11(NATSFROM(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(u(z0, z1, z2, z3))) → c11(NATSFROM(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(natsFrom(head(z0))) → c11(NATSFROM(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(natsFrom(tail(z0))) → c11(NATSFROM(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(z0, active(z1))), ACTIVE(take(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(mark(cons(z0, natsFrom(s(z0)))), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(fst(pair(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(fst(pair(z0, z1))))
ACTIVE(cons(snd(pair(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(snd(pair(z0, z1))))
ACTIVE(cons(splitAt(0, z0), x1)) → c12(CONS(mark(pair(nil, z0)), x1), ACTIVE(splitAt(0, z0)))
ACTIVE(cons(splitAt(s(z0), cons(z1, z2)), x1)) → c12(CONS(mark(u(splitAt(z0, z2), z0, z1, z2)), x1), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(cons(u(pair(z0, z1), z2, z3, z4), x1)) → c12(CONS(mark(pair(cons(z3, z0), z1)), x1), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(cons(head(cons(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(head(cons(z0, z1))))
ACTIVE(cons(tail(cons(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(tail(cons(z0, z1))))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(mark(head(afterNth(z0, z1))), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(mark(fst(splitAt(z0, z1))), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(mark(snd(splitAt(z0, z1))), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(natsFrom(active(z0)), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c12(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c12(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(fst(z0), x1)) → c12(CONS(fst(active(z0)), x1), ACTIVE(fst(z0)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(active(z0), z1), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(z0, active(z1)), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(snd(z0), x1)) → c12(CONS(snd(active(z0)), x1), ACTIVE(snd(z0)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(active(z0), z1), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(z0, active(z1)), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(u(z0, z1, z2, z3), x1)) → c12(CONS(u(active(z0), z1, z2, z3), x1), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(cons(head(z0), x1)) → c12(CONS(head(active(z0)), x1), ACTIVE(head(z0)))
ACTIVE(cons(tail(z0), x1)) → c12(CONS(tail(active(z0)), x1), ACTIVE(tail(z0)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(active(z0), z1), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(z0, active(z1)), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(active(z0), z1), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(z0, active(z1)), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(active(z0), z1), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(z0, active(z1)), x1), ACTIVE(take(z0, z1)))

S tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(fst(pair(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(natsFrom(snd(pair(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(natsFrom(splitAt(0, z0))) → c11(NATSFROM(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(natsFrom(splitAt(s(z0), cons(z1, z2)))) → c11(NATSFROM(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(natsFrom(u(pair(z0, z1), z2, z3, z4))) → c11(NATSFROM(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(natsFrom(head(cons(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(natsFrom(tail(cons(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(cons(z0, z1))) → c11(NATSFROM(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(natsFrom(s(z0))) → c11(NATSFROM(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(natsFrom(fst(z0))) → c11(NATSFROM(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(snd(z0))) → c11(NATSFROM(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(u(z0, z1, z2, z3))) → c11(NATSFROM(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(natsFrom(head(z0))) → c11(NATSFROM(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(natsFrom(tail(z0))) → c11(NATSFROM(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(z0, active(z1))), ACTIVE(take(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(mark(cons(z0, natsFrom(s(z0)))), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(fst(pair(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(fst(pair(z0, z1))))
ACTIVE(cons(snd(pair(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(snd(pair(z0, z1))))
ACTIVE(cons(splitAt(0, z0), x1)) → c12(CONS(mark(pair(nil, z0)), x1), ACTIVE(splitAt(0, z0)))
ACTIVE(cons(splitAt(s(z0), cons(z1, z2)), x1)) → c12(CONS(mark(u(splitAt(z0, z2), z0, z1, z2)), x1), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(cons(u(pair(z0, z1), z2, z3, z4), x1)) → c12(CONS(mark(pair(cons(z3, z0), z1)), x1), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(cons(head(cons(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(head(cons(z0, z1))))
ACTIVE(cons(tail(cons(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(tail(cons(z0, z1))))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(mark(head(afterNth(z0, z1))), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(mark(fst(splitAt(z0, z1))), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(mark(snd(splitAt(z0, z1))), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(natsFrom(active(z0)), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c12(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c12(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(fst(z0), x1)) → c12(CONS(fst(active(z0)), x1), ACTIVE(fst(z0)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(active(z0), z1), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(z0, active(z1)), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(snd(z0), x1)) → c12(CONS(snd(active(z0)), x1), ACTIVE(snd(z0)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(active(z0), z1), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(z0, active(z1)), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(u(z0, z1, z2, z3), x1)) → c12(CONS(u(active(z0), z1, z2, z3), x1), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(cons(head(z0), x1)) → c12(CONS(head(active(z0)), x1), ACTIVE(head(z0)))
ACTIVE(cons(tail(z0), x1)) → c12(CONS(tail(active(z0)), x1), ACTIVE(tail(z0)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(active(z0), z1), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(z0, active(z1)), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(active(z0), z1), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(z0, active(z1)), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(active(z0), z1), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(z0, active(z1)), x1), ACTIVE(take(z0, z1)))

K tuples:none
Defined Rule Symbols:

active, u, splitAt, pair, cons, natsFrom, s, fst, snd, head, tail, sel, afterNth, take, proper

Defined Pair Symbols:

ACTIVE, NATSFROM, CONS, S, FST, PAIR, SND, SPLITAT, U, HEAD, TAIL, SEL, AFTERNTH, TAKE, PROPER, TOP

Compound Symbols:

c3, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c69, c70, c71, c72, c73, c74, c75, c76, c, c8, c9, c10, c1, c11, c12

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(s(z0)) → c13(S(active(z0)), ACTIVE(z0)) by

ACTIVE(s(natsFrom(z0))) → c13(S(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(s(fst(pair(z0, z1)))) → c13(S(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(s(snd(pair(z0, z1)))) → c13(S(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(s(splitAt(0, z0))) → c13(S(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(s(splitAt(s(z0), cons(z1, z2)))) → c13(S(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(s(u(pair(z0, z1), z2, z3, z4))) → c13(S(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(s(head(cons(z0, z1)))) → c13(S(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(s(tail(cons(z0, z1)))) → c13(S(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(s(sel(z0, z1))) → c13(S(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(natsFrom(z0))) → c13(S(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(s(cons(z0, z1))) → c13(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c13(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(fst(z0))) → c13(S(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(s(pair(z0, z1))) → c13(S(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(s(pair(z0, z1))) → c13(S(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(s(snd(z0))) → c13(S(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(s(splitAt(z0, z1))) → c13(S(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(s(splitAt(z0, z1))) → c13(S(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(s(u(z0, z1, z2, z3))) → c13(S(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(s(head(z0))) → c13(S(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(s(tail(z0))) → c13(S(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(s(sel(z0, z1))) → c13(S(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(s(sel(z0, z1))) → c13(S(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(take(z0, active(z1))), ACTIVE(take(z0, z1)))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(natsFrom(z0)) → mark(cons(z0, natsFrom(s(z0))))
active(fst(pair(z0, z1))) → mark(z0)
active(snd(pair(z0, z1))) → mark(z1)
active(splitAt(0, z0)) → mark(pair(nil, z0))
active(splitAt(s(z0), cons(z1, z2))) → mark(u(splitAt(z0, z2), z0, z1, z2))
active(u(pair(z0, z1), z2, z3, z4)) → mark(pair(cons(z3, z0), z1))
active(head(cons(z0, z1))) → mark(z0)
active(tail(cons(z0, z1))) → mark(z1)
active(sel(z0, z1)) → mark(head(afterNth(z0, z1)))
active(take(z0, z1)) → mark(fst(splitAt(z0, z1)))
active(afterNth(z0, z1)) → mark(snd(splitAt(z0, z1)))
active(natsFrom(z0)) → natsFrom(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(fst(z0)) → fst(active(z0))
active(pair(z0, z1)) → pair(active(z0), z1)
active(pair(z0, z1)) → pair(z0, active(z1))
active(snd(z0)) → snd(active(z0))
active(splitAt(z0, z1)) → splitAt(active(z0), z1)
active(splitAt(z0, z1)) → splitAt(z0, active(z1))
active(u(z0, z1, z2, z3)) → u(active(z0), z1, z2, z3)
active(head(z0)) → head(active(z0))
active(tail(z0)) → tail(active(z0))
active(sel(z0, z1)) → sel(active(z0), z1)
active(sel(z0, z1)) → sel(z0, active(z1))
active(afterNth(z0, z1)) → afterNth(active(z0), z1)
active(afterNth(z0, z1)) → afterNth(z0, active(z1))
active(take(z0, z1)) → take(active(z0), z1)
active(take(z0, z1)) → take(z0, active(z1))
u(mark(z0), z1, z2, z3) → mark(u(z0, z1, z2, z3))
u(ok(z0), ok(z1), ok(z2), ok(z3)) → ok(u(z0, z1, z2, z3))
splitAt(z0, mark(z1)) → mark(splitAt(z0, z1))
splitAt(mark(z0), z1) → mark(splitAt(z0, z1))
splitAt(ok(z0), ok(z1)) → ok(splitAt(z0, z1))
pair(mark(z0), z1) → mark(pair(z0, z1))
pair(ok(z0), ok(z1)) → ok(pair(z0, z1))
pair(z0, mark(z1)) → mark(pair(z0, z1))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
natsFrom(mark(z0)) → mark(natsFrom(z0))
natsFrom(ok(z0)) → ok(natsFrom(z0))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
fst(mark(z0)) → mark(fst(z0))
fst(ok(z0)) → ok(fst(z0))
snd(mark(z0)) → mark(snd(z0))
snd(ok(z0)) → ok(snd(z0))
head(mark(z0)) → mark(head(z0))
head(ok(z0)) → ok(head(z0))
tail(mark(z0)) → mark(tail(z0))
tail(ok(z0)) → ok(tail(z0))
sel(mark(z0), z1) → mark(sel(z0, z1))
sel(ok(z0), ok(z1)) → ok(sel(z0, z1))
sel(z0, mark(z1)) → mark(sel(z0, z1))
afterNth(mark(z0), z1) → mark(afterNth(z0, z1))
afterNth(ok(z0), ok(z1)) → ok(afterNth(z0, z1))
afterNth(z0, mark(z1)) → mark(afterNth(z0, z1))
take(mark(z0), z1) → mark(take(z0, z1))
take(ok(z0), ok(z1)) → ok(take(z0, z1))
take(z0, mark(z1)) → mark(take(z0, z1))
proper(natsFrom(z0)) → natsFrom(proper(z0))
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(fst(z0)) → fst(proper(z0))
proper(pair(z0, z1)) → pair(proper(z0), proper(z1))
proper(snd(z0)) → snd(proper(z0))
proper(splitAt(z0, z1)) → splitAt(proper(z0), proper(z1))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(u(z0, z1, z2, z3)) → u(proper(z0), proper(z1), proper(z2), proper(z3))
proper(head(z0)) → head(proper(z0))
proper(tail(z0)) → tail(proper(z0))
proper(sel(z0, z1)) → sel(proper(z0), proper(z1))
proper(afterNth(z0, z1)) → afterNth(proper(z0), proper(z1))
proper(take(z0, z1)) → take(proper(z0), proper(z1))

Tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(fst(pair(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(natsFrom(snd(pair(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(natsFrom(splitAt(0, z0))) → c11(NATSFROM(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(natsFrom(splitAt(s(z0), cons(z1, z2)))) → c11(NATSFROM(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(natsFrom(u(pair(z0, z1), z2, z3, z4))) → c11(NATSFROM(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(natsFrom(head(cons(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(natsFrom(tail(cons(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(cons(z0, z1))) → c11(NATSFROM(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(natsFrom(s(z0))) → c11(NATSFROM(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(natsFrom(fst(z0))) → c11(NATSFROM(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(snd(z0))) → c11(NATSFROM(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(u(z0, z1, z2, z3))) → c11(NATSFROM(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(natsFrom(head(z0))) → c11(NATSFROM(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(natsFrom(tail(z0))) → c11(NATSFROM(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(z0, active(z1))), ACTIVE(take(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(mark(cons(z0, natsFrom(s(z0)))), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(fst(pair(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(fst(pair(z0, z1))))
ACTIVE(cons(snd(pair(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(snd(pair(z0, z1))))
ACTIVE(cons(splitAt(0, z0), x1)) → c12(CONS(mark(pair(nil, z0)), x1), ACTIVE(splitAt(0, z0)))
ACTIVE(cons(splitAt(s(z0), cons(z1, z2)), x1)) → c12(CONS(mark(u(splitAt(z0, z2), z0, z1, z2)), x1), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(cons(u(pair(z0, z1), z2, z3, z4), x1)) → c12(CONS(mark(pair(cons(z3, z0), z1)), x1), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(cons(head(cons(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(head(cons(z0, z1))))
ACTIVE(cons(tail(cons(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(tail(cons(z0, z1))))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(mark(head(afterNth(z0, z1))), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(mark(fst(splitAt(z0, z1))), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(mark(snd(splitAt(z0, z1))), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(natsFrom(active(z0)), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c12(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c12(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(fst(z0), x1)) → c12(CONS(fst(active(z0)), x1), ACTIVE(fst(z0)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(active(z0), z1), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(z0, active(z1)), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(snd(z0), x1)) → c12(CONS(snd(active(z0)), x1), ACTIVE(snd(z0)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(active(z0), z1), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(z0, active(z1)), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(u(z0, z1, z2, z3), x1)) → c12(CONS(u(active(z0), z1, z2, z3), x1), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(cons(head(z0), x1)) → c12(CONS(head(active(z0)), x1), ACTIVE(head(z0)))
ACTIVE(cons(tail(z0), x1)) → c12(CONS(tail(active(z0)), x1), ACTIVE(tail(z0)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(active(z0), z1), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(z0, active(z1)), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(active(z0), z1), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(z0, active(z1)), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(active(z0), z1), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(z0, active(z1)), x1), ACTIVE(take(z0, z1)))
ACTIVE(s(natsFrom(z0))) → c13(S(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(s(fst(pair(z0, z1)))) → c13(S(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(s(snd(pair(z0, z1)))) → c13(S(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(s(splitAt(0, z0))) → c13(S(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(s(splitAt(s(z0), cons(z1, z2)))) → c13(S(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(s(u(pair(z0, z1), z2, z3, z4))) → c13(S(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(s(head(cons(z0, z1)))) → c13(S(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(s(tail(cons(z0, z1)))) → c13(S(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(s(sel(z0, z1))) → c13(S(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(natsFrom(z0))) → c13(S(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(s(cons(z0, z1))) → c13(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c13(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(fst(z0))) → c13(S(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(s(pair(z0, z1))) → c13(S(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(s(pair(z0, z1))) → c13(S(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(s(snd(z0))) → c13(S(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(s(splitAt(z0, z1))) → c13(S(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(s(splitAt(z0, z1))) → c13(S(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(s(u(z0, z1, z2, z3))) → c13(S(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(s(head(z0))) → c13(S(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(s(tail(z0))) → c13(S(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(s(sel(z0, z1))) → c13(S(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(s(sel(z0, z1))) → c13(S(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(take(z0, active(z1))), ACTIVE(take(z0, z1)))

S tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(fst(pair(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(natsFrom(snd(pair(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(natsFrom(splitAt(0, z0))) → c11(NATSFROM(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(natsFrom(splitAt(s(z0), cons(z1, z2)))) → c11(NATSFROM(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(natsFrom(u(pair(z0, z1), z2, z3, z4))) → c11(NATSFROM(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(natsFrom(head(cons(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(natsFrom(tail(cons(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(cons(z0, z1))) → c11(NATSFROM(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(natsFrom(s(z0))) → c11(NATSFROM(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(natsFrom(fst(z0))) → c11(NATSFROM(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(snd(z0))) → c11(NATSFROM(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(u(z0, z1, z2, z3))) → c11(NATSFROM(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(natsFrom(head(z0))) → c11(NATSFROM(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(natsFrom(tail(z0))) → c11(NATSFROM(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(z0, active(z1))), ACTIVE(take(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(mark(cons(z0, natsFrom(s(z0)))), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(fst(pair(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(fst(pair(z0, z1))))
ACTIVE(cons(snd(pair(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(snd(pair(z0, z1))))
ACTIVE(cons(splitAt(0, z0), x1)) → c12(CONS(mark(pair(nil, z0)), x1), ACTIVE(splitAt(0, z0)))
ACTIVE(cons(splitAt(s(z0), cons(z1, z2)), x1)) → c12(CONS(mark(u(splitAt(z0, z2), z0, z1, z2)), x1), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(cons(u(pair(z0, z1), z2, z3, z4), x1)) → c12(CONS(mark(pair(cons(z3, z0), z1)), x1), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(cons(head(cons(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(head(cons(z0, z1))))
ACTIVE(cons(tail(cons(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(tail(cons(z0, z1))))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(mark(head(afterNth(z0, z1))), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(mark(fst(splitAt(z0, z1))), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(mark(snd(splitAt(z0, z1))), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(natsFrom(active(z0)), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c12(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c12(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(fst(z0), x1)) → c12(CONS(fst(active(z0)), x1), ACTIVE(fst(z0)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(active(z0), z1), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(z0, active(z1)), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(snd(z0), x1)) → c12(CONS(snd(active(z0)), x1), ACTIVE(snd(z0)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(active(z0), z1), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(z0, active(z1)), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(u(z0, z1, z2, z3), x1)) → c12(CONS(u(active(z0), z1, z2, z3), x1), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(cons(head(z0), x1)) → c12(CONS(head(active(z0)), x1), ACTIVE(head(z0)))
ACTIVE(cons(tail(z0), x1)) → c12(CONS(tail(active(z0)), x1), ACTIVE(tail(z0)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(active(z0), z1), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(z0, active(z1)), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(active(z0), z1), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(z0, active(z1)), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(active(z0), z1), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(z0, active(z1)), x1), ACTIVE(take(z0, z1)))
ACTIVE(s(natsFrom(z0))) → c13(S(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(s(fst(pair(z0, z1)))) → c13(S(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(s(snd(pair(z0, z1)))) → c13(S(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(s(splitAt(0, z0))) → c13(S(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(s(splitAt(s(z0), cons(z1, z2)))) → c13(S(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(s(u(pair(z0, z1), z2, z3, z4))) → c13(S(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(s(head(cons(z0, z1)))) → c13(S(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(s(tail(cons(z0, z1)))) → c13(S(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(s(sel(z0, z1))) → c13(S(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(natsFrom(z0))) → c13(S(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(s(cons(z0, z1))) → c13(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c13(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(fst(z0))) → c13(S(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(s(pair(z0, z1))) → c13(S(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(s(pair(z0, z1))) → c13(S(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(s(snd(z0))) → c13(S(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(s(splitAt(z0, z1))) → c13(S(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(s(splitAt(z0, z1))) → c13(S(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(s(u(z0, z1, z2, z3))) → c13(S(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(s(head(z0))) → c13(S(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(s(tail(z0))) → c13(S(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(s(sel(z0, z1))) → c13(S(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(s(sel(z0, z1))) → c13(S(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(take(z0, active(z1))), ACTIVE(take(z0, z1)))

K tuples:none
Defined Rule Symbols:

active, u, splitAt, pair, cons, natsFrom, s, fst, snd, head, tail, sel, afterNth, take, proper

Defined Pair Symbols:

ACTIVE, NATSFROM, CONS, S, FST, PAIR, SND, SPLITAT, U, HEAD, TAIL, SEL, AFTERNTH, TAKE, PROPER, TOP

Compound Symbols:

c3, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c69, c70, c71, c72, c73, c74, c75, c76, c, c8, c9, c10, c1, c11, c12, c13

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(fst(z0)) → c14(FST(active(z0)), ACTIVE(z0)) by

ACTIVE(fst(natsFrom(z0))) → c14(FST(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(fst(fst(pair(z0, z1)))) → c14(FST(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(fst(snd(pair(z0, z1)))) → c14(FST(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(fst(splitAt(0, z0))) → c14(FST(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(fst(splitAt(s(z0), cons(z1, z2)))) → c14(FST(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(fst(u(pair(z0, z1), z2, z3, z4))) → c14(FST(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(fst(head(cons(z0, z1)))) → c14(FST(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(fst(tail(cons(z0, z1)))) → c14(FST(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(fst(sel(z0, z1))) → c14(FST(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(fst(take(z0, z1))) → c14(FST(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(fst(afterNth(z0, z1))) → c14(FST(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(fst(natsFrom(z0))) → c14(FST(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(fst(cons(z0, z1))) → c14(FST(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(fst(s(z0))) → c14(FST(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(fst(fst(z0))) → c14(FST(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(fst(pair(z0, z1))) → c14(FST(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(fst(pair(z0, z1))) → c14(FST(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(fst(snd(z0))) → c14(FST(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(fst(splitAt(z0, z1))) → c14(FST(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(fst(splitAt(z0, z1))) → c14(FST(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(fst(u(z0, z1, z2, z3))) → c14(FST(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(fst(head(z0))) → c14(FST(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(fst(tail(z0))) → c14(FST(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(fst(sel(z0, z1))) → c14(FST(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(fst(sel(z0, z1))) → c14(FST(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(fst(afterNth(z0, z1))) → c14(FST(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(fst(afterNth(z0, z1))) → c14(FST(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(fst(take(z0, z1))) → c14(FST(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(fst(take(z0, z1))) → c14(FST(take(z0, active(z1))), ACTIVE(take(z0, z1)))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(natsFrom(z0)) → mark(cons(z0, natsFrom(s(z0))))
active(fst(pair(z0, z1))) → mark(z0)
active(snd(pair(z0, z1))) → mark(z1)
active(splitAt(0, z0)) → mark(pair(nil, z0))
active(splitAt(s(z0), cons(z1, z2))) → mark(u(splitAt(z0, z2), z0, z1, z2))
active(u(pair(z0, z1), z2, z3, z4)) → mark(pair(cons(z3, z0), z1))
active(head(cons(z0, z1))) → mark(z0)
active(tail(cons(z0, z1))) → mark(z1)
active(sel(z0, z1)) → mark(head(afterNth(z0, z1)))
active(take(z0, z1)) → mark(fst(splitAt(z0, z1)))
active(afterNth(z0, z1)) → mark(snd(splitAt(z0, z1)))
active(natsFrom(z0)) → natsFrom(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(fst(z0)) → fst(active(z0))
active(pair(z0, z1)) → pair(active(z0), z1)
active(pair(z0, z1)) → pair(z0, active(z1))
active(snd(z0)) → snd(active(z0))
active(splitAt(z0, z1)) → splitAt(active(z0), z1)
active(splitAt(z0, z1)) → splitAt(z0, active(z1))
active(u(z0, z1, z2, z3)) → u(active(z0), z1, z2, z3)
active(head(z0)) → head(active(z0))
active(tail(z0)) → tail(active(z0))
active(sel(z0, z1)) → sel(active(z0), z1)
active(sel(z0, z1)) → sel(z0, active(z1))
active(afterNth(z0, z1)) → afterNth(active(z0), z1)
active(afterNth(z0, z1)) → afterNth(z0, active(z1))
active(take(z0, z1)) → take(active(z0), z1)
active(take(z0, z1)) → take(z0, active(z1))
u(mark(z0), z1, z2, z3) → mark(u(z0, z1, z2, z3))
u(ok(z0), ok(z1), ok(z2), ok(z3)) → ok(u(z0, z1, z2, z3))
splitAt(z0, mark(z1)) → mark(splitAt(z0, z1))
splitAt(mark(z0), z1) → mark(splitAt(z0, z1))
splitAt(ok(z0), ok(z1)) → ok(splitAt(z0, z1))
pair(mark(z0), z1) → mark(pair(z0, z1))
pair(ok(z0), ok(z1)) → ok(pair(z0, z1))
pair(z0, mark(z1)) → mark(pair(z0, z1))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
natsFrom(mark(z0)) → mark(natsFrom(z0))
natsFrom(ok(z0)) → ok(natsFrom(z0))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
fst(mark(z0)) → mark(fst(z0))
fst(ok(z0)) → ok(fst(z0))
snd(mark(z0)) → mark(snd(z0))
snd(ok(z0)) → ok(snd(z0))
head(mark(z0)) → mark(head(z0))
head(ok(z0)) → ok(head(z0))
tail(mark(z0)) → mark(tail(z0))
tail(ok(z0)) → ok(tail(z0))
sel(mark(z0), z1) → mark(sel(z0, z1))
sel(ok(z0), ok(z1)) → ok(sel(z0, z1))
sel(z0, mark(z1)) → mark(sel(z0, z1))
afterNth(mark(z0), z1) → mark(afterNth(z0, z1))
afterNth(ok(z0), ok(z1)) → ok(afterNth(z0, z1))
afterNth(z0, mark(z1)) → mark(afterNth(z0, z1))
take(mark(z0), z1) → mark(take(z0, z1))
take(ok(z0), ok(z1)) → ok(take(z0, z1))
take(z0, mark(z1)) → mark(take(z0, z1))
proper(natsFrom(z0)) → natsFrom(proper(z0))
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(fst(z0)) → fst(proper(z0))
proper(pair(z0, z1)) → pair(proper(z0), proper(z1))
proper(snd(z0)) → snd(proper(z0))
proper(splitAt(z0, z1)) → splitAt(proper(z0), proper(z1))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(u(z0, z1, z2, z3)) → u(proper(z0), proper(z1), proper(z2), proper(z3))
proper(head(z0)) → head(proper(z0))
proper(tail(z0)) → tail(proper(z0))
proper(sel(z0, z1)) → sel(proper(z0), proper(z1))
proper(afterNth(z0, z1)) → afterNth(proper(z0), proper(z1))
proper(take(z0, z1)) → take(proper(z0), proper(z1))

Tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(fst(pair(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(natsFrom(snd(pair(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(natsFrom(splitAt(0, z0))) → c11(NATSFROM(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(natsFrom(splitAt(s(z0), cons(z1, z2)))) → c11(NATSFROM(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(natsFrom(u(pair(z0, z1), z2, z3, z4))) → c11(NATSFROM(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(natsFrom(head(cons(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(natsFrom(tail(cons(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(cons(z0, z1))) → c11(NATSFROM(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(natsFrom(s(z0))) → c11(NATSFROM(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(natsFrom(fst(z0))) → c11(NATSFROM(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(snd(z0))) → c11(NATSFROM(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(u(z0, z1, z2, z3))) → c11(NATSFROM(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(natsFrom(head(z0))) → c11(NATSFROM(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(natsFrom(tail(z0))) → c11(NATSFROM(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(z0, active(z1))), ACTIVE(take(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(mark(cons(z0, natsFrom(s(z0)))), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(fst(pair(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(fst(pair(z0, z1))))
ACTIVE(cons(snd(pair(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(snd(pair(z0, z1))))
ACTIVE(cons(splitAt(0, z0), x1)) → c12(CONS(mark(pair(nil, z0)), x1), ACTIVE(splitAt(0, z0)))
ACTIVE(cons(splitAt(s(z0), cons(z1, z2)), x1)) → c12(CONS(mark(u(splitAt(z0, z2), z0, z1, z2)), x1), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(cons(u(pair(z0, z1), z2, z3, z4), x1)) → c12(CONS(mark(pair(cons(z3, z0), z1)), x1), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(cons(head(cons(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(head(cons(z0, z1))))
ACTIVE(cons(tail(cons(z0, z1)), x1)) → c12(CONS(mark(z1), x1), ACTIVE(tail(cons(z0, z1))))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(mark(head(afterNth(z0, z1))), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(mark(fst(splitAt(z0, z1))), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(mark(snd(splitAt(z0, z1))), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(natsFrom(active(z0)), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c12(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c12(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(fst(z0), x1)) → c12(CONS(fst(active(z0)), x1), ACTIVE(fst(z0)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(active(z0), z1), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(pair(z0, z1), x1)) → c12(CONS(pair(z0, active(z1)), x1), ACTIVE(pair(z0, z1)))
ACTIVE(cons(snd(z0), x1)) → c12(CONS(snd(active(z0)), x1), ACTIVE(snd(z0)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(active(z0), z1), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(splitAt(z0, z1), x1)) → c12(CONS(splitAt(z0, active(z1)), x1), ACTIVE(splitAt(z0, z1)))
ACTIVE(cons(u(z0, z1, z2, z3), x1)) → c12(CONS(u(active(z0), z1, z2, z3), x1), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(cons(head(z0), x1)) → c12(CONS(head(active(z0)), x1), ACTIVE(head(z0)))
ACTIVE(cons(tail(z0), x1)) → c12(CONS(tail(active(z0)), x1), ACTIVE(tail(z0)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(active(z0), z1), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(sel(z0, z1), x1)) → c12(CONS(sel(z0, active(z1)), x1), ACTIVE(sel(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(active(z0), z1), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(afterNth(z0, z1), x1)) → c12(CONS(afterNth(z0, active(z1)), x1), ACTIVE(afterNth(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(active(z0), z1), x1), ACTIVE(take(z0, z1)))
ACTIVE(cons(take(z0, z1), x1)) → c12(CONS(take(z0, active(z1)), x1), ACTIVE(take(z0, z1)))
ACTIVE(s(natsFrom(z0))) → c13(S(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(s(fst(pair(z0, z1)))) → c13(S(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(s(snd(pair(z0, z1)))) → c13(S(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(s(splitAt(0, z0))) → c13(S(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(s(splitAt(s(z0), cons(z1, z2)))) → c13(S(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(s(u(pair(z0, z1), z2, z3, z4))) → c13(S(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(s(head(cons(z0, z1)))) → c13(S(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(s(tail(cons(z0, z1)))) → c13(S(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(s(sel(z0, z1))) → c13(S(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(natsFrom(z0))) → c13(S(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(s(cons(z0, z1))) → c13(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c13(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(fst(z0))) → c13(S(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(s(pair(z0, z1))) → c13(S(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(s(pair(z0, z1))) → c13(S(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(s(snd(z0))) → c13(S(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(s(splitAt(z0, z1))) → c13(S(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(s(splitAt(z0, z1))) → c13(S(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(s(u(z0, z1, z2, z3))) → c13(S(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(s(head(z0))) → c13(S(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(s(tail(z0))) → c13(S(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(s(sel(z0, z1))) → c13(S(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(s(sel(z0, z1))) → c13(S(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(afterNth(z0, z1))) → c13(S(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(s(take(z0, z1))) → c13(S(take(z0, active(z1))), ACTIVE(take(z0, z1)))
ACTIVE(fst(natsFrom(z0))) → c14(FST(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(fst(fst(pair(z0, z1)))) → c14(FST(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(fst(snd(pair(z0, z1)))) → c14(FST(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(fst(splitAt(0, z0))) → c14(FST(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(fst(splitAt(s(z0), cons(z1, z2)))) → c14(FST(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(fst(u(pair(z0, z1), z2, z3, z4))) → c14(FST(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(fst(head(cons(z0, z1)))) → c14(FST(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(fst(tail(cons(z0, z1)))) → c14(FST(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(fst(sel(z0, z1))) → c14(FST(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(fst(take(z0, z1))) → c14(FST(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(fst(afterNth(z0, z1))) → c14(FST(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(fst(natsFrom(z0))) → c14(FST(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(fst(cons(z0, z1))) → c14(FST(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(fst(s(z0))) → c14(FST(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(fst(fst(z0))) → c14(FST(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(fst(pair(z0, z1))) → c14(FST(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(fst(pair(z0, z1))) → c14(FST(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(fst(snd(z0))) → c14(FST(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(fst(splitAt(z0, z1))) → c14(FST(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(fst(splitAt(z0, z1))) → c14(FST(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(fst(u(z0, z1, z2, z3))) → c14(FST(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(fst(head(z0))) → c14(FST(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(fst(tail(z0))) → c14(FST(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(fst(sel(z0, z1))) → c14(FST(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(fst(sel(z0, z1))) → c14(FST(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(fst(afterNth(z0, z1))) → c14(FST(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(fst(afterNth(z0, z1))) → c14(FST(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(fst(take(z0, z1))) → c14(FST(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(fst(take(z0, z1))) → c14(FST(take(z0, active(z1))), ACTIVE(take(z0, z1)))

S tuples:

ACTIVE(splitAt(0, z0)) → c3(PAIR(nil, z0))
ACTIVE(pair(z0, z1)) → c15(PAIR(active(z0), z1), ACTIVE(z0))
ACTIVE(pair(z0, z1)) → c16(PAIR(z0, active(z1)), ACTIVE(z1))
ACTIVE(snd(z0)) → c17(SND(active(z0)), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c18(SPLITAT(active(z0), z1), ACTIVE(z0))
ACTIVE(splitAt(z0, z1)) → c19(SPLITAT(z0, active(z1)), ACTIVE(z1))
ACTIVE(u(z0, z1, z2, z3)) → c20(U(active(z0), z1, z2, z3), ACTIVE(z0))
ACTIVE(head(z0)) → c21(HEAD(active(z0)), ACTIVE(z0))
ACTIVE(tail(z0)) → c22(TAIL(active(z0)), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c23(SEL(active(z0), z1), ACTIVE(z0))
ACTIVE(sel(z0, z1)) → c24(SEL(z0, active(z1)), ACTIVE(z1))
ACTIVE(afterNth(z0, z1)) → c25(AFTERNTH(active(z0), z1), ACTIVE(z0))
ACTIVE(afterNth(z0, z1)) → c26(AFTERNTH(z0, active(z1)), ACTIVE(z1))
ACTIVE(take(z0, z1)) → c27(TAKE(active(z0), z1), ACTIVE(z0))
ACTIVE(take(z0, z1)) → c28(TAKE(z0, active(z1)), ACTIVE(z1))
NATSFROM(mark(z0)) → c29(NATSFROM(z0))
NATSFROM(ok(z0)) → c30(NATSFROM(z0))
CONS(mark(z0), z1) → c31(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c32(CONS(z0, z1))
S(mark(z0)) → c33(S(z0))
S(ok(z0)) → c34(S(z0))
FST(mark(z0)) → c35(FST(z0))
FST(ok(z0)) → c36(FST(z0))
PAIR(mark(z0), z1) → c37(PAIR(z0, z1))
PAIR(z0, mark(z1)) → c38(PAIR(z0, z1))
PAIR(ok(z0), ok(z1)) → c39(PAIR(z0, z1))
SND(mark(z0)) → c40(SND(z0))
SND(ok(z0)) → c41(SND(z0))
SPLITAT(mark(z0), z1) → c42(SPLITAT(z0, z1))
SPLITAT(z0, mark(z1)) → c43(SPLITAT(z0, z1))
SPLITAT(ok(z0), ok(z1)) → c44(SPLITAT(z0, z1))
U(mark(z0), z1, z2, z3) → c45(U(z0, z1, z2, z3))
U(ok(z0), ok(z1), ok(z2), ok(z3)) → c46(U(z0, z1, z2, z3))
HEAD(mark(z0)) → c47(HEAD(z0))
HEAD(ok(z0)) → c48(HEAD(z0))
TAIL(mark(z0)) → c49(TAIL(z0))
TAIL(ok(z0)) → c50(TAIL(z0))
SEL(mark(z0), z1) → c51(SEL(z0, z1))
SEL(z0, mark(z1)) → c52(SEL(z0, z1))
SEL(ok(z0), ok(z1)) → c53(SEL(z0, z1))
AFTERNTH(mark(z0), z1) → c54(AFTERNTH(z0, z1))
AFTERNTH(z0, mark(z1)) → c55(AFTERNTH(z0, z1))
AFTERNTH(ok(z0), ok(z1)) → c56(AFTERNTH(z0, z1))
TAKE(mark(z0), z1) → c57(TAKE(z0, z1))
TAKE(z0, mark(z1)) → c58(TAKE(z0, z1))
TAKE(ok(z0), ok(z1)) → c59(TAKE(z0, z1))
PROPER(natsFrom(z0)) → c60(NATSFROM(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c61(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c62(S(proper(z0)), PROPER(z0))
PROPER(fst(z0)) → c63(FST(proper(z0)), PROPER(z0))
PROPER(pair(z0, z1)) → c64(PAIR(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(snd(z0)) → c65(SND(proper(z0)), PROPER(z0))
PROPER(splitAt(z0, z1)) → c66(SPLITAT(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(u(z0, z1, z2, z3)) → c69(U(proper(z0), proper(z1), proper(z2), proper(z3)), PROPER(z0), PROPER(z1), PROPER(z2), PROPER(z3))
PROPER(head(z0)) → c70(HEAD(proper(z0)), PROPER(z0))
PROPER(tail(z0)) → c71(TAIL(proper(z0)), PROPER(z0))
PROPER(sel(z0, z1)) → c72(SEL(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(afterNth(z0, z1)) → c73(AFTERNTH(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(take(z0, z1)) → c74(TAKE(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c75(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c76(TOP(active(z0)), ACTIVE(z0))
ACTIVE(natsFrom(z0)) → c(S(z0))
ACTIVE(sel(z0, z1)) → c8(AFTERNTH(z0, z1))
ACTIVE(take(z0, z1)) → c9(SPLITAT(z0, z1))
ACTIVE(afterNth(z0, z1)) → c10(SPLITAT(z0, z1))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(U(splitAt(z0, z2), z0, z1, z2))
ACTIVE(splitAt(s(z0), cons(z1, z2))) → c1(SPLITAT(z0, z2))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(PAIR(cons(z3, z0), z1))
ACTIVE(u(pair(z0, z1), z2, z3, z4)) → c1(CONS(z3, z0))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(mark(cons(z0, natsFrom(s(z0))))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(fst(pair(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(fst(pair(z0, z1))))
ACTIVE(natsFrom(snd(pair(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(snd(pair(z0, z1))))
ACTIVE(natsFrom(splitAt(0, z0))) → c11(NATSFROM(mark(pair(nil, z0))), ACTIVE(splitAt(0, z0)))
ACTIVE(natsFrom(splitAt(s(z0), cons(z1, z2)))) → c11(NATSFROM(mark(u(splitAt(z0, z2), z0, z1, z2))), ACTIVE(splitAt(s(z0), cons(z1, z2))))
ACTIVE(natsFrom(u(pair(z0, z1), z2, z3, z4))) → c11(NATSFROM(mark(pair(cons(z3, z0), z1))), ACTIVE(u(pair(z0, z1), z2, z3, z4)))
ACTIVE(natsFrom(head(cons(z0, z1)))) → c11(NATSFROM(mark(z0)), ACTIVE(head(cons(z0, z1))))
ACTIVE(natsFrom(tail(cons(z0, z1)))) → c11(NATSFROM(mark(z1)), ACTIVE(tail(cons(z0, z1))))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(mark(head(afterNth(z0, z1)))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(mark(fst(splitAt(z0, z1)))), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(mark(snd(splitAt(z0, z1)))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(natsFrom(z0))) → c11(NATSFROM(natsFrom(active(z0))), ACTIVE(natsFrom(z0)))
ACTIVE(natsFrom(cons(z0, z1))) → c11(NATSFROM(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(natsFrom(s(z0))) → c11(NATSFROM(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(natsFrom(fst(z0))) → c11(NATSFROM(fst(active(z0))), ACTIVE(fst(z0)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(active(z0), z1)), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(pair(z0, z1))) → c11(NATSFROM(pair(z0, active(z1))), ACTIVE(pair(z0, z1)))
ACTIVE(natsFrom(snd(z0))) → c11(NATSFROM(snd(active(z0))), ACTIVE(snd(z0)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(active(z0), z1)), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(splitAt(z0, z1))) → c11(NATSFROM(splitAt(z0, active(z1))), ACTIVE(splitAt(z0, z1)))
ACTIVE(natsFrom(u(z0, z1, z2, z3))) → c11(NATSFROM(u(active(z0), z1, z2, z3)), ACTIVE(u(z0, z1, z2, z3)))
ACTIVE(natsFrom(head(z0))) → c11(NATSFROM(head(active(z0))), ACTIVE(head(z0)))
ACTIVE(natsFrom(tail(z0))) → c11(NATSFROM(tail(active(z0))), ACTIVE(tail(z0)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(active(z0), z1)), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(sel(z0, z1))) → c11(NATSFROM(sel(z0, active(z1))), ACTIVE(sel(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(active(z0), z1)), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(afterNth(z0, z1))) → c11(NATSFROM(afterNth(z0, active(z1))), ACTIVE(afterNth(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(active(z0), z1)), ACTIVE(take(z0, z1)))
ACTIVE(natsFrom(take(z0, z1))) → c11(NATSFROM(take(z0, active(z1))), ACTIVE(take(z0, z1)))
ACTIVE(cons(natsFrom(z0), x1)) → c12(CONS(mark(cons(z0, natsFrom(s(z0)))), x1), ACTIVE(natsFrom(z0)))
ACTIVE(cons(fst(pair(z0, z1)), x1)) → c12(CONS(mark(z0), x1), ACTIVE(fst(pair(z0, z1))))
ACTIVE(cons(snd(pair(z0, z1)),