Nuprl Definition : base-class-caused-by
hdr.X <-- p.Z[p] ==
∀e':E. ∀v:f hdr.
(v ∈ X(e') ⇒ (↓∃e,start:E. ∃p:A. (start ≤loc e ∧ (e < e') ∧ <loc(e'), make-Msg(hdr;v)> ∈ Z[p](e))))
Definitions occuring in Statement :
Message: Message(f),
classrel: v ∈ X(e),
eo-forward: eo.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,
apply: f a,
pair: <a, b>,
product: x:A × B[x]
FDL editor aliases :
base-class-caused-by
Latex:
hdr.X <-- p.Z[p] ==
\mforall{}e':E. \mforall{}v:f hdr.
(v \mmember{} X(e')
{}\mRightarrow{} (\mdownarrow{}\mexists{}e,start:E. \mexists{}p:A. (start \mleq{}loc e \mwedge{} (e < e') \mwedge{} <loc(e'), make-Msg(hdr;v)> \mmember{} Z[p](e))))
Date html generated:
2015_07_21-PM-04_51_01
Last ObjectModification:
2013_02_26-PM-01_16_58
Home
Index