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: core int 1 bool 1 int 2 finite sets list 3 autom det automata exponent