PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd auto eq auto 1 1 1
1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. Fin(St)
5. x,y:St, a:Alph. Dec(NDA(x,a,y))

Fin(St)
By: BackThru Thm* Fin(S) & Fin(T) Fin(ST)
Generated subgoal:

1 Fin()

About:
functionbooluniverseallapply