Nuprl Definition : message-class-source
message-class-source(Info; es; X; Y) == ∀e:E(X). ∃e':E. ((e' < e) ∧ <loc(e), info(e)> ↓∈ Y es e')
Definitions occuring in Statement :
es-E-interface: E(X),
es-info: info(e),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
pair: <a, b>,
bag-member: x ↓∈ bs
Latex:
message-class-source(Info; es; X; Y) == \mforall{}e:E(X). \mexists{}e':E. ((e' < e) \mwedge{} <loc(e), info(e)> \mdownarrow{}\mmember{} Y es e')
Date html generated:
2015_07_21-PM-03_36_52
Last ObjectModification:
2012_02_25-PM-02_34_11
Home
Index