Some definitions of interest.
d-realizes	Def D  Def realizes es.P(es) Def == D':Dsys.  Def == D  D'  (w:World, p:FairFifo. PossibleWorld(D';w)  P(ES(w)))
d-sub	Def D1  D2 == i:Id. M(i)  M(i)
dsys	Def Dsys == IdMsgA
	Thm* Dsys  Type{i'}
Knd	Def Knd == (IdLnkId)+Id
	Thm* Knd  Type
es-locl	Def (e <loc e') == loc(e) = loc(e')  Id & (e < e')
ma-state	Def State(ds) == x:Idds(x)?Top
Id	Def Id == Atom
	Thm* Id  Type
d-single-pre	Def @i (with ds: ds action a:T precondition a(v) is P s v)(j) Def == if eqof(IdDeq)(j,i) (with ds: ds action a:T precondition a(v) is P s v) Def == else  fi
es-E	Def E == 1of(es)
es-after	Def (x after e) Def == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))))(x,e)
es-valtype	Def valtype(e) == if isrcv(e) rcvtype(e) else acttype(e) fi
es-kind	Def kind(e) == 1of(2of(2of(2of(2of(2of(2of(2of(es))))))))(e)
es-loc	Def loc(e) == 1of(2of(2of(2of(2of(2of(2of(es)))))))(e)
es-val	Def val(e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))(e)
es-vartype	Def vartype(i;x) == 1of(2of(2of(es)))(i,x)
es-when	Def (x when e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es))))))))))(x,e)
fpf	Def a:A fp-> B(a) == d:A Lista:{a:A| (a  d) }B(a)
	Thm* A:Type, B:(AType). a:A fp-> B(a)  Type
fpf-cap	Def f(x)?z == if x  dom(f) f(x) else z fi
m-sys-at	Def @i: A(j) == if j = i A else  fi
id-deq	Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)
ma-single-pre	Def (with ds: ds Def (action a:T Def (precondition a(v) is Def (P s v) Def == mk-ma(ds; locl(a) : T; ; a : P; ; ; ; )
locl	Def locl(a) == inr(a)
	Thm* a:Id. locl(a)  Knd
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
top	Def Top == Void given Void
	Thm* Top  Type

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