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

active(U101(tt, V1, V2)) → mark(U102(isNatural(V1), V2))
active(U102(tt, V2)) → mark(U103(isLNat(V2)))
active(U103(tt)) → mark(tt)
active(U11(tt, N, XS)) → mark(snd(splitAt(N, XS)))
active(U111(tt, V1)) → mark(U112(isLNat(V1)))
active(U112(tt)) → mark(tt)
active(U121(tt, V1)) → mark(U122(isNatural(V1)))
active(U122(tt)) → mark(tt)
active(U131(tt, V1, V2)) → mark(U132(isNatural(V1), V2))
active(U132(tt, V2)) → mark(U133(isLNat(V2)))
active(U133(tt)) → mark(tt)
active(U141(tt, V1, V2)) → mark(U142(isLNat(V1), V2))
active(U142(tt, V2)) → mark(U143(isLNat(V2)))
active(U143(tt)) → mark(tt)
active(U151(tt, V1, V2)) → mark(U152(isNatural(V1), V2))
active(U152(tt, V2)) → mark(U153(isLNat(V2)))
active(U153(tt)) → mark(tt)
active(U161(tt, N)) → mark(cons(N, natsFrom(s(N))))
active(U171(tt, N, XS)) → mark(head(afterNth(N, XS)))
active(U181(tt, Y)) → mark(Y)
active(U191(tt, XS)) → mark(pair(nil, XS))
active(U201(tt, N, X, XS)) → mark(U202(splitAt(N, XS), X))
active(U202(pair(YS, ZS), X)) → mark(pair(cons(X, YS), ZS))
active(U21(tt, X)) → mark(X)
active(U211(tt, XS)) → mark(XS)
active(U221(tt, N, XS)) → mark(fst(splitAt(N, XS)))
active(U31(tt, N)) → mark(N)
active(U41(tt, V1, V2)) → mark(U42(isNatural(V1), V2))
active(U42(tt, V2)) → mark(U43(isLNat(V2)))
active(U43(tt)) → mark(tt)
active(U51(tt, V1, V2)) → mark(U52(isNatural(V1), V2))
active(U52(tt, V2)) → mark(U53(isLNat(V2)))
active(U53(tt)) → mark(tt)
active(U61(tt, V1)) → mark(U62(isPLNat(V1)))
active(U62(tt)) → mark(tt)
active(U71(tt, V1)) → mark(U72(isNatural(V1)))
active(U72(tt)) → mark(tt)
active(U81(tt, V1)) → mark(U82(isPLNat(V1)))
active(U82(tt)) → mark(tt)
active(U91(tt, V1)) → mark(U92(isLNat(V1)))
active(U92(tt)) → mark(tt)
active(afterNth(N, XS)) → mark(U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS))
active(and(tt, X)) → mark(X)
active(fst(pair(X, Y))) → mark(U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X))
active(head(cons(N, XS))) → mark(U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N))
active(isLNat(nil)) → mark(tt)
active(isLNat(afterNth(V1, V2))) → mark(U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2))
active(isLNat(cons(V1, V2))) → mark(U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2))
active(isLNat(fst(V1))) → mark(U61(isPLNatKind(V1), V1))
active(isLNat(natsFrom(V1))) → mark(U71(isNaturalKind(V1), V1))
active(isLNat(snd(V1))) → mark(U81(isPLNatKind(V1), V1))
active(isLNat(tail(V1))) → mark(U91(isLNatKind(V1), V1))
active(isLNat(take(V1, V2))) → mark(U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2))
active(isLNatKind(nil)) → mark(tt)
active(isLNatKind(afterNth(V1, V2))) → mark(and(isNaturalKind(V1), isLNatKind(V2)))
active(isLNatKind(cons(V1, V2))) → mark(and(isNaturalKind(V1), isLNatKind(V2)))
active(isLNatKind(fst(V1))) → mark(isPLNatKind(V1))
active(isLNatKind(natsFrom(V1))) → mark(isNaturalKind(V1))
active(isLNatKind(snd(V1))) → mark(isPLNatKind(V1))
active(isLNatKind(tail(V1))) → mark(isLNatKind(V1))
active(isLNatKind(take(V1, V2))) → mark(and(isNaturalKind(V1), isLNatKind(V2)))
active(isNatural(0)) → mark(tt)
active(isNatural(head(V1))) → mark(U111(isLNatKind(V1), V1))
active(isNatural(s(V1))) → mark(U121(isNaturalKind(V1), V1))
active(isNatural(sel(V1, V2))) → mark(U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2))
active(isNaturalKind(0)) → mark(tt)
active(isNaturalKind(head(V1))) → mark(isLNatKind(V1))
active(isNaturalKind(s(V1))) → mark(isNaturalKind(V1))
active(isNaturalKind(sel(V1, V2))) → mark(and(isNaturalKind(V1), isLNatKind(V2)))
active(isPLNat(pair(V1, V2))) → mark(U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2))
active(isPLNat(splitAt(V1, V2))) → mark(U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2))
active(isPLNatKind(pair(V1, V2))) → mark(and(isLNatKind(V1), isLNatKind(V2)))
active(isPLNatKind(splitAt(V1, V2))) → mark(and(isNaturalKind(V1), isLNatKind(V2)))
active(natsFrom(N)) → mark(U161(and(isNatural(N), isNaturalKind(N)), N))
active(sel(N, XS)) → mark(U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS))
active(snd(pair(X, Y))) → mark(U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y))
active(splitAt(0, XS)) → mark(U191(and(isLNat(XS), isLNatKind(XS)), XS))
active(splitAt(s(N), cons(X, XS))) → mark(U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS))
active(tail(cons(N, XS))) → mark(U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS))
active(take(N, XS)) → mark(U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS))
active(U101(X1, X2, X3)) → U101(active(X1), X2, X3)
active(U102(X1, X2)) → U102(active(X1), X2)
active(U103(X)) → U103(active(X))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(snd(X)) → snd(active(X))
active(splitAt(X1, X2)) → splitAt(active(X1), X2)
active(splitAt(X1, X2)) → splitAt(X1, active(X2))
active(U111(X1, X2)) → U111(active(X1), X2)
active(U112(X)) → U112(active(X))
active(U121(X1, X2)) → U121(active(X1), X2)
active(U122(X)) → U122(active(X))
active(U131(X1, X2, X3)) → U131(active(X1), X2, X3)
active(U132(X1, X2)) → U132(active(X1), X2)
active(U133(X)) → U133(active(X))
active(U141(X1, X2, X3)) → U141(active(X1), X2, X3)
active(U142(X1, X2)) → U142(active(X1), X2)
active(U143(X)) → U143(active(X))
active(U151(X1, X2, X3)) → U151(active(X1), X2, X3)
active(U152(X1, X2)) → U152(active(X1), X2)
active(U153(X)) → U153(active(X))
active(U161(X1, X2)) → U161(active(X1), X2)
active(cons(X1, X2)) → cons(active(X1), X2)
active(natsFrom(X)) → natsFrom(active(X))
active(s(X)) → s(active(X))
active(U171(X1, X2, X3)) → U171(active(X1), X2, X3)
active(head(X)) → head(active(X))
active(afterNth(X1, X2)) → afterNth(active(X1), X2)
active(afterNth(X1, X2)) → afterNth(X1, active(X2))
active(U181(X1, X2)) → U181(active(X1), X2)
active(U191(X1, X2)) → U191(active(X1), X2)
active(pair(X1, X2)) → pair(active(X1), X2)
active(pair(X1, X2)) → pair(X1, active(X2))
active(U201(X1, X2, X3, X4)) → U201(active(X1), X2, X3, X4)
active(U202(X1, X2)) → U202(active(X1), X2)
active(U21(X1, X2)) → U21(active(X1), X2)
active(U211(X1, X2)) → U211(active(X1), X2)
active(U221(X1, X2, X3)) → U221(active(X1), X2, X3)
active(fst(X)) → fst(active(X))
active(U31(X1, X2)) → U31(active(X1), X2)
active(U41(X1, X2, X3)) → U41(active(X1), X2, X3)
active(U42(X1, X2)) → U42(active(X1), X2)
active(U43(X)) → U43(active(X))
active(U51(X1, X2, X3)) → U51(active(X1), X2, X3)
active(U52(X1, X2)) → U52(active(X1), X2)
active(U53(X)) → U53(active(X))
active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))
active(U71(X1, X2)) → U71(active(X1), X2)
active(U72(X)) → U72(active(X))
active(U81(X1, X2)) → U81(active(X1), X2)
active(U82(X)) → U82(active(X))
active(U91(X1, X2)) → U91(active(X1), X2)
active(U92(X)) → U92(active(X))
active(and(X1, X2)) → and(active(X1), X2)
active(tail(X)) → tail(active(X))
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
U101(mark(X1), X2, X3) → mark(U101(X1, X2, X3))
U102(mark(X1), X2) → mark(U102(X1, X2))
U103(mark(X)) → mark(U103(X))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
snd(mark(X)) → mark(snd(X))
splitAt(mark(X1), X2) → mark(splitAt(X1, X2))
splitAt(X1, mark(X2)) → mark(splitAt(X1, X2))
U111(mark(X1), X2) → mark(U111(X1, X2))
U112(mark(X)) → mark(U112(X))
U121(mark(X1), X2) → mark(U121(X1, X2))
U122(mark(X)) → mark(U122(X))
U131(mark(X1), X2, X3) → mark(U131(X1, X2, X3))
U132(mark(X1), X2) → mark(U132(X1, X2))
U133(mark(X)) → mark(U133(X))
U141(mark(X1), X2, X3) → mark(U141(X1, X2, X3))
U142(mark(X1), X2) → mark(U142(X1, X2))
U143(mark(X)) → mark(U143(X))
U151(mark(X1), X2, X3) → mark(U151(X1, X2, X3))
U152(mark(X1), X2) → mark(U152(X1, X2))
U153(mark(X)) → mark(U153(X))
U161(mark(X1), X2) → mark(U161(X1, X2))
cons(mark(X1), X2) → mark(cons(X1, X2))
natsFrom(mark(X)) → mark(natsFrom(X))
s(mark(X)) → mark(s(X))
U171(mark(X1), X2, X3) → mark(U171(X1, X2, X3))
head(mark(X)) → mark(head(X))
afterNth(mark(X1), X2) → mark(afterNth(X1, X2))
afterNth(X1, mark(X2)) → mark(afterNth(X1, X2))
U181(mark(X1), X2) → mark(U181(X1, X2))
U191(mark(X1), X2) → mark(U191(X1, X2))
pair(mark(X1), X2) → mark(pair(X1, X2))
pair(X1, mark(X2)) → mark(pair(X1, X2))
U201(mark(X1), X2, X3, X4) → mark(U201(X1, X2, X3, X4))
U202(mark(X1), X2) → mark(U202(X1, X2))
U21(mark(X1), X2) → mark(U21(X1, X2))
U211(mark(X1), X2) → mark(U211(X1, X2))
U221(mark(X1), X2, X3) → mark(U221(X1, X2, X3))
fst(mark(X)) → mark(fst(X))
U31(mark(X1), X2) → mark(U31(X1, X2))
U41(mark(X1), X2, X3) → mark(U41(X1, X2, X3))
U42(mark(X1), X2) → mark(U42(X1, X2))
U43(mark(X)) → mark(U43(X))
U51(mark(X1), X2, X3) → mark(U51(X1, X2, X3))
U52(mark(X1), X2) → mark(U52(X1, X2))
U53(mark(X)) → mark(U53(X))
U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))
U71(mark(X1), X2) → mark(U71(X1, X2))
U72(mark(X)) → mark(U72(X))
U81(mark(X1), X2) → mark(U81(X1, X2))
U82(mark(X)) → mark(U82(X))
U91(mark(X1), X2) → mark(U91(X1, X2))
U92(mark(X)) → mark(U92(X))
and(mark(X1), X2) → mark(and(X1, X2))
tail(mark(X)) → mark(tail(X))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
proper(U101(X1, X2, X3)) → U101(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U102(X1, X2)) → U102(proper(X1), proper(X2))
proper(isNatural(X)) → isNatural(proper(X))
proper(U103(X)) → U103(proper(X))
proper(isLNat(X)) → isLNat(proper(X))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(snd(X)) → snd(proper(X))
proper(splitAt(X1, X2)) → splitAt(proper(X1), proper(X2))
proper(U111(X1, X2)) → U111(proper(X1), proper(X2))
proper(U112(X)) → U112(proper(X))
proper(U121(X1, X2)) → U121(proper(X1), proper(X2))
proper(U122(X)) → U122(proper(X))
proper(U131(X1, X2, X3)) → U131(proper(X1), proper(X2), proper(X3))
proper(U132(X1, X2)) → U132(proper(X1), proper(X2))
proper(U133(X)) → U133(proper(X))
proper(U141(X1, X2, X3)) → U141(proper(X1), proper(X2), proper(X3))
proper(U142(X1, X2)) → U142(proper(X1), proper(X2))
proper(U143(X)) → U143(proper(X))
proper(U151(X1, X2, X3)) → U151(proper(X1), proper(X2), proper(X3))
proper(U152(X1, X2)) → U152(proper(X1), proper(X2))
proper(U153(X)) → U153(proper(X))
proper(U161(X1, X2)) → U161(proper(X1), proper(X2))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(natsFrom(X)) → natsFrom(proper(X))
proper(s(X)) → s(proper(X))
proper(U171(X1, X2, X3)) → U171(proper(X1), proper(X2), proper(X3))
proper(head(X)) → head(proper(X))
proper(afterNth(X1, X2)) → afterNth(proper(X1), proper(X2))
proper(U181(X1, X2)) → U181(proper(X1), proper(X2))
proper(U191(X1, X2)) → U191(proper(X1), proper(X2))
proper(pair(X1, X2)) → pair(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(U201(X1, X2, X3, X4)) → U201(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U202(X1, X2)) → U202(proper(X1), proper(X2))
proper(U21(X1, X2)) → U21(proper(X1), proper(X2))
proper(U211(X1, X2)) → U211(proper(X1), proper(X2))
proper(U221(X1, X2, X3)) → U221(proper(X1), proper(X2), proper(X3))
proper(fst(X)) → fst(proper(X))
proper(U31(X1, X2)) → U31(proper(X1), proper(X2))
proper(U41(X1, X2, X3)) → U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2)) → U42(proper(X1), proper(X2))
proper(U43(X)) → U43(proper(X))
proper(U51(X1, X2, X3)) → U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2)) → U52(proper(X1), proper(X2))
proper(U53(X)) → U53(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))
proper(U62(X)) → U62(proper(X))
proper(isPLNat(X)) → isPLNat(proper(X))
proper(U71(X1, X2)) → U71(proper(X1), proper(X2))
proper(U72(X)) → U72(proper(X))
proper(U81(X1, X2)) → U81(proper(X1), proper(X2))
proper(U82(X)) → U82(proper(X))
proper(U91(X1, X2)) → U91(proper(X1), proper(X2))
proper(U92(X)) → U92(proper(X))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNaturalKind(X)) → isNaturalKind(proper(X))
proper(isLNatKind(X)) → isLNatKind(proper(X))
proper(isPLNatKind(X)) → isPLNatKind(proper(X))
proper(tail(X)) → tail(proper(X))
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(0) → ok(0)
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
U101(ok(X1), ok(X2), ok(X3)) → ok(U101(X1, X2, X3))
U102(ok(X1), ok(X2)) → ok(U102(X1, X2))
isNatural(ok(X)) → ok(isNatural(X))
U103(ok(X)) → ok(U103(X))
isLNat(ok(X)) → ok(isLNat(X))
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
snd(ok(X)) → ok(snd(X))
splitAt(ok(X1), ok(X2)) → ok(splitAt(X1, X2))
U111(ok(X1), ok(X2)) → ok(U111(X1, X2))
U112(ok(X)) → ok(U112(X))
U121(ok(X1), ok(X2)) → ok(U121(X1, X2))
U122(ok(X)) → ok(U122(X))
U131(ok(X1), ok(X2), ok(X3)) → ok(U131(X1, X2, X3))
U132(ok(X1), ok(X2)) → ok(U132(X1, X2))
U133(ok(X)) → ok(U133(X))
U141(ok(X1), ok(X2), ok(X3)) → ok(U141(X1, X2, X3))
U142(ok(X1), ok(X2)) → ok(U142(X1, X2))
U143(ok(X)) → ok(U143(X))
U151(ok(X1), ok(X2), ok(X3)) → ok(U151(X1, X2, X3))
U152(ok(X1), ok(X2)) → ok(U152(X1, X2))
U153(ok(X)) → ok(U153(X))
U161(ok(X1), ok(X2)) → ok(U161(X1, X2))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
natsFrom(ok(X)) → ok(natsFrom(X))
s(ok(X)) → ok(s(X))
U171(ok(X1), ok(X2), ok(X3)) → ok(U171(X1, X2, X3))
head(ok(X)) → ok(head(X))
afterNth(ok(X1), ok(X2)) → ok(afterNth(X1, X2))
U181(ok(X1), ok(X2)) → ok(U181(X1, X2))
U191(ok(X1), ok(X2)) → ok(U191(X1, X2))
pair(ok(X1), ok(X2)) → ok(pair(X1, X2))
U201(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U201(X1, X2, X3, X4))
U202(ok(X1), ok(X2)) → ok(U202(X1, X2))
U21(ok(X1), ok(X2)) → ok(U21(X1, X2))
U211(ok(X1), ok(X2)) → ok(U211(X1, X2))
U221(ok(X1), ok(X2), ok(X3)) → ok(U221(X1, X2, X3))
fst(ok(X)) → ok(fst(X))
U31(ok(X1), ok(X2)) → ok(U31(X1, X2))
U41(ok(X1), ok(X2), ok(X3)) → ok(U41(X1, X2, X3))
U42(ok(X1), ok(X2)) → ok(U42(X1, X2))
U43(ok(X)) → ok(U43(X))
U51(ok(X1), ok(X2), ok(X3)) → ok(U51(X1, X2, X3))
U52(ok(X1), ok(X2)) → ok(U52(X1, X2))
U53(ok(X)) → ok(U53(X))
U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))
isPLNat(ok(X)) → ok(isPLNat(X))
U71(ok(X1), ok(X2)) → ok(U71(X1, X2))
U72(ok(X)) → ok(U72(X))
U81(ok(X1), ok(X2)) → ok(U81(X1, X2))
U82(ok(X)) → ok(U82(X))
U91(ok(X1), ok(X2)) → ok(U91(X1, X2))
U92(ok(X)) → ok(U92(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNaturalKind(ok(X)) → ok(isNaturalKind(X))
isLNatKind(ok(X)) → ok(isLNatKind(X))
isPLNatKind(ok(X)) → ok(isPLNatKind(X))
tail(ok(X)) → ok(tail(X))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(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'(U101'(tt', V1, V2)) → mark'(U102'(isNatural'(V1), V2))
active'(U102'(tt', V2)) → mark'(U103'(isLNat'(V2)))
active'(U103'(tt')) → mark'(tt')
active'(U11'(tt', N, XS)) → mark'(snd'(splitAt'(N, XS)))
active'(U111'(tt', V1)) → mark'(U112'(isLNat'(V1)))
active'(U112'(tt')) → mark'(tt')
active'(U121'(tt', V1)) → mark'(U122'(isNatural'(V1)))
active'(U122'(tt')) → mark'(tt')
active'(U131'(tt', V1, V2)) → mark'(U132'(isNatural'(V1), V2))
active'(U132'(tt', V2)) → mark'(U133'(isLNat'(V2)))
active'(U133'(tt')) → mark'(tt')
active'(U141'(tt', V1, V2)) → mark'(U142'(isLNat'(V1), V2))
active'(U142'(tt', V2)) → mark'(U143'(isLNat'(V2)))
active'(U143'(tt')) → mark'(tt')
active'(U151'(tt', V1, V2)) → mark'(U152'(isNatural'(V1), V2))
active'(U152'(tt', V2)) → mark'(U153'(isLNat'(V2)))
active'(U153'(tt')) → mark'(tt')
active'(U161'(tt', N)) → mark'(cons'(N, natsFrom'(s'(N))))
active'(U171'(tt', N, XS)) → mark'(head'(afterNth'(N, XS)))
active'(U181'(tt', Y)) → mark'(Y)
active'(U191'(tt', XS)) → mark'(pair'(nil', XS))
active'(U201'(tt', N, X, XS)) → mark'(U202'(splitAt'(N, XS), X))
active'(U202'(pair'(YS, ZS), X)) → mark'(pair'(cons'(X, YS), ZS))
active'(U21'(tt', X)) → mark'(X)
active'(U211'(tt', XS)) → mark'(XS)
active'(U221'(tt', N, XS)) → mark'(fst'(splitAt'(N, XS)))
active'(U31'(tt', N)) → mark'(N)
active'(U41'(tt', V1, V2)) → mark'(U42'(isNatural'(V1), V2))
active'(U42'(tt', V2)) → mark'(U43'(isLNat'(V2)))
active'(U43'(tt')) → mark'(tt')
active'(U51'(tt', V1, V2)) → mark'(U52'(isNatural'(V1), V2))
active'(U52'(tt', V2)) → mark'(U53'(isLNat'(V2)))
active'(U53'(tt')) → mark'(tt')
active'(U61'(tt', V1)) → mark'(U62'(isPLNat'(V1)))
active'(U62'(tt')) → mark'(tt')
active'(U71'(tt', V1)) → mark'(U72'(isNatural'(V1)))
active'(U72'(tt')) → mark'(tt')
active'(U81'(tt', V1)) → mark'(U82'(isPLNat'(V1)))
active'(U82'(tt')) → mark'(tt')
active'(U91'(tt', V1)) → mark'(U92'(isLNat'(V1)))
active'(U92'(tt')) → mark'(tt')
active'(afterNth'(N, XS)) → mark'(U11'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(isLNat'(XS), isLNatKind'(XS))), N, XS))
active'(and'(tt', X)) → mark'(X)
active'(fst'(pair'(X, Y))) → mark'(U21'(and'(and'(isLNat'(X), isLNatKind'(X)), and'(isLNat'(Y), isLNatKind'(Y))), X))
active'(head'(cons'(N, XS))) → mark'(U31'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(isLNat'(XS), isLNatKind'(XS))), N))
active'(isLNat'(nil')) → mark'(tt')
active'(isLNat'(afterNth'(V1, V2))) → mark'(U41'(and'(isNaturalKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isLNat'(cons'(V1, V2))) → mark'(U51'(and'(isNaturalKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isLNat'(fst'(V1))) → mark'(U61'(isPLNatKind'(V1), V1))
active'(isLNat'(natsFrom'(V1))) → mark'(U71'(isNaturalKind'(V1), V1))
active'(isLNat'(snd'(V1))) → mark'(U81'(isPLNatKind'(V1), V1))
active'(isLNat'(tail'(V1))) → mark'(U91'(isLNatKind'(V1), V1))
active'(isLNat'(take'(V1, V2))) → mark'(U101'(and'(isNaturalKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isLNatKind'(nil')) → mark'(tt')
active'(isLNatKind'(afterNth'(V1, V2))) → mark'(and'(isNaturalKind'(V1), isLNatKind'(V2)))
active'(isLNatKind'(cons'(V1, V2))) → mark'(and'(isNaturalKind'(V1), isLNatKind'(V2)))
active'(isLNatKind'(fst'(V1))) → mark'(isPLNatKind'(V1))
active'(isLNatKind'(natsFrom'(V1))) → mark'(isNaturalKind'(V1))
active'(isLNatKind'(snd'(V1))) → mark'(isPLNatKind'(V1))
active'(isLNatKind'(tail'(V1))) → mark'(isLNatKind'(V1))
active'(isLNatKind'(take'(V1, V2))) → mark'(and'(isNaturalKind'(V1), isLNatKind'(V2)))
active'(isNatural'(0')) → mark'(tt')
active'(isNatural'(head'(V1))) → mark'(U111'(isLNatKind'(V1), V1))
active'(isNatural'(s'(V1))) → mark'(U121'(isNaturalKind'(V1), V1))
active'(isNatural'(sel'(V1, V2))) → mark'(U131'(and'(isNaturalKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isNaturalKind'(0')) → mark'(tt')
active'(isNaturalKind'(head'(V1))) → mark'(isLNatKind'(V1))
active'(isNaturalKind'(s'(V1))) → mark'(isNaturalKind'(V1))
active'(isNaturalKind'(sel'(V1, V2))) → mark'(and'(isNaturalKind'(V1), isLNatKind'(V2)))
active'(isPLNat'(pair'(V1, V2))) → mark'(U141'(and'(isLNatKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isPLNat'(splitAt'(V1, V2))) → mark'(U151'(and'(isNaturalKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isPLNatKind'(pair'(V1, V2))) → mark'(and'(isLNatKind'(V1), isLNatKind'(V2)))
active'(isPLNatKind'(splitAt'(V1, V2))) → mark'(and'(isNaturalKind'(V1), isLNatKind'(V2)))
active'(natsFrom'(N)) → mark'(U161'(and'(isNatural'(N), isNaturalKind'(N)), N))
active'(sel'(N, XS)) → mark'(U171'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(isLNat'(XS), isLNatKind'(XS))), N, XS))
active'(snd'(pair'(X, Y))) → mark'(U181'(and'(and'(isLNat'(X), isLNatKind'(X)), and'(isLNat'(Y), isLNatKind'(Y))), Y))
active'(splitAt'(0', XS)) → mark'(U191'(and'(isLNat'(XS), isLNatKind'(XS)), XS))
active'(splitAt'(s'(N), cons'(X, XS))) → mark'(U201'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(and'(isNatural'(X), isNaturalKind'(X)), and'(isLNat'(XS), isLNatKind'(XS)))), N, X, XS))
active'(tail'(cons'(N, XS))) → mark'(U211'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(isLNat'(XS), isLNatKind'(XS))), XS))
active'(take'(N, XS)) → mark'(U221'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(isLNat'(XS), isLNatKind'(XS))), N, XS))
active'(U101'(X1, X2, X3)) → U101'(active'(X1), X2, X3)
active'(U102'(X1, X2)) → U102'(active'(X1), X2)
active'(U103'(X)) → U103'(active'(X))
active'(U11'(X1, X2, X3)) → U11'(active'(X1), X2, X3)
active'(snd'(X)) → snd'(active'(X))
active'(splitAt'(X1, X2)) → splitAt'(active'(X1), X2)
active'(splitAt'(X1, X2)) → splitAt'(X1, active'(X2))
active'(U111'(X1, X2)) → U111'(active'(X1), X2)
active'(U112'(X)) → U112'(active'(X))
active'(U121'(X1, X2)) → U121'(active'(X1), X2)
active'(U122'(X)) → U122'(active'(X))
active'(U131'(X1, X2, X3)) → U131'(active'(X1), X2, X3)
active'(U132'(X1, X2)) → U132'(active'(X1), X2)
active'(U133'(X)) → U133'(active'(X))
active'(U141'(X1, X2, X3)) → U141'(active'(X1), X2, X3)
active'(U142'(X1, X2)) → U142'(active'(X1), X2)
active'(U143'(X)) → U143'(active'(X))
active'(U151'(X1, X2, X3)) → U151'(active'(X1), X2, X3)
active'(U152'(X1, X2)) → U152'(active'(X1), X2)
active'(U153'(X)) → U153'(active'(X))
active'(U161'(X1, X2)) → U161'(active'(X1), X2)
active'(cons'(X1, X2)) → cons'(active'(X1), X2)
active'(natsFrom'(X)) → natsFrom'(active'(X))
active'(s'(X)) → s'(active'(X))
active'(U171'(X1, X2, X3)) → U171'(active'(X1), X2, X3)
active'(head'(X)) → head'(active'(X))
active'(afterNth'(X1, X2)) → afterNth'(active'(X1), X2)
active'(afterNth'(X1, X2)) → afterNth'(X1, active'(X2))
active'(U181'(X1, X2)) → U181'(active'(X1), X2)
active'(U191'(X1, X2)) → U191'(active'(X1), X2)
active'(pair'(X1, X2)) → pair'(active'(X1), X2)
active'(pair'(X1, X2)) → pair'(X1, active'(X2))
active'(U201'(X1, X2, X3, X4)) → U201'(active'(X1), X2, X3, X4)
active'(U202'(X1, X2)) → U202'(active'(X1), X2)
active'(U21'(X1, X2)) → U21'(active'(X1), X2)
active'(U211'(X1, X2)) → U211'(active'(X1), X2)
active'(U221'(X1, X2, X3)) → U221'(active'(X1), X2, X3)
active'(fst'(X)) → fst'(active'(X))
active'(U31'(X1, X2)) → U31'(active'(X1), X2)
active'(U41'(X1, X2, X3)) → U41'(active'(X1), X2, X3)
active'(U42'(X1, X2)) → U42'(active'(X1), X2)
active'(U43'(X)) → U43'(active'(X))
active'(U51'(X1, X2, X3)) → U51'(active'(X1), X2, X3)
active'(U52'(X1, X2)) → U52'(active'(X1), X2)
active'(U53'(X)) → U53'(active'(X))
active'(U61'(X1, X2)) → U61'(active'(X1), X2)
active'(U62'(X)) → U62'(active'(X))
active'(U71'(X1, X2)) → U71'(active'(X1), X2)
active'(U72'(X)) → U72'(active'(X))
active'(U81'(X1, X2)) → U81'(active'(X1), X2)
active'(U82'(X)) → U82'(active'(X))
active'(U91'(X1, X2)) → U91'(active'(X1), X2)
active'(U92'(X)) → U92'(active'(X))
active'(and'(X1, X2)) → and'(active'(X1), X2)
active'(tail'(X)) → tail'(active'(X))
active'(take'(X1, X2)) → take'(active'(X1), X2)
active'(take'(X1, X2)) → take'(X1, active'(X2))
active'(sel'(X1, X2)) → sel'(active'(X1), X2)
active'(sel'(X1, X2)) → sel'(X1, active'(X2))
U101'(mark'(X1), X2, X3) → mark'(U101'(X1, X2, X3))
U102'(mark'(X1), X2) → mark'(U102'(X1, X2))
U103'(mark'(X)) → mark'(U103'(X))
U11'(mark'(X1), X2, X3) → mark'(U11'(X1, X2, X3))
snd'(mark'(X)) → mark'(snd'(X))
splitAt'(mark'(X1), X2) → mark'(splitAt'(X1, X2))
splitAt'(X1, mark'(X2)) → mark'(splitAt'(X1, X2))
U111'(mark'(X1), X2) → mark'(U111'(X1, X2))
U112'(mark'(X)) → mark'(U112'(X))
U121'(mark'(X1), X2) → mark'(U121'(X1, X2))
U122'(mark'(X)) → mark'(U122'(X))
U131'(mark'(X1), X2, X3) → mark'(U131'(X1, X2, X3))
U132'(mark'(X1), X2) → mark'(U132'(X1, X2))
U133'(mark'(X)) → mark'(U133'(X))
U141'(mark'(X1), X2, X3) → mark'(U141'(X1, X2, X3))
U142'(mark'(X1), X2) → mark'(U142'(X1, X2))
U143'(mark'(X)) → mark'(U143'(X))
U151'(mark'(X1), X2, X3) → mark'(U151'(X1, X2, X3))
U152'(mark'(X1), X2) → mark'(U152'(X1, X2))
U153'(mark'(X)) → mark'(U153'(X))
U161'(mark'(X1), X2) → mark'(U161'(X1, X2))
cons'(mark'(X1), X2) → mark'(cons'(X1, X2))
natsFrom'(mark'(X)) → mark'(natsFrom'(X))
s'(mark'(X)) → mark'(s'(X))
U171'(mark'(X1), X2, X3) → mark'(U171'(X1, X2, X3))
head'(mark'(X)) → mark'(head'(X))
afterNth'(mark'(X1), X2) → mark'(afterNth'(X1, X2))
afterNth'(X1, mark'(X2)) → mark'(afterNth'(X1, X2))
U181'(mark'(X1), X2) → mark'(U181'(X1, X2))
U191'(mark'(X1), X2) → mark'(U191'(X1, X2))
pair'(mark'(X1), X2) → mark'(pair'(X1, X2))
pair'(X1, mark'(X2)) → mark'(pair'(X1, X2))
U201'(mark'(X1), X2, X3, X4) → mark'(U201'(X1, X2, X3, X4))
U202'(mark'(X1), X2) → mark'(U202'(X1, X2))
U21'(mark'(X1), X2) → mark'(U21'(X1, X2))
U211'(mark'(X1), X2) → mark'(U211'(X1, X2))
U221'(mark'(X1), X2, X3) → mark'(U221'(X1, X2, X3))
fst'(mark'(X)) → mark'(fst'(X))
U31'(mark'(X1), X2) → mark'(U31'(X1, X2))
U41'(mark'(X1), X2, X3) → mark'(U41'(X1, X2, X3))
U42'(mark'(X1), X2) → mark'(U42'(X1, X2))
U43'(mark'(X)) → mark'(U43'(X))
U51'(mark'(X1), X2, X3) → mark'(U51'(X1, X2, X3))
U52'(mark'(X1), X2) → mark'(U52'(X1, X2))
U53'(mark'(X)) → mark'(U53'(X))
U61'(mark'(X1), X2) → mark'(U61'(X1, X2))
U62'(mark'(X)) → mark'(U62'(X))
U71'(mark'(X1), X2) → mark'(U71'(X1, X2))
U72'(mark'(X)) → mark'(U72'(X))
U81'(mark'(X1), X2) → mark'(U81'(X1, X2))
U82'(mark'(X)) → mark'(U82'(X))
U91'(mark'(X1), X2) → mark'(U91'(X1, X2))
U92'(mark'(X)) → mark'(U92'(X))
and'(mark'(X1), X2) → mark'(and'(X1, X2))
tail'(mark'(X)) → mark'(tail'(X))
take'(mark'(X1), X2) → mark'(take'(X1, X2))
take'(X1, mark'(X2)) → mark'(take'(X1, X2))
sel'(mark'(X1), X2) → mark'(sel'(X1, X2))
sel'(X1, mark'(X2)) → mark'(sel'(X1, X2))
proper'(U101'(X1, X2, X3)) → U101'(proper'(X1), proper'(X2), proper'(X3))
proper'(tt') → ok'(tt')
proper'(U102'(X1, X2)) → U102'(proper'(X1), proper'(X2))
proper'(isNatural'(X)) → isNatural'(proper'(X))
proper'(U103'(X)) → U103'(proper'(X))
proper'(isLNat'(X)) → isLNat'(proper'(X))
proper'(U11'(X1, X2, X3)) → U11'(proper'(X1), proper'(X2), proper'(X3))
proper'(snd'(X)) → snd'(proper'(X))
proper'(splitAt'(X1, X2)) → splitAt'(proper'(X1), proper'(X2))
proper'(U111'(X1, X2)) → U111'(proper'(X1), proper'(X2))
proper'(U112'(X)) → U112'(proper'(X))
proper'(U121'(X1, X2)) → U121'(proper'(X1), proper'(X2))
proper'(U122'(X)) → U122'(proper'(X))
proper'(U131'(X1, X2, X3)) → U131'(proper'(X1), proper'(X2), proper'(X3))
proper'(U132'(X1, X2)) → U132'(proper'(X1), proper'(X2))
proper'(U133'(X)) → U133'(proper'(X))
proper'(U141'(X1, X2, X3)) → U141'(proper'(X1), proper'(X2), proper'(X3))
proper'(U142'(X1, X2)) → U142'(proper'(X1), proper'(X2))
proper'(U143'(X)) → U143'(proper'(X))
proper'(U151'(X1, X2, X3)) → U151'(proper'(X1), proper'(X2), proper'(X3))
proper'(U152'(X1, X2)) → U152'(proper'(X1), proper'(X2))
proper'(U153'(X)) → U153'(proper'(X))
proper'(U161'(X1, X2)) → U161'(proper'(X1), proper'(X2))
proper'(cons'(X1, X2)) → cons'(proper'(X1), proper'(X2))
proper'(natsFrom'(X)) → natsFrom'(proper'(X))
proper'(s'(X)) → s'(proper'(X))
proper'(U171'(X1, X2, X3)) → U171'(proper'(X1), proper'(X2), proper'(X3))
proper'(head'(X)) → head'(proper'(X))
proper'(afterNth'(X1, X2)) → afterNth'(proper'(X1), proper'(X2))
proper'(U181'(X1, X2)) → U181'(proper'(X1), proper'(X2))
proper'(U191'(X1, X2)) → U191'(proper'(X1), proper'(X2))
proper'(pair'(X1, X2)) → pair'(proper'(X1), proper'(X2))
proper'(nil') → ok'(nil')
proper'(U201'(X1, X2, X3, X4)) → U201'(proper'(X1), proper'(X2), proper'(X3), proper'(X4))
proper'(U202'(X1, X2)) → U202'(proper'(X1), proper'(X2))
proper'(U21'(X1, X2)) → U21'(proper'(X1), proper'(X2))
proper'(U211'(X1, X2)) → U211'(proper'(X1), proper'(X2))
proper'(U221'(X1, X2, X3)) → U221'(proper'(X1), proper'(X2), proper'(X3))
proper'(fst'(X)) → fst'(proper'(X))
proper'(U31'(X1, X2)) → U31'(proper'(X1), proper'(X2))
proper'(U41'(X1, X2, X3)) → U41'(proper'(X1), proper'(X2), proper'(X3))
proper'(U42'(X1, X2)) → U42'(proper'(X1), proper'(X2))
proper'(U43'(X)) → U43'(proper'(X))
proper'(U51'(X1, X2, X3)) → U51'(proper'(X1), proper'(X2), proper'(X3))
proper'(U52'(X1, X2)) → U52'(proper'(X1), proper'(X2))
proper'(U53'(X)) → U53'(proper'(X))
proper'(U61'(X1, X2)) → U61'(proper'(X1), proper'(X2))
proper'(U62'(X)) → U62'(proper'(X))
proper'(isPLNat'(X)) → isPLNat'(proper'(X))
proper'(U71'(X1, X2)) → U71'(proper'(X1), proper'(X2))
proper'(U72'(X)) → U72'(proper'(X))
proper'(U81'(X1, X2)) → U81'(proper'(X1), proper'(X2))
proper'(U82'(X)) → U82'(proper'(X))
proper'(U91'(X1, X2)) → U91'(proper'(X1), proper'(X2))
proper'(U92'(X)) → U92'(proper'(X))
proper'(and'(X1, X2)) → and'(proper'(X1), proper'(X2))
proper'(isNaturalKind'(X)) → isNaturalKind'(proper'(X))
proper'(isLNatKind'(X)) → isLNatKind'(proper'(X))
proper'(isPLNatKind'(X)) → isPLNatKind'(proper'(X))
proper'(tail'(X)) → tail'(proper'(X))
proper'(take'(X1, X2)) → take'(proper'(X1), proper'(X2))
proper'(0') → ok'(0')
proper'(sel'(X1, X2)) → sel'(proper'(X1), proper'(X2))
U101'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U101'(X1, X2, X3))
U102'(ok'(X1), ok'(X2)) → ok'(U102'(X1, X2))
isNatural'(ok'(X)) → ok'(isNatural'(X))
U103'(ok'(X)) → ok'(U103'(X))
isLNat'(ok'(X)) → ok'(isLNat'(X))
U11'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U11'(X1, X2, X3))
snd'(ok'(X)) → ok'(snd'(X))
splitAt'(ok'(X1), ok'(X2)) → ok'(splitAt'(X1, X2))
U111'(ok'(X1), ok'(X2)) → ok'(U111'(X1, X2))
U112'(ok'(X)) → ok'(U112'(X))
U121'(ok'(X1), ok'(X2)) → ok'(U121'(X1, X2))
U122'(ok'(X)) → ok'(U122'(X))
U131'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U131'(X1, X2, X3))
U132'(ok'(X1), ok'(X2)) → ok'(U132'(X1, X2))
U133'(ok'(X)) → ok'(U133'(X))
U141'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U141'(X1, X2, X3))
U142'(ok'(X1), ok'(X2)) → ok'(U142'(X1, X2))
U143'(ok'(X)) → ok'(U143'(X))
U151'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U151'(X1, X2, X3))
U152'(ok'(X1), ok'(X2)) → ok'(U152'(X1, X2))
U153'(ok'(X)) → ok'(U153'(X))
U161'(ok'(X1), ok'(X2)) → ok'(U161'(X1, X2))
cons'(ok'(X1), ok'(X2)) → ok'(cons'(X1, X2))
natsFrom'(ok'(X)) → ok'(natsFrom'(X))
s'(ok'(X)) → ok'(s'(X))
U171'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U171'(X1, X2, X3))
head'(ok'(X)) → ok'(head'(X))
afterNth'(ok'(X1), ok'(X2)) → ok'(afterNth'(X1, X2))
U181'(ok'(X1), ok'(X2)) → ok'(U181'(X1, X2))
U191'(ok'(X1), ok'(X2)) → ok'(U191'(X1, X2))
pair'(ok'(X1), ok'(X2)) → ok'(pair'(X1, X2))
U201'(ok'(X1), ok'(X2), ok'(X3), ok'(X4)) → ok'(U201'(X1, X2, X3, X4))
U202'(ok'(X1), ok'(X2)) → ok'(U202'(X1, X2))
U21'(ok'(X1), ok'(X2)) → ok'(U21'(X1, X2))
U211'(ok'(X1), ok'(X2)) → ok'(U211'(X1, X2))
U221'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U221'(X1, X2, X3))
fst'(ok'(X)) → ok'(fst'(X))
U31'(ok'(X1), ok'(X2)) → ok'(U31'(X1, X2))
U41'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U41'(X1, X2, X3))
U42'(ok'(X1), ok'(X2)) → ok'(U42'(X1, X2))
U43'(ok'(X)) → ok'(U43'(X))
U51'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U51'(X1, X2, X3))
U52'(ok'(X1), ok'(X2)) → ok'(U52'(X1, X2))
U53'(ok'(X)) → ok'(U53'(X))
U61'(ok'(X1), ok'(X2)) → ok'(U61'(X1, X2))
U62'(ok'(X)) → ok'(U62'(X))
isPLNat'(ok'(X)) → ok'(isPLNat'(X))
U71'(ok'(X1), ok'(X2)) → ok'(U71'(X1, X2))
U72'(ok'(X)) → ok'(U72'(X))
U81'(ok'(X1), ok'(X2)) → ok'(U81'(X1, X2))
U82'(ok'(X)) → ok'(U82'(X))
U91'(ok'(X1), ok'(X2)) → ok'(U91'(X1, X2))
U92'(ok'(X)) → ok'(U92'(X))
and'(ok'(X1), ok'(X2)) → ok'(and'(X1, X2))
isNaturalKind'(ok'(X)) → ok'(isNaturalKind'(X))
isLNatKind'(ok'(X)) → ok'(isLNatKind'(X))
isPLNatKind'(ok'(X)) → ok'(isPLNatKind'(X))
tail'(ok'(X)) → ok'(tail'(X))
take'(ok'(X1), ok'(X2)) → ok'(take'(X1, X2))
sel'(ok'(X1), ok'(X2)) → ok'(sel'(X1, X2))
top'(mark'(X)) → top'(proper'(X))
top'(ok'(X)) → top'(active'(X))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
active'(U101'(tt', V1, V2)) → mark'(U102'(isNatural'(V1), V2))
active'(U102'(tt', V2)) → mark'(U103'(isLNat'(V2)))
active'(U103'(tt')) → mark'(tt')
active'(U11'(tt', N, XS)) → mark'(snd'(splitAt'(N, XS)))
active'(U111'(tt', V1)) → mark'(U112'(isLNat'(V1)))
active'(U112'(tt')) → mark'(tt')
active'(U121'(tt', V1)) → mark'(U122'(isNatural'(V1)))
active'(U122'(tt')) → mark'(tt')
active'(U131'(tt', V1, V2)) → mark'(U132'(isNatural'(V1), V2))
active'(U132'(tt', V2)) → mark'(U133'(isLNat'(V2)))
active'(U133'(tt')) → mark'(tt')
active'(U141'(tt', V1, V2)) → mark'(U142'(isLNat'(V1), V2))
active'(U142'(tt', V2)) → mark'(U143'(isLNat'(V2)))
active'(U143'(tt')) → mark'(tt')
active'(U151'(tt', V1, V2)) → mark'(U152'(isNatural'(V1), V2))
active'(U152'(tt', V2)) → mark'(U153'(isLNat'(V2)))
active'(U153'(tt')) → mark'(tt')
active'(U161'(tt', N)) → mark'(cons'(N, natsFrom'(s'(N))))
active'(U171'(tt', N, XS)) → mark'(head'(afterNth'(N, XS)))
active'(U181'(tt', Y)) → mark'(Y)
active'(U191'(tt', XS)) → mark'(pair'(nil', XS))
active'(U201'(tt', N, X, XS)) → mark'(U202'(splitAt'(N, XS), X))
active'(U202'(pair'(YS, ZS), X)) → mark'(pair'(cons'(X, YS), ZS))
active'(U21'(tt', X)) → mark'(X)
active'(U211'(tt', XS)) → mark'(XS)
active'(U221'(tt', N, XS)) → mark'(fst'(splitAt'(N, XS)))
active'(U31'(tt', N)) → mark'(N)
active'(U41'(tt', V1, V2)) → mark'(U42'(isNatural'(V1), V2))
active'(U42'(tt', V2)) → mark'(U43'(isLNat'(V2)))
active'(U43'(tt')) → mark'(tt')
active'(U51'(tt', V1, V2)) → mark'(U52'(isNatural'(V1), V2))
active'(U52'(tt', V2)) → mark'(U53'(isLNat'(V2)))
active'(U53'(tt')) → mark'(tt')
active'(U61'(tt', V1)) → mark'(U62'(isPLNat'(V1)))
active'(U62'(tt')) → mark'(tt')
active'(U71'(tt', V1)) → mark'(U72'(isNatural'(V1)))
active'(U72'(tt')) → mark'(tt')
active'(U81'(tt', V1)) → mark'(U82'(isPLNat'(V1)))
active'(U82'(tt')) → mark'(tt')
active'(U91'(tt', V1)) → mark'(U92'(isLNat'(V1)))
active'(U92'(tt')) → mark'(tt')
active'(afterNth'(N, XS)) → mark'(U11'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(isLNat'(XS), isLNatKind'(XS))), N, XS))
active'(and'(tt', X)) → mark'(X)
active'(fst'(pair'(X, Y))) → mark'(U21'(and'(and'(isLNat'(X), isLNatKind'(X)), and'(isLNat'(Y), isLNatKind'(Y))), X))
active'(head'(cons'(N, XS))) → mark'(U31'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(isLNat'(XS), isLNatKind'(XS))), N))
active'(isLNat'(nil')) → mark'(tt')
active'(isLNat'(afterNth'(V1, V2))) → mark'(U41'(and'(isNaturalKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isLNat'(cons'(V1, V2))) → mark'(U51'(and'(isNaturalKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isLNat'(fst'(V1))) → mark'(U61'(isPLNatKind'(V1), V1))
active'(isLNat'(natsFrom'(V1))) → mark'(U71'(isNaturalKind'(V1), V1))
active'(isLNat'(snd'(V1))) → mark'(U81'(isPLNatKind'(V1), V1))
active'(isLNat'(tail'(V1))) → mark'(U91'(isLNatKind'(V1), V1))
active'(isLNat'(take'(V1, V2))) → mark'(U101'(and'(isNaturalKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isLNatKind'(nil')) → mark'(tt')
active'(isLNatKind'(afterNth'(V1, V2))) → mark'(and'(isNaturalKind'(V1), isLNatKind'(V2)))
active'(isLNatKind'(cons'(V1, V2))) → mark'(and'(isNaturalKind'(V1), isLNatKind'(V2)))
active'(isLNatKind'(fst'(V1))) → mark'(isPLNatKind'(V1))
active'(isLNatKind'(natsFrom'(V1))) → mark'(isNaturalKind'(V1))
active'(isLNatKind'(snd'(V1))) → mark'(isPLNatKind'(V1))
active'(isLNatKind'(tail'(V1))) → mark'(isLNatKind'(V1))
active'(isLNatKind'(take'(V1, V2))) → mark'(and'(isNaturalKind'(V1), isLNatKind'(V2)))
active'(isNatural'(0')) → mark'(tt')
active'(isNatural'(head'(V1))) → mark'(U111'(isLNatKind'(V1), V1))
active'(isNatural'(s'(V1))) → mark'(U121'(isNaturalKind'(V1), V1))
active'(isNatural'(sel'(V1, V2))) → mark'(U131'(and'(isNaturalKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isNaturalKind'(0')) → mark'(tt')
active'(isNaturalKind'(head'(V1))) → mark'(isLNatKind'(V1))
active'(isNaturalKind'(s'(V1))) → mark'(isNaturalKind'(V1))
active'(isNaturalKind'(sel'(V1, V2))) → mark'(and'(isNaturalKind'(V1), isLNatKind'(V2)))
active'(isPLNat'(pair'(V1, V2))) → mark'(U141'(and'(isLNatKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isPLNat'(splitAt'(V1, V2))) → mark'(U151'(and'(isNaturalKind'(V1), isLNatKind'(V2)), V1, V2))
active'(isPLNatKind'(pair'(V1, V2))) → mark'(and'(isLNatKind'(V1), isLNatKind'(V2)))
active'(isPLNatKind'(splitAt'(V1, V2))) → mark'(and'(isNaturalKind'(V1), isLNatKind'(V2)))
active'(natsFrom'(N)) → mark'(U161'(and'(isNatural'(N), isNaturalKind'(N)), N))
active'(sel'(N, XS)) → mark'(U171'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(isLNat'(XS), isLNatKind'(XS))), N, XS))
active'(snd'(pair'(X, Y))) → mark'(U181'(and'(and'(isLNat'(X), isLNatKind'(X)), and'(isLNat'(Y), isLNatKind'(Y))), Y))
active'(splitAt'(0', XS)) → mark'(U191'(and'(isLNat'(XS), isLNatKind'(XS)), XS))
active'(splitAt'(s'(N), cons'(X, XS))) → mark'(U201'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(and'(isNatural'(X), isNaturalKind'(X)), and'(isLNat'(XS), isLNatKind'(XS)))), N, X, XS))
active'(tail'(cons'(N, XS))) → mark'(U211'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(isLNat'(XS), isLNatKind'(XS))), XS))
active'(take'(N, XS)) → mark'(U221'(and'(and'(isNatural'(N), isNaturalKind'(N)), and'(isLNat'(XS), isLNatKind'(XS))), N, XS))
active'(U101'(X1, X2, X3)) → U101'(active'(X1), X2, X3)
active'(U102'(X1, X2)) → U102'(active'(X1), X2)
active'(U103'(X)) → U103'(active'(X))
active'(U11'(X1, X2, X3)) → U11'(active'(X1), X2, X3)
active'(snd'(X)) → snd'(active'(X))
active'(splitAt'(X1, X2)) → splitAt'(active'(X1), X2)
active'(splitAt'(X1, X2)) → splitAt'(X1, active'(X2))
active'(U111'(X1, X2)) → U111'(active'(X1), X2)
active'(U112'(X)) → U112'(active'(X))
active'(U121'(X1, X2)) → U121'(active'(X1), X2)
active'(U122'(X)) → U122'(active'(X))
active'(U131'(X1, X2, X3)) → U131'(active'(X1), X2, X3)
active'(U132'(X1, X2)) → U132'(active'(X1), X2)
active'(U133'(X)) → U133'(active'(X))
active'(U141'(X1, X2, X3)) → U141'(active'(X1), X2, X3)
active'(U142'(X1, X2)) → U142'(active'(X1), X2)
active'(U143'(X)) → U143'(active'(X))
active'(U151'(X1, X2, X3)) → U151'(active'(X1), X2, X3)
active'(U152'(X1, X2)) → U152'(active'(X1), X2)
active'(U153'(X)) → U153'(active'(X))
active'(U161'(X1, X2)) → U161'(active'(X1), X2)
active'(cons'(X1, X2)) → cons'(active'(X1), X2)
active'(natsFrom'(X)) → natsFrom'(active'(X))
active'(s'(X)) → s'(active'(X))
active'(U171'(X1, X2, X3)) → U171'(active'(X1), X2, X3)
active'(head'(X)) → head'(active'(X))
active'(afterNth'(X1, X2)) → afterNth'(active'(X1), X2)
active'(afterNth'(X1, X2)) → afterNth'(X1, active'(X2))
active'(U181'(X1, X2)) → U181'(active'(X1), X2)
active'(U191'(X1, X2)) → U191'(active'(X1), X2)
active'(pair'(X1, X2)) → pair'(active'(X1), X2)
active'(pair'(X1, X2)) → pair'(X1, active'(X2))
active'(U201'(X1, X2, X3, X4)) → U201'(active'(X1), X2, X3, X4)
active'(U202'(X1, X2)) → U202'(active'(X1), X2)
active'(U21'(X1, X2)) → U21'(active'(X1), X2)
active'(U211'(X1, X2)) → U211'(active'(X1), X2)
active'(U221'(X1, X2, X3)) → U221'(active'(X1), X2, X3)
active'(fst'(X)) → fst'(active'(X))
active'(U31'(X1, X2)) → U31'(active'(X1), X2)
active'(U41'(X1, X2, X3)) → U41'(active'(X1), X2, X3)
active'(U42'(X1, X2)) → U42'(active'(X1), X2)
active'(U43'(X)) → U43'(active'(X))
active'(U51'(X1, X2, X3)) → U51'(active'(X1), X2, X3)
active'(U52'(X1, X2)) → U52'(active'(X1), X2)
active'(U53'(X)) → U53'(active'(X))
active'(U61'(X1, X2)) → U61'(active'(X1), X2)
active'(U62'(X)) → U62'(active'(X))
active'(U71'(X1, X2)) → U71'(active'(X1), X2)
active'(U72'(X)) → U72'(active'(X))
active'(U81'(X1, X2)) → U81'(active'(X1), X2)
active'(U82'(X)) → U82'(active'(X))
active'(U91'(X1, X2)) → U91'(active'(X1), X2)
active'(U92'(X)) → U92'(active'(X))
active'(and'(X1, X2)) → and'(active'(X1), X2)
active'(tail'(X)) → tail'(active'(X))
active'(take'(X1, X2)) → take'(active'(X1), X2)
active'(take'(X1, X2)) → take'(X1, active'(X2))
active'(sel'(X1, X2)) → sel'(active'(X1), X2)
active'(sel'(X1, X2)) → sel'(X1, active'(X2))
U101'(mark'(X1), X2, X3) → mark'(U101'(X1, X2, X3))
U102'(mark'(X1), X2) → mark'(U102'(X1, X2))
U103'(mark'(X)) → mark'(U103'(X))
U11'(mark'(X1), X2, X3) → mark'(U11'(X1, X2, X3))
snd'(mark'(X)) → mark'(snd'(X))
splitAt'(mark'(X1), X2) → mark'(splitAt'(X1, X2))
splitAt'(X1, mark'(X2)) → mark'(splitAt'(X1, X2))
U111'(mark'(X1), X2) → mark'(U111'(X1, X2))
U112'(mark'(X)) → mark'(U112'(X))
U121'(mark'(X1), X2) → mark'(U121'(X1, X2))
U122'(mark'(X)) → mark'(U122'(X))
U131'(mark'(X1), X2, X3) → mark'(U131'(X1, X2, X3))
U132'(mark'(X1), X2) → mark'(U132'(X1, X2))
U133'(mark'(X)) → mark'(U133'(X))
U141'(mark'(X1), X2, X3) → mark'(U141'(X1, X2, X3))
U142'(mark'(X1), X2) → mark'(U142'(X1, X2))
U143'(mark'(X)) → mark'(U143'(X))
U151'(mark'(X1), X2, X3) → mark'(U151'(X1, X2, X3))
U152'(mark'(X1), X2) → mark'(U152'(X1, X2))
U153'(mark'(X)) → mark'(U153'(X))
U161'(mark'(X1), X2) → mark'(U161'(X1, X2))
cons'(mark'(X1), X2) → mark'(cons'(X1, X2))
natsFrom'(mark'(X)) → mark'(natsFrom'(X))
s'(mark'(X)) → mark'(s'(X))
U171'(mark'(X1), X2, X3) → mark'(U171'(X1, X2, X3))
head'(mark'(X)) → mark'(head'(X))
afterNth'(mark'(X1), X2) → mark'(afterNth'(X1, X2))
afterNth'(X1, mark'(X2)) → mark'(afterNth'(X1, X2))
U181'(mark'(X1), X2) → mark'(U181'(X1, X2))
U191'(mark'(X1), X2) → mark'(U191'(X1, X2))
pair'(mark'(X1), X2) → mark'(pair'(X1, X2))
pair'(X1, mark'(X2)) → mark'(pair'(X1, X2))
U201'(mark'(X1), X2, X3, X4) → mark'(U201'(X1, X2, X3, X4))
U202'(mark'(X1), X2) → mark'(U202'(X1, X2))
U21'(mark'(X1), X2) → mark'(U21'(X1, X2))
U211'(mark'(X1), X2) → mark'(U211'(X1, X2))
U221'(mark'(X1), X2, X3) → mark'(U221'(X1, X2, X3))
fst'(mark'(X)) → mark'(fst'(X))
U31'(mark'(X1), X2) → mark'(U31'(X1, X2))
U41'(mark'(X1), X2, X3) → mark'(U41'(X1, X2, X3))
U42'(mark'(X1), X2) → mark'(U42'(X1, X2))
U43'(mark'(X)) → mark'(U43'(X))
U51'(mark'(X1), X2, X3) → mark'(U51'(X1, X2, X3))
U52'(mark'(X1), X2) → mark'(U52'(X1, X2))
U53'(mark'(X)) → mark'(U53'(X))
U61'(mark'(X1), X2) → mark'(U61'(X1, X2))
U62'(mark'(X)) → mark'(U62'(X))
U71'(mark'(X1), X2) → mark'(U71'(X1, X2))
U72'(mark'(X)) → mark'(U72'(X))
U81'(mark'(X1), X2) → mark'(U81'(X1, X2))
U82'(mark'(X)) → mark'(U82'(X))
U91'(mark'(X1), X2) → mark'(U91'(X1, X2))
U92'(mark'(X)) → mark'(U92'(X))
and'(mark'(X1), X2) → mark'(and'(X1, X2))
tail'(mark'(X)) → mark'(tail'(X))
take'(mark'(X1), X2) → mark'(take'(X1, X2))
take'(X1, mark'(X2)) → mark'(take'(X1, X2))
sel'(mark'(X1), X2) → mark'(sel'(X1, X2))
sel'(X1, mark'(X2)) → mark'(sel'(X1, X2))
proper'(U101'(X1, X2, X3)) → U101'(proper'(X1), proper'(X2), proper'(X3))
proper'(tt') → ok'(tt')
proper'(U102'(X1, X2)) → U102'(proper'(X1), proper'(X2))
proper'(isNatural'(X)) → isNatural'(proper'(X))
proper'(U103'(X)) → U103'(proper'(X))
proper'(isLNat'(X)) → isLNat'(proper'(X))
proper'(U11'(X1, X2, X3)) → U11'(proper'(X1), proper'(X2), proper'(X3))
proper'(snd'(X)) → snd'(proper'(X))
proper'(splitAt'(X1, X2)) → splitAt'(proper'(X1), proper'(X2))
proper'(U111'(X1, X2)) → U111'(proper'(X1), proper'(X2))
proper'(U112'(X)) → U112'(proper'(X))
proper'(U121'(X1, X2)) → U121'(proper'(X1), proper'(X2))
proper'(U122'(X)) → U122'(proper'(X))
proper'(U131'(X1, X2, X3)) → U131'(proper'(X1), proper'(X2), proper'(X3))
proper'(U132'(X1, X2)) → U132'(proper'(X1), proper'(X2))
proper'(U133'(X)) → U133'(proper'(X))
proper'(U141'(X1, X2, X3)) → U141'(proper'(X1), proper'(X2), proper'(X3))
proper'(U142'(X1, X2)) → U142'(proper'(X1), proper'(X2))
proper'(U143'(X)) → U143'(proper'(X))
proper'(U151'(X1, X2, X3)) → U151'(proper'(X1), proper'(X2), proper'(X3))
proper'(U152'(X1, X2)) → U152'(proper'(X1), proper'(X2))
proper'(U153'(X)) → U153'(proper'(X))
proper'(U161'(X1, X2)) → U161'(proper'(X1), proper'(X2))
proper'(cons'(X1, X2)) → cons'(proper'(X1), proper'(X2))
proper'(natsFrom'(X)) → natsFrom'(proper'(X))
proper'(s'(X)) → s'(proper'(X))
proper'(U171'(X1, X2, X3)) → U171'(proper'(X1), proper'(X2), proper'(X3))
proper'(head'(X)) → head'(proper'(X))
proper'(afterNth'(X1, X2)) → afterNth'(proper'(X1), proper'(X2))
proper'(U181'(X1, X2)) → U181'(proper'(X1), proper'(X2))
proper'(U191'(X1, X2)) → U191'(proper'(X1), proper'(X2))
proper'(pair'(X1, X2)) → pair'(proper'(X1), proper'(X2))
proper'(nil') → ok'(nil')
proper'(U201'(X1, X2, X3, X4)) → U201'(proper'(X1), proper'(X2), proper'(X3), proper'(X4))
proper'(U202'(X1, X2)) → U202'(proper'(X1), proper'(X2))
proper'(U21'(X1, X2)) → U21'(proper'(X1), proper'(X2))
proper'(U211'(X1, X2)) → U211'(proper'(X1), proper'(X2))
proper'(U221'(X1, X2, X3)) → U221'(proper'(X1), proper'(X2), proper'(X3))
proper'(fst'(X)) → fst'(proper'(X))
proper'(U31'(X1, X2)) → U31'(proper'(X1), proper'(X2))
proper'(U41'(X1, X2, X3)) → U41'(proper'(X1), proper'(X2), proper'(X3))
proper'(U42'(X1, X2)) → U42'(proper'(X1), proper'(X2))
proper'(U43'(X)) → U43'(proper'(X))
proper'(U51'(X1, X2, X3)) → U51'(proper'(X1), proper'(X2), proper'(X3))
proper'(U52'(X1, X2)) → U52'(proper'(X1), proper'(X2))
proper'(U53'(X)) → U53'(proper'(X))
proper'(U61'(X1, X2)) → U61'(proper'(X1), proper'(X2))
proper'(U62'(X)) → U62'(proper'(X))
proper'(isPLNat'(X)) → isPLNat'(proper'(X))
proper'(U71'(X1, X2)) → U71'(proper'(X1), proper'(X2))
proper'(U72'(X)) → U72'(proper'(X))
proper'(U81'(X1, X2)) → U81'(proper'(X1), proper'(X2))
proper'(U82'(X)) → U82'(proper'(X))
proper'(U91'(X1, X2)) → U91'(proper'(X1), proper'(X2))
proper'(U92'(X)) → U92'(proper'(X))
proper'(and'(X1, X2)) → and'(proper'(X1), proper'(X2))
proper'(isNaturalKind'(X)) → isNaturalKind'(proper'(X))
proper'(isLNatKind'(X)) → isLNatKind'(proper'(X))
proper'(isPLNatKind'(X)) → isPLNatKind'(proper'(X))
proper'(tail'(X)) → tail'(proper'(X))
proper'(take'(X1, X2)) → take'(proper'(X1), proper'(X2))
proper'(0') → ok'(0')
proper'(sel'(X1, X2)) → sel'(proper'(X1), proper'(X2))
U101'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U101'(X1, X2, X3))
U102'(ok'(X1), ok'(X2)) → ok'(U102'(X1, X2))
isNatural'(ok'(X)) → ok'(isNatural'(X))
U103'(ok'(X)) → ok'(U103'(X))
isLNat'(ok'(X)) → ok'(isLNat'(X))
U11'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U11'(X1, X2, X3))
snd'(ok'(X)) → ok'(snd'(X))
splitAt'(ok'(X1), ok'(X2)) → ok'(splitAt'(X1, X2))
U111'(ok'(X1), ok'(X2)) → ok'(U111'(X1, X2))
U112'(ok'(X)) → ok'(U112'(X))
U121'(ok'(X1), ok'(X2)) → ok'(U121'(X1, X2))
U122'(ok'(X)) → ok'(U122'(X))
U131'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U131'(X1, X2, X3))
U132'(ok'(X1), ok'(X2)) → ok'(U132'(X1, X2))
U133'(ok'(X)) → ok'(U133'(X))
U141'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U141'(X1, X2, X3))
U142'(ok'(X1), ok'(X2)) → ok'(U142'(X1, X2))
U143'(ok'(X)) → ok'(U143'(X))
U151'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U151'(X1, X2, X3))
U152'(ok'(X1), ok'(X2)) → ok'(U152'(X1, X2))
U153'(ok'(X)) → ok'(U153'(X))
U161'(ok'(X1), ok'(X2)) → ok'(U161'(X1, X2))
cons'(ok'(X1), ok'(X2)) → ok'(cons'(X1, X2))
natsFrom'(ok'(X)) → ok'(natsFrom'(X))
s'(ok'(X)) → ok'(s'(X))
U171'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U171'(X1, X2, X3))
head'(ok'(X)) → ok'(head'(X))
afterNth'(ok'(X1), ok'(X2)) → ok'(afterNth'(X1, X2))
U181'(ok'(X1), ok'(X2)) → ok'(U181'(X1, X2))
U191'(ok'(X1), ok'(X2)) → ok'(U191'(X1, X2))
pair'(ok'(X1), ok'(X2)) → ok'(pair'(X1, X2))
U201'(ok'(X1), ok'(X2), ok'(X3), ok'(X4)) → ok'(U201'(X1, X2, X3, X4))
U202'(ok'(X1), ok'(X2)) → ok'(U202'(X1, X2))
U21'(ok'(X1), ok'(X2)) → ok'(U21'(X1, X2))
U211'(ok'(X1), ok'(X2)) → ok'(U211'(X1, X2))
U221'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U221'(X1, X2, X3))
fst'(ok'(X)) → ok'(fst'(X))
U31'(ok'(X1), ok'(X2)) → ok'(U31'(X1, X2))
U41'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U41'(X1, X2, X3))
U42'(ok'(X1), ok'(X2)) → ok'(U42'(X1, X2))
U43'(ok'(X)) → ok'(U43'(X))
U51'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U51'(X1, X2, X3))
U52'(ok'(X1), ok'(X2)) → ok'(U52'(X1, X2))
U53'(ok'(X)) → ok'(U53'(X))
U61'(ok'(X1), ok'(X2)) → ok'(U61'(X1, X2))
U62'(ok'(X)) → ok'(U62'(X))
isPLNat'(ok'(X)) → ok'(isPLNat'(X))
U71'(ok'(X1), ok'(X2)) → ok'(U71'(X1, X2))
U72'(ok'(X)) → ok'(U72'(X))
U81'(ok'(X1), ok'(X2)) → ok'(U81'(X1, X2))
U82'(ok'(X)) → ok'(U82'(X))
U91'(ok'(X1), ok'(X2)) → ok'(U91'(X1, X2))
U92'(ok'(X)) → ok'(U92'(X))
and'(ok'(X1), ok'(X2)) → ok'(and'(X1, X2))
isNaturalKind'(ok'(X)) → ok'(isNaturalKind'(X))
isLNatKind'(ok'(X)) → ok'(isLNatKind'(X))
isPLNatKind'(ok'(X)) → ok'(isPLNatKind'(X))
tail'(ok'(X)) → ok'(tail'(X))
take'(ok'(X1), ok'(X2)) → ok'(take'(X1, X2))
sel'(ok'(X1), ok'(X2)) → ok'(sel'(X1, X2))
top'(mark'(X)) → top'(proper'(X))
top'(ok'(X)) → top'(active'(X))

Types:
active' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U101' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
tt' :: tt':mark':nil':0':ok'
mark' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U102' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
isNatural' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U103' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
isLNat' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U11' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
snd' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
splitAt' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U111' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U112' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U121' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U122' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U131' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U132' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U133' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U141' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U142' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U143' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U151' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U152' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U153' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U161' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
cons' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
natsFrom' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
s' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U171' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
head' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
afterNth' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U181' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U191' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
pair' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
nil' :: tt':mark':nil':0':ok'
U201' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U202' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U21' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U211' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U221' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
fst' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U31' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U41' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U42' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U43' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U51' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U52' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U53' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U61' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U62' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
isPLNat' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U71' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U72' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U81' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U82' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U91' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
U92' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
and' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
isNaturalKind' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
isLNatKind' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
isPLNatKind' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
tail' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
take' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
0' :: tt':mark':nil':0':ok'
sel' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
proper' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
ok' :: tt':mark':nil':0':ok' → tt':mark':nil':0':ok'
top' :: tt':mark':nil':0':ok' → top'
_hole_tt':mark':nil':0':ok'1 :: tt':mark':nil':0':ok'
_hole_top'2 :: top'
_gen_tt':mark':nil':0':ok'3 :: Nat → tt':mark':nil':0':ok'

Heuristically decided to analyse the following defined symbols:
active', U102', isNatural', U103', isLNat', snd', splitAt', U112', U122', U132', U133', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U102' < active'
isNatural' < active'
U103' < active'
isLNat' < active'
snd' < active'
splitAt' < active'
U112' < active'
U122' < active'
U132' < active'
U133' < active'
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U102' < proper'
isNatural' < proper'
U103' < proper'
isLNat' < proper'
snd' < proper'
splitAt' < proper'
U112' < proper'
U122' < proper'
U132' < proper'
U133' < proper'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

The following defined symbols remain to be analysed:
U102', active', isNatural', U103', isLNat', snd', splitAt', U112', U122', U132', U133', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

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

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

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

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

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

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

The following defined symbols remain to be analysed:
isNatural', active', U103', isLNat', snd', splitAt', U112', U122', U132', U133', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
isNatural' < active'
U103' < active'
isLNat' < active'
snd' < active'
splitAt' < active'
U112' < active'
U122' < active'
U132' < active'
U133' < active'
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
isNatural' < proper'
U103' < proper'
isLNat' < proper'
snd' < proper'
splitAt' < proper'
U112' < proper'
U122' < proper'
U132' < proper'
U133' < proper'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

Could not prove a rewrite lemma for the defined symbol isNatural'.

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

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

The following defined symbols remain to be analysed:
U103', active', isLNat', snd', splitAt', U112', U122', U132', U133', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U103' < active'
isLNat' < active'
snd' < active'
splitAt' < active'
U112' < active'
U122' < active'
U132' < active'
U133' < active'
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U103' < proper'
isLNat' < proper'
snd' < proper'
splitAt' < proper'
U112' < proper'
U122' < proper'
U132' < proper'
U133' < proper'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

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

The following defined symbols remain to be analysed:
isLNat', active', snd', splitAt', U112', U122', U132', U133', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
isLNat' < active'
snd' < active'
splitAt' < active'
U112' < active'
U122' < active'
U132' < active'
U133' < active'
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
isLNat' < proper'
snd' < proper'
splitAt' < proper'
U112' < proper'
U122' < proper'
U132' < proper'
U133' < proper'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

Could not prove a rewrite lemma for the defined symbol isLNat'.

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

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

The following defined symbols remain to be analysed:
snd', active', splitAt', U112', U122', U132', U133', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
snd' < active'
splitAt' < active'
U112' < active'
U122' < active'
U132' < active'
U133' < active'
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
snd' < proper'
splitAt' < proper'
U112' < proper'
U122' < proper'
U132' < proper'
U133' < proper'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
splitAt', active', U112', U122', U132', U133', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
splitAt' < active'
U112' < active'
U122' < active'
U132' < active'
U133' < active'
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
splitAt' < proper'
U112' < proper'
U122' < proper'
U132' < proper'
U133' < proper'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U112', active', U122', U132', U133', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U112' < active'
U122' < active'
U132' < active'
U133' < active'
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U112' < proper'
U122' < proper'
U132' < proper'
U133' < proper'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U122', active', U132', U133', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U122' < active'
U132' < active'
U133' < active'
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U122' < proper'
U132' < proper'
U133' < proper'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U132', active', U133', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U132' < active'
U133' < active'
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U132' < proper'
U133' < proper'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U133', active', U142', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U133' < active'
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U133' < proper'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U142', active', U143', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U142' < active'
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U142' < proper'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U143', active', U152', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U143' < active'
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U143' < proper'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U152', active', U153', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U152' < active'
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U152' < proper'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U153', active', cons', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U153' < active'
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U153' < proper'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
cons', active', natsFrom', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
cons' < active'
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
cons' < proper'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
natsFrom', active', s', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
natsFrom' < active'
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
natsFrom' < proper'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
s', active', head', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
s' < active'
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
s' < proper'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
head', active', afterNth', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
head' < active'
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
head' < proper'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
afterNth', active', pair', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
afterNth' < active'
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
afterNth' < proper'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
pair', active', U202', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
pair' < active'
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
pair' < proper'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U202', active', fst', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U202' < active'
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U202' < proper'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
fst', active', U42', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
fst' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
fst' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U42', active', U43', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U43', active', U52', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U43' < active'
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U52', active', U53', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U52' < active'
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U52' < proper'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U53', active', U62', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U53' < active'
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U53' < proper'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U62', active', isPLNat', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U62' < active'
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U62' < proper'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
isPLNat', active', U72', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
isPLNat' < active'
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
isPLNat' < proper'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

Could not prove a rewrite lemma for the defined symbol isPLNat'.

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

The following defined symbols remain to be analysed:
U72', active', U82', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U72' < active'
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U72' < proper'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U82', active', U92', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U82' < active'
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U82' < proper'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U92', active', U11', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U92' < active'
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U92' < proper'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U11', active', and', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U11' < active'
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U11' < proper'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
and', active', isNaturalKind', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
and' < active'
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
and' < proper'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
isNaturalKind', active', isLNatKind', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
isNaturalKind' < active'
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
isNaturalKind' < proper'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

Could not prove a rewrite lemma for the defined symbol isNaturalKind'.

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

The following defined symbols remain to be analysed:
isLNatKind', active', U21', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
isLNatKind' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
isLNatKind' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

Could not prove a rewrite lemma for the defined symbol isLNatKind'.

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

The following defined symbols remain to be analysed:
U21', active', U31', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U31', active', U41', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U41', active', U51', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U41' < active'
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U41' < proper'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U51', active', U61', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U51' < active'
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U51' < proper'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U61', active', isPLNatKind', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U61' < active'
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U61' < proper'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
isPLNatKind', active', U71', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
isPLNatKind' < active'
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
isPLNatKind' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

Could not prove a rewrite lemma for the defined symbol isPLNatKind'.

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

The following defined symbols remain to be analysed:
U71', active', U81', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U71' < active'
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U71' < proper'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U81', active', U91', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U81' < active'
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U81' < proper'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U91', active', U101', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U91' < active'
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U91' < proper'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U101', active', U111', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U101' < active'
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U101' < proper'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U111', active', U121', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U111' < active'
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U111' < proper'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U121', active', U131', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U121' < active'
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U121' < proper'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

Lemmas:
U102'(_gen_tt':mark':nil':0':ok'3(+(1, _n5)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n5)
U103'(_gen_tt':mark':nil':0':ok'3(+(1, _n15765))) → _*4, rt ∈ Ω(_n15765)
snd'(_gen_tt':mark':nil':0':ok'3(+(1, _n26264))) → _*4, rt ∈ Ω(_n26264)
splitAt'(_gen_tt':mark':nil':0':ok'3(+(1, _n36865)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n36865)
U112'(_gen_tt':mark':nil':0':ok'3(+(1, _n53678))) → _*4, rt ∈ Ω(_n53678)
U122'(_gen_tt':mark':nil':0':ok'3(+(1, _n64594))) → _*4, rt ∈ Ω(_n64594)
U132'(_gen_tt':mark':nil':0':ok'3(+(1, _n75634)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n75634)
U133'(_gen_tt':mark':nil':0':ok'3(+(1, _n93078))) → _*4, rt ∈ Ω(_n93078)
U142'(_gen_tt':mark':nil':0':ok'3(+(1, _n104433)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n104433)
U143'(_gen_tt':mark':nil':0':ok'3(+(1, _n122486))) → _*4, rt ∈ Ω(_n122486)
U152'(_gen_tt':mark':nil':0':ok'3(+(1, _n134156)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n134156)
U153'(_gen_tt':mark':nil':0':ok'3(+(1, _n152818))) → _*4, rt ∈ Ω(_n152818)
cons'(_gen_tt':mark':nil':0':ok'3(+(1, _n164803)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n164803)
natsFrom'(_gen_tt':mark':nil':0':ok'3(+(1, _n184074))) → _*4, rt ∈ Ω(_n184074)
s'(_gen_tt':mark':nil':0':ok'3(+(1, _n196374))) → _*4, rt ∈ Ω(_n196374)
head'(_gen_tt':mark':nil':0':ok'3(+(1, _n208798))) → _*4, rt ∈ Ω(_n208798)
afterNth'(_gen_tt':mark':nil':0':ok'3(+(1, _n221346)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n221346)
pair'(_gen_tt':mark':nil':0':ok'3(+(1, _n241927)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n241927)
U202'(_gen_tt':mark':nil':0':ok'3(+(1, _n262876)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n262876)
fst'(_gen_tt':mark':nil':0':ok'3(+(1, _n283974))) → _*4, rt ∈ Ω(_n283974)
U42'(_gen_tt':mark':nil':0':ok'3(+(1, _n297219)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n297219)
U43'(_gen_tt':mark':nil':0':ok'3(+(1, _n318926))) → _*4, rt ∈ Ω(_n318926)
U52'(_gen_tt':mark':nil':0':ok'3(+(1, _n332486)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n332486)
U53'(_gen_tt':mark':nil':0':ok'3(+(1, _n354802))) → _*4, rt ∈ Ω(_n354802)
U62'(_gen_tt':mark':nil':0':ok'3(+(1, _n368677))) → _*4, rt ∈ Ω(_n368677)
U72'(_gen_tt':mark':nil':0':ok'3(+(1, _n382876))) → _*4, rt ∈ Ω(_n382876)
U82'(_gen_tt':mark':nil':0':ok'3(+(1, _n396999))) → _*4, rt ∈ Ω(_n396999)
U92'(_gen_tt':mark':nil':0':ok'3(+(1, _n411246))) → _*4, rt ∈ Ω(_n411246)
U11'(_gen_tt':mark':nil':0':ok'3(+(1, _n425617)), _gen_tt':mark':nil':0':ok'3(b), _gen_tt':mark':nil':0':ok'3(c)) → _*4, rt ∈ Ω(_n425617)
and'(_gen_tt':mark':nil':0':ok'3(+(1, _n459014)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n459014)
U21'(_gen_tt':mark':nil':0':ok'3(+(1, _n483882)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n483882)
U31'(_gen_tt':mark':nil':0':ok'3(+(1, _n508634)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n508634)
U41'(_gen_tt':mark':nil':0':ok'3(+(1, _n533754)), _gen_tt':mark':nil':0':ok'3(b), _gen_tt':mark':nil':0':ok'3(c)) → _*4, rt ∈ Ω(_n533754)
U51'(_gen_tt':mark':nil':0':ok'3(+(1, _n569518)), _gen_tt':mark':nil':0':ok'3(b), _gen_tt':mark':nil':0':ok'3(c)) → _*4, rt ∈ Ω(_n569518)
U61'(_gen_tt':mark':nil':0':ok'3(+(1, _n606014)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n606014)
U71'(_gen_tt':mark':nil':0':ok'3(+(1, _n632792)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n632792)
U81'(_gen_tt':mark':nil':0':ok'3(+(1, _n659638)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n659638)
U91'(_gen_tt':mark':nil':0':ok'3(+(1, _n686852)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n686852)
U101'(_gen_tt':mark':nil':0':ok'3(+(1, _n714434)), _gen_tt':mark':nil':0':ok'3(b), _gen_tt':mark':nil':0':ok'3(c)) → _*4, rt ∈ Ω(_n714434)
U111'(_gen_tt':mark':nil':0':ok'3(+(1, _n753842)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n753842)
U121'(_gen_tt':mark':nil':0':ok'3(+(1, _n782287)), _gen_tt':mark':nil':0':ok'3(b)) → _*4, rt ∈ Ω(_n782287)

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

The following defined symbols remain to be analysed:
U131', active', U141', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U131' < active'
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U131' < proper'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U141', active', U151', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U141' < active'
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U141' < proper'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U151', active', U161', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U151' < active'
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U151' < proper'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U161', active', U171', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U161' < active'
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U161' < proper'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U171', active', U181', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U171' < active'
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U171' < proper'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

The following defined symbols remain to be analysed:
U181', active', U191', U201', U211', U221', tail', take', sel', proper', top'

They will be analysed ascendingly in the following order:
U181' < active'
U191' < active'
U201' < active'
U211' < active'
U221' < active'
tail' < active'
take' < active'
sel' < active'
active' < top'
U181' < proper'
U191' < proper'
U201' < proper'
U211' < proper'
U221' < proper'
tail' < proper'
take' < proper'
sel' < proper'
proper' < top'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Induction Step:
U201'(_gen_tt':mark':nil':0':ok'3(+(1, +(_$n1075050, 1))), _gen_tt':mark':nil':0':ok'3(_b1105846), _gen_tt':mark':nil':0':ok'3(_c1105847), _gen_tt':mark':nil':0':ok'3(_d1105848)) →_R^Ω(1)
mark'(U201'(_gen_tt':mark':nil':0':ok'3(+(1, _$n1075050)), _gen_tt':mark':nil':0':ok'3(_b1105846), _gen_tt':mark':nil':0':ok'3(_c1105847), _gen_tt':mark':nil':0':ok'3(_d1105848))) →_IH
mark'(_*4)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Generator Equations:
_gen_tt':mark':nil':0':ok'3(0) ⇔ tt'
_gen_tt':mark':nil':0':ok'3(+(x, 1)) ⇔ mark'(_gen_tt':mark':nil':0':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'