Nuprl Lemma : Paxos-spec6-properties
[Info:Type]
es:EO+(Info)
[T:Type]
leader:
Id. failset:Id List. Reserve:EClass(). Decide,Input:EClass(T).
(Paxos-spec6{i:l}(Info; es; T; leader; failset; Reserve; Decide; Input)
(Decide values come from Input values
Consistent(Decide)
(Finitely many leaders
(
ldr:Id. ((
(ldr 
failset)) eventually ldr is the only leader (n:E(Input). (loc(n) = ldr))))
(d:E. (
d 
Decide)))))
Proof not projected
Definitions occuring in Statement :
eventually-one-leader: eventually ldr is the only leader,
leaders-finite: Finitely many leaders,
Paxos-spec6: Paxos-spec6{i:l}(Info; es; T; leader; failset; Reserve; Decide; Input),
consensus-spec2: Decide values come from Input values,
consensus-spec1: Consistent(Decide),
es-E-interface: E(X),
in-eclass: e X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-loc: loc(e),
es-E: E,
Id: Id,
assert: b,
nat: ,
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
and: P Q,
function: x:A B[x],
list: type List,
universe: Type,
equal: s = t,
l_member: (x l)
Definitions :
guard: {T},
btrue: tt,
sq_type: SQType(T),
true: True,
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
rev_implies: P 
Q,
or: P 
Q,
limited-type: LimitedType,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ge: i 
j ,
uiff: uiff(P;Q),
subtype_rel: A 
r B,
atom: Atom,
es-base-E: es-base-E(es),
token: "$token",
ifthenelse: if b then t else f fi ,
record-select: r.x,
void: Void,
false: False,
atom: Atom$n,
cand: A c B,
dep-isect: Error :dep-isect,
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
record+: record+,
union: left + right,
alle-lt: e<e'.P[e],
less_than: a < b,
es-le: e 
loc e' ,
iff: P Q,
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,
le: A B,
no_repeats: no_repeats(T;l),
l_all: (xL.P[x]),
Paxos-spec6-body: Paxos-spec6-body,
int: 
,
bool: 
,
paxos-acceptor-state: AcceptorState,
nat_plus: 
,
subtype: S T,
lambda: 
x.A[x],
Paxos-spec5: Paxos-spec5{i:l}(Info; es; T; Decide; Input),
in-eclass: e X,
member: t T,
set: {x:A| B[x]} ,
prop: 
,
list: type List,
so_lambda: 
x y.t[x; y],
eclass: EClass(A[eo; e]),
Paxos-spec6: Paxos-spec6{i:l}(Info; es; T; leader; failset; Reserve; Decide; Input),
consensus-spec2: Decide values come from Input values,
consensus-spec1: Consistent(Decide),
leaders-finite: Finitely many leaders,
l_member: (x l),
top: Top,
es-E-interface: E(X),
isect: 
x:A. B[x],
uall: [x:A]. B[x],
so_lambda: x.t[x],
implies: P Q,
function: x:A B[x],
assert: b,
es-E: E,
event-ordering+: EO+(Info),
event_ordering: EO,
and: P Q,
product: x:A 
B[x],
exists: x:A. B[x],
sqequal: s ~ t,
MaAuto: Error :MaAuto,
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
RepeatFor: Error :RepeatFor,
apply: f a,
leader-eventually-retires: l eventually retires,
es-loc: loc(e),
Id: Id,
equal: s = t,
not: A,
uimplies: b supposing a,
nat: ,
all: x:A. B[x],
AssertBY: Error :AssertBY,
eventually-one-leader: eventually ldr is the only leader,
ExRepD: Error :ExRepD,
D: Error :D,
CollapseTHENA: Error :CollapseTHENA,
Try: Error :Try,
universe: Type,
THENM: Error :THENM
Lemmas :
atom2_subtype_base,
consensus-spec2_wf,
consensus-spec1_wf,
leaders-finite_wf,
Id_wf,
not_wf,
l_member_wf,
eventually-one-leader_wf,
es-E-interface_wf,
es-E_wf,
assert_wf,
event-ordering+_wf,
uall_wf,
nat_wf,
eclass_wf,
Paxos-spec6_wf,
Paxos-spec6-implies-Paxos-spec5,
event-ordering+_inc,
Paxos-spec5-safety,
member_wf,
es-interface-top,
es-loc_wf,
es-base-E_wf,
subtype_rel_self,
leader-eventually-retires_wf,
Paxos-spec6-non-blocking,
false_wf,
in-eclass_wf,
subtype_rel_wf,
ifthenelse_wf,
true_wf,
bool_wf,
subtype_base_sq,
bool_subtype_base,
assert_elim
\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-spec6\{i:l\}(Info; es; T; leader; failset; Reserve; Decide; Input)
{}\mRightarrow{} (Decide values come from Input values
\mwedge{} Consistent(Decide)
\mwedge{} (Finitely many leaders
{}\mRightarrow{} (\mexists{}ldr:Id
((\mneg{}(ldr \mmember{} failset))
\mwedge{} eventually ldr is the only leader
\mwedge{} (\mexists{}n:E(Input). (loc(n) = ldr))))
{}\mRightarrow{} (\mexists{}d:E. (\muparrow{}d \mmember{}\msubb{} Decide)))))
Date html generated:
2011_10_20-PM-04_43_14
Last ObjectModification:
2011_06_18-PM-02_09_43
Home
Index