---

{ [Info:Type]. [P:es:EO+(Info)  E  ].
    ((es:EO+(Info). e:E.  Dec(P es e))
     (X:EClass({e:E| P es e} )
         es:EO+(Info). e:E.
           ((e  X  a:{e:E| P es e} . (es-p-le-pred(es;P es) e a))
            es-p-le-pred(es;P es) 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,  decidable: Dec(P),  uimplies: b supposing a,  uall: [x:A]. B[x],  prop: ,  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  implies: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  apply: f a,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  prop: ,  implies: P  Q,  all: x:A. B[x],  member: t  T,  so_lambda: x y.t[x; y],  so_lambda: so_lambda(x,y,z.t[x; y; z]),  decidable: Dec(P),  exists: x:A. B[x],  or: P  Q,  not: A,  guard: {T},  so_apply: x[s1;s2],  so_apply: x[s1;s2;s3],  false: False,  es-p-le-pred: es-p-le-pred(es;P),  and: P  Q,  cand: A c B,  subtype: S  T
Lemmas :  es-interface-from-decidable,  es-E_wf,  event-ordering+_inc,  es-p-le-pred_wf,  event-ordering+_wf,  decidable_wf,  decidable__exists-es-p-le-pred,  not_wf

---

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


Date html generated: 2011_08_16-PM-04_39_27
Last ObjectModification: 2011_06_20-AM-01_01_42

Home Index