Nuprl Definition : es-p-le-pred
es-p-le-pred(es;P) == λe,e'. (e' ≤loc e ∧ (P e') ∧ (∀e'':E. (e'' ≤loc e ⇒ (e' <loc e'') ⇒ (¬(P e'')))))
Definitions occuring in Statement :
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-E: E,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
es-p-le-pred
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:
2015_07_17-AM-08_58_36
Last ObjectModification:
2013_03_25-PM-01_54_31
Home
Index