PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: total back listify

Alph:Type, S:ActionSet(Alph), sL:S.car*. Fin(Alph) Fin(S.car) (TBL:S.car*. s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL)))
By: RepD
Generated subgoal:

11. Alph: Type
2. S: ActionSet(Alph)
3. sL: S.car*
4. Fin(Alph)
5. Fin(S.car)
TBL:S.car*. s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))

About:
alluniverselistimpliesexists