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