Nuprl Lemma : Paxos-spec4-implies-Paxos-spec3
[Info:Type]
es:EO+(Info)
[T:Type]. Decide:EClass(T). (Paxos-spec4{i:l}(Info; es; T; Decide) 
Paxos-spec3{i:l}(Info; es; T; Decide))
Proof not projected
Definitions occuring in Statement :
Paxos-spec4: Paxos-spec4{i:l}(Info; es; T; Decide),
Paxos-spec3: Paxos-spec3{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-spec3: Paxos-spec3{i:l}(Info; es; T; Decide),
exists: 
x:A. B[x],
Paxos-spec3-body: Paxos-spec3-body{i:l}(Info; es; T; f; acceptors; Reserve; VoteState; Proposal; Accept; leader; Decide),
member: t 
T,
and: P 
Q,
prop: 
,
so_lambda: 
x y.t[x; y],
top: Top,
subtype: S 
T,
assert: 
b,
so_lambda: x.t[x],
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
cand: A c B,
pi1: fst(t),
inject: Inj(A;B;f),
pi2: snd(t),
es-E-interface: E(X),
squash: 
T,
nat: 
,
le: A 
B,
not: 
A,
false: False,
rev_implies: P 
Q,
iff: P Q,
l_all: (xL.P[x]),
Id: Id,
Paxos-spec4: Paxos-spec4{i:l}(Info; es; T; Decide),
Paxos-spec4-body: Paxos-spec4-body{i:l}(Info; es; T; f; acceptors; Reserve; VoteState; Proposal; Accept; leader; Decide; OK),
so_apply: x[s1;s2],
es-first-at: e is first@ i s.t. e.P[e],
so_apply: x[s],
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T},
sq_stable: SqStable(P),
let: let
Lemmas :
es-E-interface_wf,
es-interface-top,
Paxos-spec3-body_wf,
nat_wf,
Id_wf,
eclass_wf,
es-E_wf,
event-ordering+_inc,
paxos-acceptor-state_wf,
Paxos-spec4_wf,
event-ordering+_wf,
map_wf,
es-loc_wf,
filter_type,
eq_int_wf,
pi2_wf,
eclass-val_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
nat_properties,
es-interface-predecessors_wf,
assert_wf,
pi1_wf_top,
length_wf1,
no_repeats_wf,
l_all_wf2,
l_member_wf,
assert_elim,
in-eclass_wf,
length-map,
no_repeats_map,
es-interface-val_wf2,
no_repeats_filter,
es-interface-predecessors-no_repeats2,
member_filter,
iff_weakening_uiff,
assert_of_eq_int,
sq_stable__assert,
le_wf,
pair_eta_rw,
member_map,
atom2_subtype_base,
Paxos-spec3-one-value-per-ballot,
set_subtype_base,
int_subtype_base
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[T:Type]
\mforall{}Decide:EClass(T)
(Paxos-spec4\{i:l\}(Info; es; T; Decide) {}\mRightarrow{} Paxos-spec3\{i:l\}(Info; es; T; Decide))
Date html generated:
2011_10_20-PM-04_30_58
Last ObjectModification:
2011_06_18-PM-01_58_27
Home
Index