Nuprl Lemma : rsc5_vote'send_wf

[Cmd:ValueAllType]. (rsc5_vote'send(Cmd)  Id      Cmd  Id  (Id  Message))


Proof not projected



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


Date html generated: 2012_02_20-PM-05_03_31
Last ObjectModification: 2012_02_02-PM-02_17_01

Home Index