is mentioned by

Thm* D:Dsys, L:Id List. Thm* (i:Id. (i  L)  ma-is-empty(M(i))) Thm*  Thm* (i:Id. Feasible(M(i))) Thm*  Thm* (iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg))  L) Thm* (iL.(ltgma-outlinks(M(i);i). Thm* interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg))))) Thm*  Thm* d-feasible(D)	[finite-support-feasible]
Thm* A:Dsys, i,a:Id. Dec(a declared in M(i))	[decidable__ma-decla]
Thm* A:Dsys, i,a:Id. a declared in M(i)  Prop	[ma-decla_wf2]

In prior sections: mb event system 5

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html