Nuprl Definition : es-p-local-pred
es-p-local-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-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-local-pred
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:
2015_07_17-AM-08_58_27
Last ObjectModification:
2013_03_25-PM-01_54_29
Home
Index