---

{ [Info:Type]
    es:EO+(Info)
      [A:Type]
        Ias:EClass(A) List. e:E.
          (e  first-eclass(Ias)  (IIas. e  I)) }

{ Proof }

---

Definitions occuring in Statement :  first-eclass: first-eclass(Xs),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  assert: b,  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  list: type List,  universe: Type,  l_exists: (xL. P[x])
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  member: t  T,  subtype: S  T,  so_lambda: x y.t[x; y],  prop: ,  so_lambda: x.t[x],  and: P  Q,  implies: P  Q,  rev_implies: P  Q,  so_apply: x[s1;s2],  so_apply: x[s]
Lemmas :  es-E_wf,  event-ordering+_inc,  eclass_wf,  event-ordering+_wf,  assert_wf,  in-eclass_wf,  first-eclass_wf,  top_wf,  es-interface-top,  l_exists_wf,  l_member_wf,  iff_functionality_wrt_iff,  in-first-eclass

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A:Type].  \mforall{}Ias:EClass(A)  List.  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  first-eclass(Ias)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}I\mmember{}Ias.  \muparrow{}e  \mmember{}\msubb{}  I))


Date html generated: 2011_08_16-PM-04_31_40
Last ObjectModification: 2011_06_20-AM-00_53_22

Home Index