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 }))
send-once	Def send-once(loc;T;A;a;f;tg;l;x) Def == [(once(loc;a;source(l)));  Def == [if loc = source(l) Def == [if ma-single-sends1(A; Unit; T; x; locl(a); l; tg; (a,b. [(f(a))])) Def == [else  fi]
ma-join-list	Def (L) == reduce(A,B. A  B;;L)
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
Id	Def Id == Atom
	Thm* Id  Type
lsrc	Def source(l) == 1of(l)
	Thm* l:IdLnk. source(l)  Id
mkid	Def x_n == <x,n>
	Thm* x:Atom, n:. x_n  Id
not	Def A == A  False
	Thm* A:Prop. (A)  Prop

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