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
c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ]
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