action sets Sections AutomataTheory Doc

Def as @ bs == Case of as; nil 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 @ tl2s) = (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 @ (bk)) @ 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