Nuprl - mb_event_system_6 LEMMAs for ma_DASH_single_DASH_effect_DASH

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
3	Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* xdom(ds). A=ds(x) A Thm* Thm* kdom(da). A=da(k) A Feasible(ma-single-effect(ds; da; k; x; f))	[ma-single-effect-feasible]
cites the following:
2	Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) (x L)	[assert-deq-member]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html