Nuprl Lemma : RSC-slow-round_wf
[Cmd:ValueAllType]. [slow:bag(Id)]. [es:EO']. [n,r:
]. (RSC-slow-round(Cmd;es;n;r;slow) 
')
Proof not projected
Definitions occuring in Statement :
RSC-slow-round: RSC-slow-round(Cmd;es;n;r;slow),
Message: Message,
event-ordering+: EO+(Info),
Id: Id,
uall: [x:A]. B[x],
prop: ,
member: t T,
int: ,
bag: bag(T),
vatype: ValueAllType
Definitions :
uall: [x:A]. B[x],
member: t T,
prop: ,
RSC-slow-round: RSC-slow-round(Cmd;es;n;r;slow),
all: x:A. B[x],
implies: P 
Q,
vatype: ValueAllType,
subtype: S 
T
Lemmas :
Id_wf,
es-E_wf,
event-ordering+_inc,
Message_wf,
es-loc_wf,
bag-member_wf,
not_wf,
classrel_wf,
Error :RSC_Vote_wf,
es-locl_wf,
event-ordering+_wf,
bag_wf,
vatype_wf
\mforall{}[Cmd:ValueAllType]. \mforall{}[slow:bag(Id)]. \mforall{}[es:EO']. \mforall{}[n,r:\mBbbZ{}]. (RSC-slow-round(Cmd;es;n;r;slow) \mmember{} \mBbbP{}')
Date html generated:
2012_02_20-PM-04_04_56
Last ObjectModification:
2012_02_02-PM-01_59_59
Home
Index