is mentioned by

Thm* T:(Id), to,from:(|T|(IdLnk List)), f:(Edge(T)). Thm* bi-graph(T;to;from)  spanner(f;T;to;from)  Prop	[spanner_wf]
Thm* G:(Id), to,from:(|G|(IdLnk List)). bi-tree(G;to;from)  Prop	[bi-tree_wf]
Thm* G:(Id), to,from:(|G|(IdLnk List)). bi-graph(G;to;from)  Prop	[bi-graph_wf]
Thm* R:(Id), in,out:(|R|IdLnk). ring(R;in;out)  Prop	[ring_wf]
Thm* i,a,x:Id, A,T:Type, c:A, P:(ATProp). Thm* @i: ma-single-pre-init1(x;A;c;a;T;x,v.P(x,v))  Dsys Thm* & (D:Dsys.  Thm* & (@i: ma-single-pre-init1(x;A;c;a;T;x,v.P(x,v))  D Thm* & ( Thm* & (D  Thm* & (realizes es.(vartype(i;x) r A) Thm* & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T)) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = locl(a)  Knd  P((x when e),val(e))) Thm* & (realizes es.& & ((v:T. P(c,v)) Thm* & (realizes es.& & ( Thm* & (realizes es.& & ((e:E.  Thm* & (realizes es.& & ((loc(e) = i  Id Thm* & (realizes es.& & ((& kind(e) = locl(a)  Knd Thm* & (realizes es.& & ((&  (v:T. P((x after e),v)))))	[s-pre-init-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 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