Nuprl Definition : sequence-class
sequence-class(X;Y;Z) == λes,e. case es-first-event(es;λe.((¬be ∈b X) ∧b e ∈b Y);e) of inl(e') => Z(e) | inr(x) => X(e)
Definitions occuring in Statement :
member-eclass: e ∈b X,
class-ap: X(e),
eo-forward: eo.e,
es-first-event: es-first-event(es;P;e),
band: p ∧b q,
bnot: ¬bb,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :
sequence-class
Latex:
sequence-class(X;Y;Z) ==
\mlambda{}es,e. case es-first-event(es;\mlambda{}e.((\mneg{}\msubb{}e \mmember{}\msubb{} X) \mwedge{}\msubb{} e \mmember{}\msubb{} Y);e) of inl(e') => Z(e) | inr(x) => X(e)
Date html generated:
2015_07_21-PM-03_04_25
Last ObjectModification:
2012_12_06-AM-00_25_51
Home
Index