---

es-p-le-pred(es;P) ==
  e,e'.
   (e' loc e 
    (P e')
    (e'':E. (e'' loc e   (e' <loc e'')  ((P e'')))))

---

Definitions :  lambda: x.A[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'),  not: A,  apply: f a
FDL editor aliases :  es-p-le-pred

---

es-p-le-pred(es;P)  ==
    \mlambda{}e,e'.(e'  \mleq{}loc  e    \mwedge{}  (P  e')  \mwedge{}  (\mforall{}e'':E.  (e''  \mleq{}loc  e    {}\mRightarrow{}  (e'  <loc  e'')  {}\mRightarrow{}  (\mneg{}(P  e'')))))


Date html generated: 2010_08_27-AM-09_36_33
Last ObjectModification: 2009_12_16-AM-08_23_40

Home Index