Nuprl Definition : es-local-le-pred
≤(P) == fix((λes-local-le-pred,es,e. if P es e then {e} if first(e) then {} else es-local-le-pred es pred(e) fi ))
Definitions occuring in Statement :
es-first: first(e),
es-pred: pred(e),
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
single-bag: {x},
empty-bag: {}
FDL editor aliases :
es-local-le-pred
Latex:
\mleq{}(P) ==
fix((\mlambda{}es-local-le-pred,es,e. if P es e then \{e\}
if first(e) then \{\}
else es-local-le-pred es pred(e)
fi ))
Date html generated:
2015_07_20-PM-04_07_32
Last ObjectModification:
2012_07_02-PM-04_11_33
Home
Index