Nuprl Definition : sc_validity
sc_validity(Cmd;es) ==
e:E. v:
Cmd.
(v 
sc_Decided{mark-simple-consensus.esh:o}(Cmd)(e)
(
e':E. ((e' < e) 
v sc_Propose{mark-simple-consensus.esh:o}(Cmd)(e))))
Definitions occuring in Statement :
classrel: v X(e),
es-causl: (e < e'),
es-E: E,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
product: x:A B[x],
int:
FDL editor aliases :
sc_validity
sc\_validity(Cmd;es) ==
\mforall{}e:E. \mforall{}v:\mBbbZ{} \mtimes{} Cmd.
(v \mmember{} sc\_Decided\{mark-simple-consensus.esh:o\}(Cmd)(e)
{}\mRightarrow{} (\mexists{}e':E. ((e' < e) \mwedge{} v \mmember{} sc\_Propose\{mark-simple-consensus.esh:o\}(Cmd)(e))))
Date html generated:
2012_02_20-PM-03_38_12
Last ObjectModification:
2012_02_02-PM-01_57_45
Home
Index