Nuprl - mb_event_system_6 LEMMAs for ma_DASH_single_DASH_pre1_DASH

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

Theorem	Name
Thm* a:Id, T,A:Type, x:Id, P:(ATProp). Thm* T Thm* Thm* A Thm* Thm* (a:A. Dec(v:T. P(a,v))) Feasible(ma-single-pre1(x;A;a;T;x,v.P(x,v)))	[ma-single-pre1-feasible]
cites the following:
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). Thm* T Thm* Thm* xdom(ds). A=ds(x) A Thm* Thm* (s:State(ds). Dec(v:T. P(s,v))) Thm* Thm* Feasible((with ds: ds Thm* Faction a:T Thm* Fprecondition a(v) is Thm* FP s v))	[ma-single-pre-feasible]

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