---

{ [Info:Type]
    es:EO+(Info). X:EClass(Top). L:E List. e:E.
      ((e  eclass-events(es;X;L))  {(e  X)  (e  L)}) }

{ Proof }

---

Definitions occuring in Statement :  eclass-events: eclass-events(es;X;L),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  assert: b,  uall: [x:A]. B[x],  top: Top,  guard: {T},  all: x:A. B[x],  iff: P  Q,  and: P  Q,  list: type List,  universe: Type,  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  eclass-events: eclass-events(es;X;L),  guard: {T},  member: t  T,  so_lambda: x y.t[x; y],  prop: ,  and: P  Q,  cand: A c B,  iff: P  Q,  implies: P  Q,  rev_implies: P  Q,  so_apply: x[s1;s2],  subtype: S  T
Lemmas :  es-E_wf,  event-ordering+_inc,  eclass_wf,  top_wf,  event-ordering+_wf,  l_member_wf,  filter_wf,  in-eclass_wf,  assert_wf,  assert_witness,  iff_functionality_wrt_iff,  member_filter

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}L:E  List.  \mforall{}e:E.
        ((e  \mmember{}  eclass-events(es;X;L))  \mLeftarrow{}{}\mRightarrow{}  \{(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (e  \mmember{}  L)\})


Date html generated: 2011_08_16-PM-04_33_00
Last ObjectModification: 2011_06_20-AM-00_54_42

Home Index