---

(X | Y)  Z:T ==
  f:E(X)  E(Z)
   g:E(Y)  E(Z)
    (((f:X  Z:T  g:Y  Z:T)  (e:E(X). e':E(Y).  (((f e) = (g e')))))
     (e:E(Z). ((e':E(X). ((f e') = e))  (e':E(Y). ((g e') = e)))))

---

Definitions :  function: x:A  B[x],  and: P  Q,  es-fwd-propagation-via: f:X  Y:T,  not: A,  all: x:A. B[x],  or: P  Q,  exists: x:A. B[x],  es-E-interface: E(X),  equal: s = t,  es-E: E,  apply: f a
FDL editor aliases :  es-propagate-iff2

---

(X  |  Y)  \mLeftarrow{}{}\mRightarrow{}  Z:T  ==
    \mexists{}f:E(X)  {}\mrightarrow{}  E(Z)
      \mexists{}g:E(Y)  {}\mrightarrow{}  E(Z)
        (((f:X  {}\mRightarrow{}  Z:T  \mwedge{}  g:Y  {}\mRightarrow{}  Z:T)  \mwedge{}  (\mforall{}e:E(X).  \mforall{}e':E(Y).    (\mneg{}((f  e)  =  (g  e')))))
        \mwedge{}  (\mforall{}e:E(Z).  ((\mexists{}e':E(X).  ((f  e')  =  e))  \mvee{}  (\mexists{}e':E(Y).  ((g  e')  =  e)))))


Date html generated: 2010_08_27-PM-02_42_06
Last ObjectModification: 2009_12_16-AM-08_35_57

Home Index