Who Cites da-outlinks?
da-outlinks	Def da-outlinks(da;i) Def == mapfilter(k.da-outlink-f(da;k);k.has-src(i;k);fpf-dom-list(da))
fpf-dom-list	Def fpf-dom-list(f) == 1of(f)
has-src	Def has-src(i;k) == isrcv(k)source(lnk(k)) = i
da-outlink-f	Def da-outlink-f(da;k) == <lnk(k),tag(k),da(k)>
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
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
eq_id	Def a = b == eqof(IdDeq)(a,b)
	Thm* a,b:Id. a = b
Kind-deq	Def KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)
idlnk-deq	Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))
id-deq	Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)
eqof	Def eqof(d) == 1of(d)
	Thm* T:Type, d:EqDecider(T). eqof(d)  TT
product-deq	Def product-deq(A;B;a;b) == <proddeq(a;b),prod-deq(A;B;a;b)>
union-deq	Def union-deq(A;B;a;b) == <sumdeq(a;b),sum-deq(A;B;a;b)>
proddeq	Def proddeq(a;b)(p,q) == (1of(a)(1of(p),1of(q)))(1of(b)(2of(p),2of(q)))
	Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). proddeq(a;b)  ABAB
sumdeq	Def sumdeq(a;b)(p,q) Def == InjCase(p; pa. InjCase(q; qa. 1of(a)(pa,qa); qb. false); pb. Def == InjCase(q; qa. false; qb. 1of(b)(pb,qb)))
	Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). sumdeq(a;b)  (A+B)(A+B)
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
isrcv	Def isrcv(k) == isl(k)
	Thm* k:Knd. isrcv(k)
prod-deq	Def prod-deq(A;B;a;b) Def == (A,B,a,b,p,q. q/q1,q2. Def == (p/p1,p2. Def == (b/eq,b1. Def == (a/e1,a1. Def == ((%1.%1 Def == ((%1.(<%.<(%1.%1(p1,q1)/%4,%5. %4((%1.%1)((%1.*)(*))))(a1) Def == ((%1.(<%.,(%1.%1(p2,q2)/%4,%5. %4((%1.%1)((%1.*)(*))))(b1)> Def == ((%1.(,%.%/%1,%2. *>)) Def == (((%1.%1.2) Def == ((((%1.%1 Def == ((((%1.(<p1,p2> = <q1,q2>  AB Def == ((((%1.,<p1,p2> = <q1,q2>  AB Def == ((((%1.,((e1(p1,q1))(eq(p2,q2))) Def == ((((%1.,(e1(p1,q1)) & (eq(p2,q2)) Def == ((((%1.,(%1.%1)((%1.<%2.%2,%2.%2>)(*)) Def == ((((%1.,(%1.%1) Def == ((((%1.,((%1.%1(e1(p1,q1),eq(p2,q2))) Def == ((((%1.,((p,q. InjCase(q; x. InjCase(p Def == ((((%1.,((p,q. InjCase(q; x. InjCase; x. <%.<*,*>,%.*> Def == ((((%1.,((p,q. InjCase(q; x. InjCase; y. <%.<any(%),*> Def == ((((%1.,((p,q. InjCase(q; x. InjCase; y. ,%.%/%1,%2. any(%1)>) Def == ((((%1.,((p,q. ; y. Def == ((((%1.,((p,q. InjCase(p Def == ((((%1.,((p,q. InjCase; x. <%.<*,any(%)>,%.%/%1,%2. any(%2)> Def == ((((%1.,((p,q. InjCase; y. <%.<any(%),any(%)> Def == ((((%1.,((p,q. InjCase; y. ,%.%/%1,%2. any(%2)>)))))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%6((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%1) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%6 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%6((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%1)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%)> Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%5 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%5((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%1) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%5((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%1)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%)>>)))) Def == (A Def == ,B Def == ,a Def == ,b)
band	Def pq == if p q else false fi
	Thm* p,q:. (pq)
fpf-ap	Def f(x) == 2of(f)(x)
tagof	Def tag(k) == 2of(outl(k))
	Thm* k:Knd. isrcv(k)  tag(k)  Id
filter	Def filter(P;l) == reduce(a,v. if P(a) [a / v] else v fi;nil;l)
	Thm* T:Type, P:(T), l:T List. filter(P;l)  T List
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
outl	Def outl(x) == InjCase(x; y. y; z. "???")
	Thm* A,B:Type, x:A+B. isl(x)  outl(x)  A
isl	Def isl(x) == InjCase(x; y. true; z. false)
	Thm* A,B:Type, x:A+B. isl(x)
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
Id	Def Id == Atom
	Thm* Id  Type
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
reduce	Def reduce(f;k;as) == Case of as; nil  k ; a.as'  f(a,reduce(f;k;as')) Def (recursive)
	Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as)  B
nat-deq	Def NatDeq == <a,b. a=b,nat_DASH_deq_DASH_aux{1:l}>
atom-deq	Def AtomDeq == <a,b. a=bAtom,atom_DASH_deq_DASH_aux{1:l}>
nat	Def  == {i:| 0i }
	Thm*   Type
sum-deq	Def sum-deq(A;B;a;b) Def == (A,B,a,b,p,q. Def == (InjCase(q; x. InjCase(p Def == (InjCase(q; x. InjCase; x1. b/eq,b1. Def == (InjCase(q; x. InjCase; x1. a/e1,a1. Def == (InjCase(q; x. InjCase; x1. <%.(%1.%1(x1,x)/%4,%5. Def == (InjCase(q; x. InjCase; x1. <%.(%4 Def == (InjCase(q; x. InjCase; x1. <%.(((%1.%1) Def == (InjCase(q; x. InjCase; x1. <%.((((%1.*) Def == (InjCase(q; x. InjCase; x1. <%.(((((%1.%1(x)) Def == (InjCase(q; x. InjCase; x1. <%.((((((%1.%1(x1)) Def == (InjCase(q; x. InjCase; x1. <%.(((((((%1.%1(B)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((%1.%1(A)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. (%1.%1) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. ((%1.(%2.*)(*)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. ((%)))))))))) Def == (InjCase(q; x. InjCase; x1. <%.(a1) Def == (InjCase(q; x. InjCase; x1. ,%.*> Def == (InjCase(q; x. InjCase; y. b/eq,b1. Def == (InjCase(q; x. InjCase; y. a/e1,a1. Def == (InjCase(q; x. InjCase; y. <%.(%1.any((%1(*)))) Def == (InjCase(q; x. InjCase; y. <%.((%1.%1(x)) Def == (InjCase(q; x. InjCase; y. <%.(((%1.%1(y)) Def == (InjCase(q; x. InjCase; y. <%.((((%1.%1(B)) Def == (InjCase(q; x. InjCase; y. <%.(((((%1.%1(A)) Def == (InjCase(q; x. InjCase; y. <%.(((((A,B,y,x,%. Def == (InjCase(q; x. InjCase; y. <%.((((((%1. Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase(%1 Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %2. any(%2) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. (%4.any(%4)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(%6. Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(any(%6)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(*)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(*)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%)))) Def == (InjCase(q; x. InjCase; y. <%.(((((((%1.%1)(inr(%.*)))))))) Def == (InjCase(q; x. InjCase; y. ,%.*>) Def == (; y. Def == (InjCase(p Def == (InjCase; x. b/eq,b1. Def == (InjCase; x. a/e1,a1. Def == (InjCase; x. <%.(%1.any((%1(*)))) Def == (InjCase; x. <%.((%1.%1(y)) Def == (InjCase; x. <%.(((%1.%1(x)) Def == (InjCase; x. <%.((((%1.%1(B)) Def == (InjCase; x. <%.(((((%1.%1(A)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase(%1 Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %2. any(%2) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. (%4.any(%4)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(%6. Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(any(%6)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(*)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(*)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%)))) Def == (InjCase; x. <%.(((((A,B,x,y,%. ((%1.%1)(inr(%.*)))))))) Def == (InjCase; x. ,%.*> Def == (InjCase; y1. b/eq,b1. Def == (InjCase; y1. a/e1,a1. Def == (InjCase; y1. <%.(%1.%1(y1,y)/%4,%5. Def == (InjCase; y1. <%.(%4 Def == (InjCase; y1. <%.(((%1.%1) Def == (InjCase; y1. <%.((((%1.*) Def == (InjCase; y1. <%.(((((%1.%1(y)) Def == (InjCase; y1. <%.((((((%1.%1(y1)) Def == (InjCase; y1. <%.(((((((%1.%1(B)) Def == (InjCase; y1. <%.((((((((%1.%1(A)) Def == (InjCase; y1. <%.((((((((A,B,y1,y,%. (%1.%1) Def == (InjCase; y1. <%.((((((((A,B,y1,y,%. ((%1.(%2.*)(*))(%)))))))))) Def == (InjCase; y1. <%.(b1) Def == (InjCase; y1. ,%.*>))) Def == (A Def == ,B Def == ,a Def == ,b)
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)
eq_atom	Def x=yAtom == if x=yAtomtrue; false fi
	Thm* x,y:Atom. x=yAtom
le	Def AB == B<A
	Thm* i,j:. (ij)  Prop
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
not	Def A == A  False
	Thm* A:Prop. (A)  Prop

Syntax:

da-outlinks(da;i)

has structure:

da-outlinks(da; i)

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