---

{ [Info:Type]
    es:EO+(Info)
      [T:Type]
        X:EClass(T). e:E.  (e  (X)  e':E. (e' loc e   (e'  X))) }

{ Proof }

---

Definitions occuring in Statement :  es-latest-val: (X),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-le: e loc e' ,  es-E: E,  assert: b,  uall: [x:A]. B[x],  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  and: P  Q,  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  exists: x:A. B[x],  and: P  Q,  implies: P  Q,  rev_implies: P  Q,  member: t  T,  prop: ,  so_lambda: x y.t[x; y],  es-le: e loc e' ,  cand: A c B,  or: P  Q,  guard: {T},  squash: T,  true: True,  so_apply: x[s1;s2],  uimplies: b supposing a,  subtype: S  T
Lemmas :  assert_witness,  in-eclass_wf,  es-latest-val_wf,  top_wf,  es-interface-top,  assert_wf,  es-E_wf,  event-ordering+_inc,  es-le_wf,  eclass_wf,  event-ordering+_wf,  latest-val-cases,  es-locl_wf,  is-prior-val,  es-le_weakening,  has-latest-val,  es-prior-val_wf,  squash_wf,  true_wf,  bool_wf

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}[T:Type].  \mforall{}X:EClass(T).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  (X)\msupminus{}  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  (e'  \mleq{}loc  e    \mwedge{}  (\muparrow{}e'  \mmember{}\msubb{}  X)))


Date html generated: 2011_08_16-PM-05_08_29
Last ObjectModification: 2011_06_20-AM-01_11_41

Home Index