Nuprl Definition : RSC_validity
RSC_validity(Cmd;es) == 
e:E. v:
Cmd. (v 
RSC_Decided(Cmd)(e) 
(
e':E. ((e' < e) 
v RSC_Propose(Cmd)(e'))))
Definitions occuring in Statement :
RSC_Propose: RSC_Propose(Cmd),
RSC_Decided: RSC_Decided(Cmd),
classrel: v X(e),
es-causl: (e < e'),
es-E: E,
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
and: P Q,
product: x:A B[x],
int:
FDL editor aliases :
RSC_validity
RSC\_validity(Cmd;es) ==
\mforall{}e:E. \mforall{}v:\mBbbZ{} \mtimes{} Cmd. (v \mmember{} RSC\_Decided(Cmd)(e) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} v \mmember{} RSC\_Propose(Cmd)(e'))))
Date html generated:
2012_02_20-PM-04_01_52
Last ObjectModification:
2012_02_02-PM-01_59_28
Home
Index