Nuprl Lemma : Paxos-spec7-properties

[Info:Type]

es:EO+(Info)

[T:Type]

leader:

Id.

failset:Id List.

Reserve:EClass(

).

Decide,Input:EClass(T).
(Paxos-spec7{i:l}(Info; es; T; leader; failset; Reserve; Decide; Input)

Consistency of Decide
Validity wrt Input
Non-blocking (wrt Reserve;leader;failset))

Proof not projected

Definitions occuring in Statement : Paxos-properties: Paxos-properties, Paxos-spec7: Paxos-spec7{i:l}(Info; es; T; leader; failset; Reserve; Decide; Input), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), Id: Id, nat:

, uall:

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

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

Q, function: x:A

B[x], list: type List, universe: Type
Definitions : int:

, paxos-acceptor-state: AcceptorState, ifthenelse: if b then t else f fi , es-causle: e c

e', pair: <a, b>, bool:

, union: left + right, Paxos-spec7-body: Paxos-spec7-body, strong-subtype: strong-subtype(A;B), eq_atom: x =a y, eq_atom: eq_atom$n(x;y), dep-isect: Error :dep-isect, record+: record+, le: A

B, ge: i

j , less_than: a < b, uimplies: b supposing a, uiff: uiff(P;Q), subtype_rel: A

r B, nat_plus:

, Paxos-spec6-body: Paxos-spec6-body, prop:

, subtype: S

T, event_ordering: EO, lambda:

x.A[x], in-eclass: e

X, assert:

b, es-E: E, es-loc: loc(e), eventually-one-leader: eventually ldr is the only leader, l_member: (x

l), not:

A, leaders-finite: Finitely many leaders, consensus-spec1: Consistent(Decide), Paxos-spec6: Paxos-spec6{i:l}(Info; es; T; leader; failset; Reserve; Decide; Input), equal: s = t, member: t

T, set: {x:A| B[x]} , es-E-interface: E(X), exists:

x:A. B[x], consensus-spec2: Decide values come from Input values, product: x:A

B[x], and: P

Q, implies: P

Q, Paxos-properties: Paxos-properties, Paxos-spec7: Paxos-spec7{i:l}(Info; es; T; leader; failset; Reserve; Decide; Input), eclass: EClass(A[eo; e]), so_lambda:

x y.t[x; y], list: type List, Id: Id, nat:

, event-ordering+: EO+(Info), universe: Type, isect:

x:A. B[x], uall:

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

x.t[x], all:

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

B[x], Auto: Error :Auto, CollapseTHEN: Error :CollapseTHEN, ParallelOp: Error :ParallelOp, RepeatFor: Error :RepeatFor, Unfold: Error :Unfold, Try: Error :Try, MaAuto: Error :MaAuto, D: Error :D, THENM: Error :THENM, CollapseTHENA: Error :CollapseTHENA
Lemmas : eclass_wf, Paxos-spec7_wf, Paxos-properties_wf, Id_wf, nat_wf, uall_wf, event-ordering+_wf, Paxos-spec6-properties, es-E_wf, event-ordering+_inc, Paxos-spec6_wf, Paxos-spec6-body_wf, nat_plus_wf, paxos-acceptor-state_wf, bool_wf, nat_plus_inc, Paxos-spec7-body-spec6

\mforall{}[Info:Type] \mforall{}es:EO+(Info) \mforall{}[T:Type] \mforall{}leader:\mBbbN{} {}\mrightarrow{} Id. \mforall{}failset:Id List. \mforall{}Reserve:EClass(\mBbbN{}). \mforall{}Decide,Input:EClass(T). (Paxos-spec7\{i:l\}(Info; es; T; leader; failset; Reserve; Decide; Input) {}\mRightarrow{} Consistency of Decide Validity wrt Input Non-blocking (wrt Reserve;leader;failset)) Date html generated: 2011_10_20-PM-04_45_33 Last ObjectModification: 2011_06_18-PM-02_11_27 Home Index