PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: back listify

Alph:Type, 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))
By: RepD
Generated subgoal:

11. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. Fin(Alph)
5. Fin(S.car)
BL:S.car*. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act(a,t) = s)

About:
alluniverseimpliesexistslistequalapply