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

U101(tt, V2) → U102(isLNat(activate(V2)))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(activate(XS)), activate(N), activate(XS))
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(activate(V2)))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(activate(V2)))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(activate(V2)))
U152(tt) → tt
U161(tt, N) → cons(activate(N), n__natsFrom(s(activate(N))))
U171(tt, N, XS) → U172(isLNat(activate(XS)), activate(N), activate(XS))
U172(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U181(tt, Y) → U182(isLNat(activate(Y)), activate(Y))
U182(tt, Y) → activate(Y)
U191(tt, XS) → pair(nil, activate(XS))
U201(tt, N, X, XS) → U202(isNatural(activate(X)), activate(N), activate(X), activate(XS))
U202(tt, N, X, XS) → U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS))
U203(tt, N, X, XS) → U204(splitAt(activate(N), activate(XS)), activate(X))
U204(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U21(tt, X, Y) → U22(isLNat(activate(Y)), activate(X))
U211(tt, XS) → U212(isLNat(activate(XS)), activate(XS))
U212(tt, XS) → activate(XS)
U22(tt, X) → activate(X)
U221(tt, N, XS) → U222(isLNat(activate(XS)), activate(N), activate(XS))
U222(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U31(tt, N, XS) → U32(isLNat(activate(XS)), activate(N))
U32(tt, N) → activate(N)
U41(tt, V2) → U42(isLNat(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(activate(V2)))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, activate(XS))
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → U41(isNatural(activate(V1)), activate(V2))
isLNat(n__cons(V1, V2)) → U51(isNatural(activate(V1)), activate(V2))
isLNat(n__fst(V1)) → U61(isPLNat(activate(V1)))
isLNat(n__natsFrom(V1)) → U71(isNatural(activate(V1)))
isLNat(n__snd(V1)) → U81(isPLNat(activate(V1)))
isLNat(n__tail(V1)) → U91(isLNat(activate(V1)))
isLNat(n__take(V1, V2)) → U101(isNatural(activate(V1)), activate(V2))
isNatural(n__0) → tt
isNatural(n__head(V1)) → U111(isLNat(activate(V1)))
isNatural(n__s(V1)) → U121(isNatural(activate(V1)))
isNatural(n__sel(V1, V2)) → U131(isNatural(activate(V1)), activate(V2))
isPLNat(n__pair(V1, V2)) → U141(isLNat(activate(V1)), activate(V2))
isPLNat(n__splitAt(V1, V2)) → U151(isNatural(activate(V1)), activate(V2))
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, activate(XS))
tail(cons(N, XS)) → U211(isNatural(N), activate(XS))
take(N, XS) → U221(isNatural(N), N, XS)
natsFrom(X) → n__natsFrom(X)
nil → n__nil
afterNth(X1, X2) → n__afterNth(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
fst(X) → n__fst(X)
snd(X) → n__snd(X)
tail(X) → n__tail(X)
take(X1, X2) → n__take(X1, X2)
0 → n__0
head(X) → n__head(X)
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
pair(X1, X2) → n__pair(X1, X2)
splitAt(X1, X2) → n__splitAt(X1, X2)
activate(n__natsFrom(X)) → natsFrom(X)
activate(n__nil) → nil
activate(n__afterNth(X1, X2)) → afterNth(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__fst(X)) → fst(X)
activate(n__snd(X)) → snd(X)
activate(n__tail(X)) → tail(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__head(X)) → head(X)
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__pair(X1, X2)) → pair(X1, X2)
activate(n__splitAt(X1, X2)) → splitAt(X1, X2)
activate(X) → X

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

U101'(tt', V2) → U102'(isLNat'(activate'(V2)))
U102'(tt') → tt'
U11'(tt', N, XS) → U12'(isLNat'(activate'(XS)), activate'(N), activate'(XS))
U111'(tt') → tt'
U12'(tt', N, XS) → snd'(splitAt'(activate'(N), activate'(XS)))
U121'(tt') → tt'
U131'(tt', V2) → U132'(isLNat'(activate'(V2)))
U132'(tt') → tt'
U141'(tt', V2) → U142'(isLNat'(activate'(V2)))
U142'(tt') → tt'
U151'(tt', V2) → U152'(isLNat'(activate'(V2)))
U152'(tt') → tt'
U161'(tt', N) → cons'(activate'(N), n__natsFrom'(s'(activate'(N))))
U171'(tt', N, XS) → U172'(isLNat'(activate'(XS)), activate'(N), activate'(XS))
U172'(tt', N, XS) → head'(afterNth'(activate'(N), activate'(XS)))
U181'(tt', Y) → U182'(isLNat'(activate'(Y)), activate'(Y))
U182'(tt', Y) → activate'(Y)
U191'(tt', XS) → pair'(nil', activate'(XS))
U201'(tt', N, X, XS) → U202'(isNatural'(activate'(X)), activate'(N), activate'(X), activate'(XS))
U202'(tt', N, X, XS) → U203'(isLNat'(activate'(XS)), activate'(N), activate'(X), activate'(XS))
U203'(tt', N, X, XS) → U204'(splitAt'(activate'(N), activate'(XS)), activate'(X))
U204'(pair'(YS, ZS), X) → pair'(cons'(activate'(X), YS), ZS)
U21'(tt', X, Y) → U22'(isLNat'(activate'(Y)), activate'(X))
U211'(tt', XS) → U212'(isLNat'(activate'(XS)), activate'(XS))
U212'(tt', XS) → activate'(XS)
U22'(tt', X) → activate'(X)
U221'(tt', N, XS) → U222'(isLNat'(activate'(XS)), activate'(N), activate'(XS))
U222'(tt', N, XS) → fst'(splitAt'(activate'(N), activate'(XS)))
U31'(tt', N, XS) → U32'(isLNat'(activate'(XS)), activate'(N))
U32'(tt', N) → activate'(N)
U41'(tt', V2) → U42'(isLNat'(activate'(V2)))
U42'(tt') → tt'
U51'(tt', V2) → U52'(isLNat'(activate'(V2)))
U52'(tt') → tt'
U61'(tt') → tt'
U71'(tt') → tt'
U81'(tt') → tt'
U91'(tt') → tt'
afterNth'(N, XS) → U11'(isNatural'(N), N, XS)
fst'(pair'(X, Y)) → U21'(isLNat'(X), X, Y)
head'(cons'(N, XS)) → U31'(isNatural'(N), N, activate'(XS))
isLNat'(n__nil') → tt'
isLNat'(n__afterNth'(V1, V2)) → U41'(isNatural'(activate'(V1)), activate'(V2))
isLNat'(n__cons'(V1, V2)) → U51'(isNatural'(activate'(V1)), activate'(V2))
isLNat'(n__fst'(V1)) → U61'(isPLNat'(activate'(V1)))
isLNat'(n__natsFrom'(V1)) → U71'(isNatural'(activate'(V1)))
isLNat'(n__snd'(V1)) → U81'(isPLNat'(activate'(V1)))
isLNat'(n__tail'(V1)) → U91'(isLNat'(activate'(V1)))
isLNat'(n__take'(V1, V2)) → U101'(isNatural'(activate'(V1)), activate'(V2))
isNatural'(n__0') → tt'
isNatural'(n__head'(V1)) → U111'(isLNat'(activate'(V1)))
isNatural'(n__s'(V1)) → U121'(isNatural'(activate'(V1)))
isNatural'(n__sel'(V1, V2)) → U131'(isNatural'(activate'(V1)), activate'(V2))
isPLNat'(n__pair'(V1, V2)) → U141'(isLNat'(activate'(V1)), activate'(V2))
isPLNat'(n__splitAt'(V1, V2)) → U151'(isNatural'(activate'(V1)), activate'(V2))
natsFrom'(N) → U161'(isNatural'(N), N)
sel'(N, XS) → U171'(isNatural'(N), N, XS)
snd'(pair'(X, Y)) → U181'(isLNat'(X), Y)
splitAt'(0', XS) → U191'(isLNat'(XS), XS)
splitAt'(s'(N), cons'(X, XS)) → U201'(isNatural'(N), N, X, activate'(XS))
tail'(cons'(N, XS)) → U211'(isNatural'(N), activate'(XS))
take'(N, XS) → U221'(isNatural'(N), N, XS)
natsFrom'(X) → n__natsFrom'(X)
nil' → n__nil'
afterNth'(X1, X2) → n__afterNth'(X1, X2)
cons'(X1, X2) → n__cons'(X1, X2)
fst'(X) → n__fst'(X)
snd'(X) → n__snd'(X)
tail'(X) → n__tail'(X)
take'(X1, X2) → n__take'(X1, X2)
0' → n__0'
head'(X) → n__head'(X)
s'(X) → n__s'(X)
sel'(X1, X2) → n__sel'(X1, X2)
pair'(X1, X2) → n__pair'(X1, X2)
splitAt'(X1, X2) → n__splitAt'(X1, X2)
activate'(n__natsFrom'(X)) → natsFrom'(X)
activate'(n__nil') → nil'
activate'(n__afterNth'(X1, X2)) → afterNth'(X1, X2)
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__fst'(X)) → fst'(X)
activate'(n__snd'(X)) → snd'(X)
activate'(n__tail'(X)) → tail'(X)
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(n__0') → 0'
activate'(n__head'(X)) → head'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__sel'(X1, X2)) → sel'(X1, X2)
activate'(n__pair'(X1, X2)) → pair'(X1, X2)
activate'(n__splitAt'(X1, X2)) → splitAt'(X1, X2)
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
U101'(tt', V2) → U102'(isLNat'(activate'(V2)))
U102'(tt') → tt'
U11'(tt', N, XS) → U12'(isLNat'(activate'(XS)), activate'(N), activate'(XS))
U111'(tt') → tt'
U12'(tt', N, XS) → snd'(splitAt'(activate'(N), activate'(XS)))
U121'(tt') → tt'
U131'(tt', V2) → U132'(isLNat'(activate'(V2)))
U132'(tt') → tt'
U141'(tt', V2) → U142'(isLNat'(activate'(V2)))
U142'(tt') → tt'
U151'(tt', V2) → U152'(isLNat'(activate'(V2)))
U152'(tt') → tt'
U161'(tt', N) → cons'(activate'(N), n__natsFrom'(s'(activate'(N))))
U171'(tt', N, XS) → U172'(isLNat'(activate'(XS)), activate'(N), activate'(XS))
U172'(tt', N, XS) → head'(afterNth'(activate'(N), activate'(XS)))
U181'(tt', Y) → U182'(isLNat'(activate'(Y)), activate'(Y))
U182'(tt', Y) → activate'(Y)
U191'(tt', XS) → pair'(nil', activate'(XS))
U201'(tt', N, X, XS) → U202'(isNatural'(activate'(X)), activate'(N), activate'(X), activate'(XS))
U202'(tt', N, X, XS) → U203'(isLNat'(activate'(XS)), activate'(N), activate'(X), activate'(XS))
U203'(tt', N, X, XS) → U204'(splitAt'(activate'(N), activate'(XS)), activate'(X))
U204'(pair'(YS, ZS), X) → pair'(cons'(activate'(X), YS), ZS)
U21'(tt', X, Y) → U22'(isLNat'(activate'(Y)), activate'(X))
U211'(tt', XS) → U212'(isLNat'(activate'(XS)), activate'(XS))
U212'(tt', XS) → activate'(XS)
U22'(tt', X) → activate'(X)
U221'(tt', N, XS) → U222'(isLNat'(activate'(XS)), activate'(N), activate'(XS))
U222'(tt', N, XS) → fst'(splitAt'(activate'(N), activate'(XS)))
U31'(tt', N, XS) → U32'(isLNat'(activate'(XS)), activate'(N))
U32'(tt', N) → activate'(N)
U41'(tt', V2) → U42'(isLNat'(activate'(V2)))
U42'(tt') → tt'
U51'(tt', V2) → U52'(isLNat'(activate'(V2)))
U52'(tt') → tt'
U61'(tt') → tt'
U71'(tt') → tt'
U81'(tt') → tt'
U91'(tt') → tt'
afterNth'(N, XS) → U11'(isNatural'(N), N, XS)
fst'(pair'(X, Y)) → U21'(isLNat'(X), X, Y)
head'(cons'(N, XS)) → U31'(isNatural'(N), N, activate'(XS))
isLNat'(n__nil') → tt'
isLNat'(n__afterNth'(V1, V2)) → U41'(isNatural'(activate'(V1)), activate'(V2))
isLNat'(n__cons'(V1, V2)) → U51'(isNatural'(activate'(V1)), activate'(V2))
isLNat'(n__fst'(V1)) → U61'(isPLNat'(activate'(V1)))
isLNat'(n__natsFrom'(V1)) → U71'(isNatural'(activate'(V1)))
isLNat'(n__snd'(V1)) → U81'(isPLNat'(activate'(V1)))
isLNat'(n__tail'(V1)) → U91'(isLNat'(activate'(V1)))
isLNat'(n__take'(V1, V2)) → U101'(isNatural'(activate'(V1)), activate'(V2))
isNatural'(n__0') → tt'
isNatural'(n__head'(V1)) → U111'(isLNat'(activate'(V1)))
isNatural'(n__s'(V1)) → U121'(isNatural'(activate'(V1)))
isNatural'(n__sel'(V1, V2)) → U131'(isNatural'(activate'(V1)), activate'(V2))
isPLNat'(n__pair'(V1, V2)) → U141'(isLNat'(activate'(V1)), activate'(V2))
isPLNat'(n__splitAt'(V1, V2)) → U151'(isNatural'(activate'(V1)), activate'(V2))
natsFrom'(N) → U161'(isNatural'(N), N)
sel'(N, XS) → U171'(isNatural'(N), N, XS)
snd'(pair'(X, Y)) → U181'(isLNat'(X), Y)
splitAt'(0', XS) → U191'(isLNat'(XS), XS)
splitAt'(s'(N), cons'(X, XS)) → U201'(isNatural'(N), N, X, activate'(XS))
tail'(cons'(N, XS)) → U211'(isNatural'(N), activate'(XS))
take'(N, XS) → U221'(isNatural'(N), N, XS)
natsFrom'(X) → n__natsFrom'(X)
nil' → n__nil'
afterNth'(X1, X2) → n__afterNth'(X1, X2)
cons'(X1, X2) → n__cons'(X1, X2)
fst'(X) → n__fst'(X)
snd'(X) → n__snd'(X)
tail'(X) → n__tail'(X)
take'(X1, X2) → n__take'(X1, X2)
0' → n__0'
head'(X) → n__head'(X)
s'(X) → n__s'(X)
sel'(X1, X2) → n__sel'(X1, X2)
pair'(X1, X2) → n__pair'(X1, X2)
splitAt'(X1, X2) → n__splitAt'(X1, X2)
activate'(n__natsFrom'(X)) → natsFrom'(X)
activate'(n__nil') → nil'
activate'(n__afterNth'(X1, X2)) → afterNth'(X1, X2)
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__fst'(X)) → fst'(X)
activate'(n__snd'(X)) → snd'(X)
activate'(n__tail'(X)) → tail'(X)
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(n__0') → 0'
activate'(n__head'(X)) → head'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__sel'(X1, X2)) → sel'(X1, X2)
activate'(n__pair'(X1, X2)) → pair'(X1, X2)
activate'(n__splitAt'(X1, X2)) → splitAt'(X1, X2)
activate'(X) → X

Types:
U101' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → tt'
tt' :: tt'
U102' :: tt' → tt'
isLNat' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → tt'
activate' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U11' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U12' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U111' :: tt' → tt'
snd' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
splitAt' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U121' :: tt' → tt'
U131' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → tt'
U132' :: tt' → tt'
U141' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → tt'
U142' :: tt' → tt'
U151' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → tt'
U152' :: tt' → tt'
U161' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
cons' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__natsFrom' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
s' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U171' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U172' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
head' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
afterNth' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U181' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U182' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U191' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
pair' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
nil' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U201' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U202' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
isNatural' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → tt'
U203' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U204' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U21' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U22' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U211' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U212' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U221' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U222' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
fst' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U31' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U32' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
U41' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → tt'
U42' :: tt' → tt'
U51' :: tt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → tt'
U52' :: tt' → tt'
U61' :: tt' → tt'
U71' :: tt' → tt'
U81' :: tt' → tt'
U91' :: tt' → tt'
n__nil' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__afterNth' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__cons' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__fst' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
isPLNat' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → tt'
n__snd' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__tail' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__take' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__0' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__head' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__s' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__sel' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__pair' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
n__splitAt' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
natsFrom' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
sel' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
0' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
tail' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
take' :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt' → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
_hole_tt'1 :: tt'
_hole_n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'2 :: n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'
_gen_n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'3 :: Nat → n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'

Heuristically decided to analyse the following defined symbols:
isLNat', activate', snd', splitAt', head', afterNth', U191', isNatural', U204', fst', isPLNat', natsFrom', tail'

They will be analysed ascendingly in the following order:
isLNat' = activate'
isLNat' = snd'
isLNat' = splitAt'
isLNat' = head'
isLNat' = afterNth'
isLNat' = U191'
isLNat' = isNatural'
isLNat' = U204'
isLNat' = fst'
isLNat' = isPLNat'
isLNat' = natsFrom'
isLNat' = tail'
activate' = snd'
activate' = splitAt'
activate' = head'
activate' = afterNth'
activate' = U191'
activate' = isNatural'
activate' = U204'
activate' = fst'
activate' = isPLNat'
activate' = natsFrom'
activate' = tail'
snd' = splitAt'
snd' = head'
snd' = afterNth'
snd' = U191'
snd' = isNatural'
snd' = U204'
snd' = fst'
snd' = isPLNat'
snd' = natsFrom'
snd' = tail'
splitAt' = head'
splitAt' = afterNth'
splitAt' = U191'
splitAt' = isNatural'
splitAt' = U204'
splitAt' = fst'
splitAt' = isPLNat'
splitAt' = natsFrom'
splitAt' = tail'
head' = afterNth'
head' = U191'
head' = isNatural'
head' = U204'
head' = fst'
head' = isPLNat'
head' = natsFrom'
head' = tail'
afterNth' = U191'
afterNth' = isNatural'
afterNth' = U204'
afterNth' = fst'
afterNth' = isPLNat'
afterNth' = natsFrom'
afterNth' = tail'
U191' = isNatural'
U191' = U204'
U191' = fst'
U191' = isPLNat'
U191' = natsFrom'
U191' = tail'
isNatural' = U204'
isNatural' = fst'
isNatural' = isPLNat'
isNatural' = natsFrom'
isNatural' = tail'
U204' = fst'
U204' = isPLNat'
U204' = natsFrom'
U204' = tail'
fst' = isPLNat'
fst' = natsFrom'
fst' = tail'
isPLNat' = natsFrom'
isPLNat' = tail'
natsFrom' = tail'

Generator Equations:
_gen_n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'3(0) ⇔ n__nil'
_gen_n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'3(+(x, 1)) ⇔ n__natsFrom'(_gen_n__natsFrom':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__s':n__sel':n__pair':n__splitAt'3(x))

The following defined symbols remain to be analysed:
isNatural', isLNat', activate', snd', splitAt', head', afterNth', U191', U204', fst', isPLNat', natsFrom', tail'

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

The following defined symbols remain to be analysed:
isLNat', activate', snd', splitAt', head', afterNth', U191', U204', fst', isPLNat', natsFrom', tail'

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

The following defined symbols remain to be analysed:
activate', snd', splitAt', head', afterNth', U191', U204', fst', isPLNat', natsFrom', tail'

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

The following defined symbols remain to be analysed:
natsFrom', snd', splitAt', head', afterNth', U191', U204', fst', isPLNat', tail'

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

The following defined symbols remain to be analysed:
afterNth', snd', splitAt', head', U191', U204', fst', isPLNat', tail'

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

The following defined symbols remain to be analysed:
snd', splitAt', head', U191', U204', fst', isPLNat', tail'

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

The following defined symbols remain to be analysed:
splitAt', head', U191', U204', fst', isPLNat', tail'

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

The following defined symbols remain to be analysed:
U191', head', U204', fst', isPLNat', tail'

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

The following defined symbols remain to be analysed:
U204', head', fst', isPLNat', tail'

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

The following defined symbols remain to be analysed:
fst', head', isPLNat', tail'

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

The following defined symbols remain to be analysed:
tail', head', isPLNat'

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

The following defined symbols remain to be analysed:
head', isPLNat'

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

The following defined symbols remain to be analysed:
isPLNat'

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

No more defined symbols left to analyse.