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