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

a__and(tt, T) → mark(T)
a__isNatIList(IL) → a__isNatList(IL)
a__isNat(0) → tt
a__isNat(s(N)) → a__isNat(N)
a__isNat(length(L)) → a__isNatList(L)
a__isNatIList(zeros) → tt
a__isNatIList(cons(N, IL)) → a__and(a__isNat(N), a__isNatIList(IL))
a__isNatList(nil) → tt
a__isNatList(cons(N, L)) → a__and(a__isNat(N), a__isNatList(L))
a__isNatList(take(N, IL)) → a__and(a__isNat(N), a__isNatIList(IL))
a__zeros → cons(0, zeros)
a__take(0, IL) → a__uTake1(a__isNatIList(IL))
a__uTake1(tt) → nil
a__take(s(M), cons(N, IL)) → a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL)
a__uTake2(tt, M, N, IL) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)
a__uLength(tt, L) → s(a__length(mark(L)))
mark(and(X1, X2)) → a__and(mark(X1), mark(X2))
mark(isNatIList(X)) → a__isNatIList(X)
mark(isNatList(X)) → a__isNatList(X)
mark(isNat(X)) → a__isNat(X)
mark(length(X)) → a__length(mark(X))
mark(zeros) → a__zeros
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(uTake1(X)) → a__uTake1(mark(X))
mark(uTake2(X1, X2, X3, X4)) → a__uTake2(mark(X1), X2, X3, X4)
mark(uLength(X1, X2)) → a__uLength(mark(X1), X2)
mark(tt) → tt
mark(0) → 0
mark(s(X)) → s(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
a__and(X1, X2) → and(X1, X2)
a__isNatIList(X) → isNatIList(X)
a__isNatList(X) → isNatList(X)
a__isNat(X) → isNat(X)
a__length(X) → length(X)
a__zeros → zeros
a__take(X1, X2) → take(X1, X2)
a__uTake1(X) → uTake1(X)
a__uTake2(X1, X2, X3, X4) → uTake2(X1, X2, X3, X4)
a__uLength(X1, X2) → uLength(X1, X2)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

a__and'(tt', T) → mark'(T)
a__isNatIList'(IL) → a__isNatList'(IL)
a__isNat'(0') → tt'
a__isNat'(s'(N)) → a__isNat'(N)
a__isNat'(length'(L)) → a__isNatList'(L)
a__isNatIList'(zeros') → tt'
a__isNatIList'(cons'(N, IL)) → a__and'(a__isNat'(N), a__isNatIList'(IL))
a__isNatList'(nil') → tt'
a__isNatList'(cons'(N, L)) → a__and'(a__isNat'(N), a__isNatList'(L))
a__isNatList'(take'(N, IL)) → a__and'(a__isNat'(N), a__isNatIList'(IL))
a__zeros' → cons'(0', zeros')
a__take'(0', IL) → a__uTake1'(a__isNatIList'(IL))
a__uTake1'(tt') → nil'
a__take'(s'(M), cons'(N, IL)) → a__uTake2'(a__and'(a__isNat'(M), a__and'(a__isNat'(N), a__isNatIList'(IL))), M, N, IL)
a__uTake2'(tt', M, N, IL) → cons'(mark'(N), take'(M, IL))
a__length'(cons'(N, L)) → a__uLength'(a__and'(a__isNat'(N), a__isNatList'(L)), L)
a__uLength'(tt', L) → s'(a__length'(mark'(L)))
mark'(and'(X1, X2)) → a__and'(mark'(X1), mark'(X2))
mark'(isNatIList'(X)) → a__isNatIList'(X)
mark'(isNatList'(X)) → a__isNatList'(X)
mark'(isNat'(X)) → a__isNat'(X)
mark'(length'(X)) → a__length'(mark'(X))
mark'(zeros') → a__zeros'
mark'(take'(X1, X2)) → a__take'(mark'(X1), mark'(X2))
mark'(uTake1'(X)) → a__uTake1'(mark'(X))
mark'(uTake2'(X1, X2, X3, X4)) → a__uTake2'(mark'(X1), X2, X3, X4)
mark'(uLength'(X1, X2)) → a__uLength'(mark'(X1), X2)
mark'(tt') → tt'
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(nil') → nil'
a__and'(X1, X2) → and'(X1, X2)
a__isNatIList'(X) → isNatIList'(X)
a__isNatList'(X) → isNatList'(X)
a__isNat'(X) → isNat'(X)
a__length'(X) → length'(X)
a__zeros' → zeros'
a__take'(X1, X2) → take'(X1, X2)
a__uTake1'(X) → uTake1'(X)
a__uTake2'(X1, X2, X3, X4) → uTake2'(X1, X2, X3, X4)
a__uLength'(X1, X2) → uLength'(X1, X2)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__and'(tt', T) → mark'(T)
a__isNatIList'(IL) → a__isNatList'(IL)
a__isNat'(0') → tt'
a__isNat'(s'(N)) → a__isNat'(N)
a__isNat'(length'(L)) → a__isNatList'(L)
a__isNatIList'(zeros') → tt'
a__isNatIList'(cons'(N, IL)) → a__and'(a__isNat'(N), a__isNatIList'(IL))
a__isNatList'(nil') → tt'
a__isNatList'(cons'(N, L)) → a__and'(a__isNat'(N), a__isNatList'(L))
a__isNatList'(take'(N, IL)) → a__and'(a__isNat'(N), a__isNatIList'(IL))
a__zeros' → cons'(0', zeros')
a__take'(0', IL) → a__uTake1'(a__isNatIList'(IL))
a__uTake1'(tt') → nil'
a__take'(s'(M), cons'(N, IL)) → a__uTake2'(a__and'(a__isNat'(M), a__and'(a__isNat'(N), a__isNatIList'(IL))), M, N, IL)
a__uTake2'(tt', M, N, IL) → cons'(mark'(N), take'(M, IL))
a__length'(cons'(N, L)) → a__uLength'(a__and'(a__isNat'(N), a__isNatList'(L)), L)
a__uLength'(tt', L) → s'(a__length'(mark'(L)))
mark'(and'(X1, X2)) → a__and'(mark'(X1), mark'(X2))
mark'(isNatIList'(X)) → a__isNatIList'(X)
mark'(isNatList'(X)) → a__isNatList'(X)
mark'(isNat'(X)) → a__isNat'(X)
mark'(length'(X)) → a__length'(mark'(X))
mark'(zeros') → a__zeros'
mark'(take'(X1, X2)) → a__take'(mark'(X1), mark'(X2))
mark'(uTake1'(X)) → a__uTake1'(mark'(X))
mark'(uTake2'(X1, X2, X3, X4)) → a__uTake2'(mark'(X1), X2, X3, X4)
mark'(uLength'(X1, X2)) → a__uLength'(mark'(X1), X2)
mark'(tt') → tt'
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(nil') → nil'
a__and'(X1, X2) → and'(X1, X2)
a__isNatIList'(X) → isNatIList'(X)
a__isNatList'(X) → isNatList'(X)
a__isNat'(X) → isNat'(X)
a__length'(X) → length'(X)
a__zeros' → zeros'
a__take'(X1, X2) → take'(X1, X2)
a__uTake1'(X) → uTake1'(X)
a__uTake2'(X1, X2, X3, X4) → uTake2'(X1, X2, X3, X4)
a__uLength'(X1, X2) → uLength'(X1, X2)

Types:
a__and' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
tt' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
mark' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
a__isNatIList' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
a__isNatList' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
a__isNat' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
0' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
s' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
length' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
zeros' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
cons' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
nil' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
take' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
a__zeros' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
a__take' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
a__uTake1' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
a__uTake2' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
a__length' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
a__uLength' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
and' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
isNatIList' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
isNatList' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
isNat' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
uTake1' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
uTake2' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
uLength' :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength' → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
_hole_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'1 :: tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'
_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2 :: Nat → tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'

Heuristically decided to analyse the following defined symbols:
a__and', mark', a__isNatIList', a__isNatList', a__isNat', a__length', a__uLength'

They will be analysed ascendingly in the following order:
a__and' = mark'
a__and' = a__isNatIList'
a__and' = a__isNatList'
a__and' = a__isNat'
a__and' = a__length'
a__and' = a__uLength'
mark' = a__isNatIList'
mark' = a__isNatList'
mark' = a__isNat'
mark' = a__length'
mark' = a__uLength'
a__isNatIList' = a__isNatList'
a__isNatIList' = a__isNat'
a__isNatIList' = a__length'
a__isNatIList' = a__uLength'
a__isNatList' = a__isNat'
a__isNatList' = a__length'
a__isNatList' = a__uLength'
a__isNat' = a__length'
a__isNat' = a__uLength'
a__length' = a__uLength'

Generator Equations:
_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(0) ⇔ tt'
_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(+(x, 1)) ⇔ s'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(x))

The following defined symbols remain to be analysed:
mark', a__and', a__isNatIList', a__isNatList', a__isNat', a__length', a__uLength'

Proved the following rewrite lemma:
mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_n4)) → _gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_n4), rt ∈ Ω(1 + _n4)

Induction Base:
mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(0)) →_R^Ω(1)
tt'

Induction Step:
mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(+(_$n5, 1))) →_R^Ω(1)
s'(mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_$n5))) →_IH
s'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_$n5))

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

The following defined symbols remain to be analysed:
a__and', a__isNatIList', a__isNatList', a__isNat', a__length', a__uLength'

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

The following defined symbols remain to be analysed:
a__isNatIList', a__isNatList', a__isNat', a__length', a__uLength'

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

The following defined symbols remain to be analysed:
a__isNatList', a__isNat', a__length', a__uLength'

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

The following defined symbols remain to be analysed:
a__isNat', a__length', a__uLength'

Proved the following rewrite lemma:
a__isNat'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(+(1, _n564179))) → _*3, rt ∈ Ω(_n564179)

Induction Base:
a__isNat'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(+(1, 0)))

Induction Step:
a__isNat'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(+(1, +(_$n564180, 1)))) →_R^Ω(1)
a__isNat'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(+(1, _$n564180))) →_IH
_*3

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

Lemmas:
mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_n4)) → _gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_n4), rt ∈ Ω(1 + _n4)
a__isNat'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(+(1, _n564179))) → _*3, rt ∈ Ω(_n564179)

The following defined symbols remain to be analysed:
a__length', a__and', mark', a__isNatIList', a__isNatList', a__uLength'

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

The following defined symbols remain to be analysed:
a__uLength', a__and', mark', a__isNatIList', a__isNatList'

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

The following defined symbols remain to be analysed:
mark', a__and', a__isNatIList', a__isNatList'

Proved the following rewrite lemma:
mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_n567252)) → _gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_n567252), rt ∈ Ω(1 + _n567252)

Induction Base:
mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(0)) →_R^Ω(1)
tt'

Induction Step:
mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(+(_$n567253, 1))) →_R^Ω(1)
s'(mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_$n567253))) →_IH
s'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_$n567253))

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

Lemmas:
mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_n567252)) → _gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_n567252), rt ∈ Ω(1 + _n567252)
a__isNat'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(+(1, _n564179))) → _*3, rt ∈ Ω(_n564179)

The following defined symbols remain to be analysed:
a__and', a__isNatIList', a__isNatList'

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

The following defined symbols remain to be analysed:
a__isNatIList', a__isNatList'

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

The following defined symbols remain to be analysed:
a__isNatList'

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
mark'(_gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_n567252)) → _gen_tt':0':s':length':zeros':cons':nil':take':and':isNatIList':isNatList':isNat':uTake1':uTake2':uLength'2(_n567252), rt ∈ Ω(1 + _n567252)