Nuprl Definition : es-propagation-rule

=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'∈e.(e < e') ∧ (B(e') (f loc(e) A(e)) ∈ T) ∧ (loc(e') ∈ A(e))))
   ∧ (∀e:E(A). (∀x∈A(e).(∃e'∈e. loc(e') x ∈ Id))))



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: List all: x:A. B[x] exists: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q apply: a function: x:A ─→ B[x] equal: t ∈ T
FDL editor aliases :  es-propagation-rule

Latex:
A  {}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))))



Date html generated: 2015_07_21-PM-03_29_06
Last ObjectModification: 2012_07_23-PM-11_35_42

Home Index