Nuprl Lemma : Paxos-spec7-body_wf

[Info:Type]. [es:EO+(Info)]. [failset:Id List]. [T:Type]. [f:]. [acceptors:Id List].
[Reserve,NoProposal,NewBallot:EClass()]. [VoteState:EClass(AcceptorState)]. [Proposal:EClass(  T)].
[AcceptOrReject:EClass(  T  )]. [leader:  Id]. [Decide,Input:EClass(T)]. [Vote:EClass(Id    )].
[Collect:EClass(    T)].
  (Paxos-spec7-body{i:l}(Info;
                         es;
                         T;
                         f;
                         acceptors;
                         Reserve;
                         VoteState;
                         Proposal;
                         AcceptOrReject;
                         leader;
                         Decide;
                         Vote;
                         Input;
                         Collect;
                         NoProposal;
                         NewBallot;
                         failset)  ')


Proof not projected



Definitions occuring in Statement :  Paxos-spec7-body: Paxos-spec7-body,  paxos-acceptor-state: AcceptorState,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  Id: Id,  bool: ,  nat: ,  uall: [x:A]. B[x],  prop: ,  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  int: ,  universe: Type
Definitions :  true: True,  ifthenelse: if b then t else f fi ,  btrue: tt,  so_lambda: x y.t[x; y],  so_lambda: x.t[x],  assert: b,  subtype: S  T,  top: Top,  all: x:A. B[x],  member: t  T,  cand: A c B,  so_lambda: so_lambda(x,y,z.t[x; y; z]),  prop: ,  and: P  Q,  implies: P  Q,  bfalse: ff,  spreadn: spread4,  guard: {T},  sq_type: SQType(T),  uimplies: b supposing a,  so_apply: x[s1;s2],  so_apply: x[s],  uall: [x:A]. B[x],  es-E-interface: E(X),  so_apply: x[s1;s2;s3],  iff: P  Q,  unit: Unit,  bool: ,  it:
Lemmas :  in-eclass_wf,  assert_elim,  bool_subtype_base,  subtype_base_sq,  event-ordering+_wf,  es-E_wf,  eclass-val_wf,  pi1_wf_top,  pi2_wf,  event-ordering+_inc,  es-loc_wf,  bool_wf,  nat_wf,  Id_wf,  es-interface-top,  es-E-interface_wf,  paxos-state-reservation_wf,  paxos-acceptor-state_wf,  paxos-state-info_wf,  es-tagged-true-class_wf,  MaxVote_wf,  paxos-state-name_wf,  es-class-causal-rel-fail_wf,  top_wf,  es-collect-filter-max_wf,  es-interface-pair-prior_wf,  paxos-state-value_wf,  not_functionality_wrt_uiff,  assert_of_bnot,  eqff_to_assert,  bnot_wf,  not_wf,  assert_of_eq_int,  eqtt_to_assert,  assert_wf,  uiff_transitivity,  iff_weakening_uiff,  paxos-state-ballot_wf,  eq_int_wf,  map-class_wf,  eclass_wf
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[failset:Id  List].  \mforall{}[T:Type].  \mforall{}[f:\mBbbN{}].  \mforall{}[acceptors:Id  List].
\mforall{}[Reserve,NoProposal,NewBallot:EClass(\mBbbN{})].  \mforall{}[VoteState:EClass(AcceptorState)].
\mforall{}[Proposal:EClass(\mBbbN{}  \mtimes{}  T)].  \mforall{}[AcceptOrReject:EClass(\mBbbN{}  \mtimes{}  T  \mtimes{}  \mBbbB{})].  \mforall{}[leader:\mBbbN{}  {}\mrightarrow{}  Id].
\mforall{}[Decide,Input:EClass(T)].  \mforall{}[Vote:EClass(Id  \mtimes{}  \mBbbN{}  \mtimes{}  \mBbbB{})].  \mforall{}[Collect:EClass(\mBbbN{}  \mtimes{}  \mBbbZ{}  \mtimes{}  T)].
    (Paxos-spec7-body\{i:l\}(Info;
                                                  es;
                                                  T;
                                                  f;
                                                  acceptors;
                                                  Reserve;
                                                  VoteState;
                                                  Proposal;
                                                  AcceptOrReject;
                                                  leader;
                                                  Decide;
                                                  Vote;
                                                  Input;
                                                  Collect;
                                                  NoProposal;
                                                  NewBallot;
                                                  failset)  \mmember{}  \mBbbP{}')


Date html generated: 2011_10_20-PM-04_43_56
Last ObjectModification: 2011_06_18-PM-02_10_03

Home Index