Nuprl Lemma : Paxos-spec2-implies-paxos-spec1
[Info:Type]
es:EO+(Info)
[T:Type]. Decide:EClass(T). (Paxos-spec2{i:l}(Info; es; T; Decide) 
paxos-spec1{i:l}(Info;es;T;Decide))
Proof not projected
Definitions occuring in Statement :
Paxos-spec2: Paxos-spec2{i:l}(Info; es; T; Decide),
paxos-spec1: paxos-spec1{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-spec1: paxos-spec1{i:l}(Info;es;T;Decide),
exists: 
x:A. B[x],
and: P 
Q,
member: t 
T,
cand: A c B,
prop: 
,
top: Top,
assert: 
b,
so_lambda: 
x y.t[x; y],
subtype: S 
T,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
so_lambda: x.t[x],
pi1: fst(t),
nat: 
,
le: A 
B,
ge: i 
j ,
not: 
A,
false: False,
pi2: snd(t),
map: map(f;as),
or: P 
Q,
length: ||as||,
ycomb: Y,
let: let,
l_exists: (xL. P[x]),
MaxVote: MaxVote(es;T;Vote;e;s),
paxos-state-info: Info(s),
paxos-state-ballot: Ballot(s),
squash: 
T,
unit: Unit,
outl: outl(x),
isl: isl(x),
Paxos-spec2: Paxos-spec2{i:l}(Info; es; T; Decide),
Paxos-spec2-body: Paxos-spec2-body{i:l}(Info;es;T;Reserve;VoteState;Proposal;Vote;W;Decide),
es-E-interface: E(X),
so_apply: x[s1;s2],
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T},
so_apply: x[s],
l_all: (xL.P[x]),
iff: P 
Q,
rev_implies: P Q,
paxos-acceptor-state: AcceptorState,
decidable: Dec(P),
paxos-state-reservation: Reservation(s),
paxos-state-name: Name(s)
Lemmas :
es-E-interface_wf,
es-interface-top,
nat_wf,
pi1_wf_top,
eclass-val_wf,
es-E_wf,
event-ordering+_inc,
subtype_base_sq,
bool_wf,
bool_subtype_base,
Id_wf,
l_all_wf2,
l_member_wf,
es-loc_wf,
pi2_wf,
Paxos-spec2_wf,
eclass_wf,
event-ordering+_wf,
assert_elim,
in-eclass_wf,
set_subtype_base,
le_wf,
int_subtype_base,
nat_properties,
ge_wf,
imax-list_wf,
map_wf,
paxos-state-ballot_wf,
paxos-acceptor-state_wf,
cons_member,
nil_member,
length_wf1,
non_neg_length,
length_wf_nat,
top_wf,
map_length,
imax-list-ub,
length-map,
member_map,
es-locl_wf,
decidable__es-locl,
squash_wf,
true_wf,
es-le-not-locl,
paxos-state-reservation_wf,
not_wf,
assert_wf,
btrue_neq_bfalse,
not_assert_elim,
unit_wf,
paxos-state-info_wf,
outl_wf,
isl_wf,
paxos-state-name_wf,
MaxVote_wf,
decidable__lt,
member_wf,
pair_wf
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[T:Type]
\mforall{}Decide:EClass(T)
(Paxos-spec2\{i:l\}(Info; es; T; Decide) {}\mRightarrow{} paxos-spec1\{i:l\}(Info;es;T;Decide))
Date html generated:
2011_10_20-PM-04_28_37
Last ObjectModification:
2011_06_18-PM-01_56_06
Home
Index