Thm* NDA:NDA(Alph;St), C:NComp(Alph;St), q:St, a:Alph, p:St. NDA(C) q NDA(q,a,p) NDA(C+[a;p]) p nd_ext_valcom

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