---

{ [Info:Type]
    P:es:EO+(Info)  E  
      X:EClass({e:E| (P es e)} )
       es:EO+(Info). e:E.
         ((e  X  a:E. (es-p-le-pred(es;e.((P es e))) e a))
          es-p-le-pred(es;e.((P es e))) e X(e) supposing e  X) }

{ Proof }

---

Definitions occuring in Statement :  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-p-le-pred: es-p-le-pred(es;P),  es-E: E,  assert: b,  bool: ,  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  universe: Type
Definitions :  member: t  T,  and: P  Q,  all: x:A. B[x],  rev_implies: P  Q,  cand: A c B,  so_lambda: x y.t[x; y],  top: Top,  prop: ,  implies: P  Q,  es-p-le-pred: es-p-le-pred(es;P),  exists: x:A. B[x],  iff: P  Q,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  uimplies: b supposing a,  subtype: S  T
Lemmas :  event-ordering+_wf,  event-ordering+_inc,  es-E_wf,  iff_functionality_wrt_iff,  not_wf,  es-locl_wf,  es-le_wf,  top_wf,  es-interface-subtype_rel2,  in-eclass_wf,  assert_wf

---

\mforall{}[Info:Type]
    \mforall{}P:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbB{}
        \mexists{}X:EClass(\{e:E|  \muparrow{}(P  es  e)\}  )
          \mforall{}es:EO+(Info).  \mforall{}e:E.
              ((\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:E.  (es-p-le-pred(es;\mlambda{}e.(\muparrow{}(P  es  e)))  e  a))
              \mwedge{}  es-p-le-pred(es;\mlambda{}e.(\muparrow{}(P  es  e)))  e  X(e)  supposing  \muparrow{}e  \mmember{}\msubb{}  X)


Date html generated: 2011_08_16-PM-04_39_35
Last ObjectModification: 2011_06_20-AM-01_01_51

Home Index