---

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

---

Definitions :  lambda: x.A[x],  and: P  Q,  all: x:A. B[x],  es-E: E,  implies: P  Q,  es-causl: (e < e'),  not: A,  apply: f a
FDL editor aliases :  es-p-immediate-pred

---

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


Date html generated: 2010_08_27-AM-09_42_50
Last ObjectModification: 2009_12_17-PM-10_50_54

Home Index