### Nuprl Definition : es-propagation-rule-iff

`A ``f`` B@g ==`
`  ∃p:E(A) ─→ (E(B) List)`
`   ((∀e1,e2:E(A).  ((¬(e1 = e2 ∈ E)) `` l_disjoint(E(B);p e1;p e2)))`
`   ∧ (∀e:E(A). (∀e'∈p e.(e < e') ∧ (B(e') = (f loc(e) A(e)) ∈ T) ∧ (loc(e') ∈ g A(e))))`
`   ∧ (∀e:E(A). (∀x∈g A(e).(∃e'∈p e. loc(e') = x ∈ Id)))`
`   ∧ (∀e':E(B). ∃e:E(A). (e' ∈ p e)))`

Definitions occuring in Statement :  es-E-interface: `E(X)` eclass-val: `X(e)` es-causl: `(e < e')` es-loc: `loc(e)` es-E: `E` Id: `Id` l_disjoint: `l_disjoint(T;l1;l2)` l_exists: `(∃x∈L. P[x])` l_all: `(∀x∈L.P[x])` l_member: `(x ∈ l)` list: `T List` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
FDL editor aliases :  es-propagation-rule-iff

Latex:
A  \mLeftarrow{}{}f{}\mRightarrow{}  B@g  ==
\mexists{}p:E(A)  {}\mrightarrow{}  (E(B)  List)
((\mforall{}e1,e2:E(A).    ((\mneg{}(e1  =  e2))  {}\mRightarrow{}  l\_disjoint(E(B);p  e1;p  e2)))
\mwedge{}  (\mforall{}e:E(A).  (\mforall{}e'\mmember{}p  e.(e  <  e')  \mwedge{}  (B(e')  =  (f  loc(e)  A(e)))  \mwedge{}  (loc(e')  \mmember{}  g  A(e))))
\mwedge{}  (\mforall{}e:E(A).  (\mforall{}x\mmember{}g  A(e).(\mexists{}e'\mmember{}p  e.  loc(e')  =  x)))
\mwedge{}  (\mforall{}e':E(B).  \mexists{}e:E(A).  (e'  \mmember{}  p  e)))

Date html generated: 2015_07_21-PM-03_29_29
Last ObjectModification: 2012_07_23-PM-11_37_25

Home Index