Nuprl Definition : first-in-eclass
first-in-eclass(es;e;X) == member-eclass(es;e;X) 
(
e 
prior(X))
Proof not projected
Definitions occuring in Statement :
es-prior-interface: prior(X),
in-eclass: e X,
member-eclass: member-eclass(es;e;X),
band: p q,
bnot: b
Definitions :
band: p q,
member-eclass: member-eclass(es;e;X),
bnot: b,
in-eclass: e X,
es-prior-interface: prior(X)
FDL editor aliases :
first-in-eclass
first-in-eclass(es;e;X) == member-eclass(es;e;X) \mwedge{}\msubb{} (\mneg{}\msubb{}e \mmember{}\msubb{} prior(X))
Date html generated:
2011_10_21-AM-00_00_46
Last ObjectModification:
2011_05_20-AM-11_04_59
Home
Index