---

{ [Info:Type]
    es:EO+(Info). e:E. P:{e':E| (e' <loc e)}   .
      ((can-apply(last(P);e)  a:E. ((a <loc e)  ((P a))))
       (do-apply(last(P);e) <loc e)
         ((P do-apply(last(P);e)))
         (e'':E
             ((e'' <loc e)  (do-apply(last(P);e) <loc e'')  ((P e'')))) 
        supposing can-apply(last(P);e)) }

{ Proof }

---

Definitions occuring in Statement :  es-local-pred: last(P),  event-ordering+: EO+(Info),  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,  set: {x:A| B[x]} ,  apply: f a,  function: x:A  B[x],  universe: Type,  do-apply: do-apply(f;x),  can-apply: can-apply(f;x)
Definitions :  isect: x:A. B[x],  uall: [x:A]. B[x],  Try: Error :Try,  Auto: Error :Auto,  CollapseTHENA: Error :CollapseTHENA,  CollapseTHEN: Error :CollapseTHEN,  tactic: Error :tactic
Lemmas :  es-local-pred-property2

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}P:\{e':E|  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbB{}.
        ((\muparrow{}can-apply(last(P);e)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:E.  ((a  <loc  e)  \mwedge{}  (\muparrow{}(P  a))))
        \mwedge{}  (do-apply(last(P);e)  <loc  e)
            \mwedge{}  (\muparrow{}(P  do-apply(last(P);e)))
            \mwedge{}  (\mforall{}e'':E.  ((e''  <loc  e)  {}\mRightarrow{}  (do-apply(last(P);e)  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e'')))) 
            supposing  \muparrow{}can-apply(last(P);e))


Date html generated: 2011_08_16-PM-04_42_56
Last ObjectModification: 2011_06_20-AM-01_02_46

Home Index