---

f:X  Y:T ==
  (e:E(X). ((Y(f e) = X(e))  (e < f e)))
   LocalOrderPreserving(f)
   Inj(E(X);E(Y);f)

---

Definitions :  all: x:A. B[x],  equal: s = t,  eclass-val: X(e),  es-causl: (e < e'),  apply: f a,  and: P  Q,  es-locl-op: LocalOrderPreserving(f),  inject: Inj(A;B;f),  es-E-interface: E(X)
FDL editor aliases :  es-fwd-propagation-via

---

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: 2010_08_27-PM-02_41_46
Last ObjectModification: 2010_03_24-PM-03_19_00

Home Index