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(n__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__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(n__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)
s(X) → n__s(X)
isLNat(X) → n__isLNat(X)
niln__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)
0n__0
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)
isNatural(X) → n__isNatural(X)
activate(n__natsFrom(X)) → natsFrom(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__isLNat(X)) → isLNat(X)
activate(n__nil) → nil
activate(n__afterNth(X1, X2)) → afterNth(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__fst(X)) → fst(activate(X))
activate(n__snd(X)) → snd(activate(X))
activate(n__tail(X)) → tail(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(n__pair(X1, X2)) → pair(activate(X1), activate(X2))
activate(n__splitAt(X1, X2)) → splitAt(activate(X1), activate(X2))
activate(n__and(X1, X2)) → and(activate(X1), X2)
activate(n__isNatural(X)) → isNatural(X)
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'(n__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__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'(n__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)
s'(X) → n__s'(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'
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)
isNatural'(X) → n__isNatural'(X)
activate'(n__natsFrom'(X)) → natsFrom'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__isLNat'(X)) → isLNat'(X)
activate'(n__nil') → nil'
activate'(n__afterNth'(X1, X2)) → afterNth'(activate'(X1), activate'(X2))
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__fst'(X)) → fst'(activate'(X))
activate'(n__snd'(X)) → snd'(activate'(X))
activate'(n__tail'(X)) → tail'(activate'(X))
activate'(n__take'(X1, X2)) → take'(activate'(X1), activate'(X2))
activate'(n__0') → 0'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__pair'(X1, X2)) → pair'(activate'(X1), activate'(X2))
activate'(n__splitAt'(X1, X2)) → splitAt'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNatural'(X)) → isNatural'(X)
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'(n__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__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'(n__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)
s'(X) → n__s'(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'
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)
isNatural'(X) → n__isNatural'(X)
activate'(n__natsFrom'(X)) → natsFrom'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__isLNat'(X)) → isLNat'(X)
activate'(n__nil') → nil'
activate'(n__afterNth'(X1, X2)) → afterNth'(activate'(X1), activate'(X2))
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__fst'(X)) → fst'(activate'(X))
activate'(n__snd'(X)) → snd'(activate'(X))
activate'(n__tail'(X)) → tail'(activate'(X))
activate'(n__take'(X1, X2)) → take'(activate'(X1), activate'(X2))
activate'(n__0') → 0'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__pair'(X1, X2)) → pair'(activate'(X1), activate'(X2))
activate'(n__splitAt'(X1, X2)) → splitAt'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNatural'(X)) → isNatural'(X)
activate'(X) → X

Types:

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' = afterNth'
fst' = U71'
fst' = U82'
fst' = and'
fst' = isNatural'
fst' = isLNat'
fst' = isPLNat'
fst' = natsFrom'
fst' = tail'
splitAt' = activate'
splitAt' = snd'
splitAt' = afterNth'
splitAt' = U71'
splitAt' = U82'
splitAt' = and'
splitAt' = isNatural'
splitAt' = isLNat'
splitAt' = isPLNat'
splitAt' = natsFrom'
splitAt' = tail'
activate' = snd'
activate' = afterNth'
activate' = U71'
activate' = U82'
activate' = and'
activate' = isNatural'
activate' = isLNat'
activate' = isPLNat'
activate' = natsFrom'
activate' = tail'
snd' = afterNth'
snd' = U71'
snd' = U82'
snd' = and'
snd' = isNatural'
snd' = isLNat'
snd' = isPLNat'
snd' = natsFrom'
snd' = 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'

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'(n__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__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'(n__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)
s'(X) → n__s'(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'
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)
isNatural'(X) → n__isNatural'(X)
activate'(n__natsFrom'(X)) → natsFrom'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__isLNat'(X)) → isLNat'(X)
activate'(n__nil') → nil'
activate'(n__afterNth'(X1, X2)) → afterNth'(activate'(X1), activate'(X2))
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__fst'(X)) → fst'(activate'(X))
activate'(n__snd'(X)) → snd'(activate'(X))
activate'(n__tail'(X)) → tail'(activate'(X))
activate'(n__take'(X1, X2)) → take'(activate'(X1), activate'(X2))
activate'(n__0') → 0'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__pair'(X1, X2)) → pair'(activate'(X1), activate'(X2))
activate'(n__splitAt'(X1, X2)) → splitAt'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNatural'(X)) → isNatural'(X)
activate'(X) → X

Types:

Generator Equations:

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

They will be analysed ascendingly in the following order:
fst' = splitAt'
fst' = activate'
fst' = snd'
fst' = afterNth'
fst' = U71'
fst' = U82'
fst' = and'
fst' = isNatural'
fst' = isLNat'
fst' = isPLNat'
fst' = natsFrom'
fst' = tail'
splitAt' = activate'
splitAt' = snd'
splitAt' = afterNth'
splitAt' = U71'
splitAt' = U82'
splitAt' = and'
splitAt' = isNatural'
splitAt' = isLNat'
splitAt' = isPLNat'
splitAt' = natsFrom'
splitAt' = tail'
activate' = snd'
activate' = afterNth'
activate' = U71'
activate' = U82'
activate' = and'
activate' = isNatural'
activate' = isLNat'
activate' = isPLNat'
activate' = natsFrom'
activate' = tail'
snd' = afterNth'
snd' = U71'
snd' = U82'
snd' = and'
snd' = isNatural'
snd' = isLNat'
snd' = isPLNat'
snd' = natsFrom'
snd' = 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'

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

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'(n__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__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'(n__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)
s'(X) → n__s'(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'
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)
isNatural'(X) → n__isNatural'(X)
activate'(n__natsFrom'(X)) → natsFrom'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__isLNat'(X)) → isLNat'(X)
activate'(n__nil') → nil'
activate'(n__afterNth'(X1, X2)) → afterNth'(activate'(X1), activate'(X2))
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__fst'(X)) → fst'(activate'(X))
activate'(n__snd'(X)) → snd'(activate'(X))
activate'(n__tail'(X)) → tail'(activate'(X))
activate'(n__take'(X1, X2)) → take'(activate'(X1), activate'(X2))
activate'(n__0') → 0'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__pair'(X1, X2)) → pair'(activate'(X1), activate'(X2))
activate'(n__splitAt'(X1, X2)) → splitAt'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNatural'(X)) → isNatural'(X)
activate'(X) → X

Types:

Generator Equations:

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

They will be analysed ascendingly in the following order:
fst' = splitAt'
fst' = activate'
fst' = snd'
fst' = afterNth'
fst' = U71'
fst' = U82'
fst' = and'
fst' = isNatural'
fst' = isLNat'
fst' = isPLNat'
fst' = natsFrom'
fst' = tail'
splitAt' = activate'
splitAt' = snd'
splitAt' = afterNth'
splitAt' = U71'
splitAt' = U82'
splitAt' = and'
splitAt' = isNatural'
splitAt' = isLNat'
splitAt' = isPLNat'
splitAt' = natsFrom'
splitAt' = tail'
activate' = snd'
activate' = afterNth'
activate' = U71'
activate' = U82'
activate' = and'
activate' = isNatural'
activate' = isLNat'
activate' = isPLNat'
activate' = natsFrom'
activate' = tail'
snd' = afterNth'
snd' = U71'
snd' = U82'
snd' = and'
snd' = isNatural'
snd' = isLNat'
snd' = isPLNat'
snd' = natsFrom'
snd' = 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'

Proved the following rewrite lemma:
activate'(_gen_tt':n__s':n__natsFrom':n__isLNat':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__sel':n__pair':n__splitAt':n__isNatural':n__and'2(+(1, _n18))) → _*3, rt ∈ Ω(n18)

Induction Base:

Induction Step:
natsFrom'(_*3)

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

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'(n__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__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'(n__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)
s'(X) → n__s'(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'
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)
isNatural'(X) → n__isNatural'(X)
activate'(n__natsFrom'(X)) → natsFrom'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__isLNat'(X)) → isLNat'(X)
activate'(n__nil') → nil'
activate'(n__afterNth'(X1, X2)) → afterNth'(activate'(X1), activate'(X2))
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__fst'(X)) → fst'(activate'(X))
activate'(n__snd'(X)) → snd'(activate'(X))
activate'(n__tail'(X)) → tail'(activate'(X))
activate'(n__take'(X1, X2)) → take'(activate'(X1), activate'(X2))
activate'(n__0') → 0'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__pair'(X1, X2)) → pair'(activate'(X1), activate'(X2))
activate'(n__splitAt'(X1, X2)) → splitAt'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNatural'(X)) → isNatural'(X)
activate'(X) → X

Types:

Lemmas:
activate'(_gen_tt':n__s':n__natsFrom':n__isLNat':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__sel':n__pair':n__splitAt':n__isNatural':n__and'2(+(1, _n18))) → _*3, rt ∈ Ω(n18)

Generator Equations:

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

They will be analysed ascendingly in the following order:
fst' = splitAt'
fst' = activate'
fst' = snd'
fst' = afterNth'
fst' = U71'
fst' = U82'
fst' = and'
fst' = isNatural'
fst' = isLNat'
fst' = isPLNat'
fst' = natsFrom'
fst' = tail'
splitAt' = activate'
splitAt' = snd'
splitAt' = afterNth'
splitAt' = U71'
splitAt' = U82'
splitAt' = and'
splitAt' = isNatural'
splitAt' = isLNat'
splitAt' = isPLNat'
splitAt' = natsFrom'
splitAt' = tail'
activate' = snd'
activate' = afterNth'
activate' = U71'
activate' = U82'
activate' = and'
activate' = isNatural'
activate' = isLNat'
activate' = isPLNat'
activate' = natsFrom'
activate' = tail'
snd' = afterNth'
snd' = U71'
snd' = U82'
snd' = and'
snd' = isNatural'
snd' = isLNat'
snd' = isPLNat'
snd' = natsFrom'
snd' = 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'

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

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'(n__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__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'(n__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)
s'(X) → n__s'(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'
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)
isNatural'(X) → n__isNatural'(X)
activate'(n__natsFrom'(X)) → natsFrom'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__isLNat'(X)) → isLNat'(X)
activate'(n__nil') → nil'
activate'(n__afterNth'(X1, X2)) → afterNth'(activate'(X1), activate'(X2))
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__fst'(X)) → fst'(activate'(X))
activate'(n__snd'(X)) → snd'(activate'(X))
activate'(n__tail'(X)) → tail'(activate'(X))
activate'(n__take'(X1, X2)) → take'(activate'(X1), activate'(X2))
activate'(n__0') → 0'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__pair'(X1, X2)) → pair'(activate'(X1), activate'(X2))
activate'(n__splitAt'(X1, X2)) → splitAt'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNatural'(X)) → isNatural'(X)
activate'(X) → X

Types:

Lemmas:
activate'(_gen_tt':n__s':n__natsFrom':n__isLNat':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__sel':n__pair':n__splitAt':n__isNatural':n__and'2(+(1, _n18))) → _*3, rt ∈ Ω(n18)

Generator Equations:

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

They will be analysed ascendingly in the following order:
fst' = splitAt'
fst' = activate'
fst' = snd'
fst' = afterNth'
fst' = U71'
fst' = U82'
fst' = and'
fst' = isNatural'
fst' = isLNat'
fst' = isPLNat'
fst' = natsFrom'
fst' = tail'
splitAt' = activate'
splitAt' = snd'
splitAt' = afterNth'
splitAt' = U71'
splitAt' = U82'
splitAt' = and'
splitAt' = isNatural'
splitAt' = isLNat'
splitAt' = isPLNat'
splitAt' = natsFrom'
splitAt' = tail'
activate' = snd'
activate' = afterNth'
activate' = U71'
activate' = U82'
activate' = and'
activate' = isNatural'
activate' = isLNat'
activate' = isPLNat'
activate' = natsFrom'
activate' = tail'
snd' = afterNth'
snd' = U71'
snd' = U82'
snd' = and'
snd' = isNatural'
snd' = isLNat'
snd' = isPLNat'
snd' = natsFrom'
snd' = 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'

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

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'(n__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__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'(n__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)
s'(X) → n__s'(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'
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)
isNatural'(X) → n__isNatural'(X)
activate'(n__natsFrom'(X)) → natsFrom'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__isLNat'(X)) → isLNat'(X)
activate'(n__nil') → nil'
activate'(n__afterNth'(X1, X2)) → afterNth'(activate'(X1), activate'(X2))
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__fst'(X)) → fst'(activate'(X))
activate'(n__snd'(X)) → snd'(activate'(X))
activate'(n__tail'(X)) → tail'(activate'(X))
activate'(n__take'(X1, X2)) → take'(activate'(X1), activate'(X2))
activate'(n__0') → 0'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__pair'(X1, X2)) → pair'(activate'(X1), activate'(X2))
activate'(n__splitAt'(X1, X2)) → splitAt'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNatural'(X)) → isNatural'(X)
activate'(X) → X

Types:

Lemmas:
activate'(_gen_tt':n__s':n__natsFrom':n__isLNat':n__nil':n__afterNth':n__cons':n__fst':n__snd':n__tail':n__take':n__0':n__head':n__sel':n__pair':n__splitAt':n__isNatural':n__and'2(+(1, _n18))) → _*3, rt ∈ Ω(n18)

Generator Equations:

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

They will be analysed ascendingly in the following order:
fst' = splitAt'
fst' = activate'
fst' = snd'
fst' = afterNth'
fst' = U71'
fst' = U82'
fst' = and'
fst' = isNatural'
fst' = isLNat'
fst' = isPLNat'
fst' = natsFrom'
fst' = tail'
splitAt' = activate'
splitAt' = snd'
splitAt' = afterNth'
splitAt' = U71'
splitAt' = U82'
splitAt' = and'
splitAt' = isNatural'
splitAt' = isLNat'
splitAt' = isPLNat'
splitAt' = natsFrom'
splitAt' = tail'
activate' = snd'
activate' = afterNth'
activate' = U71'
activate' = U82'
activate' = and'
activate' = isNatural'
activate' = isLNat'
activate' = isPLNat'
activate' = natsFrom'
activate' = tail'
snd' = afterNth'
snd' = U71'
snd' = U82'
snd' = and'
snd' = isNatural'
snd' = isLNat'
snd' = isPLNat'
snd' = natsFrom'
snd' = 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'