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
Alph* List
)| i:
(||C||-1). ||2of(C[i])|| > 0 }
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* Alph,St:Type, NDA:NDA(Alph;St), C:NComp(Alph;St), q:St. NDA(C) q 
Prop
nd_valcom_wf
Thm* Alph,St:Type, C:NComp(Alph;St), a:Alph, q:St. C+[a;q] NComp(Alph;St)
nd_comp_extend_wf
Thm* Alph,St:Type, q:St. [ < q,[] > ] NComp(Alph;St) nd_comp_init_wf
Thm* Alph,St:Type, C:NComp(Alph;St). ||C|| 
nd_comp_length_wf
Thm* Alph,St:Type, C:NComp(Alph;St). |C| Alph* nd_comp_car_wf