---

{ [Info:Type]
    es:EO+(Info). X:EClass(Top). e:E.
      le(X)(e) loc e 
       (le(X)(e)  X)
       (e'':E. (e'' loc e   (le(X)(e) <loc e'')  (e''  X))) 
      supposing e  le(X) }

{ Proof }

---

Definitions occuring in Statement :  es-le-interface: le(X),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-le: e loc e' ,  es-locl: (e <loc e'),  es-E: E,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  all: x:A. B[x],  not: A,  implies: P  Q,  and: P  Q,  universe: Type
Definitions :  top: Top,  member: t  T,  all: x:A. B[x],  so_lambda: x y.t[x; y],  uall: [x:A]. B[x],  uimplies: b supposing a,  so_apply: x[s1;s2],  and: P  Q,  subtype: S  T,  es-le-interface: le(X)
Lemmas :  in-eclass_wf,  es-le-interface_wf,  top_wf,  es-interface-subtype_rel2,  es-E-interface_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  es-local-le-pred-property,  assert_wf,  eclass_wf

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.
        le(X)(e)  \mleq{}loc  e 
        \mwedge{}  (\muparrow{}le(X)(e)  \mmember{}\msubb{}  X)
        \mwedge{}  (\mforall{}e'':E.  (e''  \mleq{}loc  e    {}\mRightarrow{}  (le(X)(e)  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}e''  \mmember{}\msubb{}  X))) 
        supposing  \muparrow{}e  \mmember{}\msubb{}  le(X)


Date html generated: 2011_08_16-PM-04_47_49
Last ObjectModification: 2011_06_20-AM-01_05_33

Home Index