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). NDA([ < I(NDA),[] > ]) I(NDA) nd_init_valcom

Thm* Alph,St:Type, NDA:NDA(Alph;St), C:NComp(Alph;St), q:St. NDA(C) q Prop nd_valcom_wf

Thm* NDA:NDA(Alph;St). NDA([ < I(NDA),[] > ]) I(NDA) nd_comp_init_thm

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

Thm* Alph,St:Type, NDA:NDA(Alph;St), l:Alph*, q:St. NDA(l)q Prop nd_compute_list_wf

Thm* Alph,States:Type, n:NDA(Alph;States). F(n) States NDA_fin_wf

Thm* Alph,States:Type, n:NDA(Alph;States). I(n) States NDA_init_wf

Thm* Alph,States:Type, n:NDA(Alph;States). n StatesAlphStatesProp NDA_act_wf