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)  ((e  to(i))  destination(e) = i)	[edge-to]
Thm* T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T). Thm* bi-graph(T;to;from)  destination(u)  |T|	[dst-edge]
Thm* L:Knd List, l:IdLnk, tg:Id. Thm* @source(l): only L sends on (l with tg)  Dsys Thm* & (D:Dsys.  Thm* & (@source(l): only L sends on (l with tg)  D Thm* & ( Thm* & (D  Thm* & (realizes es.e:E.  Thm* & (realizes es.loc(e) = destination(l)  Id Thm* & (realizes es. Thm* & (realizes es.kind(e) = rcv(l; tg)  Knd  (kind(sender(e))  L))	[better-sframe-rule]
Def bi-graph(G;to;from) Def == i:|G|.  Def == (lto(i).destination(l) = i Def == & (G(source(l))) Def == & (l  from(source(l))) Def == & (lnk-inv(l)  from(i))) Def == & (lfrom(i).source(l) = i Def == & & (G(destination(l))) Def == & & (l  to(destination(l))) Def == & & (lnk-inv(l)  to(i)))	[bi-graph]
Def n(i) == destination(out(i))	[rnext]
Def ring(R;in;out) Def == (i:|R|.  Def == ((R(source(in(i)))) & (R(destination(out(i)))) Def == (& source(out(i)) = i Def == (& & destination(in(i)) = i Def == (& & in(destination(out(i))) = out(i)  IdLnk Def == (& & out(source(in(i))) = in(i)  IdLnk) Def == & (i,j:|R|. k:. x.destination(out(x))^k(i) = j  Id) Def == & |R|	[ring]

In prior sections: mb event system 2 mb event system 6 mb event system 3 mb event system 5

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