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)))
nd_auto_eq_auto
AlphStates)
States(States
)
Thm* 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)))
nd_auto_eq_auto
In prior sections: det automata