Nuprl Lemma : RSC_voteMSGSto_wf

[Cmd:ValueAllType]. (RSC_voteMSGSto(Cmd)  bag(Id)      Cmd  Id  bag(Id  Message))


Proof not projected



Definitions occuring in Statement :  RSC_voteMSGSto: RSC_voteMSGSto(Cmd),  Message: Message,  Id: Id,  uall: [x:A]. B[x],  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  int: ,  bag: bag(T),  vatype: ValueAllType
Definitions :  uall: [x:A]. B[x],  vatype: ValueAllType,  member: t  T,  RSC_voteMSGSto: RSC_voteMSGSto(Cmd),  all: x:A. B[x],  so_lambda: x.t[x],  implies: P  Q,  so_apply: x[s]
Lemmas :  bag-map_wf,  Id_wf,  Message_wf,  make-Msg_wf,  product-valueall-type,  int-valueall-type,  Id-valueall-type,  valueall-type_wf,  bag_wf
\mforall{}[Cmd:ValueAllType].  (RSC\_voteMSGSto(Cmd)  \mmember{}  bag(Id)  {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id  {}\mrightarrow{}  bag(Id  \mtimes{}  Message))


Date html generated: 2012_02_20-PM-03_38_57
Last ObjectModification: 2012_02_02-PM-01_57_57

Home Index