---

(P  Q) ==
  e.e':E
      (e loc e' 
       (Q e')
       (e'':E. (e loc e''   (e'' <loc e')  (P e''))))

---

Definitions :  lambda: x.A[x],  exists: x:A. B[x],  and: P  Q,  all: x:A. B[x],  es-E: E,  es-le: e loc e' ,  implies: P  Q,  es-locl: (e <loc e'),  apply: f a
FDL editor aliases :  es-until

---

(P  \mcup{}  Q)  ==    \mlambda{}e.\mexists{}e':E.  (e  \mleq{}loc  e'    \mwedge{}  (Q  e')  \mwedge{}  (\mforall{}e'':E.  (e  \mleq{}loc  e''    {}\mRightarrow{}  (e''  <loc  e')  {}\mRightarrow{}  (P  e''))))


Date html generated: 2010_08_27-AM-09_29_44
Last ObjectModification: 2009_12_16-AM-01_05_17

Home Index