Nuprl Lemma : Paxos-spec8-locations
[Info:Type]. [es:EO+(Info)]. [T:Type]. [leader:
Id]. [failset:Id List]. [1a:EClass(Id 
)].
[Decide,Input:EClass(T)]. [f:
]. [acceptors:Id List]. [1b:EClass(Id ( T?))]. [2a:EClass(Id T)].
[2b:EClass(Id 
)].
([e:E(1a)]. ((fst(1a(e))) = (leader (snd(1a(e))))))
([e:E(1b)]. (loc(e) = (leader (fst(snd(1b(e)))))))
([e:E(2a)]. ((fst(2a(e))) = (leader (fst(snd(2a(e)))))))
([e:E(2b)]. (loc(e) = (leader (fst(snd(2b(e)))))))
supposing Paxos-spec8-body{i:l}(es; Info; T; f; acceptors; leader; Input; Decide; 1a; 1b; 2a; 2b; failset)
Proof not projected
Definitions occuring in Statement :
Paxos-spec8-body: Paxos-spec8-body{i:l}(es; Info; T; f; acceptors; leader; Input; Decide; 1a; 1b; 2a; 2b; failset),
es-E-interface: E(X),
eclass-val: X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-loc: loc(e),
Id: Id,
bool: ,
nat_plus: ,
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
and: P Q,
unit: Unit,
apply: f a,
function: x:A B[x],
product: x:A B[x],
union: left + right,
list: type List,
universe: Type,
equal: s = t
Definitions :
guard: {T},
btrue: tt,
sq_type: SQType(T),
true: True,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
l_member: (x 
l),
limited-type: LimitedType,
multiply: n * m,
length: ||as||,
es-collect-filter: Collect(size v's from X with maximum num[v] such that P[v]),
es-interface-pair-prior: X;Y,
eq_int: (i =
j),
mapfilter-class: (f[v] where v from X such that P[v]),
es-locl: (e <loc e'),
in-eclass: e 
X,
alle-lt: e<e'.P[e],
bfalse: ff,
es-le: e 
loc e' ,
add: n + m,
or: P 
Q,
it: 
,
inr: inr x ,
minus: -n,
imax: imax(a;b),
es-interface-accum: es-interface-accum(f;x;X),
le_int: i z j,
spread: spread def,
es-tagged-true-class: Tagged_tt(X),
lt_int: i <z j,
ifthenelse: if b then t else f fi ,
accum-class: accum-class(a,x.f[a; x];x.base[x];X),
inl: inl x ,
map-class: (f[v] where v from X),
es-prior-class-when: (X'?d) when Y,
es-class-reply-or-fail: es-class-reply-or-fail,
cand: A c B,
natural_number: $n,
real: 
,
rationals: 
,
spreadn: spread3,
es-collect-opt-max: es-collect-opt-max,
es-filter-image: f[X],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
es-class-mcast-fail: es-class-mcast-fail,
exists: 
x:A. B[x],
Paxos-partial-spec8: Paxos-partial-spec8{i:l}(Info; es; T; f; acceptors; leader; Input; Decide; 1a; 1b; 2a; 2b; failset),
event_ordering: EO,
es-E: E,
lambda: 
x.A[x],
subtype: S 
T,
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
void: Void,
false: False,
assert: 
b,
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
let: let,
implies: P 
Q,
no_repeats: no_repeats(T;l),
dep-isect: Error :dep-isect,
record+: record+,
le: A B,
ge: i 
j ,
not: 
A,
less_than: a < b,
uiff: uiff(P;Q),
subtype_rel: A r B,
int: 
,
set: {x:A| B[x]} ,
unit: Unit,
union: left + right,
bool: ,
all: x:A. B[x],
es-loc: loc(e),
axiom: Ax,
pi2: snd(t),
apply: f a,
eclass-val: X(e),
pi1: fst(t),
pair: <a, b>,
prop: 
,
member: t T,
event-ordering+: EO+(Info),
universe: Type,
nat: ,
function: x:A B[x],
nat_plus: ,
list: type List,
so_lambda: 
x y.t[x; y],
eclass: EClass(A[eo; e]),
Paxos-spec8-body: Paxos-spec8-body{i:l}(es; Info; T; f; acceptors; leader; Input; Decide; 1a; 1b; 2a; 2b; failset),
uimplies: b supposing a,
isect: 
x:A. B[x],
and: P Q,
uall: [x:A]. B[x],
so_lambda: x.t[x],
equal: s = t,
Id: Id,
es-E-interface: E(X),
product: x:A B[x],
top: Top,
Try: Error :Try,
CollapseTHEN: Error :CollapseTHEN,
RepUR: Error :RepUR,
D: Error :D,
Auto: Error :Auto,
MaAuto: Error :MaAuto,
THENM: Error :THENM,
CollapseTHENA: Error :CollapseTHENA,
RepeatFor: Error :RepeatFor
Lemmas :
eclass_wf,
member_wf,
es-E-interface_wf,
Paxos-spec8-body_wf,
Id_wf,
nat_plus_wf,
nat_wf,
event-ordering+_wf,
uall_wf,
Paxos-partial-spec8-locations,
subtype_rel_wf,
es-interface-top,
unit_wf,
bool_wf,
nat_plus_inc,
es-E_wf,
event-ordering+_inc,
Paxos-partial-spec8_wf,
es-class-mcast-fail_wf,
es-collect-opt-max_wf,
nat_plus_properties,
le_wf,
es-loc_wf,
eclass-val_wf,
length_wf_nat,
assert_wf,
false_wf,
ifthenelse_wf,
in-eclass_wf,
true_wf,
subtype_base_sq,
bool_subtype_base,
assert_elim
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[T:Type]. \mforall{}[leader:\mBbbN{} {}\mrightarrow{} Id]. \mforall{}[failset:Id List].
\mforall{}[1a:EClass(Id \mtimes{} \mBbbN{})]. \mforall{}[Decide,Input:EClass(T)]. \mforall{}[f:\mBbbN{}\msupplus{}]. \mforall{}[acceptors:Id List]. \mforall{}[1b:EClass(Id
\mtimes{} \mBbbN{}
\mtimes{} (\mBbbN{} \mtimes{} T?))].
\mforall{}[2a:EClass(Id \mtimes{} \mBbbN{} \mtimes{} T)]. \mforall{}[2b:EClass(Id \mtimes{} \mBbbN{} \mtimes{} \mBbbB{})].
(\mforall{}[e:E(1a)]. ((fst(1a(e))) = (leader (snd(1a(e))))))
\mwedge{} (\mforall{}[e:E(1b)]. (loc(e) = (leader (fst(snd(1b(e)))))))
\mwedge{} (\mforall{}[e:E(2a)]. ((fst(2a(e))) = (leader (fst(snd(2a(e)))))))
\mwedge{} (\mforall{}[e:E(2b)]. (loc(e) = (leader (fst(snd(2b(e)))))))
supposing Paxos-spec8-body\{i:l\}(es;
Info;
T;
f;
acceptors;
leader;
Input;
Decide;
1a;
1b;
2a;
2b;
failset)
Date html generated:
2011_10_20-PM-04_48_13
Last ObjectModification:
2011_06_18-PM-02_14_32
Home
Index