Nuprl Lemma : Paxos-spec6-progress-invariant

[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-spec6-body{i:l}(Info;es;T;f;acceptors;
                               Reserve;VoteState;Proposal;
                               AcceptOrReject;leader;Decide;
                               Vote;Input;Collect;NoProposal;
                               NewBallot;failset)
         (nb:E(NewBallot)
              let b = NewBallot(nb) in
                  (r:E(Reserve). ((Reserve(r) < b)  ((leader Reserve(r)) = (leader b))))
                   (e:E
                        (fst(Proposal(e)))  b supposing e  Proposal  NewBallot(e)  b supposing e  NewBallot 
                        supposing loc(e) = (leader b))))


Proof not projected



Definitions occuring in Statement :  Paxos-spec6-body: Paxos-spec6-body,  paxos-acceptor-state: AcceptorState,  es-E-interface: E(X),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-loc: loc(e),  es-E: E,  Id: Id,  assert: b,  bool: ,  nat_plus: ,  nat: ,  let: let,  uimplies: b supposing a,  uall: [x:A]. B[x],  pi1: fst(t),  le: A  B,  all: x:A. B[x],  implies: P  Q,  or: P  Q,  and: P  Q,  less_than: a < b,  apply: f a,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  int: ,  universe: Type,  equal: s = t
Definitions :  so_lambda: x y.t[x; y],  member: t  T,  decidable: Dec(P),  or: P  Q,  es-le: e loc e' ,  so_apply: x[s1;s2],  uall: [x:A]. B[x],  uimplies: b supposing a,  all: x:A. B[x],  nat: ,  subtype: S  T
Lemmas :  event-ordering+_wf,  event-ordering+_inc,  es-E_wf,  nat_wf,  eclass-val_wf
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}failset:Id  List.
        \mforall{}[T:Type]
            \mforall{}f:\mBbbN{}\msupplus{}.  \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-spec6-body\{i:l\}(Info;es;T;f;acceptors;
                                                              Reserve;VoteState;Proposal;
                                                              AcceptOrReject;leader;Decide;
                                                              Vote;Input;Collect;NoProposal;
                                                              NewBallot;failset)
                {}\mRightarrow{}  (\mforall{}nb:E(NewBallot)
                            let  b  =  NewBallot(nb)  in
                                    (\mforall{}r:E(Reserve).  ((Reserve(r)  <  b)  \mvee{}  ((leader  Reserve(r))  =  (leader  b))))
                                    {}\mRightarrow{}  (\mforall{}e:E
                                                (fst(Proposal(e)))  \mleq{}  b  supposing  \muparrow{}e  \mmember{}\msubb{}  Proposal
                                                \mwedge{}  NewBallot(e)  \mleq{}  b  supposing  \muparrow{}e  \mmember{}\msubb{}  NewBallot 
                                                supposing  loc(e)  =  (leader  b))))


Date html generated: 2011_10_20-PM-04_41_07
Last ObjectModification: 2011_06_18-PM-02_06_56

Home Index