Nuprl Lemma : RSC_Vote_wf

[Cmd:ValueAllType]. (RSC_Vote(Cmd)  EClass'(    Cmd  Id))


Proof not projected



Definitions occuring in Statement :  RSC_Vote: RSC_Vote(Cmd),  Message: Message,  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  member: t  T,  product: x:A  B[x],  int: ,  vatype: ValueAllType
Definitions :  uall: [x:A]. B[x],  vatype: ValueAllType,  member: t  T,  RSC_Vote: RSC_Vote(Cmd),  name: Name
Lemmas :  base-headers-msg-val_wf,  Id_wf,  valueall-type_wf
\mforall{}[Cmd:ValueAllType].  (RSC\_Vote(Cmd)  \mmember{}  EClass'(\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id))


Date html generated: 2012_02_20-PM-03_38_49
Last ObjectModification: 2012_02_02-PM-01_57_54

Home Index