Nuprl Lemma : Vote_wf
[Cmd:ValueAllType]. (Vote(Cmd) 
EClass(
Cmd))
Proof not projected
Definitions occuring in Statement :
Vote: Vote(Cmd),
Message: Message,
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
member: t T,
product: x:A B[x],
int: ,
vatype: ValueAllType
Lemmas :
member_wf,
name_wf,
base-headers-msg-val_wf,
vatype_wf
\mforall{}[Cmd:ValueAllType]. (Vote(Cmd) \mmember{} EClass(\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd))
Date html generated:
2011_10_21-AM-08_17_51
Last ObjectModification:
2011_07_20-AM-04_35_57
Home
Index