Definitions mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
d-feasibleDef d-feasible(D)
Def == (i:Id. Feasible(M(i)))
Def == & (l:IdLnk, tg:Id.
Def == & (M(source(l)).dout(l,tgr M(destination(l)).din(l,tg))
Def == & (i:Id. 
Def == & (finite-type({l:IdLnk
Def == & (finite-type({| destination(l) = i & M(source(l)) sends on link l }))
ma-join-listDef (L) == reduce(A,BA  B;;L)
KndDef Knd == (IdLnkId)+Id
Thm* Knd  Type
IdDef Id == Atom
Thm* Id  Type
recognizer1Def recognizer1(loc;T;A;P;k;i;r;x)
Def == if loc = i
Def == if [r :  initially r = false
Def == if [only members of [k] affect r :
Def == if [ma-single-effect1(r;;x;A;k;T;r,x,vP(x,v r)]
Def == else nil fi
Thm* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id.
Thm* A  T  x = r  recognizer1(loc;T;A;P;k;i;r;x MsgA List
notDef A == A  False
Thm* A:Prop. (A Prop

About:
productlistconsnilboolbfalseifthenelseatom
unionsetlambdaapplyfunctionuniverseequal
membersubtype_relpropimpliesandfalseall
!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb event system 7 Sections EventSystems Doc