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:
2016_05_17-AM-06_48_51
Last ObjectModification:
2012_07_23-PM-11_37_25
Theory : event-ordering
Home
Index