Nuprl Lemma : Paxos-spec5-implies-Paxos-spec4
[Info:Type]
es:EO+(Info)
[T:Type]
Decide,Input:EClass(T). (Paxos-spec5{i:l}(Info; es; T; Decide; Input) 
Paxos-spec4{i:l}(Info; es; T; Decide))
Proof not projected
Definitions occuring in Statement :
Paxos-spec5: Paxos-spec5{i:l}(Info; es; T; Decide; Input),
Paxos-spec4: Paxos-spec4{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-spec4: Paxos-spec4{i:l}(Info; es; T; Decide),
exists: 
x:A. B[x],
Paxos-spec4-body: Paxos-spec4-body{i:l}(Info; es; T; f; acceptors; Reserve; VoteState; Proposal; Accept; leader; Decide; OK),
member: t 
T,
and: P 
Q,
let: let,
le: A 
B,
prop: 
,
cand: A c B,
subtype: S 
T,
assert: 
b,
so_lambda: 
x y.t[x; y],
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
false: False,
top: Top,
not: 
A,
es-first-at: e is first@ i s.t. e.P[e],
alle-lt: e<e'.P[e],
or: P 
Q,
guard: {T},
rev_implies: P 
Q,
iff: P Q,
so_lambda: x.t[x],
Paxos-spec5: Paxos-spec5{i:l}(Info; es; T; Decide; Input),
nat: 
,
Paxos-spec5-body: Paxos-spec5-body{i:l}(Info; es; T; f; acceptors; Reserve; VoteState; Proposal; Accept; leader; Decide; OK; Input),
es-E-interface: E(X),
so_apply: x[s1;s2],
uimplies: b supposing a,
sq_type: SQType(T),
uiff: uiff(P;Q),
so_apply: x[s]
Lemmas :
l_member_wf,
Id_wf,
es-loc_wf,
event-ordering+_inc,
nat_wf,
eclass-val_wf,
es-E_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
MaxVote_wf,
paxos-state-info_wf,
es-E-interface_wf,
es-interface-top,
pi1_wf_top,
es-le_wf,
Paxos-spec4-body_wf,
eclass_wf,
paxos-acceptor-state_wf,
Paxos-spec5_wf,
event-ordering+_wf,
assert_elim,
in-eclass_wf,
length_wf1,
filter_wf,
es-interface-predecessors_wf,
eq_int_wf,
paxos-state-reservation_wf,
es-locl_wf,
le_wf,
imax-list_wf,
map_wf,
filter_type,
assert_wf,
paxos-state-ballot_wf,
map_length,
pos-length,
equal-nil-sq-nil,
l_exists_nil
\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{} Paxos-spec4\{i:l\}(Info; es; T; Decide))
Date html generated:
2011_10_20-PM-04_31_40
Last ObjectModification:
2011_06_18-PM-01_59_26
Home
Index