Nuprl Definition : class-le-before
class-le-before(X;es;e) == 
e'
loc(e).X es e'
Proof not projected
Definitions occuring in Statement :
es-le-before: loc(e),
apply: f a,
bag-combine: xbs.f[x]
FDL editor aliases :
class-le-before
class-le-before(X;es;e) == \mcup{}e'\mmember{}\mleq{}loc(e).X es e'
Date html generated:
2011_10_20-PM-03_17_58
Last ObjectModification:
2011_09_02-PM-05_10_31
Home
Index