Def if b t else f fi == InjCase(b ; t; f)

is mentioned by

Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type. Thm* (rcv(l; tg) = k  T = B) Thm*  Thm* (f:(ABT), c:(AB). Thm* (@source(l): ma-single-sends1(A; Thm* (@source(l): ma-single-sends1(B; Thm* (@source(l): ma-single-sends1(T; Thm* (@source(l): ma-single-sends1(x; Thm* (@source(l): ma-single-sends1(k; Thm* (@source(l): ma-single-sends1(l; Thm* (@source(l): ma-single-sends1(tg; Thm* (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi)) Thm* ( Dsys Thm* (& (D:Dsys.  Thm* (& (@source(l): ma-single-sends1(A; Thm* (& (@source(l): ma-single-sends1(B; Thm* (& (@source(l): ma-single-sends1(T; Thm* (& (@source(l): ma-single-sends1(x; Thm* (& (@source(l): ma-single-sends1(k; Thm* (& (@source(l): ma-single-sends1(l; Thm* (& (@source(l): ma-single-sends1(tg; Thm* (& (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi) Thm* (& (@source(l): ma-single-sends1()  D Thm* (& ( Thm* (& (D  Thm* (& (realizes es.(vartype(source(l);x) r A) Thm* (& (realizes es.& (e:E.  Thm* (& (realizes es.& (loc(e) = source(l)  Id Thm* (& (realizes es.& ( Thm* (& (realizes es.& (kind(e) = k  Knd  (valtype(e) r B)) Thm* (& (realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T)) Thm* (& (realizes es.& (e:E.  Thm* (& (realizes es.& (loc(e) = source(l)  Id Thm* (& (realizes es.& ( Thm* (& (realizes es.& (kind(e) = k  Knd Thm* (& (realizes es.& ( Thm* (& (realizes es.& ((c((x when e),val(e)) Thm* (& (realizes es.& (( Thm* (& (realizes es.& (((e':E.  Thm* (& (realizes es.& (((kind(e') = rcv(l; tg)  Knd Thm* (& (realizes es.& (((& sender(e') = e  E Thm* (& (realizes es.& (((& & (e'':E.  Thm* (& (realizes es.& (((& & (kind(e'') = rcv(l; tg)  Knd Thm* (& (realizes es.& (((& & ( Thm* (& (realizes es.& (((& & (sender(e'') = e  E  e'' = e'  E) Thm* (& (realizes es.& (((& & val(e') = f((x when e),val(e))  T)) Thm* (& (realizes es.& (& (c((x when e),val(e)) Thm* (& (realizes es.& (& ( Thm* (& (realizes es.& (& ((e':E.  Thm* (& (realizes es.& (& ((kind(e') = rcv(l; tg)  Knd Thm* (& (realizes es.& (& ((& sender(e') = e  E)))))	[conditional-send1-rule]
Def f[x:=v](y) == if eq(y,x) v else f(y) fi	[update]
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	[ring-leader1]
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]	[trigger1]
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	[recognizer1]
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]	[send-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	[once]
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	[Dconstant]

In prior sections: bool 1 mb nat mb list 2 mb event system 1 mb event system 4 mb event system 5 int 2 list 1 mb list 1 num thy 1 mb event system 2 mb event system 3 mb event system 6

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html