Nuprl Definition : class-caused-by-some
X <-- p.Z[p] ==
∀e':E. ∀v:T. (v ∈ X(e') ⇒ (↓∃e,start:E. ∃p:A. (start ≤loc e ∧ (e < e') ∧ <loc(e'), info(e')> ∈ Z[p](e))))
Definitions occuring in Statement :
Message: Message(f),
classrel: v ∈ X(e),
eo-forward: eo.e,
es-info: info(e),
es-le: e ≤loc 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-some
Latex:
X <-- p.Z[p] ==
\mforall{}e':E. \mforall{}v:T.
(v \mmember{} X(e') {}\mRightarrow{} (\mdownarrow{}\mexists{}e,start:E. \mexists{}p:A. (start \mleq{}loc e \mwedge{} (e < e') \mwedge{} <loc(e'), info(e')> \mmember{} Z[p](e))))
Date html generated:
2016_05_17-AM-08_54_38
Last ObjectModification:
2013_02_27-PM-02_51_46
Theory : messages
Home
Index