Runtime Complexity TRS:
The TRS R consists of the following rules:

active(U11(tt, N, X, XS)) → mark(U12(splitAt(N, XS), X))
active(U12(pair(YS, ZS), X)) → mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))
active(and(tt, X)) → mark(X)
active(fst(pair(X, Y))) → mark(X)
active(head(cons(N, XS))) → mark(N)
active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))
active(sel(N, XS)) → mark(head(afterNth(N, XS)))
active(snd(pair(X, Y))) → mark(Y)
active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(U11(tt, N, X, XS))
active(tail(cons(N, XS))) → mark(XS)
active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(U11(X1, X2, X3, X4)) → U11(active(X1), X2, X3, X4)
active(U12(X1, X2)) → U12(active(X1), X2)
active(splitAt(X1, X2)) → splitAt(active(X1), X2)
active(splitAt(X1, X2)) → splitAt(X1, active(X2))
active(pair(X1, X2)) → pair(active(X1), X2)
active(pair(X1, X2)) → pair(X1, active(X2))
active(cons(X1, X2)) → cons(active(X1), X2)
active(afterNth(X1, X2)) → afterNth(active(X1), X2)
active(afterNth(X1, X2)) → afterNth(X1, active(X2))
active(snd(X)) → snd(active(X))
active(and(X1, X2)) → and(active(X1), X2)
active(fst(X)) → fst(active(X))
active(head(X)) → head(active(X))
active(natsFrom(X)) → natsFrom(active(X))
active(s(X)) → s(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(tail(X)) → tail(active(X))
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
U11(mark(X1), X2, X3, X4) → mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2) → mark(U12(X1, X2))
splitAt(mark(X1), X2) → mark(splitAt(X1, X2))
splitAt(X1, mark(X2)) → mark(splitAt(X1, X2))
pair(mark(X1), X2) → mark(pair(X1, X2))
pair(X1, mark(X2)) → mark(pair(X1, X2))
cons(mark(X1), X2) → mark(cons(X1, X2))
afterNth(mark(X1), X2) → mark(afterNth(X1, X2))
afterNth(X1, mark(X2)) → mark(afterNth(X1, X2))
snd(mark(X)) → mark(snd(X))
and(mark(X1), X2) → mark(and(X1, X2))
fst(mark(X)) → mark(fst(X))
head(mark(X)) → mark(head(X))
natsFrom(mark(X)) → mark(natsFrom(X))
s(mark(X)) → mark(s(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
tail(mark(X)) → mark(tail(X))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
proper(U11(X1, X2, X3, X4)) → U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt) → ok(tt)
proper(U12(X1, X2)) → U12(proper(X1), proper(X2))
proper(splitAt(X1, X2)) → splitAt(proper(X1), proper(X2))
proper(pair(X1, X2)) → pair(proper(X1), proper(X2))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(afterNth(X1, X2)) → afterNth(proper(X1), proper(X2))
proper(snd(X)) → snd(proper(X))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(fst(X)) → fst(proper(X))
proper(head(X)) → head(proper(X))
proper(natsFrom(X)) → natsFrom(proper(X))
proper(s(X)) → s(proper(X))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(0) → ok(0)
proper(nil) → ok(nil)
proper(tail(X)) → tail(proper(X))
proper(take(X1, X2)) → take(proper(X1), proper(X2))
U11(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2)) → ok(U12(X1, X2))
splitAt(ok(X1), ok(X2)) → ok(splitAt(X1, X2))
pair(ok(X1), ok(X2)) → ok(pair(X1, X2))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
afterNth(ok(X1), ok(X2)) → ok(afterNth(X1, X2))
snd(ok(X)) → ok(snd(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
fst(ok(X)) → ok(fst(X))
head(ok(X)) → ok(head(X))
natsFrom(ok(X)) → ok(natsFrom(X))
s(ok(X)) → ok(s(X))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
tail(ok(X)) → ok(tail(X))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

active'(U11'(tt', N, X, XS)) → mark'(U12'(splitAt'(N, XS), X))
active'(U12'(pair'(YS, ZS), X)) → mark'(pair'(cons'(X, YS), ZS))
active'(afterNth'(N, XS)) → mark'(snd'(splitAt'(N, XS)))
active'(and'(tt', X)) → mark'(X)
active'(fst'(pair'(X, Y))) → mark'(X)
active'(head'(cons'(N, XS))) → mark'(N)
active'(natsFrom'(N)) → mark'(cons'(N, natsFrom'(s'(N))))
active'(sel'(N, XS)) → mark'(head'(afterNth'(N, XS)))
active'(snd'(pair'(X, Y))) → mark'(Y)
active'(splitAt'(0', XS)) → mark'(pair'(nil', XS))
active'(splitAt'(s'(N), cons'(X, XS))) → mark'(U11'(tt', N, X, XS))
active'(tail'(cons'(N, XS))) → mark'(XS)
active'(take'(N, XS)) → mark'(fst'(splitAt'(N, XS)))
active'(U11'(X1, X2, X3, X4)) → U11'(active'(X1), X2, X3, X4)
active'(U12'(X1, X2)) → U12'(active'(X1), X2)
active'(splitAt'(X1, X2)) → splitAt'(active'(X1), X2)
active'(splitAt'(X1, X2)) → splitAt'(X1, active'(X2))
active'(pair'(X1, X2)) → pair'(active'(X1), X2)
active'(pair'(X1, X2)) → pair'(X1, active'(X2))
active'(cons'(X1, X2)) → cons'(active'(X1), X2)
active'(afterNth'(X1, X2)) → afterNth'(active'(X1), X2)
active'(afterNth'(X1, X2)) → afterNth'(X1, active'(X2))
active'(snd'(X)) → snd'(active'(X))
active'(and'(X1, X2)) → and'(active'(X1), X2)
active'(fst'(X)) → fst'(active'(X))
active'(head'(X)) → head'(active'(X))
active'(natsFrom'(X)) → natsFrom'(active'(X))
active'(s'(X)) → s'(active'(X))
active'(sel'(X1, X2)) → sel'(active'(X1), X2)
active'(sel'(X1, X2)) → sel'(X1, active'(X2))
active'(tail'(X)) → tail'(active'(X))
active'(take'(X1, X2)) → take'(active'(X1), X2)
active'(take'(X1, X2)) → take'(X1, active'(X2))
U11'(mark'(X1), X2, X3, X4) → mark'(U11'(X1, X2, X3, X4))
U12'(mark'(X1), X2) → mark'(U12'(X1, X2))
splitAt'(mark'(X1), X2) → mark'(splitAt'(X1, X2))
splitAt'(X1, mark'(X2)) → mark'(splitAt'(X1, X2))
pair'(mark'(X1), X2) → mark'(pair'(X1, X2))
pair'(X1, mark'(X2)) → mark'(pair'(X1, X2))
cons'(mark'(X1), X2) → mark'(cons'(X1, X2))
afterNth'(mark'(X1), X2) → mark'(afterNth'(X1, X2))
afterNth'(X1, mark'(X2)) → mark'(afterNth'(X1, X2))
snd'(mark'(X)) → mark'(snd'(X))
and'(mark'(X1), X2) → mark'(and'(X1, X2))
fst'(mark'(X)) → mark'(fst'(X))
head'(mark'(X)) → mark'(head'(X))
natsFrom'(mark'(X)) → mark'(natsFrom'(X))
s'(mark'(X)) → mark'(s'(X))
sel'(mark'(X1), X2) → mark'(sel'(X1, X2))
sel'(X1, mark'(X2)) → mark'(sel'(X1, X2))
tail'(mark'(X)) → mark'(tail'(X))
take'(mark'(X1), X2) → mark'(take'(X1, X2))
take'(X1, mark'(X2)) → mark'(take'(X1, X2))
proper'(U11'(X1, X2, X3, X4)) → U11'(proper'(X1), proper'(X2), proper'(X3), proper'(X4))
proper'(tt') → ok'(tt')
proper'(U12'(X1, X2)) → U12'(proper'(X1), proper'(X2))
proper'(splitAt'(X1, X2)) → splitAt'(proper'(X1), proper'(X2))
proper'(pair'(X1, X2)) → pair'(proper'(X1), proper'(X2))
proper'(cons'(X1, X2)) → cons'(proper'(X1), proper'(X2))
proper'(afterNth'(X1, X2)) → afterNth'(proper'(X1), proper'(X2))
proper'(snd'(X)) → snd'(proper'(X))
proper'(and'(X1, X2)) → and'(proper'(X1), proper'(X2))
proper'(fst'(X)) → fst'(proper'(X))
proper'(head'(X)) → head'(proper'(X))
proper'(natsFrom'(X)) → natsFrom'(proper'(X))
proper'(s'(X)) → s'(proper'(X))
proper'(sel'(X1, X2)) → sel'(proper'(X1), proper'(X2))
proper'(0') → ok'(0')
proper'(nil') → ok'(nil')
proper'(tail'(X)) → tail'(proper'(X))
proper'(take'(X1, X2)) → take'(proper'(X1), proper'(X2))
U11'(ok'(X1), ok'(X2), ok'(X3), ok'(X4)) → ok'(U11'(X1, X2, X3, X4))
U12'(ok'(X1), ok'(X2)) → ok'(U12'(X1, X2))
splitAt'(ok'(X1), ok'(X2)) → ok'(splitAt'(X1, X2))
pair'(ok'(X1), ok'(X2)) → ok'(pair'(X1, X2))
cons'(ok'(X1), ok'(X2)) → ok'(cons'(X1, X2))
afterNth'(ok'(X1), ok'(X2)) → ok'(afterNth'(X1, X2))
snd'(ok'(X)) → ok'(snd'(X))
and'(ok'(X1), ok'(X2)) → ok'(and'(X1, X2))
fst'(ok'(X)) → ok'(fst'(X))
head'(ok'(X)) → ok'(head'(X))
natsFrom'(ok'(X)) → ok'(natsFrom'(X))
s'(ok'(X)) → ok'(s'(X))
sel'(ok'(X1), ok'(X2)) → ok'(sel'(X1, X2))
tail'(ok'(X)) → ok'(tail'(X))
take'(ok'(X1), ok'(X2)) → ok'(take'(X1, X2))
top'(mark'(X)) → top'(proper'(X))
top'(ok'(X)) → top'(active'(X))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
active'(U11'(tt', N, X, XS)) → mark'(U12'(splitAt'(N, XS), X))
active'(U12'(pair'(YS, ZS), X)) → mark'(pair'(cons'(X, YS), ZS))
active'(afterNth'(N, XS)) → mark'(snd'(splitAt'(N, XS)))
active'(and'(tt', X)) → mark'(X)
active'(fst'(pair'(X, Y))) → mark'(X)
active'(head'(cons'(N, XS))) → mark'(N)
active'(natsFrom'(N)) → mark'(cons'(N, natsFrom'(s'(N))))
active'(sel'(N, XS)) → mark'(head'(afterNth'(N, XS)))
active'(snd'(pair'(X, Y))) → mark'(Y)
active'(splitAt'(0', XS)) → mark'(pair'(nil', XS))
active'(splitAt'(s'(N), cons'(X, XS))) → mark'(U11'(tt', N, X, XS))
active'(tail'(cons'(N, XS))) → mark'(XS)
active'(take'(N, XS)) → mark'(fst'(splitAt'(N, XS)))
active'(U11'(X1, X2, X3, X4)) → U11'(active'(X1), X2, X3, X4)
active'(U12'(X1, X2)) → U12'(active'(X1), X2)
active'(splitAt'(X1, X2)) → splitAt'(active'(X1), X2)
active'(splitAt'(X1, X2)) → splitAt'(X1, active'(X2))
active'(pair'(X1, X2)) → pair'(active'(X1), X2)
active'(pair'(X1, X2)) → pair'(X1, active'(X2))
active'(cons'(X1, X2)) → cons'(active'(X1), X2)
active'(afterNth'(X1, X2)) → afterNth'(active'(X1), X2)
active'(afterNth'(X1, X2)) → afterNth'(X1, active'(X2))
active'(snd'(X)) → snd'(active'(X))
active'(and'(X1, X2)) → and'(active'(X1), X2)
active'(fst'(X)) → fst'(active'(X))
active'(head'(X)) → head'(active'(X))
active'(natsFrom'(X)) → natsFrom'(active'(X))
active'(s'(X)) → s'(active'(X))
active'(sel'(X1, X2)) → sel'(active'(X1), X2)
active'(sel'(X1, X2)) → sel'(X1, active'(X2))
active'(tail'(X)) → tail'(active'(X))
active'(take'(X1, X2)) → take'(active'(X1), X2)
active'(take'(X1, X2)) → take'(X1, active'(X2))
U11'(mark'(X1), X2, X3, X4) → mark'(U11'(X1, X2, X3, X4))
U12'(mark'(X1), X2) → mark'(U12'(X1, X2))
splitAt'(mark'(X1), X2) → mark'(splitAt'(X1, X2))
splitAt'(X1, mark'(X2)) → mark'(splitAt'(X1, X2))
pair'(mark'(X1), X2) → mark'(pair'(X1, X2))
pair'(X1, mark'(X2)) → mark'(pair'(X1, X2))
cons'(mark'(X1), X2) → mark'(cons'(X1, X2))
afterNth'(mark'(X1), X2) → mark'(afterNth'(X1, X2))
afterNth'(X1, mark'(X2)) → mark'(afterNth'(X1, X2))
snd'(mark'(X)) → mark'(snd'(X))
and'(mark'(X1), X2) → mark'(and'(X1, X2))
fst'(mark'(X)) → mark'(fst'(X))
head'(mark'(X)) → mark'(head'(X))
natsFrom'(mark'(X)) → mark'(natsFrom'(X))
s'(mark'(X)) → mark'(s'(X))
sel'(mark'(X1), X2) → mark'(sel'(X1, X2))
sel'(X1, mark'(X2)) → mark'(sel'(X1, X2))
tail'(mark'(X)) → mark'(tail'(X))
take'(mark'(X1), X2) → mark'(take'(X1, X2))
take'(X1, mark'(X2)) → mark'(take'(X1, X2))
proper'(U11'(X1, X2, X3, X4)) → U11'(proper'(X1), proper'(X2), proper'(X3), proper'(X4))
proper'(tt') → ok'(tt')
proper'(U12'(X1, X2)) → U12'(proper'(X1), proper'(X2))
proper'(splitAt'(X1, X2)) → splitAt'(proper'(X1), proper'(X2))
proper'(pair'(X1, X2)) → pair'(proper'(X1), proper'(X2))
proper'(cons'(X1, X2)) → cons'(proper'(X1), proper'(X2))
proper'(afterNth'(X1, X2)) → afterNth'(proper'(X1), proper'(X2))
proper'(snd'(X)) → snd'(proper'(X))
proper'(and'(X1, X2)) → and'(proper'(X1), proper'(X2))
proper'(fst'(X)) → fst'(proper'(X))
proper'(head'(X)) → head'(proper'(X))
proper'(natsFrom'(X)) → natsFrom'(proper'(X))
proper'(s'(X)) → s'(proper'(X))
proper'(sel'(X1, X2)) → sel'(proper'(X1), proper'(X2))
proper'(0') → ok'(0')
proper'(nil') → ok'(nil')
proper'(tail'(X)) → tail'(proper'(X))
proper'(take'(X1, X2)) → take'(proper'(X1), proper'(X2))
U11'(ok'(X1), ok'(X2), ok'(X3), ok'(X4)) → ok'(U11'(X1, X2, X3, X4))
U12'(ok'(X1), ok'(X2)) → ok'(U12'(X1, X2))
splitAt'(ok'(X1), ok'(X2)) → ok'(splitAt'(X1, X2))
pair'(ok'(X1), ok'(X2)) → ok'(pair'(X1, X2))
cons'(ok'(X1), ok'(X2)) → ok'(cons'(X1, X2))
afterNth'(ok'(X1), ok'(X2)) → ok'(afterNth'(X1, X2))
snd'(ok'(X)) → ok'(snd'(X))
and'(ok'(X1), ok'(X2)) → ok'(and'(X1, X2))
fst'(ok'(X)) → ok'(fst'(X))
head'(ok'(X)) → ok'(head'(X))
natsFrom'(ok'(X)) → ok'(natsFrom'(X))
s'(ok'(X)) → ok'(s'(X))
sel'(ok'(X1), ok'(X2)) → ok'(sel'(X1, X2))
tail'(ok'(X)) → ok'(tail'(X))
take'(ok'(X1), ok'(X2)) → ok'(take'(X1, X2))
top'(mark'(X)) → top'(proper'(X))
top'(ok'(X)) → top'(active'(X))

Types:
active' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
U11' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
tt' :: tt':mark':0':nil':ok'
mark' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
U12' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
splitAt' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
pair' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
cons' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
afterNth' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
snd' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
and' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
fst' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
head' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
natsFrom' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
s' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
sel' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
0' :: tt':mark':0':nil':ok'
nil' :: tt':mark':0':nil':ok'
tail' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
take' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
proper' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
ok' :: tt':mark':0':nil':ok' → tt':mark':0':nil':ok'
top' :: tt':mark':0':nil':ok' → top'
_hole_tt':mark':0':nil':ok'1 :: tt':mark':0':nil':ok'
_hole_top'2 :: top'
_gen_tt':mark':0':nil':ok'3 :: Nat → tt':mark':0':nil':ok'

Heuristically decided to analyse the following defined symbols:
active', U12', splitAt', pair', cons', snd', natsFrom', s', head', afterNth', U11', fst', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
U12' < active'
splitAt' < active'
pair' < active'
cons' < active'
snd' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
U11' < active'
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
U12' < proper'
splitAt' < proper'
pair' < proper'
cons' < proper'
snd' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
U11' < proper'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
U12', active', splitAt', pair', cons', snd', natsFrom', s', head', afterNth', U11', fst', and', sel', tail', take', proper', top'

Proved the following rewrite lemma:
U12'(_gen_tt':mark':0':nil':ok'3(+(1, _n5)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n5)

Induction Base:
U12'(_gen_tt':mark':0':nil':ok'3(+(1, 0)), _gen_tt':mark':0':nil':ok'3(b))

Induction Step:
U12'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n6, 1))), _gen_tt':mark':0':nil':ok'3(_b610)) →_R^Ω(1)
mark'(U12'(_gen_tt':mark':0':nil':ok'3(+(1, _$n6)), _gen_tt':mark':0':nil':ok'3(_b610))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
U12'(_gen_tt':mark':0':nil':ok'3(+(1, _n5)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
splitAt', active', pair', cons', snd', natsFrom', s', head', afterNth', U11', fst', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
splitAt' < active'
pair' < active'
cons' < active'
snd' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
U11' < active'
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
splitAt' < proper'
pair' < proper'
cons' < proper'
snd' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
U11' < proper'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
splitAt'(_gen_tt':mark':0':nil':ok'3(+(1, _n4865)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n4865)

Induction Base:
splitAt'(_gen_tt':mark':0':nil':ok'3(+(1, 0)), _gen_tt':mark':0':nil':ok'3(b))

Induction Step:
splitAt'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n4866, 1))), _gen_tt':mark':0':nil':ok'3(_b6010)) →_R^Ω(1)
mark'(splitAt'(_gen_tt':mark':0':nil':ok'3(+(1, _$n4866)), _gen_tt':mark':0':nil':ok'3(_b6010))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
pair', active', cons', snd', natsFrom', s', head', afterNth', U11', fst', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
pair' < active'
cons' < active'
snd' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
U11' < active'
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
pair' < proper'
cons' < proper'
snd' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
U11' < proper'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
pair'(_gen_tt':mark':0':nil':ok'3(+(1, _n10312)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n10312)

Induction Base:
pair'(_gen_tt':mark':0':nil':ok'3(+(1, 0)), _gen_tt':mark':0':nil':ok'3(b))

Induction Step:
pair'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n10313, 1))), _gen_tt':mark':0':nil':ok'3(_b11781)) →_R^Ω(1)
mark'(pair'(_gen_tt':mark':0':nil':ok'3(+(1, _$n10313)), _gen_tt':mark':0':nil':ok'3(_b11781))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
cons', active', snd', natsFrom', s', head', afterNth', U11', fst', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
cons' < active'
snd' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
U11' < active'
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
cons' < proper'
snd' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
U11' < proper'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
cons'(_gen_tt':mark':0':nil':ok'3(+(1, _n16127)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n16127)

Induction Base:
cons'(_gen_tt':mark':0':nil':ok'3(+(1, 0)), _gen_tt':mark':0':nil':ok'3(b))

Induction Step:
cons'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n16128, 1))), _gen_tt':mark':0':nil':ok'3(_b17704)) →_R^Ω(1)
mark'(cons'(_gen_tt':mark':0':nil':ok'3(+(1, _$n16128)), _gen_tt':mark':0':nil':ok'3(_b17704))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
snd', active', natsFrom', s', head', afterNth', U11', fst', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
snd' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
U11' < active'
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
snd' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
U11' < proper'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
snd'(_gen_tt':mark':0':nil':ok'3(+(1, _n22091))) → _*4, rt ∈ Ω(_n22091)

Induction Base:
snd'(_gen_tt':mark':0':nil':ok'3(+(1, 0)))

Induction Step:
snd'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n22092, 1)))) →_R^Ω(1)
mark'(snd'(_gen_tt':mark':0':nil':ok'3(+(1, _$n22092)))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
natsFrom', active', s', head', afterNth', U11', fst', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
U11' < active'
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
U11' < proper'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
natsFrom'(_gen_tt':mark':0':nil':ok'3(+(1, _n25971))) → _*4, rt ∈ Ω(_n25971)

Induction Base:
natsFrom'(_gen_tt':mark':0':nil':ok'3(+(1, 0)))

Induction Step:
natsFrom'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n25972, 1)))) →_R^Ω(1)
mark'(natsFrom'(_gen_tt':mark':0':nil':ok'3(+(1, _$n25972)))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
s', active', head', afterNth', U11', fst', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
s' < active'
head' < active'
afterNth' < active'
U11' < active'
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
s' < proper'
head' < proper'
afterNth' < proper'
U11' < proper'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
s'(_gen_tt':mark':0':nil':ok'3(+(1, _n29975))) → _*4, rt ∈ Ω(_n29975)

Induction Base:
s'(_gen_tt':mark':0':nil':ok'3(+(1, 0)))

Induction Step:
s'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n29976, 1)))) →_R^Ω(1)
mark'(s'(_gen_tt':mark':0':nil':ok'3(+(1, _$n29976)))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
head', active', afterNth', U11', fst', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
head' < active'
afterNth' < active'
U11' < active'
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
head' < proper'
afterNth' < proper'
U11' < proper'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
head'(_gen_tt':mark':0':nil':ok'3(+(1, _n34103))) → _*4, rt ∈ Ω(_n34103)

Induction Base:
head'(_gen_tt':mark':0':nil':ok'3(+(1, 0)))

Induction Step:
head'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n34104, 1)))) →_R^Ω(1)
mark'(head'(_gen_tt':mark':0':nil':ok'3(+(1, _$n34104)))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
afterNth', active', U11', fst', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
afterNth' < active'
U11' < active'
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
afterNth' < proper'
U11' < proper'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
afterNth'(_gen_tt':mark':0':nil':ok'3(+(1, _n38355)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n38355)

Induction Base:
afterNth'(_gen_tt':mark':0':nil':ok'3(+(1, 0)), _gen_tt':mark':0':nil':ok'3(b))

Induction Step:
afterNth'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n38356, 1))), _gen_tt':mark':0':nil':ok'3(_b41336)) →_R^Ω(1)
mark'(afterNth'(_gen_tt':mark':0':nil':ok'3(+(1, _$n38356)), _gen_tt':mark':0':nil':ok'3(_b41336))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
U11', active', fst', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
U11' < active'
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
U11' < proper'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
U11'(_gen_tt':mark':0':nil':ok'3(+(1, _n45870)), _gen_tt':mark':0':nil':ok'3(b), _gen_tt':mark':0':nil':ok'3(c), _gen_tt':mark':0':nil':ok'3(d)) → _*4, rt ∈ Ω(_n45870)

Induction Base:
U11'(_gen_tt':mark':0':nil':ok'3(+(1, 0)), _gen_tt':mark':0':nil':ok'3(b), _gen_tt':mark':0':nil':ok'3(c), _gen_tt':mark':0':nil':ok'3(d))

Induction Step:
U11'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n45871, 1))), _gen_tt':mark':0':nil':ok'3(_b52475), _gen_tt':mark':0':nil':ok'3(_c52476), _gen_tt':mark':0':nil':ok'3(_d52477)) →_R^Ω(1)
mark'(U11'(_gen_tt':mark':0':nil':ok'3(+(1, _$n45871)), _gen_tt':mark':0':nil':ok'3(_b52475), _gen_tt':mark':0':nil':ok'3(_c52476), _gen_tt':mark':0':nil':ok'3(_d52477))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
fst', active', and', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
fst' < active'
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
fst' < proper'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
fst'(_gen_tt':mark':0':nil':ok'3(+(1, _n60184))) → _*4, rt ∈ Ω(_n60184)

Induction Base:
fst'(_gen_tt':mark':0':nil':ok'3(+(1, 0)))

Induction Step:
fst'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n60185, 1)))) →_R^Ω(1)
mark'(fst'(_gen_tt':mark':0':nil':ok'3(+(1, _$n60185)))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
U12'(_gen_tt':mark':0':nil':ok'3(+(1, _n5)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n5)
splitAt'(_gen_tt':mark':0':nil':ok'3(+(1, _n4865)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n4865)
pair'(_gen_tt':mark':0':nil':ok'3(+(1, _n10312)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n10312)
cons'(_gen_tt':mark':0':nil':ok'3(+(1, _n16127)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n16127)
snd'(_gen_tt':mark':0':nil':ok'3(+(1, _n22091))) → _*4, rt ∈ Ω(_n22091)
natsFrom'(_gen_tt':mark':0':nil':ok'3(+(1, _n25971))) → _*4, rt ∈ Ω(_n25971)
s'(_gen_tt':mark':0':nil':ok'3(+(1, _n29975))) → _*4, rt ∈ Ω(_n29975)
head'(_gen_tt':mark':0':nil':ok'3(+(1, _n34103))) → _*4, rt ∈ Ω(_n34103)
afterNth'(_gen_tt':mark':0':nil':ok'3(+(1, _n38355)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n38355)
U11'(_gen_tt':mark':0':nil':ok'3(+(1, _n45870)), _gen_tt':mark':0':nil':ok'3(b), _gen_tt':mark':0':nil':ok'3(c), _gen_tt':mark':0':nil':ok'3(d)) → _*4, rt ∈ Ω(_n45870)
fst'(_gen_tt':mark':0':nil':ok'3(+(1, _n60184))) → _*4, rt ∈ Ω(_n60184)

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
and', active', sel', tail', take', proper', top'

They will be analysed ascendingly in the following order:
and' < active'
sel' < active'
tail' < active'
take' < active'
active' < top'
and' < proper'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
and'(_gen_tt':mark':0':nil':ok'3(+(1, _n65076)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n65076)

Induction Base:
and'(_gen_tt':mark':0':nil':ok'3(+(1, 0)), _gen_tt':mark':0':nil':ok'3(b))

Induction Step:
and'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n65077, 1))), _gen_tt':mark':0':nil':ok'3(_b68921)) →_R^Ω(1)
mark'(and'(_gen_tt':mark':0':nil':ok'3(+(1, _$n65077)), _gen_tt':mark':0':nil':ok'3(_b68921))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
sel', active', tail', take', proper', top'

They will be analysed ascendingly in the following order:
sel' < active'
tail' < active'
take' < active'
active' < top'
sel' < proper'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
sel'(_gen_tt':mark':0':nil':ok'3(+(1, _n73603)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n73603)

Induction Base:
sel'(_gen_tt':mark':0':nil':ok'3(+(1, 0)), _gen_tt':mark':0':nil':ok'3(b))

Induction Step:
sel'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n73604, 1))), _gen_tt':mark':0':nil':ok'3(_b77988)) →_R^Ω(1)
mark'(sel'(_gen_tt':mark':0':nil':ok'3(+(1, _$n73604)), _gen_tt':mark':0':nil':ok'3(_b77988))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
tail', active', take', proper', top'

They will be analysed ascendingly in the following order:
tail' < active'
take' < active'
active' < top'
tail' < proper'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
tail'(_gen_tt':mark':0':nil':ok'3(+(1, _n82717))) → _*4, rt ∈ Ω(_n82717)

Induction Base:
tail'(_gen_tt':mark':0':nil':ok'3(+(1, 0)))

Induction Step:
tail'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n82718, 1)))) →_R^Ω(1)
mark'(tail'(_gen_tt':mark':0':nil':ok'3(+(1, _$n82718)))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
take', active', proper', top'

They will be analysed ascendingly in the following order:
take' < active'
active' < top'
take' < proper'
proper' < top'

Proved the following rewrite lemma:
take'(_gen_tt':mark':0':nil':ok'3(+(1, _n88115)), _gen_tt':mark':0':nil':ok'3(b)) → _*4, rt ∈ Ω(_n88115)

Induction Base:
take'(_gen_tt':mark':0':nil':ok'3(+(1, 0)), _gen_tt':mark':0':nil':ok'3(b))

Induction Step:
take'(_gen_tt':mark':0':nil':ok'3(+(1, +(_$n88116, 1))), _gen_tt':mark':0':nil':ok'3(_b93040)) →_R^Ω(1)
mark'(take'(_gen_tt':mark':0':nil':ok'3(+(1, _$n88116)), _gen_tt':mark':0':nil':ok'3(_b93040))) →_IH
mark'(_*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
_gen_tt':mark':0':nil':ok'3(0) ⇔ tt'
_gen_tt':mark':0':nil':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':0':nil':ok'3(x))

The following defined symbols remain to be analysed:
active', proper', top'

They will be analysed ascendingly in the following order:
active' < top'
proper' < top'