Nuprl Definition : es-first
first(e) == pred(e) = e ∨b(¬b(es-dom(es) pred(e)))
Definitions occuring in Statement :
es-pred: pred(e),
es-eq-E: e = e',
es-dom: es-dom(es),
bor: p ∨bq,
bnot: ¬bb,
apply: f a
FDL editor aliases :
es-first
es-first
first(e) == pred(e) = e \mvee{}\msubb{}(\mneg{}\msubb{}(es-dom(es) pred(e)))
Date html generated:
2015_07_17-AM-08_35_02
Last ObjectModification:
2013_03_23-PM-06_40_40
Home
Index