mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
6Thm* the_w:World. 
Thm* FairFifo
Thm* 
Thm* ESAxioms{i:l}
Thm* ESAxioms(E;
Thm* ESAxioms((i,x. vartype(i;x));
Thm* ESAxioms(the_w.M;
Thm* ESAxioms((e.loc(e));
Thm* ESAxioms((e.kind(e));
Thm* ESAxioms((e.val(e));
Thm* ESAxioms((x,e. (x when e));
Thm* ESAxioms((x,e. (x after e));
Thm* ESAxioms((l,e. sends(l;e));
Thm* ESAxioms((e.sender(e));
Thm* ESAxioms((e.index(e));
Thm* ESAxioms((e.first(e));
Thm* ESAxioms((e.pred(e));
Thm* ESAxioms((e,e'. e <c e'))		[world-event-system]
cites the following:
0Thm* the_w:World, e:E. isnull(act(e))[w-act-not-null]
1Thm* the_w:World, e:E. first(e)  (t':. t'<time(e)  isnull(a(loc(e);t')))[assert-w-first]
0Thm* the_w:World, t:, i:Id. first(<i,t>)  pred(<i,t>)  E[w-pred-aux]
0Thm* the_w:World, i:Id, t:. first(<i,t>)  [w-first-aux]
0Thm* the_w:World, e:E. <loc(e),time(e)> ~ e[w-loc-time]
1Thm* R:(TTProp). Trans x,y:T. x R^+ y[rel_plus_trans]
4Thm* the_w:World, e,e':E. FairFifo  e <c e'  time(e)<time(e')[w-causl-time]
5Thm* the_w:World, e:E, t:.
Thm* FairFifo
Thm* 
Thm* isrcv(kind(e))
Thm* 
Thm* match(lnk(kind(e));t;time(e))
Thm* 
Thm* onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))||
Thm* -||snds(lnk(kind(e));t)||)]
Thm* =
Thm* msg(a(loc(e);time(e)))
Thm*  Msg		[w-match-property]
0Thm* R:(TTProp), x,y:T. (x R^+ y)  (x R y)  (z:T. (x R^+ z) & (z R y))[rel_plus_implies]
0Thm* T:Type, P:(T), l:T List. filter(P;l)  {x:T| P(x) } List[filter_type]
3Thm* the_w:World, e:E.
Thm* FairFifo  isrcv(kind(e))  (t:time(e). match(lnk(kind(e));t;time(e)))		[w-match-exists]
4Thm* i,j:.
Thm* i<j
Thm* 
Thm* (f:(T), P:(T).
Thm* (P(f(i))  ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(j)))||)		[filter_map_upto]
5Thm* the_w:World, e,e':E.
Thm* FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e')		[w-locl-iff]
0Thm* P:(T), A:T List, B:Top. filter(P;A @ B) ~ (filter(P;A) @ filter(P;B))[filter_append_sq]
1Thm* P:(T), L2,L1:T List. L1  L2  filter(P;L1)  filter(P;L2)[filter_iseg]
1Thm* r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi[general_length_nth_tl]
2Thm* i,j:. ij  upto(i)  upto(j)[upto_iseg]
0Thm* f:(AB), L1,L2:A List. L1  L2  map(f;L1)  map(f;L2)[iseg_map]
2Thm* ll1,ll2:(T List) List. ll1  ll2  concat(ll1)  concat(ll2)[concat_iseg]
1Thm* l1,l2:T List. l1  l2  ||l1||||l2||[iseg_length]
0Thm* f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as'))[map_append_sq]
0Thm* l:T List. (l @ nil) ~ l[append_nil_sq]
0Thm* l:Top List, ll:(Top List) List. concat([l / ll]) ~ (l @ concat(ll))[concat-cons]
1Thm* ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2))[concat_append]
0Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||  [length_append]
1Thm* t',m:, T:Type, f:(T), P:(T).
Thm* m+1||filter(P;map(f;upto(t')))||
Thm* 
Thm* (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )		[filter_map_upto2]
0Thm* the_w:World, l:IdLnk, t,t':.
Thm* match(l;t;t')
Thm* 
Thm* ||snds(l;t)||||rcvs(l;t')||
Thm* & ||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||		[assert-w-match]
0Thm* w:World, t:, l:IdLnk, i:Id. ||onlnk(l;m(i;t))||  [w-onlnk-m]
0Thm* f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))[mu-property]
4Thm* the_w:World, e:E, t,t':.
Thm* FairFifo
Thm* 
Thm* isrcv(kind(e))
Thm* 
Thm* match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))  t = t'		[w-match-unique]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb event system 3 Sections EventSystems Doc