Nuprl Lemma : Paxos-spec8-properties

[Info:Type]

es:EO+(Info)

[T:Type]

leader:

Id.

failset:Id List.

1a:EClass(Id

).

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

Consistency of Decide
Validity wrt Input
Non-blocking (wrt (snd(x) where x from 1a);leader;failset))

Proof not projected

Definitions occuring in Statement : Paxos-spec8: Paxos-spec8{i:l}(Info; es; T; leader; failset; 1a; Decide; Input), Paxos-properties: Paxos-properties, map-class: (f[v] where v from X), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), Id: Id, nat:

, uall:

[x:A]. B[x], pi2: snd(t), all:

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

Q, function: x:A

B[x], product: x:A

B[x], list: type List, universe: Type
Definitions : pair: <a, b>, consensus-spec1: Consistent(Decide), union: left + right, assert:

b, Paxos-spec8-body: Paxos-spec8-body{i:l}(es; Info; T; f; acceptors; leader; Input; Decide; 1a; 1b; 2a; 2b; failset), 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 , not:

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

r B, nat_plus:

, Paxos-spec7-body: Paxos-spec7-body, prop:

, subtype: S

T, event_ordering: EO, es-E: E, lambda:

x.A[x], Paxos-spec7: Paxos-spec7{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, and: P

Q, implies: P

Q, Paxos-properties: Paxos-properties, so_lambda:

x.t[x], product: x:A

B[x], Paxos-spec8: Paxos-spec8{i:l}(Info; es; T; leader; failset; 1a; 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, uall:

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

x:A. B[x], all:

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

B[x], Auto: Error :Auto, MaAuto: Error :MaAuto, D: Error :D, THENM: Error :THENM, CollapseTHENA: Error :CollapseTHENA, CollapseTHEN: Error :CollapseTHEN, RepeatFor: Error :RepeatFor, pi2: snd(t), map-class: (f[v] where v from X)
Lemmas : Paxos-spec8-spec7, eclass_wf, Paxos-spec8_wf, Paxos-properties_wf, map-class_wf, Id_wf, nat_wf, pi2_wf, uall_wf, event-ordering+_wf, Paxos-spec7-properties, es-E_wf, event-ordering+_inc, Paxos-spec7_wf, Paxos-spec7-body_wf, nat_plus_wf

\mforall{}[Info:Type] \mforall{}es:EO+(Info) \mforall{}[T:Type] \mforall{}leader:\mBbbN{} {}\mrightarrow{} Id. \mforall{}failset:Id List. \mforall{}1a:EClass(Id \mtimes{} \mBbbN{}). \mforall{}Decide,Input:EClass(T). (Paxos-spec8\{i:l\}(Info; es; T; leader; failset; 1a; Decide; Input) {}\mRightarrow{} Consistency of Decide Validity wrt Input Non-blocking (wrt (snd(x) where x from 1a);leader;failset)) Date html generated: 2011_10_20-PM-04_49_30 Last ObjectModification: 2011_06_18-PM-02_14_53 Home Index