Some definitions of interest.
msystem	Def System == {M:(IdMsgA)| loc:Id. Feasible(M(loc)) }
ma-feasible	Def Feasible(M) Def == xdom(1of(M)). T=1of(M)(x)   T Def == & kdom(1of(2of(M))). T=1of(2of(M))(k)   Dec(T) Def == & adom(1of(2of(2of(2of(M))))). p=1of(2of(2of(2of(M))))(a)   Def == &s:State(1of(M)). Dec(v:1of(2of(M))(locl(a))?Top. p(s,v)) Def == & kxdom(1of(2of(2of(2of(2of(M)))))).  Def == ef=1of(2of(2of(2of(2of(M)))))(kx)   M.frame(1of(kx) affects 2of(kx)) Def == & kldom(1of(2of(2of(2of(2of(2of(M))))))).  Def == & snd=1of(2of(2of(2of(2of(2of(M))))))(kl)   tg:Id.  Def == & (tg  map(p.1of(p);snd))  M.sframe(1of(kl) sends <2of(kl),tg>)
msga	Def MsgA Def == ds:x:Id fp-> Type Def == da:a:Knd fp-> Type Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void Def == kl:KndIdLnk fp-> (tg:Id Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl)) Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop
	Thm* MsgA  Type{i'}
Id	Def Id == Atom
	Thm* Id  Type
m-sys-at	Def @i: A(j) == if j = i A else  fi
eq_id	Def a = b == eqof(IdDeq)(a,b)
	Thm* a,b:Id. a = b
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
ma-empty	Def  == mk-ma(; ; ; ; ; ; ; )
not	Def A == A  False
	Thm* A:Prop. (A)  Prop

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