Thm* S:ActionSet(Alph), s:S.car. Fin(Alph) Fin(S.car) (BL:S.car*. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act(a,t) = s)) back_listify

In prior sections: det automata