Some definitions of interest.
ma-send	Def M.send(k;l;s;v;ms;i) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ms Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> = Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if source(l) = i Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if concat(map(tgf. Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if map(x. Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;2of(tgf) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;(s Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;,v));L)) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> else nil fi Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (tg:Id Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if source(l) = i Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if M.da(rcv(l; tg)) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (else Top fi) List
ma-da	Def M.da(a) == 1of(2of(M))(a)?Top
ma-sub	Def M1  M2 Def == 1of(M1)  1of(M2) & 1of(2of(M1))  1of(2of(M2)) Def == & 1of(2of(2of(M1)))  1of(2of(2of(M2))) Def == & & 1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))) Def == & & 1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))) Def == & & 1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(M2)))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(2of(2of(2of(2of(2of(2of( Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(M2))))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & & 1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))
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'}
Kind-deq	Def KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)
Knd	Def Knd == (IdLnkId)+Id
	Thm* Knd  Type
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
idlnk-deq	Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))
ma-st	Def M.state == State(1of(M))
ma-state	Def State(ds) == x:Idds(x)?Top
Id	Def Id == Atom
	Thm* Id  Type
eq_id	Def a = b == eqof(IdDeq)(a,b)
	Thm* a,b:Id. a = b
fpf-sub	Def f  g == x:A. x  dom(f)  x  dom(g) & f(x) = g(x)  B(x)
id-deq	Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)
product-deq	Def product-deq(A;B;a;b) == <proddeq(a;b),prod-deq(A;B;a;b)>
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
concat	Def concat(ll) == reduce(l,l'. l @ l';nil;ll)
	Thm* T:Type, ll:(T List) List. concat(ll)  T List
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-ap	Def f(x) == 2of(f)(x)
fpf-dom	Def x  dom(f) == deq-member(eq;x;1of(f))
locl	Def locl(a) == inr(a)
	Thm* a:Id. locl(a)  Knd
lsrc	Def source(l) == 1of(l)
	Thm* l:IdLnk. source(l)  Id
map	Def map(f;as) == Case of as; nil  nil ; a.as'  [(f(a)) / map(f;as')] Def (recursive)
	Thm* A,B:Type, f:(AB), l:A List. map(f;l)  B List
	Thm* A,B:Type, f:(AB), l:A List. map(f;l)  B List
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
rcv	Def rcv(l; tg) == inl(<l,tg>)
	Thm* l:IdLnk, tg:Id. rcv(l; tg)  Knd
top	Def Top == Void given Void
	Thm* Top  Type

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