Nuprl Definition : es-fwd-propagation-via
f:X ⇒ Y:T == (∀e:E(X). ((Y(f e) = X(e) ∈ T) ∧ (e < f e))) ∧ LocalOrderPreserving(f) ∧ Inj(E(X);E(Y);f)
Definitions occuring in Statement :
es-E-interface: E(X),
eclass-val: X(e),
es-locl-op: LocalOrderPreserving(f),
es-causl: (e < e'),
inject: Inj(A;B;f),
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
es-fwd-propagation-via
Latex:
f:X {}\mRightarrow{} Y:T == (\mforall{}e:E(X). ((Y(f e) = X(e)) \mwedge{} (e < f e))) \mwedge{} LocalOrderPreserving(f) \mwedge{} Inj(E(X);E(Y);f)
Date html generated:
2015_07_21-PM-03_26_46
Last ObjectModification:
2012_02_25-PM-02_26_36
Home
Index