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

U101(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U11(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U21(tt, X) → activate(X)
U31(tt, N) → activate(N)
U41(tt, N) → cons(activate(N), n__natsFrom(s(activate(N))))
U51(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U61(tt, Y) → activate(Y)
U71(tt, XS) → pair(nil, activate(XS))
U81(tt, N, X, XS) → U82(splitAt(activate(N), activate(XS)), activate(X))
U82(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U91(tt, XS) → activate(XS)
afterNth(N, XS) → U11(and(isNatural(N), n__isLNat(XS)), N, XS)
and(tt, X) → activate(X)
fst(pair(X, Y)) → U21(and(isLNat(X), n__isLNat(Y)), X)
head(cons(N, XS)) → U31(and(isNatural(N), n__isLNat(activate(XS))), N)
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isLNat(n__cons(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isLNat(n__fst(V1)) → isPLNat(activate(V1))
isLNat(n__natsFrom(V1)) → isNatural(activate(V1))
isLNat(n__snd(V1)) → isPLNat(activate(V1))
isLNat(n__tail(V1)) → isLNat(activate(V1))
isLNat(n__take(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isNatural(n__0) → tt
isNatural(n__head(V1)) → isLNat(activate(V1))
isNatural(n__s(V1)) → isNatural(activate(V1))
isNatural(n__sel(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isPLNat(n__pair(V1, V2)) → and(isLNat(activate(V1)), n__isLNat(activate(V2)))
isPLNat(n__splitAt(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
natsFrom(N) → U41(isNatural(N), N)
sel(N, XS) → U51(and(isNatural(N), n__isLNat(XS)), N, XS)
snd(pair(X, Y)) → U61(and(isLNat(X), n__isLNat(Y)), Y)
splitAt(0, XS) → U71(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U81(and(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))
tail(cons(N, XS)) → U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
take(N, XS) → U101(and(isNatural(N), n__isLNat(XS)), N, XS)
natsFrom(X) → n__natsFrom(X)
isLNat(X) → n__isLNat(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)
and(X1, X2) → n__and(X1, X2)
activate(n__natsFrom(X)) → natsFrom(X)
activate(n__isLNat(X)) → isLNat(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(n__and(X1, X2)) → and(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', N, XS) → fst'(splitAt'(activate'(N), activate'(XS)))
U11'(tt', N, XS) → snd'(splitAt'(activate'(N), activate'(XS)))
U21'(tt', X) → activate'(X)
U31'(tt', N) → activate'(N)
U41'(tt', N) → cons'(activate'(N), n__natsFrom'(s'(activate'(N))))
U51'(tt', N, XS) → head'(afterNth'(activate'(N), activate'(XS)))
U61'(tt', Y) → activate'(Y)
U71'(tt', XS) → pair'(nil', activate'(XS))
U81'(tt', N, X, XS) → U82'(splitAt'(activate'(N), activate'(XS)), activate'(X))
U82'(pair'(YS, ZS), X) → pair'(cons'(activate'(X), YS), ZS)
U91'(tt', XS) → activate'(XS)
afterNth'(N, XS) → U11'(and'(isNatural'(N), n__isLNat'(XS)), N, XS)
and'(tt', X) → activate'(X)
fst'(pair'(X, Y)) → U21'(and'(isLNat'(X), n__isLNat'(Y)), X)
head'(cons'(N, XS)) → U31'(and'(isNatural'(N), n__isLNat'(activate'(XS))), N)
isLNat'(n__nil') → tt'
isLNat'(n__afterNth'(V1, V2)) → and'(isNatural'(activate'(V1)), n__isLNat'(activate'(V2)))
isLNat'(n__cons'(V1, V2)) → and'(isNatural'(activate'(V1)), n__isLNat'(activate'(V2)))
isLNat'(n__fst'(V1)) → isPLNat'(activate'(V1))
isLNat'(n__natsFrom'(V1)) → isNatural'(activate'(V1))
isLNat'(n__snd'(V1)) → isPLNat'(activate'(V1))
isLNat'(n__tail'(V1)) → isLNat'(activate'(V1))
isLNat'(n__take'(V1, V2)) → and'(isNatural'(activate'(V1)), n__isLNat'(activate'(V2)))
isNatural'(n__0') → tt'
isNatural'(n__head'(V1)) → isLNat'(activate'(V1))
isNatural'(n__s'(V1)) → isNatural'(activate'(V1))
isNatural'(n__sel'(V1, V2)) → and'(isNatural'(activate'(V1)), n__isLNat'(activate'(V2)))
isPLNat'(n__pair'(V1, V2)) → and'(isLNat'(activate'(V1)), n__isLNat'(activate'(V2)))
isPLNat'(n__splitAt'(V1, V2)) → and'(isNatural'(activate'(V1)), n__isLNat'(activate'(V2)))
natsFrom'(N) → U41'(isNatural'(N), N)
sel'(N, XS) → U51'(and'(isNatural'(N), n__isLNat'(XS)), N, XS)
snd'(pair'(X, Y)) → U61'(and'(isLNat'(X), n__isLNat'(Y)), Y)
splitAt'(0', XS) → U71'(isLNat'(XS), XS)
splitAt'(s'(N), cons'(X, XS)) → U81'(and'(isNatural'(N), n__and'(isNatural'(X), n__isLNat'(activate'(XS)))), N, X, activate'(XS))
tail'(cons'(N, XS)) → U91'(and'(isNatural'(N), n__isLNat'(activate'(XS))), activate'(XS))
take'(N, XS) → U101'(and'(isNatural'(N), n__isLNat'(XS)), N, XS)
natsFrom'(X) → n__natsFrom'(X)
isLNat'(X) → n__isLNat'(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)
and'(X1, X2) → n__and'(X1, X2)
activate'(n__natsFrom'(X)) → natsFrom'(X)
activate'(n__isLNat'(X)) → isLNat'(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'(n__and'(X1, X2)) → and'(X1, X2)
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
U101'(tt', N, XS) → fst'(splitAt'(activate'(N), activate'(XS)))
U11'(tt', N, XS) → snd'(splitAt'(activate'(N), activate'(XS)))
U21'(tt', X) → activate'(X)
U31'(tt', N) → activate'(N)
U41'(tt', N) → cons'(activate'(N), n__natsFrom'(s'(activate'(N))))
U51'(tt', N, XS) → head'(afterNth'(activate'(N), activate'(XS)))
U61'(tt', Y) → activate'(Y)
U71'(tt', XS) → pair'(nil', activate'(XS))
U81'(tt', N, X, XS) → U82'(splitAt'(activate'(N), activate'(XS)), activate'(X))
U82'(pair'(YS, ZS), X) → pair'(cons'(activate'(X), YS), ZS)
U91'(tt', XS) → activate'(XS)
afterNth'(N, XS) → U11'(and'(isNatural'(N), n__isLNat'(XS)), N, XS)
and'(tt', X) → activate'(X)
fst'(pair'(X, Y)) → U21'(and'(isLNat'(X), n__isLNat'(Y)), X)
head'(cons'(N, XS)) → U31'(and'(isNatural'(N), n__isLNat'(activate'(XS))), N)
isLNat'(n__nil') → tt'
isLNat'(n__afterNth'(V1, V2)) → and'(isNatural'(activate'(V1)), n__isLNat'(activate'(V2)))
isLNat'(n__cons'(V1, V2)) → and'(isNatural'(activate'(V1)), n__isLNat'(activate'(V2)))
isLNat'(n__fst'(V1)) → isPLNat'(activate'(V1))
isLNat'(n__natsFrom'(V1)) → isNatural'(activate'(V1))
isLNat'(n__snd'(V1)) → isPLNat'(activate'(V1))
isLNat'(n__tail'(V1)) → isLNat'(activate'(V1))
isLNat'(n__take'(V1, V2)) → and'(isNatural'(activate'(V1)), n__isLNat'(activate'(V2)))
isNatural'(n__0') → tt'
isNatural'(n__head'(V1)) → isLNat'(activate'(V1))
isNatural'(n__s'(V1)) → isNatural'(activate'(V1))
isNatural'(n__sel'(V1, V2)) → and'(isNatural'(activate'(V1)), n__isLNat'(activate'(V2)))
isPLNat'(n__pair'(V1, V2)) → and'(isLNat'(activate'(V1)), n__isLNat'(activate'(V2)))
isPLNat'(n__splitAt'(V1, V2)) → and'(isNatural'(activate'(V1)), n__isLNat'(activate'(V2)))
natsFrom'(N) → U41'(isNatural'(N), N)
sel'(N, XS) → U51'(and'(isNatural'(N), n__isLNat'(XS)), N, XS)
snd'(pair'(X, Y)) → U61'(and'(isLNat'(X), n__isLNat'(Y)), Y)
splitAt'(0', XS) → U71'(isLNat'(XS), XS)
splitAt'(s'(N), cons'(X, XS)) → U81'(and'(isNatural'(N), n__and'(isNatural'(X), n__isLNat'(activate'(XS)))), N, X, activate'(XS))
tail'(cons'(N, XS)) → U91'(and'(isNatural'(N), n__isLNat'(activate'(XS))), activate'(XS))
take'(N, XS) → U101'(and'(isNatural'(N), n__isLNat'(XS)), N, XS)
natsFrom'(X) → n__natsFrom'(X)
isLNat'(X) → n__isLNat'(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)
and'(X1, X2) → n__and'(X1, X2)
activate'(n__natsFrom'(X)) → natsFrom'(X)
activate'(n__isLNat'(X)) → isLNat'(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'(n__and'(X1, X2)) → and'(X1, X2)
activate'(X) → X

Types:
U101' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
tt' :: tt':n__natsFrom':n__isLNat':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__and'
fst' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
splitAt' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
activate' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
U11' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
snd' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
U21' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
U31' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
U41' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
cons' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__natsFrom' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
s' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
U51' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
head' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
afterNth' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
U61' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
U71' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
pair' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
nil' :: tt':n__natsFrom':n__isLNat':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__and'
U81' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
U82' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
U91' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
and' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
isNatural' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__isLNat' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
isLNat' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__nil' :: tt':n__natsFrom':n__isLNat':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__and'
n__afterNth' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__cons' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__fst' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
isPLNat' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__snd' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__tail' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__take' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__0' :: tt':n__natsFrom':n__isLNat':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__and'
n__head' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__s' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__sel' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__pair' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
n__splitAt' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
natsFrom' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
sel' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
0' :: tt':n__natsFrom':n__isLNat':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__and'
n__and' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
tail' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
take' :: tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and' → tt':n__natsFrom':n__isLNat':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__and'
_hole_tt':n__natsFrom':n__isLNat':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__and'1 :: tt':n__natsFrom':n__isLNat':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__and'
_gen_tt':n__natsFrom':n__isLNat':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__and'2 :: Nat → tt':n__natsFrom':n__isLNat':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__and'

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

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

Generator Equations:
_gen_tt':n__natsFrom':n__isLNat':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__and'2(0) ⇔ n__nil'
_gen_tt':n__natsFrom':n__isLNat':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__and'2(+(x, 1)) ⇔ n__natsFrom'(_gen_tt':n__natsFrom':n__isLNat':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__and'2(x))

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

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

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

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

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

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

The following defined symbols remain to be analysed:
isNatural', fst', splitAt', snd', head', afterNth', U71', U82', isLNat', isPLNat', tail'

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

The following defined symbols remain to be analysed:
isLNat', fst', splitAt', snd', head', afterNth', U71', U82', isPLNat', tail'

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

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

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

The following defined symbols remain to be analysed:
afterNth', fst', splitAt', snd', head', U71', U82', tail'

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

The following defined symbols remain to be analysed:
snd', fst', splitAt', head', U71', U82', tail'

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

The following defined symbols remain to be analysed:
splitAt', fst', head', U71', U82', tail'

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

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

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

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

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

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

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

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

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

The following defined symbols remain to be analysed:
head'

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

No more defined symbols left to analyse.