PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd auto eq auto

Alph,St:Type, NDA:NDA(Alph;St). Fin(St) (x,y:St, a:Alph. Dec(NDA(x,a,y))) (S:Type. Fin(S) & (DA:Automata(Alph;S). L(NDA) = LangOf(DA)))
By: UnivCD
Generated subgoal:

11. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. Fin(St)
5. x,y:St, a:Alph. Dec(NDA(x,a,y))
S:Type. Fin(S) & (DA:Automata(Alph;S). L(NDA) = LangOf(DA))

About:
alluniverseimpliesapplyexistsand