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
q
== I(NDA) = 1of(hd(C)) 
St
& (i:
(||C||-1).
NDA(1of(C[i]),hd(rev(2of(C[i]))),1of(C[(i+1)]))
& 2of(C[(i+1)]) = rev(tl(rev(2of(C[i])))) Alph*)
& 1of(hd(rev(C))) = q St
& 2of(hd(rev(C))) = nil Alph*
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* NDA:NDA(Alph;St). NDA([ < I(NDA),[] > ]) I(NDA) nd_comp_init_thm