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

is mentioned by

Thm* M1,M2:MsgA. Thm* M1  M2 Thm*  Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(tg:Id Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if source(l) = i Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if M2.da(rcv(l; tg)) Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(else Top fi) List. Thm* (M2.send(k;l;s;v;ms;i)  M1.send(k;l;s;v;ms;i))	[ma-send-sub]
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(tg:Id Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if source(l) = i Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if M.da(rcv Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if (l; tg)) Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(else Top fi) List. Thm* M.send(k;l;s;v;ms;i)  Prop	[ma-send_wf]
Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top. Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi	[fpf-join-cap-sq]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x  dom(f  g)  f  g(x) = if x  dom(f) f(x) else g(x) fi  B(x)	[fpf-join-ap]
Def @i (with ds: ds init: init action a:T precondition a(v) is P s v)(j) Def == if eqof(IdDeq)(j,i) Def == if (with ds: ds Def == if (init: init Def == if action a:T Def == if aprecondition a(v) is Def == if aP) Def == else  fi	[d-single-pre-init]
Def @i (with ds: ds action a:T precondition a(v) is P s v)(j) Def == if eqof(IdDeq)(j,i) (with ds: ds action a:T precondition a(v) is P s v) Def == else  fi	[d-single-pre]
Def d-single-sends(i; ds; da; k; l; f)(j) Def == if eqof(IdDeq)(j,i) ma-single-sends(ds; da; k; l; f) else  fi	[d-single-sends]
Def d-single-effect(i; ds; da; k; x; f)(j) Def == if eqof(IdDeq)(j,i) ma-single-effect(ds; da; k; x; f) else  fi	[d-single-effect]
Def @i: only L sends on (l with tg)(j) Def == if eqof(IdDeq)(j,i) only L sends on (l with tg) else  fi	[d-single-sframe]
Def @i: only L affects x : t(j) Def == if eqof(IdDeq)(j,i) only members of L affect x :t else  fi	[d-single-frame]
Def @i: x:T initially x = v(j) Def == if eqof(IdDeq)(j,i) x : T initially x = v else  fi	[d-single-init]

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

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