Nuprl Lemma : rsc3_when_quorum_wf

[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:].
  (rsc3_when_quorum(Cmd;cmdeq;coeff;flrs)
       Id      Cmd  Id  Cmd List  (Id List)  bag(Id  Message))


Proof not projected



Definitions occuring in Statement :  rsc3_when_quorum: rsc3_when_quorum(Cmd;cmdeq;coeff;flrs),  Message: Message,  Id: Id,  uall: [x:A]. B[x],  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  int: ,  deq: EqDecider(T),  bag: bag(T),  vatype: ValueAllType
Definitions :  rsc3_when_quorum: rsc3_when_quorum(Cmd;cmdeq;coeff;flrs),  member: t  T,  vatype: ValueAllType,  uall: [x:A]. B[x]
Lemmas :  deq_wf,  empty-bag_wf,  rsc3_roundout_wf,  Message_wf,  Id_wf,  bag_wf,  valueall-type_wf,  rsc3_newvote_wf,  ifthenelse_wf
\mforall{}[Cmd:ValueAllType].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[coeff,flrs:\mBbbZ{}].
    (rsc3\_when\_quorum(Cmd;cmdeq;coeff;flrs)  \mmember{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}
                                                                                        {}\mrightarrow{}  Id
                                                                                        {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id
                                                                                        {}\mrightarrow{}  Cmd  List  \mtimes{}  (Id  List)
                                                                                        {}\mrightarrow{}  bag(Id  \mtimes{}  Message))


Date html generated: 2012_02_20-PM-04_12_10
Last ObjectModification: 2012_02_02-PM-02_03_29

Home Index