Nuprl Definition : sc_agreement
sc_agreement(Cmd;es) ==
e1,e2:E. v1,v2:
Cmd.
(v1 
sc_Decided{mark-simple-consensus.esh:o}(Cmd)(e1)
v2 sc_Decided{mark-simple-consensus.esh:o}(Cmd)(e2)
((fst(v1)) = (fst(v2)))
((snd(v1)) = (snd(v2))))
Definitions occuring in Statement :
classrel: v X(e),
es-E: E,
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
implies: P Q,
product: x:A B[x],
int: ,
equal: s = t
FDL editor aliases :
sc_agreement
sc\_agreement(Cmd;es) ==
\mforall{}e1,e2:E. \mforall{}v1,v2:\mBbbZ{} \mtimes{} Cmd.
(v1 \mmember{} sc\_Decided\{mark-simple-consensus.esh:o\}(Cmd)(e1)
{}\mRightarrow{} v2 \mmember{} sc\_Decided\{mark-simple-consensus.esh:o\}(Cmd)(e2)
{}\mRightarrow{} ((fst(v1)) = (fst(v2)))
{}\mRightarrow{} ((snd(v1)) = (snd(v2))))
Date html generated:
2012_02_20-PM-03_38_07
Last ObjectModification:
2012_02_02-PM-01_57_43
Home
Index