---

{ [Info:Type]
    P:es:EO+(Info)  E  . es:EO+(Info). e:E.
      ((e  (P)  a:E. (a loc e   ((P es a))))
       (P)(e) loc e 
         ((P es (P)(e)))
         (e'':E. (e'' loc e   ((P)(e) <loc e'')  ((P es e'')))) 
        supposing e  (P)) }

{ Proof }

---

Definitions occuring in Statement :  es-local-le-pred: (P),  eclass-val: X(e),  in-eclass: e  X,  event-ordering+: EO+(Info),  es-le: e loc e' ,  es-locl: (e <loc e'),  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,  not: A,  implies: P  Q,  and: P  Q,  apply: f a,  function: x:A  B[x],  universe: Type
Definitions :  prop: ,  so_lambda: x y.t[x; y],  member: t  T,  cand: A c B,  and: P  Q,  implies: P  Q,  all: x:A. B[x],  so_apply: x[s1;s2],  uall: [x:A]. B[x],  uimplies: b supposing a,  subtype: S  T
Lemmas :  es-le_wf,  es-locl_wf,  es-le_weakening,  es-pred_wf,  es-local-le-pred_wf,  event-ordering+_wf,  assert_wf,  event-ordering+_inc,  es-E_wf,  eclass-val_wf,  es-locl_transitivity1,  es-pred-locl

---

\mforall{}[Info:Type]
    \mforall{}P:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbB{}.  \mforall{}es:EO+(Info).  \mforall{}e:E.
        ((\muparrow{}e  \mmember{}\msubb{}  \mleq{}(P)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:E.  (a  \mleq{}loc  e    \mwedge{}  (\muparrow{}(P  es  a))))
        \mwedge{}  \mleq{}(P)(e)  \mleq{}loc  e 
            \mwedge{}  (\muparrow{}(P  es  \mleq{}(P)(e)))
            \mwedge{}  (\mforall{}e'':E.  (e''  \mleq{}loc  e    {}\mRightarrow{}  (\mleq{}(P)(e)  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  es  e'')))) 
            supposing  \muparrow{}e  \mmember{}\msubb{}  \mleq{}(P))


Date html generated: 2011_08_16-PM-04_43_41
Last ObjectModification: 2011_06_20-AM-01_03_08

Home Index