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'}
Id	Def Id == Atom
	Thm* Id  Type
d-single-init	Def @i: x:T initially x = v(j) Def == if eqof(IdDeq)(j,i) x : T initially x = v else  fi
m-sys-at	Def @i: A(j) == if j = i A else  fi
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
es-E	Def E == 1of(es)
es-first	Def first(e) Def == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of( Def == 1of(es))))))))))))))) Def == (e)
es-loc	Def loc(e) == 1of(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)
ma-single-init	Def x : t initially x = v == mk-ma(x : t; ; x : v; ; ; ; ; )

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