Some definitions of interest.
d-es	Def es is an event system of D Def == w:World, p:FairFifo. PossibleWorld(D;w) & es = ES(w)  ES
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-realizes2	Def D realizes2 es.P(es) == w:World, p:FairFifo. PossibleWorld(D;w)  P(ES(w))
dsys	Def Dsys == IdMsgA
	Thm* Dsys  Type{i'}
event_system	Def ES Def == E:Type Def == EqDecider(E)(T:IdIdType Def == EqDecider(E)(V:IdIdType Def == EqDecider(E)(M:IdLnkIdType Def == EqDecider(E)(Top(loc:EId Def == EqDecider(E)(Top(kind:EKnd Def == EqDecider(E)(Top(val:(e:Eeventtype(kind;loc;V;M;e)) Def == EqDecider(E)(Top(when:(x:Ide:ET(loc(e),x)) Def == EqDecider(E)(Top(after:(x:Ide:ET(loc(e),x)) Def == EqDecider(E)(Top(sends:(l:IdLnkE(Msg_sub(l; M) List)) Def == EqDecider(E)(Top(sender:{e:E| isrcv(kind(e)) }E Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||sends Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||(lnk(kind(e)) Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||,sender(e))||) Def == EqDecider(E)(Top(first:E Def == EqDecider(E)(Top(pred:{e':E| (first(e')) }E Def == EqDecider(E)(Top(causl:EEProp Def == EqDecider(E)(Top(ESAxioms{i:l} Def == EqDecider(E)(Top(ESAxioms(E; Def == EqDecider(E)(Top(ESAxioms(T; Def == EqDecider(E)(Top(ESAxioms(M; Def == EqDecider(E)(Top(ESAxioms(loc; Def == EqDecider(E)(Top(ESAxioms(kind; Def == EqDecider(E)(Top(ESAxioms(val; Def == EqDecider(E)(Top(ESAxioms(when; Def == EqDecider(E)(Top(ESAxioms(after; Def == EqDecider(E)(Top(ESAxioms(sends; Def == EqDecider(E)(Top(ESAxioms(sender; Def == EqDecider(E)(Top(ESAxioms(index; Def == EqDecider(E)(Top(ESAxioms(first; Def == EqDecider(E)(Top(ESAxioms(pred; Def == EqDecider(E)(Top(ESAxioms(causl) Def == EqDecider(E)(Top(Top))
	Thm* ES  Type{i'}
ma-state	Def State(ds) == x:Idds(x)?Top
Id	Def Id == Atom
	Thm* Id  Type
d-single-pre-init	Def @i (with ds: ds init: init action a:T precondition a(v) is P s v)(j) Def == if eqof(IdDeq)(j,i) Def == if (with ds: ds Def == if (init: init Def == if action a:T Def == if aprecondition a(v) is Def == if aP) Def == else  fi
id-deq	Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
es-E	Def E == 1of(es)
es-loc	Def loc(e) == 1of(2of(2of(2of(2of(2of(2of(es)))))))(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
fpf-dom	Def x  dom(f) == deq-member(eq;x;1of(f))

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