Nuprl Definition : es-propagate-iff2

(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:E(Z). ((∃e':E(X). ((f e') = e ∈ E)) ∨ (∃e':E(Y). ((g e') = e ∈ E)))))

Definitions occuring in Statement : es-fwd-propagation-via: f:X ⇒ Y:T, es-E-interface: E(X), es-E: E, all: ∀x:A. B[x], exists: ∃x:A. B[x], not: ¬A, or: P ∨ Q, and: P ∧ Q, apply: f a, function: x:A ─→ B[x], equal: s = t ∈ T
FDL editor aliases : es-propagate-iff2

Latex:
(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: 2015_07_21-PM-03_28_14 Last ObjectModification: 2012_02_25-PM-02_27_34 Home Index