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
s) == if null(L)
s else S.act(hd(L),(S:tl(L)s)) fi (recursive)
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* S:ActionSet(T), s:S.car, tl1,tl2:T*. (S:tl1 @ tl2s) = (S:tl1(S:tl2s))
action_append
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
Thm* S:ActionSet(Alph), s:S.car, L1,L2,L:Alph*.
(S:L1s) = (S:L2s) (S:L @ L1s) = (S:L @ L2s)
maction_lemma