Def b == if b True else False fi

is mentioned by

Thm* A,B:MsgA. ma-is-empty(A)  A  B	[ma-is-empty-sub]
Thm* ma-is-empty()	[ma-empty-is-empty]
Thm* M:MsgA. ma-is-empty(M)  M =   MsgA	[assert-ma-is-empty]
Thm* ltg:(IdLnkIdType), i:Id, k:Knd, T:Type. Thm* (ltg  da-outlinks(k : T;i)) Thm*  Thm* isrcv(k) & source(lnk(k)) = i Thm* & (1of(ltg) ~ lnk(k)) Thm* & (1of(2of(ltg)) ~ tag(k)) Thm* & 2of(2of(ltg)) = T	[da-outlinks-single]
Thm* da:k:Knd fp-> Type, k:{k:Knd| k  dom(da) & isrcv(k) }. Thm* da-outlink-f(da;k)  IdLnkIdType	[da-outlink-f_wf]
Thm* B,C:(AType), eq:EqDecider(A), f:a:A fp-> B(a), g:a:A fp-> C(a), x:A. Thm* x  dom(f)  f  g(x) = f(x)  B(x)	[fpf-join-ap-left]
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]
Thm* A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A, Thm* P:(a:{a:A| a  dom(f) }B(a)Prop). z != f(x) ==> P(x,z)  Prop	[fpf-val_wf]
Def PossibleWorld(D;w) Def == FairFifo Def == & (i,x:Id. vartype(i;x) r M(i).ds(x)) Def == & & (i:Id, a:Action(i). Def == & & (isnull(a)  (valtype(i;a) r M(i).da(kind(a)))) Def == & & (l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg))) Def == & & (i,x:Id. M(i).init(x,s(i;0).x)) Def == & & (i:Id, t:. Def == & & (isnull(a(i;t)) Def == & & ( Def == & & ((islocal(kind(a(i;t))) Def == & & (( Def == & & ((M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t)))) Def == & & (& (x:Id.  Def == & & (& (M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x)) Def == & & (& (l:IdLnk.  Def == & & (& (M(i).send(kind(a(i;t));l;x. Def == & & (& (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i)) Def == & & (& (x:Id.  Def == & & (& (M(i).frame(kind(a(i;t)) affects x) Def == & & (& ( Def == & & (& (s(i;t).x = s(i;t+1).x  M(i).ds(x)) Def == & & (& (l:IdLnk, tg:Id. Def == & & (& (M(i).sframe(kind(a(i;t)) sends <l,tg>) Def == & & (& ( Def == & & (& (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List)) Def == & & (i,a:Id, t:. Def == & & (t':.  Def == & & (tt' Def == & & (& isnull(a(i;t')) & kind(a(i;t')) = locl(a) Def == & & (&  a declared in M(i) Def == & & (&  unsolvable M(i).pre(a,x.s(i;t').x))	[possible-world]
Def d-feasible(D) Def == (i:Id. Feasible(M(i))) Def == & (l:IdLnk, tg:Id. Def == & (M(source(l)).dout(l,tg) r M(destination(l)).din(l,tg)) Def == & (i:Id.  Def == & (finite-type({l:IdLnk Def == & (finite-type({| destination(l) = i & M(source(l)) sends on link l }))	[d-feasible]

In prior sections: bool 1 list 1 union mb nat mb list 1 mb list 2 mb event system 1 mb event system 2 mb event system 3 mb event system 4 rel 1

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