Thm* S:ActionSet(), s,q:S.car. (n:. #(S.car)=n ) & (k:. (S:n0n1(k)s) = q) (L:*. (S:Ls) = q & (k:. L = n0n1(k))) n0n1_irregular

Thm* e:, L:*, n:. ||e:(Ln)|| = n||e:L|| counter_lpower

Thm* e:, L,M:*. ||e:L @ M|| = ||e:L||+||e:M|| counter_append

Thm* e:. ||e:nil|| = 0 counter_of_nil

Thm* n:, L:*. ||n:L|| el_counter_wf

Thm* n:. n0n1(n) * n0n1_wf

Thm* S:ActionSet(Alph), N:, s:S.car. #(S.car)=N (A:Alph*. N < ||A|| (a,b,c:Alph*. 0 < ||b|| & A = ((a @ b) @ c) & (k:. (S:(a @ (bk)) @ cs) = (S:As)))) pump_theorem

Thm* L:Alph*, n:. (Ln) = if n=0 nil else L @ (Ln-1) fi lpower_alt

Thm* Alph:Type, L:Alph*, n:. (Ln) Alph* lpower_wf

Thm* (0)! = 1 ex1_of_factorial

Thm* n:. (n)! factorial_wf

In prior sections: int 1 bool 1 int 2 list 1 finite sets list 3 autom