Nuprl Lemma : Paxos-spec6-Input

[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)

(

leaders:Id List. ((

b:

. (leader b

leaders))

{

n:E(Input). (loc(n)

leaders)})))

Proof not projected

Definitions occuring in Statement : Paxos-spec6-body: Paxos-spec6-body, paxos-acceptor-state: AcceptorState, es-E-interface: E(X), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-loc: loc(e), Id: Id, bool:

, nat_plus:

, nat:

, uall:

[x:A]. B[x], guard: {T}, all:

x:A. B[x], implies: P

Q, apply: f a, function: x:A

B[x], product: x:A

B[x], list: type List, int:

, universe: Type, l_member: (x

l)
Definitions : uall:

[x:A]. B[x], all:

x:A. B[x], implies: P

Q, guard: {T}, member: t

T, prop:

, so_lambda:

x y.t[x; y], assert:

b, so_lambda:

x.t[x], btrue: tt, ifthenelse: if b then t else f fi , true: True, Id: Id, es-E-interface: E(X), not:

A, exists:

x:A. B[x], and: P

Q, so_apply: x[s1;s2], so_apply: x[s], uimplies: b supposing a, es-first-at: e is first@ i s.t. e.P[e], sq_type: SQType(T), Paxos-spec6-body: Paxos-spec6-body, alle-lt:

e<e'.P[e], false: False, subtype: S

T
Lemmas : es-E-interface_wf, nat_wf, l_member_wf, Id_wf, Paxos-spec6-body_wf, eclass_wf, es-E_wf, event-ordering+_wf, bool_wf, paxos-acceptor-state_wf, nat_plus_wf, es-first-at-exists, event-ordering+_inc, es-loc_wf, assert_wf, in-eclass_wf, es-interface-top, decidable__assert, subtype_base_sq, bool_subtype_base, assert_elim, atom2_subtype_base, eclass-val_wf, es-le-loc

\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{}leaders:Id List. ((\mforall{}b:\mBbbN{}. (leader b \mmember{} leaders)) {}\mRightarrow{} \{\mforall{}n:E(Input). (loc(n) \mmember{} leaders)\}))) Date html generated: 2011_10_20-PM-04_41_59 Last ObjectModification: 2011_06_18-PM-02_07_59 Home Index