Nuprl Lemma : rsc5_when_quorum_wf

[Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:]. [locs:bag(Id)].
  (rsc5_when_quorum(Cmd;clients;cmdeq;coeff;flrs;locs)    
                                                          Id
                                                              Cmd  Id
                                                            Cmd?  (Id List)
                                                          bag(Id  Message))


Proof not projected



Definitions occuring in Statement :  rsc5_when_quorum: rsc5_when_quorum(Cmd;clients;cmdeq;coeff;flrs;locs),  Message: Message,  Id: Id,  uall: [x:A]. B[x],  unit: Unit,  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  list: type List,  int: ,  deq: EqDecider(T),  bag: bag(T),  vatype: ValueAllType
Definitions :  guard: {T},  bfalse: ff,  outl: outl(x),  isl: isl(x),  rsc5_possmajstep: rsc5_possmajstep(Cmd;cmdeq),  btrue: tt,  implies: P  Q,  all: x:A. B[x],  rsc5_roundout: rsc5_roundout(Cmd;clients;cmdeq;coeff;flrs;locs),  rsc5_newvote: rsc5_newvote(Cmd),  ifthenelse: if b then t else f fi ,  rsc5_when_quorum: rsc5_when_quorum(Cmd;clients;cmdeq;coeff;flrs;locs),  member: t  T,  vatype: ValueAllType,  uall: [x:A]. B[x],  and: P  Q,  uiff: uiff(P;Q),  uimplies: b supposing a,  bool: ,  unit: Unit,  it:
Lemmas :  deq_wf,  unit_wf2,  empty-bag_wf,  not_functionality_wrt_uiff,  assert_of_bnot,  eqff_to_assert,  not_wf,  rsc5_retry'send_wf,  single-bag_wf,  valueall-type_wf,  rsc5_notify'broadcast_wf,  rsc5_decided'broadcast_wf,  bag-append_wf,  Message_wf,  bag_wf,  ifthenelse_wf,  safe-assert-deq,  assert_wf,  equal_wf,  uiff_transitivity,  length_wf,  eqtt_to_assert,  bool_wf,  id-deq_wf,  Id_wf,  deq-member_wf,  bnot_wf,  int-deq_wf,  product-deq_wf,  eqof_wf,  band_wf
\mforall{}[Cmd:ValueAllType].  \mforall{}[clients:bag(Id)].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[coeff,flrs:\mBbbZ{}].  \mforall{}[locs:bag(Id)].
    (rsc5\_when\_quorum(Cmd;clients;cmdeq;coeff;flrs;locs)  \mmember{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}
                                                                                                                  {}\mrightarrow{}  Id
                                                                                                                  {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id
                                                                                                                  {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  Cmd?  \mtimes{}  (Id  List)
                                                                                                                  {}\mrightarrow{}  bag(Id  \mtimes{}  Message))


Date html generated: 2012_02_20-PM-05_05_32
Last ObjectModification: 2012_02_02-PM-02_18_04

Home Index