Nuprl Lemma : Paxos-spec5-implies-consensus-spec2
[Info:Type]
es:EO+(Info)
[T:Type]
Decide,Input:EClass(T). (Paxos-spec5{i:l}(Info; es; T; Decide; Input) 
Decide values come from Input values)
Proof not projected
Definitions occuring in Statement :
Paxos-spec5: Paxos-spec5{i:l}(Info; es; T; Decide; Input),
consensus-spec2: Decide values come from Input values,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
universe: Type
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
consensus-spec2: Decide values come from Input values,
member: t 
T,
so_lambda: 
x y.t[x; y],
nat: 
,
subtype: S 
T,
guard: {T},
top: Top,
prop: 
,
le: A 
B,
ge: i 
j ,
not: 
A,
false: False,
exists: 
x:A. B[x],
and: P 
Q,
cand: A c B,
assert: 
b,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
es-causle: e c e',
or: P 
Q,
label: ...$L... t,
pi2: snd(t),
so_lambda: x.t[x],
Paxos-spec5: Paxos-spec5{i:l}(Info; es; T; Decide; Input),
Paxos-spec5-body: Paxos-spec5-body{i:l}(Info; es; T; f; acceptors; Reserve; VoteState; Proposal; Accept; leader; Decide; OK; Input),
so_apply: x[s1;s2],
es-E-interface: E(X),
strongwellfounded: SWellFounded(R[x; y]),
let: let,
uimplies: b supposing a,
sq_type: SQType(T),
l_exists: (xL. P[x]),
MaxVote: MaxVote(es;T;Vote;e;s),
pi1: fst(t),
iff: P 
Q,
es-locl: (e <loc e'),
so_apply: x[s],
!hyp_hide: x
Lemmas :
Paxos-spec5_wf,
eclass_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
es-E-interface_wf,
es-interface-top,
es-causl-swellfnd,
nat_wf,
non_neg_length,
Id_wf,
length_wf_nat,
top_wf,
le_wf,
es-causl_wf,
nat_properties,
ge_wf,
es-causle_wf,
eclass-val_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert_elim,
in-eclass_wf,
es-causle_weakening_locl,
es-causl_weakening,
MaxVote_wf,
member_filter,
paxos-acceptor-state_wf,
eq_int_wf,
paxos-state-reservation_wf,
pi1_wf_top,
es-interface-predecessors_wf,
es-loc_wf,
member-interface-predecessors2,
es-causle_transitivity,
es-le_weakening,
es-causl_transitivity1,
es-causl_transitivity2,
es-causl_irreflexivity,
pi2_wf,
es-causle_weakening
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[T:Type]
\mforall{}Decide,Input:EClass(T).
(Paxos-spec5\{i:l\}(Info; es; T; Decide; Input) {}\mRightarrow{} Decide values come from Input values)
Date html generated:
2011_10_20-PM-04_31_56
Last ObjectModification:
2011_06_18-PM-01_59_46
Home
Index