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
n:
, f:(n
s). Bij(n; s; f)
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: finite sets list 3 autom det automata exponent