Nuprl - mb_event_system_3 Citations of all

mb event system 3 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def

x:A. B(x) == x:A

B(x)

is mentioned by

Thm* B,eq,g:Top.   g [fpf-empty-sub]

Thm* A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A.
Thm* x  dom(f)  f(x)  B(x) [fpf-ap_wf]

Thm* B:(AType), f:x:A fp-> B(x). fpf-is-empty(f)  f =   x:A fp-> B(x) [assert-fpf-is-empty]

Thm* A:Type, B:(AType).   x:A fp-> B(x) [fpf-empty_wf]

Thm* eq:EqDecider(Y), f:x:X fp-> Top, x:Y.
Thm* strong-subtype(X;Y)  x  dom(f)  x  X [fpf-dom-type2]

Thm* eq:EqDecider(Y), f:x:X fp-> Top, x:Y.
Thm* strong-subtype(X;Y)  x  dom(f)  x  X [fpf-dom-type]

Thm* eq1,eq2:EqDecider(A), f:a:A fp-> Top, x:A. x  dom(f)  x  dom(f) [fpf-dom_functionality2]

Thm* B:(AType), eq1,eq2:EqDecider(A), f:a:A fp-> B(a), x:A.
Thm* x  dom(f) = x  dom(f)   [fpf-dom_functionality]

Thm* B1:(A1Type), B2:(A2Type).
Thm* strong-subtype(A1;A2)
Thm*
Thm* (a:A1. B1(a) r B2(a))  (a:A1 fp-> B1(a) r a:A2 fp-> B2(a)) [subtype-fpf3]

Thm* B1,B2:(AType).
Thm* (a:A. B1(a) r B2(a))  (a:A fp-> B1(a) r a:A fp-> B2(a)) [subtype-fpf2]

Thm* i:Id, w:World, p:FairFifo, t:.
Thm* isnull(a(i;t))  (valtype(<i,t>) ~ valtype(i;a(i;t))) [es-valtype-w-valtype]

Thm* 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]

Thm* the_w:World, e,e':E.
Thm* FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e') [w-locl-iff]

Thm* the_w:World, e,e':E. FairFifo  e <c e'  time(e)<time(e') [w-causl-time]

Thm* the_w:World, e:E.
Thm* FairFifo  isrcv(kind(e))  index(e)  ||sends(lnk(kind(e));sender(e))|| [w-index_wf]

Thm* the_w:World, e:E. FairFifo  isrcv(kind(e))  sender(e)  E [w-sender_wf]

Thm* 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]

Thm* 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]

Thm* the_w:World, e:E.
Thm* FairFifo
Thm*
Thm* isrcv(kind(e))
Thm*
Thm* (t:time(e).
Thm* (match(lnk(kind(e));t;time(e))
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) [better-w-match-exists]

Thm* the_w:World, e:E.
Thm* FairFifo  isrcv(kind(e))  (t:time(e). match(lnk(kind(e));t;time(e))) [w-match-exists]

Thm* 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]

Thm* the_w:World, l:IdLnk, t,t':. match(l;t;t')   [w-match_wf]

Thm* the_w:World, l:IdLnk, e:E. sends(l;e)  Msg_sub(l; the_w.M) List [better-w-sends-wf]

Thm* the_w:World, e:E. first(e)  pred(e)  E [w-pred_wf]

Thm* the_w:World, t:, i:Id. first(<i,t>)  pred(<i,t>)  E [w-pred-aux]

Thm* the_w:World, e:E. <loc(e),time(e)> ~ e [w-loc-time]

Thm* the_w:World, e:E. first(e)  (t':. t'<time(e)  isnull(a(loc(e);t'))) [assert-w-first]

Thm* the_w:World, e:E. first(e)   [w-first_wf]

Thm* the_w:World, i:Id, t:. first(<i,t>)   [w-first-aux]

Thm* the_w:World, x:Id, e:E. (x after e)  vartype(loc(e);x) [w-after_wf]

Thm* the_w:World, x:Id, e:E. (x when e)  vartype(loc(e);x) [w-when_wf]

Thm* the_w:World, e:E. val(e)  V(loc(e);kind(e)) [w-eval_wf]

Thm* the_w:World, i:Id, k:Knd. V(i;k)  Type [w-V_wf]

Thm* the_w:World, e:E. kind(e)  Knd [w-ekind_wf]

Thm* the_w:World, e:E. isnull(act(e)) [w-act-not-null]

Thm* the_w:World, e:E. act(e)  {a:Action(loc(e))| isnull(a) } [w-act_wf]

Thm* the_w:World, e,e':E. e = e'  e = e' [assert-w-eq-E-iff]

Thm* the_w:World, e,e':E. e = e'  e = e' [assert-w-eq-E]

Thm* the_w:World. FairFifo  Prop [fair-fifo_wf]

Thm* the_w:World, i:Id, a:Action(i), l:IdLnk. isrcv(l;a)  msg(a)  Msg [w-msg_wf]

Thm* the_w:World, l:IdLnk, t:. m(l;t)  Msg List [w-ml_wf]

Thm* the_w:World, tg:Id, mss:Msg List. w-tagged(tg; mss)  Msg List [w-tagged_wf]

Thm* the_w:World, l:IdLnk, mss:Msg List.
Thm* withlnk(l;mss)  (t:Idthe_w.M(l,t)) List [w-withlnk_wf]

Thm* w:World, t:, l:IdLnk, i:Id. ||onlnk(l;m(i;t))||   [w-onlnk-m]

Thm* the_w:World, l:IdLnk, mss:Msg List. onlnk(l;mss)  Msg List [w-onlnk_wf]

Thm* the_w:World, i:Id, t:.
Thm* m(i;t)  {m:Msg(the_w.M)| source(mlnk(m)) = i } List [w-m_wf]

Thm* the_w:World, i:Id, t:. a(i;t)  Action(i) [w-a_wf]

Thm* the_w:World, i:Id, t:, x:Id. s(i;t).x  vartype(i;x) [w-s_wf]

Thm* the_w:World. Msg  Type [w-Msg_wf]

Thm* the_w:World, l:IdLnk, i:Id, a:Action(i).
Thm* isrcv(l;a)  isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = l [assert-w-isrcvl]

Thm* the_w:World, l:IdLnk, i:Id, a:Action(i). isrcv(l;a)   [w-isrcvl_wf]

Thm* the_w:World, i:Id, a:Action(i). isnull(a)  val(a)  valtype(i;a) [w-val_wf]

Thm* the_w:World, i:Id, a:Action(i). isnull(a)  valtype(i;a)  Type [w-valtype_wf]

Thm* the_w:World, i:Id, a:Action(i). isnull(a)  kind(a)  Knd [w-kind_wf]

Thm* the_w:World, i:Id, a:Action(i). isnull(a)   [w-isnull_wf]

Thm* w:World. w.T  IdIdType [w-T_wf]

Thm* w:World. w.TA  IdIdType [w-TA_wf]

Thm* w:World. w.M  IdLnkIdType [w-M_wf]

Thm* i:Id, TA:(IdIdType), M:(IdLnkIdType).
Thm* w-action-dec(TA;M;i)  KndType [w-action-dec_wf]

Thm* es:ES, l:IdLnk, tg:Id, e:E.
Thm* kind(e) = rcv(l; tg)
Thm*
Thm* isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l) [es-kind-rcv]

Thm* es:ES, l:IdLnk, tg:Id, e:E.
Thm* isrcv(e)  lnk(e) = l  tag(e) = tg  kind(e) = rcv(l; tg) [es-rcv-kind]

Thm* es:ES, x,i:Id, T:Type, c:T.
Thm* (x,y:T. Dec(x = y  T))
Thm*
Thm* (vartype(i;x) r T)
Thm*
Thm* (e:E. loc(e) = i  Id  first(e)  (x when e) = c  T)
Thm*
Thm* (e':E.
Thm* (loc(e') = i  Id
Thm* (
Thm* ((x after e') = c  T
Thm* (
Thm* ((ev:E. ev  e'  & (x after ev) = (x when ev)  T)) [change-since-init]

Thm* es:ES, e':E. e:E. first(e) & e  e' [es-first-exists]

Thm* es:ES, x,i:Id, T:Type.
Thm* (x,y:T. Dec(x = y  T))
Thm*
Thm* (vartype(i;x) r T)
Thm*
Thm* (e',e:E.
Thm* (e  e'
Thm* (
Thm* (loc(e') = i  Id
Thm* (
Thm* ((x after e') = (x when e)  T
Thm* (
Thm* ((ev:E. e  ev  & ev  e'  & (x after ev) = (x when ev)  T)) [change-lemma]

Thm* es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop). e@i.P(e)  Prop [existse-at_wf]

Thm* es:ES, i,x:Id, T:Type, I:(TProp).
Thm* (vartype(i;x) r T) & e@i.first(e)  I((x when e))
Thm*
Thm* e@i.I((x when e))  I((x after e))  @i always.I(x) [es-invariant1]

Thm* es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop).
Thm* e@i.P(e)  e@i.first(e)  P(e) & e@i.first(e)  P(pred(e))  P(e) [alle-at-iff]

Thm* es:ES, x:Id, e:E.
Thm* first(e)  (x after pred(e)) = (x when e)  vartype(loc(e);x) [es-after-pred]

Thm* the_es:ES, e:E, l:IdLnk, tg:Id. sends(l,tg,e)  (Msg on l) List [es-tg-sends_wf]

Thm* the_es:ES, m:Msg. mlnk(m)  IdLnk [mlnk_wf2]

Thm* es:ES, e,e':E. [e, e']  {ev:E| loc(ev) = loc(e')  Id } List [es-interval_wf2]

Thm* es:ES, e,e',ev:E. (ev  [e, e'])  e  ev  & ev  e' [member-es-interval]

Thm* the_es:ES, e',e:E. (e  before(e'))  (e <loc e') [member-es-before]

Thm* the_es:ES, e:E. before(e)  E List [es-before_wf]

Thm* the_es:ES, m:Msg. mtag(m)  Id [es-mtag_wf]

Thm* es:ES, e,e':E. es-ble{i:l}(es;e;e')  e  e' [assert-es-ble]

Thm* es:ES, e,e':E. es-ble{i:l}(es;e;e')   [es-ble_wf]

Def f  g == x:A. x  dom(f)  x  dom(g) & f(x) = g(x)  B(x) [fpf-sub]

Def FairFifo
Def == (i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List)
Def == & (i:Id, t:.
Def == & (isnull(a(i;t))
Def == & (
Def == & ((x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x))
Def == & (& m(i;t) = nil  Msg List)
Def == & (i:Id, t:, l:IdLnk.
Def == & (isrcv(l;a(i;t))
Def == & (
Def == & (destination(l) = i
Def == & (& ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg)
Def == & (l:IdLnk, t:.
Def == & (t':.
Def == & (tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List) [fair-fifo]

Def e@i.P(e) == e:E. loc(e) = i  Id  P(e) [alle-at]

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 mb event system 2

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

mb event system 3 Sections EventSystems Doc

Thm* B,eq,g:Top. g	[fpf-empty-sub]
Thm* A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A. Thm* x dom(f) f(x) B(x)	[fpf-ap_wf]
Thm* B:(AType), f:x:A fp-> B(x). fpf-is-empty(f) f = x:A fp-> B(x)	[assert-fpf-is-empty]
Thm* A:Type, B:(AType). x:A fp-> B(x)	[fpf-empty_wf]
Thm* eq:EqDecider(Y), f:x:X fp-> Top, x:Y. Thm* strong-subtype(X;Y) x dom(f) x X	[fpf-dom-type2]
Thm* eq:EqDecider(Y), f:x:X fp-> Top, x:Y. Thm* strong-subtype(X;Y) x dom(f) x X	[fpf-dom-type]
Thm* eq1,eq2:EqDecider(A), f:a:A fp-> Top, x:A. x dom(f) x dom(f)	[fpf-dom_functionality2]
Thm* B:(AType), eq1,eq2:EqDecider(A), f:a:A fp-> B(a), x:A. Thm* x dom(f) = x dom(f)	[fpf-dom_functionality]
Thm* B1:(A1Type), B2:(A2Type). Thm* strong-subtype(A1;A2) Thm* Thm* (a:A1. B1(a) r B2(a)) (a:A1 fp-> B1(a) r a:A2 fp-> B2(a))	[subtype-fpf3]
Thm* B1,B2:(AType). Thm* (a:A. B1(a) r B2(a)) (a:A fp-> B1(a) r a:A fp-> B2(a))	[subtype-fpf2]
Thm* i:Id, w:World, p:FairFifo, t:. Thm* isnull(a(i;t)) (valtype(<i,t>) ~ valtype(i;a(i;t)))	[es-valtype-w-valtype]
Thm* 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]
Thm* the_w:World, e,e':E. Thm* FairFifo (e <loc e' loc(e) = loc(e') Id & e <c e')	[w-locl-iff]
Thm* the_w:World, e,e':E. FairFifo e <c e' time(e)<time(e')	[w-causl-time]
Thm* the_w:World, e:E. Thm* FairFifo isrcv(kind(e)) index(e) \|\|sends(lnk(kind(e));sender(e))\|\|	[w-index_wf]
Thm* the_w:World, e:E. FairFifo isrcv(kind(e)) sender(e) E	[w-sender_wf]
Thm* 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]
Thm* 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]
Thm* the_w:World, e:E. Thm* FairFifo Thm* Thm* isrcv(kind(e)) Thm* Thm* (t:time(e). Thm* (match(lnk(kind(e));t;time(e)) 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)	[better-w-match-exists]
Thm* the_w:World, e:E. Thm* FairFifo isrcv(kind(e)) (t:time(e). match(lnk(kind(e));t;time(e)))	[w-match-exists]
Thm* 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]
Thm* the_w:World, l:IdLnk, t,t':. match(l;t;t')	[w-match_wf]
Thm* the_w:World, l:IdLnk, e:E. sends(l;e) Msg_sub(l; the_w.M) List	[better-w-sends-wf]
Thm* the_w:World, e:E. first(e) pred(e) E	[w-pred_wf]
Thm* the_w:World, t:, i:Id. first(<i,t>) pred(<i,t>) E	[w-pred-aux]
Thm* the_w:World, e:E. <loc(e),time(e)> ~ e	[w-loc-time]
Thm* the_w:World, e:E. first(e) (t':. t'<time(e) isnull(a(loc(e);t')))	[assert-w-first]
Thm* the_w:World, e:E. first(e)	[w-first_wf]
Thm* the_w:World, i:Id, t:. first(<i,t>)	[w-first-aux]
Thm* the_w:World, x:Id, e:E. (x after e) vartype(loc(e);x)	[w-after_wf]
Thm* the_w:World, x:Id, e:E. (x when e) vartype(loc(e);x)	[w-when_wf]
Thm* the_w:World, e:E. val(e) V(loc(e);kind(e))	[w-eval_wf]
Thm* the_w:World, i:Id, k:Knd. V(i;k) Type	[w-V_wf]
Thm* the_w:World, e:E. kind(e) Knd	[w-ekind_wf]
Thm* the_w:World, e:E. isnull(act(e))	[w-act-not-null]
Thm* the_w:World, e:E. act(e) {a:Action(loc(e))\| isnull(a) }	[w-act_wf]
Thm* the_w:World, e,e':E. e = e' e = e'	[assert-w-eq-E-iff]
Thm* the_w:World, e,e':E. e = e' e = e'	[assert-w-eq-E]
Thm* the_w:World. FairFifo Prop	[fair-fifo_wf]
Thm* the_w:World, i:Id, a:Action(i), l:IdLnk. isrcv(l;a) msg(a) Msg	[w-msg_wf]
Thm* the_w:World, l:IdLnk, t:. m(l;t) Msg List	[w-ml_wf]
Thm* the_w:World, tg:Id, mss:Msg List. w-tagged(tg; mss) Msg List	[w-tagged_wf]
Thm* the_w:World, l:IdLnk, mss:Msg List. Thm* withlnk(l;mss) (t:Idthe_w.M(l,t)) List	[w-withlnk_wf]
Thm* w:World, t:, l:IdLnk, i:Id. \|\|onlnk(l;m(i;t))\|\|	[w-onlnk-m]
Thm* the_w:World, l:IdLnk, mss:Msg List. onlnk(l;mss) Msg List	[w-onlnk_wf]
Thm* the_w:World, i:Id, t:. Thm* m(i;t) {m:Msg(the_w.M)\| source(mlnk(m)) = i } List	[w-m_wf]
Thm* the_w:World, i:Id, t:. a(i;t) Action(i)	[w-a_wf]
Thm* the_w:World, i:Id, t:, x:Id. s(i;t).x vartype(i;x)	[w-s_wf]
Thm* the_w:World. Msg Type	[w-Msg_wf]
Thm* the_w:World, l:IdLnk, i:Id, a:Action(i). Thm* isrcv(l;a) isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = l	[assert-w-isrcvl]
Thm* the_w:World, l:IdLnk, i:Id, a:Action(i). isrcv(l;a)	[w-isrcvl_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a) val(a) valtype(i;a)	[w-val_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a) valtype(i;a) Type	[w-valtype_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a) kind(a) Knd	[w-kind_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a)	[w-isnull_wf]
Thm* w:World. w.T IdIdType	[w-T_wf]
Thm* w:World. w.TA IdIdType	[w-TA_wf]
Thm* w:World. w.M IdLnkIdType	[w-M_wf]
Thm* i:Id, TA:(IdIdType), M:(IdLnkIdType). Thm* w-action-dec(TA;M;i) KndType	[w-action-dec_wf]
Thm* es:ES, l:IdLnk, tg:Id, e:E. Thm* kind(e) = rcv(l; tg) Thm* Thm* isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l)	[es-kind-rcv]
Thm* es:ES, l:IdLnk, tg:Id, e:E. Thm* isrcv(e) lnk(e) = l tag(e) = tg kind(e) = rcv(l; tg)	[es-rcv-kind]
Thm* es:ES, x,i:Id, T:Type, c:T. Thm* (x,y:T. Dec(x = y T)) Thm* Thm* (vartype(i;x) r T) Thm* Thm* (e:E. loc(e) = i Id first(e) (x when e) = c T) Thm* Thm* (e':E. Thm* (loc(e') = i Id Thm* ( Thm* ((x after e') = c T Thm* ( Thm* ((ev:E. ev e' & (x after ev) = (x when ev) T))	[change-since-init]
Thm* es:ES, e':E. e:E. first(e) & e e'	[es-first-exists]
Thm* es:ES, x,i:Id, T:Type. Thm* (x,y:T. Dec(x = y T)) Thm* Thm* (vartype(i;x) r T) Thm* Thm* (e',e:E. Thm* (e e' Thm* ( Thm* (loc(e') = i Id Thm* ( Thm* ((x after e') = (x when e) T Thm* ( Thm* ((ev:E. e ev & ev e' & (x after ev) = (x when ev) T))	[change-lemma]
Thm* es:ES, i:Id, P:({e:E\| loc(e) = i Id }Prop). e@i.P(e) Prop	[existse-at_wf]
Thm* es:ES, i,x:Id, T:Type, I:(TProp). Thm* (vartype(i;x) r T) & e@i.first(e) I((x when e)) Thm* Thm* e@i.I((x when e)) I((x after e)) @i always.I(x)	[es-invariant1]
Thm* es:ES, i:Id, P:({e:E\| loc(e) = i Id }Prop). Thm* e@i.P(e) e@i.first(e) P(e) & e@i.first(e) P(pred(e)) P(e)	[alle-at-iff]
Thm* es:ES, x:Id, e:E. Thm* first(e) (x after pred(e)) = (x when e) vartype(loc(e);x)	[es-after-pred]
Thm* the_es:ES, e:E, l:IdLnk, tg:Id. sends(l,tg,e) (Msg on l) List	[es-tg-sends_wf]
Thm* the_es:ES, m:Msg. mlnk(m) IdLnk	[mlnk_wf2]
Thm* es:ES, e,e':E. [e, e'] {ev:E\| loc(ev) = loc(e') Id } List	[es-interval_wf2]
Thm* es:ES, e,e',ev:E. (ev [e, e']) e ev & ev e'	[member-es-interval]
Thm* the_es:ES, e',e:E. (e before(e')) (e <loc e')	[member-es-before]
Thm* the_es:ES, e:E. before(e) E List	[es-before_wf]
Thm* the_es:ES, m:Msg. mtag(m) Id	[es-mtag_wf]
Thm* es:ES, e,e':E. es-ble{i:l}(es;e;e') e e'	[assert-es-ble]
Thm* es:ES, e,e':E. es-ble{i:l}(es;e;e')	[es-ble_wf]
Def f g == x:A. x dom(f) x dom(g) & f(x) = g(x) B(x)	[fpf-sub]
Def FairFifo Def == (i:Id, t:, l:IdLnk. source(l) = i onlnk(l;m(i;t)) = nil Msg List) Def == & (i:Id, t:. Def == & (isnull(a(i;t)) Def == & ( Def == & ((x:Id. s(i;t+1).x = s(i;t).x vartype(i;x)) Def == & (& m(i;t) = nil Msg List) Def == & (i:Id, t:, l:IdLnk. Def == & (isrcv(l;a(i;t)) Def == & ( Def == & (destination(l) = i Def == & (& \|\|queue(l;t)\|\|1 & hd(queue(l;t)) = msg(a(i;t)) Msg) Def == & (l:IdLnk, t:. Def == & (t':. Def == & (tt' & isrcv(l;a(destination(l);t')) queue(l;t') = nil Msg List)	[fair-fifo]
Def e@i.P(e) == e:E. loc(e) = i Id P(e)	[alle-at]