`∀e,x,y. e∈X(x) ``c`` ∃ reply Y(y)@loc1[x] such that`
`                    R[e; x; y]∧loc2[y]=loc(e)`
`                   unless loc(e) ∈ failset ==`
`  (∀e:E(Y). ∃e':E(X). (e' c≤ e ∧ ((loc(e) = loc1[X(e')] ∈ Id) ∧ (loc(e') = loc2[Y(e)] ∈ Id)) ∧ R[e'; X(e'); Y(e)]))`
`  ∧ (∀e':E(X)`
`       ((∃e:E(Y). (e' c≤ e ∧ ((loc(e) = loc1[X(e')] ∈ Id) ∧ (loc(e') = loc2[Y(e)] ∈ Id)) ∧ R[e'; X(e'); Y(e)]))`
`       ∨ (loc(e') ∈ failset)))`

Definitions occuring in Statement :  es-E-interface: `E(X)` eclass-val: `X(e)` es-causle: `e c≤ e'` es-loc: `loc(e)` Id: `Id` l_member: `(x ∈ l)` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` or: `P ∨ Q` and: `P ∧ Q` equal: `s = t ∈ T`

Latex:
\mforall{}e,x,y.  e\mmember{}X(x)  \mLeftarrow{}c\mRightarrow{}  \mexists{}  reply  Y(y)@loc1[x]  such  that
R[e;  x;  y]\mwedge{}loc2[y]=loc(e)
unless  loc(e)  \mmember{}  failset  ==
(\mforall{}e:E(Y)
\mexists{}e':E(X).  (e'  c\mleq{}  e  \mwedge{}  ((loc(e)  =  loc1[X(e')])  \mwedge{}  (loc(e')  =  loc2[Y(e)]))  \mwedge{}  R[e';  X(e');  Y(e)]))
\mwedge{}  (\mforall{}e':E(X)
((\mexists{}e:E(Y)
(e'  c\mleq{}  e  \mwedge{}  ((loc(e)  =  loc1[X(e')])  \mwedge{}  (loc(e')  =  loc2[Y(e)]))  \mwedge{}  R[e';  X(e');  Y(e)]))
\mvee{}  (loc(e')  \mmember{}  failset)))

Date html generated: 2015_07_21-PM-04_27_02
Last ObjectModification: 2012_02_25-PM-03_16_32

Home Index