Nuprl Lemma : Paxos-spec3-implies-Paxos-spec2
[Info:Type]
es:EO+(Info)
[T:Type]. Decide:EClass(T). (Paxos-spec3{i:l}(Info; es; T; Decide) 
Paxos-spec2{i:l}(Info; es; T; Decide))
Proof not projected
Definitions occuring in Statement :
Paxos-spec3: Paxos-spec3{i:l}(Info; es; T; Decide),
Paxos-spec2: Paxos-spec2{i:l}(Info; es; T; Decide),
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,
Paxos-spec2: Paxos-spec2{i:l}(Info; es; T; Decide),
exists: 
x:A. B[x],
member: t 
T,
prop: 
,
so_lambda: 
x y.t[x; y],
and: P 
Q,
Paxos-spec2-body: Paxos-spec2-body{i:l}(Info;es;T;Reserve;VoteState;Proposal;Vote;W;Decide),
cand: A c B,
assert: 
b,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
nat: 
,
let: let,
or: P 
Q,
l_exists: (xL. P[x]),
top: Top,
subtype: S 
T,
so_lambda: x.t[x],
squash: 
T,
inject: Inj(A;B;f),
es-E-interface: E(X),
l_all: (xL.P[x]),
Id: Id,
length: ||as||,
iff: P 
Q,
rev_implies: P Q,
ycomb: Y,
le: A 
B,
not: 
A,
false: False,
no_repeats: no_repeats(T;l),
Paxos-spec3: Paxos-spec3{i:l}(Info; es; T; Decide),
Paxos-spec3-body: Paxos-spec3-body{i:l}(Info; es; T; f; acceptors; Reserve; VoteState; Proposal; Accept; leader; Decide),
uimplies: b supposing a,
so_apply: x[s1;s2],
sq_type: SQType(T),
guard: {T},
so_apply: x[s],
sq_stable: SqStable(P),
es-first-at: e is first@ i s.t. e.P[e],
l_member: (x l)
Lemmas :
two-intersecting-wait-set-exists',
Paxos-spec2-body_wf,
Id_wf,
eclass_wf,
nat_wf,
es-E_wf,
event-ordering+_inc,
paxos-acceptor-state_wf,
Paxos-spec3_wf,
event-ordering+_wf,
eclass-val_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
es-loc_wf,
MaxVote_wf,
paxos-state-info_wf,
assert_elim,
in-eclass_wf,
es-interface-top,
map_wf,
es-E-interface_wf,
filter_type,
eq_int_wf,
paxos-state-reservation_wf,
pi1_wf_top,
es-interface-predecessors_wf,
assert_wf,
paxos-state-name_wf,
l_member_wf,
l_all_wf2,
imax-list_wf,
paxos-state-ballot_wf,
le_wf,
unit_wf,
pi2_wf,
sq_stable__assert,
filter_wf,
length-map,
length_wf1,
no_repeats_map,
es-interface-val_wf2,
no_repeats_filter,
es-interface-predecessors-no_repeats2,
member_filter,
iff_weakening_uiff,
assert_of_eq_int,
non_neg_length,
length_wf_nat,
filter_wf_top,
map_length,
member_map,
atom2_subtype_base,
l_member-settype,
l_exists_wf,
top_wf,
cons_member,
nil_member,
pair_wf,
Paxos-spec3-one-value-per-ballot,
es-le_wf,
select_wf,
not_wf
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[T:Type]
\mforall{}Decide:EClass(T)
(Paxos-spec3\{i:l\}(Info; es; T; Decide) {}\mRightarrow{} Paxos-spec2\{i:l\}(Info; es; T; Decide))
Date html generated:
2011_10_20-PM-04_29_47
Last ObjectModification:
2011_06_18-PM-01_57_27
Home
Index