Def P  Q == (P  Q) & (P  Q)

is mentioned by

Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. Thm* bi-graph(G;to;from)  ((inverse(e)  from(i))  destination(e) = i)	[edge-inv-from]
Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. Thm* bi-graph(G;to;from)  ((inverse(e)  to(i))  source(e) = i)	[edge-inv-to]
Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. Thm* bi-graph(G;to;from)  ((e  from(i))  source(e) = i)	[edge-from]
Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. Thm* bi-graph(G;to;from)  ((e  to(i))  destination(e) = i)	[edge-to]
Thm* P:(AT), k:Knd, i,r,x:Id. Thm* A Thm*  Thm* T Thm*  Thm* x = r Thm*  Thm* loc.(recognizer1(loc;T;A;P;k;i;r;x))  Thm* realizes es.e@i.kind(e) = k  Knd  (valtype(e) r T) Thm* realizes es.& (vartype(i;x) r A) Thm* realizes es.& e@i.first(e)  (r when e) = false   Thm* realizes es.& e'@i.(r after e') Thm* realizes es.& e'@i. Thm* realizes es.& e'@i.(e:E.  Thm* realizes es.& e'@i.((e <loc e')  e = e'  E Thm* realizes es.& e'@i.(& kind(e) = k  Knd Thm* realizes es.& e'@i.(& P((x when e),val(e)))	[recognizer1__realizes]
Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type, f:(AB(T List)). Thm* (rcv(l; tg) = k  T = B) Thm*  Thm* @source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)  Dsys Thm* & (D:Dsys.  Thm* & (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)  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.& ((L:{e':E| kind(e') = rcv(l; tg)  Knd } List.  Thm* & (realizes es.& (((e':E.  Thm* & (realizes es.& ((((e'  L) Thm* & (realizes es.& ((( Thm* & (realizes es.& (((kind(e') = rcv(l; tg)  Knd & sender(e') = e  E) Thm* & (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2)) Thm* & (realizes es.& ((& map(e'.val(e');L) = f((x when e),val(e))  T List)))	[s-sends-rule1]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 rel 1 mb basic mb nat mb list 1 num thy 1 mb list 2 mb event system 1 mb event system 2 mb event system 3 mb event system 4 mb event system 5 mb event system 6

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