mb event system 2 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def P  Q == PQ

is mentioned by

Thm* es:ES, e,e':E. e  e'   loc(e) = loc(e')  Id[es-le-loc]
Thm* es:ES, e:E, l:IdLnk, tg:Id.
Thm* kind(e) = rcv(l; tg)
Thm* 
Thm* loc(e) = destination(l) & loc(sender(e)) = source(l)		[es-loc-rcv]
Thm* the_es:ES, e:E. first(e)  loc(pred(e)) = loc(e)  Id[es-loc-pred]
Thm* the_es:ES, j,e:E. first(j)  (e <loc j)[es-first-implies]
Thm* the_es:ES, j:E. first(j)  (pred(j) <loc j)[es-pred-locl]
Thm* the_es:ES. 
Thm* (Trans e,e':E. (e <loc e'))
Thm* & SWellFounded((e <loc e'))
Thm* & (e,e':E. loc(e) = loc(e')  Id  (e <loc e')  e = e'  (e' <loc e))
Thm* & (e:E. first(e)  (e':E. (e' <loc e)))
Thm* & (e:E. 
Thm* & (first(e)
Thm* & (
Thm* & ((pred(e) <loc e) & (e':E. ((pred(e) <loc e') & (e' <loc e))))
Thm* & (e:E. 
Thm* & (first(e)
Thm* & (
Thm* & ((x:Id. (x when e) = (x after pred(e))  vartype(loc(e);x)))
Thm* & (Trans e,e':E. (e < e'))
Thm* & SWellFounded((e < e'))
Thm* & (e:E. 
Thm* & (isrcv(e)
Thm* & (
Thm* & (sends(lnk(e);sender(e))[index(e)] = msg(lnk(e);tag(e);val(e))  Msg)
Thm* & (e,e':E. (e <loc e')  (e < e'))
Thm* & (e:E. isrcv(e)  (sender(e) < e))
Thm* & (e,e':E.
Thm* & ((e < e')
Thm* & (
Thm* & (first(e') & (e < pred(e'))  e = pred(e')  E
Thm* & ( isrcv(e') & (e < sender(e'))  e = sender(e')  E)
Thm* & (e:E. isrcv(e)  loc(e) = destination(lnk(e)))
Thm* & (e:E, l:IdLnk.
Thm* & (loc(e) = source(l)  sends(l;e) = nil  (Msg on l) List)
Thm* & (e,e':E.
Thm* & (isrcv(e)
Thm* & (
Thm* & (isrcv(e')
Thm* & (
Thm* & (lnk(e) = lnk(e')
Thm* & (
Thm* & (((e <loc e')
Thm* & ((
Thm* & (((sender(e) <loc sender(e'))
Thm* & (( sender(e) = sender(e')  E & index(e)<index(e')))
Thm* & (e:E, l:IdLnk, n:||sends(l;e)||.
Thm* & (e':E. isrcv(e') & lnk(e') = l & sender(e') = e  E & index(e') = n  )		[es-axioms]
Thm* the_es:ES, e:E. first(e)  pred(e)  E[es-pred_wf]
Thm* the_es:ES, e:E. isrcv(e)  index(e)  ||sends(lnk(e);sender(e))||[es-index_wf]
Thm* the_es:ES, e:E. isrcv(e)  sender(e)  E[es-sender_wf]
Thm* the_es:ES, e:E. isrcv(e)  acttype(e)  Type[es-acttype_wf]
Thm* the_es:ES, e:E. isrcv(e)  rcvtype(e)  Type[es-rcvtype_wf]
Thm* the_es:ES, e:E. isrcv(e)  lnk(e)  IdLnk[es-lnk_wf]
Thm* the_es:ES, e:E. isrcv(e)  tag(e)  Id[es-tag_wf]
Thm* R:(TTProp), x,y:T. (x R^+ y)  (x R y)  (z:T. (x R^+ z) & (z R y))[rel_plus_implies]
Thm* R:(TTType). SWellFounded(R(x,y))  WellFnd{i}(T;x,y.R(x,y))[strongwf-implies]
Thm* p:IdLnk List, i:||p||, j:(i+1).
Thm* lpath(p)  lconnects(l_interval(p;j;i);source(p[j]);source(p[i]))		[lpath-members-connected]
Thm* l:IdLnk, p:IdLnk List.
Thm* lpath([l / p])
Thm* 
Thm* lpath(p)
Thm* & (||p|| = 0    destination(l) = source(hd(p)) & hd(p) = lnk-inv(l))		[lpath_cons]
Thm* x:A. (x,y:A. Dec(x = y))  (L:A List. Dec((x  L)))[decidable__l_member]
Thm* strong-subtype(A;B)  (EqDecider(B) r EqDecider(A))[strong-subtype-deq-subtype]
Thm* d:EqDecider(B). strong-subtype(A;B)  d  EqDecider(A)[strong-subtype-deq]
Def ESAxioms{i:l}
Def ESAxioms(E;
Def ESAxioms(T;
Def ESAxioms(M;
Def ESAxioms(loc;
Def ESAxioms(kind;
Def ESAxioms(val;
Def ESAxioms(when;
Def ESAxioms(after;
Def ESAxioms(sends;
Def ESAxioms(sender;
Def ESAxioms(index;
Def ESAxioms(first;
Def ESAxioms(pred;
Def ESAxioms(causl)
Def == (e,e':E. loc(e) = loc(e')  Id  causl(e,e')  e = e'  causl(e',e))
Def == & (e:E. (first(e))  (e':E. loc(e') = loc(e)  Id  causl(e',e)))
Def == & (e:E. 
Def == & ((first(e))
Def == & (
Def == & (loc(pred(e)) = loc(e)  Id & causl(pred(e),e)
Def == & (& (e':E. 
Def == & (& (loc(e') = loc(e)  Id  (causl(pred(e),e') & causl(e',e))))
Def == & (e:E. 
Def == & ((first(e))  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x)))
Def == & (Trans e,e':E. causl(e,e'))
Def == & SWellFounded(causl(e,e'))
Def == & (e:E. 
Def == & (isrcv(kind(e))
Def == & (
Def == & ((sends(lnk(kind(e)),sender(e)))[(index(e))]
Def == & (=
Def == & (msg(lnk(kind(e));tag(kind(e));val(e))
Def == & ( Msg(M))
Def == & (e:E. isrcv(kind(e))  causl(sender(e),e))
Def == & (e,e':E.
Def == & (causl(e,e')
Def == & (
Def == & ((first(e')) & causl(e,pred(e'))  e = pred(e')
Def == & ( isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e'))
Def == & (e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e))))
Def == & (e:E, l:IdLnk.
Def == & (loc(e) = source(l)  sends(l,e) = nil  Msg_sub(l; M) List)
Def == & (e,e':E.
Def == & (isrcv(kind(e))
Def == & (
Def == & (isrcv(kind(e'))
Def == & (
Def == & (lnk(kind(e)) = lnk(kind(e'))
Def == & (
Def == & ((causl(e,e')
Def == & ((
Def == & ((causl(sender(e),sender(e'))
Def == & (( sender(e) = sender(e')  E & index(e)<index(e')))
Def == & (e:E, l:IdLnk, n:||sends(l,e)||.
Def == & (e':E. 
Def == & (isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n)		[ESAxioms]
Def SWellFounded(R(x;y)) == f:(T). x,y:T. R(x;y)  f(x)<f(y)[strongwellfounded]
Def lconnects(p;i;j)
Def == lpath(p)
Def == & (||p|| = 0    i = j  Id)
Def == & (||p|| = 0    i = source(hd(p)) & j = destination(last(p)))		[lconnects]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 rel 1 sqequal 1 union mb basic mb nat mb list 1 num thy 1 mb list 2 mb event system 1

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

mb event system 2 Sections EventSystems Doc