Nuprl Lemma : RSC_VoterState_wf
[Cmd:ValueAllType]. (RSC_VoterState(Cmd) 
 
 
 EClass'(
))
Proof not projected
Definitions occuring in Statement : 
RSC_VoterState: RSC_VoterState(Cmd), 
Message: Message, 
eclass: EClass(A[eo; e]), 
uall:
[x:A]. B[x], 
member: t 
 T, 
function: x:A 
 B[x], 
int:
, 
vatype: ValueAllType
Definitions : 
so_lambda: 
x.t[x], 
prop:
, 
implies: P 
 Q, 
all:
x:A. B[x], 
RSC_VoterState: RSC_VoterState(Cmd), 
member: t 
 T, 
vatype: ValueAllType, 
uall:
[x:A]. B[x], 
so_apply: x[s]
Lemmas : 
valueall-type_wf, 
RSC_RoundInfo_wf, 
bag_wf, 
Id_wf, 
RSC_init_wf, 
equal_wf, 
all_wf, 
uall_wf, 
RSC_incround_wf, 
bool_wf, 
RSC_round_increase_wf, 
ifthenelse_wf, 
Accum-class_wf
\mforall{}[Cmd:ValueAllType].  (RSC\_VoterState(Cmd)  \mmember{}  \mBbbZ{}  {}\mrightarrow{}  EClass'(\mBbbZ{}))
Date html generated:
2012_02_20-PM-04_01_43
Last ObjectModification:
2012_02_02-PM-01_59_25
Home
Index