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
B == 
B < A
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
In prior sections: int 1 bool 1 int 2 list 1 list 3 autom