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

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