e:
, L,M:*. ||e:L @ M|| = ||e:L||+||e:M|| 
counter_append
bs ; a.as' a.(as' @ bs) (recursive)
Thm* e:, L,M:*. ||e:L @ M|| = ||e:L||+||e:M|| counter_append
Thm* S:ActionSet(T), s:S.car, tl1,tl2:T*. (S:tl1 @ tl2
s) = (S:tl1(S:tl2s))
action_append
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* L:Alph*, n:. (Ln) = if n=
0 nil else L @ (Ln-1) fi lpower_alt
Thm* S:ActionSet(Alph), s:S.car, L1,L2,L:Alph*.
(S:L1s) = (S:L2s) (S:L @ L1s) = (S:L @ L2s)
maction_lemma
In prior sections: list 1 list 3 autom