---

es-p-local-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,  implies: P  Q,  es-locl: (e <loc e'),  not: A,  apply: f a
FDL editor aliases :  es-p-local-pred

---

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


Date html generated: 2010_08_27-AM-09_36_31
Last ObjectModification: 2009_12_16-AM-08_23_31

Home Index