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'}
Knd	Def Knd == (IdLnkId)+Id
	Thm* Knd  Type
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
Id	Def Id == Atom
	Thm* Id  Type
d-single-sframe	Def @i: only L sends on (l with tg)(j) Def == if eqof(IdDeq)(j,i) only L sends on (l with tg) else  fi
es-tg-sends	Def sends(l,tg,e) == filter(m.mtag(m) = tg;sends(l;e))
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
es-E	Def E == 1of(es)
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)
l_member	Def (x  l) == i:. i<||l|| & x = l[i]  T
	Thm* T:Type, x:T, l:T List. (x  l)  Prop
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
null	Def null(as) == Case of as; nil  true ; a.as'  false
	Thm* T:Type, as:T List. null(as)
	Thm* null(nil)

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