Nuprl Definition : es-class-reply-or-fail
∀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
FDL editor aliases :
es-class-reply-or-fail
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