Nuprl Definition : causal-class-rel-in-out
if class_out outputs (m) then class_in observed x == ∀e:E. (m ∈ class_out(e) ⇒ (↓∃e':E. (e' c≤ e ∧ x ∈ class_in(e'))))
Definitions occuring in Statement :
Message: Message(f),
classrel: v ∈ X(e),
es-causle: e c≤ e',
es-E: E,
Id: Id,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
product: x:A × B[x]
FDL editor aliases :
causal-class-rel-in-out
Latex:
if class$_{out}$ outputs (m) then class$_{in}$ observed x ==
\mforall{}e:E. (m \mmember{} class$_{out}$(e) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. (e' c\mleq{} e \mwedge{} x \mmember{} class$_{in\mbackslash{}\000Cff7d$(e'))))
Date html generated:
2015_07_21-PM-04_53_10
Last ObjectModification:
2013_02_27-PM-03_24_12
Home
Index