Some definitions of interest.
fair-fifo	Def FairFifo Def == (i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List) Def == & (i:Id, t:. Def == & (isnull(a(i;t)) Def == & ( Def == & ((x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x)) Def == & (& m(i;t) = nil  Msg List) Def == & (i:Id, t:, l:IdLnk. Def == & (isrcv(l;a(i;t)) Def == & ( Def == & (destination(l) = i Def == & (& ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg) Def == & (l:IdLnk, t:. Def == & (t':.  Def == & (tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List)
w-E	Def E == {p:(Id)| isnull(a(1of(p);2of(p))) }
w-sender	Def sender(e) == <source(lnk(kind(e))),mu(t.match(lnk(kind(e));t;time(e)))>
world	Def World Def == T:IdIdType Def == TA:IdIdType Def == M:IdLnkIdType Def == (i:Id(x:IdT(i,x)))(i:Idaction(w-action-dec(TA;M;i))) Def == (i:Id({m:Msg(M)| source(mlnk(m)) = i } List))Top
	Thm* World  Type{i'}
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
isrcv	Def isrcv(k) == isl(k)
	Thm* k:Knd. isrcv(k)
nat_plus	Def  == {i:| 0<i }
	Thm*   Type
rel_exp	Def R^n == if n=0 x,y. x = y  T else x,y. z:T. (x R z) & (z R^n-1 y) fi Def (recursive)
	Thm* n:, T:Type, R:(TTProp). R^n  TTProp
w-ekind	Def kind(e) == kind(act(e))
w-locl	Def e <loc e' == loc(e) = loc(e')  Id & time(e)<time(e')
w-time	Def time(e) == 2of(e)

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