Nuprl - mb_event_system_6 LEMMAs for ma_DASH_single_DASH_effect0_DASH

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

Rank	Theorem	Name
4	Thm* x:Id, k:Knd, A,T:Type, f:(ATA). Thm* A T Feasible(ma-single-effect0(x;A;k;T;f))	[ma-single-effect0-feasible]
cites the following:
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]

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