Who Cites w-causl?
w-causl	Def e <c e' == e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^+ e'
w-sender	Def sender(e) == <source(lnk(kind(e))),mu(t.match(lnk(kind(e));t;time(e)))>
w-E	Def E == {p:(Id)| isnull(a(1of(p);2of(p))) }
w-ekind	Def kind(e) == kind(act(e))
w-match	Def match(l;t;t') Def == (||snds(l;t)||||rcvs(l;t')||) Def == (||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||)
w-rcvs	Def rcvs(l;t) == filter(a.isrcv(l;a);map(t1.a(destination(l);t1);upto(t)))
w-isrcvl	Def isrcv(l;a) == isnull(a)isrcv(kind(a))lnk(kind(a)) = l
isrcv	Def isrcv(k) == isl(k)
	Thm* k:Knd. isrcv(k)
w-snds	Def snds(l;t) == concat(map(t1.m(l;t1);upto(t)))
w-ml	Def m(l;t) == onlnk(l;m(source(l);t))
w-onlnk	Def onlnk(l;mss) == filter(ms.mlnk(ms) = l;mss)
eq_lnk	Def a = b == eqof(IdLnkDeq)(a,b)
	Thm* a,b:IdLnk. a = b
idlnk-deq	Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))
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)>
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)
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
w-locl	Def e <loc e' == loc(e) = loc(e')  Id & time(e)<time(e')
rel_plus	Def R^+(x,y) == n:. x R^n y
	Thm* T:Type, R:(TTType). R^+  TTType
w-time	Def time(e) == 2of(e)
lnk	Def lnk(k) == 1of(outl(k))
	Thm* k:Knd. isrcv(k)  lnk(k)  IdLnk
mu	Def mu(f) == if f(0) 0 else mu(x.f(x+1))+1 fi  (recursive)
	Thm* f:(). (n:. f(n))  mu(f)
lsrc	Def source(l) == 1of(l)
	Thm* l:IdLnk. source(l)  Id
w-act	Def act(e) == a(1of(e);2of(e))
w-a	Def a(i;t) == 1of(2of(2of(2of(2of(w)))))(i,t)
w-m	Def m(i;t) == 1of(2of(2of(2of(2of(2of(w))))))(i,t)
ldst	Def destination(l) == 1of(2of(l))
	Thm* l:IdLnk. destination(l)  Id
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
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
w-kind	Def kind(a) == 1of(outr(a))
w-loc	Def loc(e) == 1of(e)
mlnk	Def mlnk(m) == 1of(m)
	Thm* M:(IdLnkIdType), m:Msg(M). mlnk(m)  IdLnk
	Thm* the_es:ES, m:Msg. mlnk(m)  IdLnk
eqof	Def eqof(d) == 1of(d)
	Thm* T:Type, d:EqDecider(T). eqof(d)  TT
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
w-isnull	Def isnull(a) == isl(a)
Id	Def Id == Atom
	Thm* Id  Type
nat	Def  == {i:| 0i }
	Thm*   Type
le	Def AB == B<A
	Thm* i,j:. (ij)  Prop
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
isl	Def isl(x) == InjCase(x; y. true; z. false)
	Thm* A,B:Type, x:A+B. isl(x)
rel_exp	Def R^n == if n=0 x,y. x = y  T else x,y. z:T. (x R z) & (z R^n-1 y) fi Def (recursive)
	Thm* n:, T:Type, R:(TTProp). R^n  TTProp
nat_plus	Def  == {i:| 0<i }
	Thm*   Type
outl	Def outl(x) == InjCase(x; y. y; z. "???")
	Thm* A,B:Type, x:A+B. isl(x)  outl(x)  A
length	Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
le_int	Def ij == j<i
	Thm* i,j:. (ij)
lt_int	Def i<j == if i<j true ; false fi
	Thm* i,j:. (i<j)
band	Def pq == if p q else false fi
	Thm* p,q:. (pq)
outr	Def outr(x) == InjCase(x; y. "???"; z. z)
	Thm* A,B:Type, x:A+B. isl(x)  outr(x)  B
upto	Def upto(n) == if n=0 nil else upto(n-1) @ [(n-1)] fi  (recursive)
	Thm* n:. upto(n)  n List
nat-deq	Def NatDeq == <a,b. a=b,nat_DASH_deq_DASH_aux{1:l}>
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)
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
concat	Def concat(ll) == reduce(l,l'. l @ l';nil;ll)
	Thm* T:Type, ll:(T List) List. concat(ll)  T List
bnot	Def b == if b false else true fi
	Thm* b:. b
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
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
atom-deq	Def AtomDeq == <a,b. a=bAtom,atom_DASH_deq_DASH_aux{1:l}>
eq_atom	Def x=yAtom == if x=yAtomtrue; false fi
	Thm* x,y:Atom. x=yAtom

Syntax:

e <c e'

has structure:

w-causl(w; e; e')

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