Some definitions of interest.
d-feasible	Def d-feasible(D) Def == (i:Id. Feasible(M(i))) Def == & (l:IdLnk, tg:Id. Def == & (M(source(l)).dout(l,tg) r 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-list	Def (L) == reduce(A,B. A  B;;L)
Id	Def Id == Atom
	Thm* Id  Type
once	Def once(loc;a;i) Def == if loc = i Def == if [ma-single-pre-init1("done";;false;a;Unit;x,v.x);  Def == if [only members of [locl(a)] affect "done" :;  Def == if [ma-single-effect0("done";;locl(a);Unit;x,v. true)] Def == else nil fi
	Thm* loc,a,i:Id. once(loc;a;i)  MsgA List

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