Nuprl Lemma : Paxos-spec6-progress

[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)
         (n:E(Input)
              (b:
                 ((d:E(Decide). (loc(d) = loc(n)))  (e:E(NewBallot). (n loc e   (b  NewBallot(e)))))) supposing 
                 ((n':E(Input). ((n' <loc n))) and 
                 ((loc(n)  failset)))))


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),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-le: e loc e' ,  es-locl: (e <loc e'),  es-loc: loc(e),  Id: Id,  bool: ,  nat_plus: ,  nat: ,  uimplies: b supposing a,  uall: [x:A]. B[x],  le: A  B,  all: x:A. B[x],  exists: x:A. B[x],  not: A,  implies: P  Q,  or: P  Q,  and: P  Q,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  int: ,  universe: Type,  equal: s = t,  l_member: (x  l)
Definitions :  subtract: n - m,  grp_car: |g|,  fpf: a:A fp-> B[a],  strong-subtype: strong-subtype(A;B),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  rev_implies: P  Q,  iff: P  Q,  assert: b,  es-class-causal-mrel-fail: es-class-causal-mrel-fail,  es-class-def: es-class-def,  es-class-causal-rel-fail: es-class-causal-rel-fail,  no_repeats: no_repeats(T;l),  ge: i  j ,  uiff: uiff(P;Q),  subtype_rel: A r B,  natural_number: $n,  void: Void,  false: False,  real: ,  rationals: ,  dep-isect: Error :dep-isect,  eq_atom: x =a y,  eq_atom: eq_atom$n(x;y),  record+: record+,  prop: ,  subtype: S  T,  es-E: E,  lambda: x.A[x],  less_than: a < b,  eclass-val: X(e),  es-loc: loc(e),  bool: ,  paxos-acceptor-state: AcceptorState,  member: t  T,  universe: Type,  nat_plus: ,  list: type List,  so_lambda: x y.t[x; y],  eclass: EClass(A[eo; e]),  Paxos-spec6-body: Paxos-spec6-body,  l_member: (x  l),  es-locl: (e <loc e'),  not: A,  int: ,  set: {x:A| B[x]} ,  nat: ,  event-ordering+: EO+(Info),  event_ordering: EO,  es-le: e loc e' ,  le: A  B,  and: P  Q,  top: Top,  es-E-interface: E(X),  Id: Id,  equal: s = t,  product: x:A  B[x],  exists: x:A. B[x],  union: left + right,  or: P  Q,  uall: [x:A]. B[x],  so_lambda: x.t[x],  implies: P  Q,  all: x:A. B[x],  function: x:A  B[x],  isect: x:A. B[x],  uimplies: b supposing a,  minus: -n,  add: n + m,  record-select: r.x,  btrue: tt,  sq_type: SQType(T),  true: True,  in-eclass: e  X,  cand: A c B,  limited-type: LimitedType,  guard: {T},  atom: Atom,  apply: f a,  es-base-E: es-base-E(es),  token: "$token",  alle-lt: e<e'.P[e],  pair: <a, b>
Lemmas :  subtype_rel_self,  es-base-E_wf,  es-le_transitivity,  ifthenelse_wf,  false_wf,  in-eclass_wf,  true_wf,  subtype_base_sq,  bool_subtype_base,  assert_elim,  ge_wf,  nat_properties,  nat_wf,  es-E-interface_wf,  es-le_wf,  le_wf,  Id_wf,  event-ordering+_wf,  uall_wf,  nat_plus_wf,  eclass_wf,  Paxos-spec6-body_wf,  not_wf,  l_member_wf,  es-locl_wf,  Paxos-spec6-progress-lemma1,  es-E_wf,  event-ordering+_inc,  paxos-acceptor-state_wf,  bool_wf,  nat_plus_properties,  nat_plus_inc,  member_wf,  subtype_rel_wf,  es-interface-top,  es-loc_wf,  nat_ind_tp,  eclass-val_wf,  assert_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{}n:E(Input)
                            (\mforall{}b:\mBbbN{}
                                  ((\mexists{}d:E(Decide).  (loc(d)  =  loc(n)))
                                  \mvee{}  (\mexists{}e:E(NewBallot).  (n  \mleq{}loc  e    \mwedge{}  (b  \mleq{}  NewBallot(e))))))  supposing 
                                  ((\mforall{}n':E(Input).  (\mneg{}(n'  <loc  n)))  and 
                                  (\mneg{}(loc(n)  \mmember{}  failset)))))


Date html generated: 2011_10_20-PM-04_41_28
Last ObjectModification: 2011_06_18-PM-02_07_17

Home Index