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

and(tt, T) → T
isNatIList(IL) → isNatList(activate(IL))
isNat(n__0) → tt
isNat(n__s(N)) → isNat(activate(N))
isNat(n__length(L)) → isNatList(activate(L))
isNatIList(n__zeros) → tt
isNatIList(n__cons(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
isNatList(n__nil) → tt
isNatList(n__cons(N, L)) → and(isNat(activate(N)), isNatList(activate(L)))
isNatList(n__take(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
zeros → cons(0, n__zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL) → cons(activate(N), n__take(activate(M), activate(IL)))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L) → s(length(activate(L)))
0 → n__0
s(X) → n__s(X)
length(X) → n__length(X)
zeros → n__zeros
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
take(X1, X2) → n__take(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(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:

and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__length'(X)) → length'(activate'(X))
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(activate'(X1), activate'(X2))
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__length'(X)) → length'(activate'(X))
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(activate'(X1), activate'(X2))
activate'(X) → X

Types:
and' :: tt' → tt' → tt'
tt' :: tt'
isNatIList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
isNatList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
activate' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
isNat' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
n__0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake1' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake2' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uLength' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_hole_tt'1 :: tt'
_hole_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'2 :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3 :: Nat → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'

Heuristically decided to analyse the following defined symbols:
isNatIList', isNatList', activate', isNat', length'

They will be analysed ascendingly in the following order:
isNatIList' = isNatList'
isNatIList' = activate'
isNatIList' = isNat'
isNatIList' = length'
isNatList' = activate'
isNatList' = isNat'
isNatList' = length'
activate' = isNat'
activate' = length'
isNat' = length'

Generator Equations:
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0) ⇔ n__0'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(x))

The following defined symbols remain to be analysed:
isNatList', isNatIList', activate', isNat', length'

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

The following defined symbols remain to be analysed:
isNat', isNatIList', activate', length'

Proved the following rewrite lemma:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41)) → tt', rt ∈ Ω(1 + _n41)

Induction Base:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0)) →_R^Ω(1)
tt'

Induction Step:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(_$n42, 1))) →_R^Ω(1)
isNat'(activate'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_$n42))) →_R^Ω(1)
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_$n42)) →_IH
tt'

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

Lemmas:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41)) → tt', rt ∈ Ω(1 + _n41)

The following defined symbols remain to be analysed:
activate', isNatIList', isNatList', length'

Proved the following rewrite lemma:
activate'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41101)) → _gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41101), rt ∈ Ω(1 + _n41101)

Induction Base:
activate'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0)) →_R^Ω(1)
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0)

Induction Step:
activate'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(_$n41102, 1))) →_R^Ω(1)
s'(activate'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_$n41102))) →_IH
s'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_$n41102)) →_R^Ω(1)
n__s'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_$n41102))

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

Lemmas:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41)) → tt', rt ∈ Ω(1 + _n41)
activate'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41101)) → _gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41101), rt ∈ Ω(1 + _n41101)

The following defined symbols remain to be analysed:
length', isNatIList', isNatList', isNat'

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

The following defined symbols remain to be analysed:
isNatIList', isNatList', isNat'

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

The following defined symbols remain to be analysed:
isNatList', isNat'

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

The following defined symbols remain to be analysed:
isNat'

Proved the following rewrite lemma:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n48333)) → tt', rt ∈ Ω(1 + _n48333 + _n48333²)

Induction Base:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0)) →_R^Ω(1)
tt'

Induction Step:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(_$n48334, 1))) →_R^Ω(1)
isNat'(activate'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_$n48334))) →_L^{Ω(1 + _$n48334)}
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_$n48334)) →_IH
tt'

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

Lemmas:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n48333)) → tt', rt ∈ Ω(1 + _n48333 + _n48333²)
activate'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41101)) → _gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41101), rt ∈ Ω(1 + _n41101)

No more defined symbols left to analyse.

The lowerbound Ω(n²) was proven with the following lemma:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n48333)) → tt', rt ∈ Ω(1 + _n48333 + _n48333²)