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
Latex:
first(e) == pred(e) = e \mvee{}\msubb{}(\mneg{}\msubb{}(es-dom(es) pred(e)))
Date html generated:
2016_05_16-AM-09_16_05
Last ObjectModification:
2013_03_23-PM-06_40_40
Theory : new!event-ordering
Home
Index