Some definitions of interest.
es-before	Def before(e) == if first(e) nil else before(pred(e)) @ [pred(e)] fi Def (recursive)
append	Def as @ bs == Case of as; nil  bs ; a.as'  [a / (as' @ bs)]  (recursive)
	Thm* T:Type, as,bs:T List. (as @ bs)  T List
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'}
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-locl	Def (e <loc e') == loc(e) = loc(e')  Id & (e < e')
es-pred	Def pred(e) Def == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of( Def == 1of(es)))))))))))))))) Def == (e)
iff	Def P  Q == (P  Q) & (P  Q)
	Thm* A,B:Prop. (A  B)  Prop
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
wellfounded	Def WellFnd{i}(A;x,y.R(x;y)) Def == P:(AProp). (j:A. (k:A. R(k;j)  P(k))  P(j))  {n:A. P(n)}
	Thm* A:Type{i}, r:(AAProp{i}). WellFnd{i}(A;x,y.r(x,y))  Prop{i'}

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