Some definitions of interest.
da-outlinks	Def da-outlinks(da;i) Def == mapfilter(k.da-outlink-f(da;k);k.has-src(i;k);fpf-dom-list(da))
da-outlink-f	Def da-outlink-f(da;k) == <lnk(k),tag(k),da(k)>
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
Id	Def Id == Atom
	Thm* Id  Type
has-src	Def has-src(i;k) == isrcv(k)source(lnk(k)) = i
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
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-join	Def f  g == <1of(f) @ filter(a.a  dom(f);1of(g)),a.f(a)?g(a)>
fpf-dom	Def x  dom(f) == deq-member(eq;x;1of(f))
fpf-dom-list	Def fpf-dom-list(f) == 1of(f)
iff	Def P  Q == (P  Q) & (P  Q)
	Thm* A,B:Prop. (A  B)  Prop
isrcv	Def isrcv(k) == isl(k)
	Thm* k:Knd. isrcv(k)
l_member	Def (x  l) == i:. i<||l|| & x = l[i]  T
	Thm* T:Type, x:T, l:T List. (x  l)  Prop
lnk	Def lnk(k) == 1of(outl(k))
	Thm* k:Knd. isrcv(k)  lnk(k)  IdLnk
lsrc	Def source(l) == 1of(l)
	Thm* l:IdLnk. source(l)  Id
mapfilter	Def mapfilter(f;P;L) == map(f;filter(P;L))
	Thm* T:Type, P:(T), T':Type, f:({x:T| P(x) }T'), L:T List. Thm* mapfilter(f;P;L)  T' List

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