Who Cites ring-leader1?
ring-leader1	Def ring-leader1(loc;R;uid;out;in) Def == if R(loc) Def == if [(send-once(loc;;;"send-me";x.x;"vote";out(loc);"me"));  Def == if [(trigger1(loc;;;x,y. x=y;loc;rcv Def == if [((in(loc)); "vote");"leader";"me"));  Def == if [(Dconstant(loc;;uid(loc);"me";loc));  Def == if [ma-single-sends1(; Def == if [ma-single-sends1(; Def == if [ma-single-sends1(; Def == if [ma-single-sends1("me"; Def == if [ma-single-sends1(rcv((in(loc)); "vote"); Def == if [ma-single-sends1((out(loc)); Def == if [ma-single-sends1("vote"; Def == if [ma-single-sends1((a,b. if a<b [b] else nil fi));  Def == if [only [rcv((in(loc)); "vote");  Def == if [only [locl("send-me")] sends on (out(loc) with "vote")] Def == else nil fi
trigger1	Def trigger1(loc;T;A;P;i;k;a;x) Def == [(recognizer1(loc;T;A;P;k;i;"trigger";x));  Def == [if loc = i ma-single-pre1("trigger";;a;Unit;x,v.x) else  fi]
	Thm* loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id. Thm* A Thm*  Thm* T Thm*  Thm* x = "trigger"  locl(a) = k  trigger1(loc;T;A;P;i;k;a;x)  MsgA List
send-once	Def send-once(loc;T;A;a;f;tg;l;x) Def == [(once(loc;a;source(l)));  Def == [if loc = source(l) Def == [if ma-single-sends1(A; Unit; T; x; locl(a); l; tg; (a,b. [(f(a))])) Def == [else  fi]
once	Def once(loc;a;i) Def == if loc = i Def == if [ma-single-pre-init1("done";;false;a;Unit;x,v.x);  Def == if [only members of [locl(a)] affect "done" :;  Def == if [ma-single-effect0("done";;locl(a);Unit;x,v. true)] Def == else nil fi
	Thm* loc,a,i:Id. once(loc;a;i)  MsgA List
mkid	Def x_n == <x,n>
	Thm* x:Atom, n:. x_n  Id
ma-single-pre1	Def ma-single-pre1(x;A;a;T;y,v.P(y;v)) Def == (with ds: x : A Def == (action a:T Def == (precondition a(v) is Def == (s,v. P(s(x);v) s v)
ma-single-pre	Def (with ds: ds Def (action a:T Def (precondition a(v) is Def (P s v) Def == mk-ma(ds; locl(a) : T; ; a : P; ; ; ; )
ma-single-pre-init1	Def ma-single-pre-init1(x;T;c;a;T';y,v.P(y;v)) Def == (with ds: x : T Def == (init: x : c Def == action a:T' Def == aprecondition a(v) is Def == as,v. P(s(x);v))
ma-single-pre-init	Def (with ds: ds Def (init: init Def action a:T Def aprecondition a(v) is Def aP) Def == mk-ma(ds; locl(a) : T; init; a : P; ; ; ; )
locl	Def locl(a) == inr(a)
	Thm* a:Id. locl(a)  Knd
ma-single-sends1	Def ma-single-sends1(A; B; T; x; a; l; tg; f) Def == ma-single-sends(x : A; Def == ma-single-sends(a : B  rcv(l; tg) : T; Def == ma-single-sends(a; Def == ma-single-sends(l; Def == ma-single-sends([<tg,s,v. f(s(x),v)>])
rcv	Def rcv(l; tg) == inl(<l,tg>)
	Thm* l:IdLnk, tg:Id. rcv(l; tg)  Knd
ma-single-sframe	Def only L sends on (l with tg) == mk-ma(; ; ; ; ; ; ; <l,tg> : L)
lt_int	Def i<j == if i<j true ; false fi
	Thm* i,j:. (i<j)
Dconstant	Def Dconstant(loc;T;c;x;i) Def == if loc = i [x : T initially x = c; only members of nil affect x :T] Def == else nil fi
	Thm* loc:Id, T:Type, c:T, x,i:Id. Dconstant(loc;T;c;x;i)  MsgA List
ma-join-list	Def (L) == reduce(A,B. A  B;;L)
ma-join	Def M1  M2 Def == mk-ma(1of(M1)  1of(M2); Def == mk-ma(1of(2of(M1))  1of(2of(M2)); Def == mk-ma(1of(2of(2of(M1)))  1of(2of(2of(M2))); Def == mk-ma(1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))); Def == mk-ma(1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of( Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(M2)))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(2of( Def == mk-ma(1of(M1)))))))  1of(2of(2of(2of(2of(2of(2of(M2))))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(2of(2of( Def == mk-ma(1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))
Kind-deq	Def KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)
recognizer1	Def recognizer1(loc;T;A;P;k;i;r;x) Def == if loc = i Def == if [r :  initially r = false;  Def == if [only members of [k] affect r :;  Def == if [ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v)  r)] Def == else nil fi
	Thm* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id. Thm* A  T  x = r  recognizer1(loc;T;A;P;k;i;r;x)  MsgA List
eq_id	Def a = b == eqof(IdDeq)(a,b)
	Thm* a,b:Id. a = b
idlnk-deq	Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))
ma-single-effect1	Def ma-single-effect1(x;A;y;B;k;T;f) Def == ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v)))
id-deq	Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)
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)
ma-single-sends	Def ma-single-sends(ds; da; k; l; f) == mk-ma(ds; da; ; ; ; <k,l> : f; ; )
ma-single-frame	Def only members of L affect x :t == mk-ma(x : t; ; ; ; ; ; x : L; )
ma-single-init	Def x : t initially x = v == mk-ma(x : t; ; x : v; ; ; ; ; )
ma-single-effect0	Def ma-single-effect0(x;A;k;T;f) Def == ma-single-effect(x : A; k : T; k; x; (s,v. f(s(x),v)))
ma-single-effect	Def ma-single-effect(ds; da; k; x; f) == mk-ma(ds; da; ; ; <k,x> : f; ; ; )
fpf-single	Def x : v == <[x],x.v>
ma-empty	Def  == mk-ma(; ; ; ; ; ; ; )
fpf-empty	Def  == <nil,x.>
mk-ma	Def mk-ma(ds; da; init; pre; ef; send; frame; sframe) Def == <ds,da,init,pre,ef,send,frame,sframe,>
fpf-join	Def f  g == <1of(f) @ filter(a.a  dom(f);1of(g)),a.f(a)?g(a)>
fpf-cap	Def f(x)?z == if x  dom(f) f(x) else z fi
fpf-dom	Def x  dom(f) == deq-member(eq;x;1of(f))
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
deq-member	Def deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x)  b;false;L)
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
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
lsrc	Def source(l) == 1of(l)
	Thm* l:IdLnk. source(l)  Id
Knd	Def Knd == (IdLnkId)+Id
	Thm* Knd  Type
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
Id	Def Id == Atom
	Thm* Id  Type
union-deq	Def union-deq(A;B;a;b) == <sumdeq(a;b),sum-deq(A;B;a;b)>
fpf-ap	Def f(x) == 2of(f)(x)
eqof	Def eqof(d) == 1of(d)
	Thm* T:Type, d:EqDecider(T). eqof(d)  TT
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
bnot	Def b == if b false else true fi
	Thm* b:. 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
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
so_lambda2	Def (1,2. b(1;2))(1,2) == b(1;2)
bor	Def p  q == if p true else q fi
	Thm* p,q:. (p  q)
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
atom-deq	Def AtomDeq == <a,b. a=bAtom,atom_DASH_deq_DASH_aux{1:l}>
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_atom	Def x=yAtom == if x=yAtomtrue; false fi
	Thm* x,y:Atom. x=yAtom
band	Def pq == if p q else false fi
	Thm* p,q:. (pq)

Syntax:

ring-leader1(loc;R;uid;out;in)

has structure:

ring-leader1(loc; R; uid; out; in)

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