Nuprl Definition : class-caused-by
X <-- Z == ∀e':E. ∀v:T. (v ∈ X(e') ⇒ (↓∃e:E. ((e < e') ∧ <loc(e'), info(e')> ∈ Z(e))))
Definitions occuring in Statement :
Message: Message(f),
classrel: v ∈ X(e),
es-info: info(e),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
pair: <a, b>,
product: x:A × B[x]
FDL editor aliases :
class-caused-by
Latex:
X <-- Z == \mforall{}e':E. \mforall{}v:T. (v \mmember{} X(e') {}\mRightarrow{} (\mdownarrow{}\mexists{}e:E. ((e < e') \mwedge{} <loc(e'), info(e')> \mmember{} Z(e))))
Date html generated:
2015_07_21-PM-04_50_55
Last ObjectModification:
2013_02_27-PM-02_50_13
Home
Index