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
== {i:| 0 < i }
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* n:, Alph:Type, S:ActionSet(Alph), s,f:S.car.
#(S.car)=n (l:Alph*. (S:ls) = f) (l:Alph*. ||l||
n & (S:ls) = f)
pump_thm_cor
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 @ (b
k)) @ cs) = (S:As))))
pump_theorem
In prior sections: int 1 int 2 finite sets