n:
, Alph:Type, S:ActionSet(Alph), s,f:S.car.
#(S.car)=n 
(
l:Alph*. (S:l
s) = f) (l:Alph*. ||l||
n & (S:ls) = f)
pump_thm_cor
0 ; a.as' ||as'||+1 (recursive)
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: list 1 finite sets list 3 autom