{ 
es:event_system{i:l}. failset:Id List. T:Type. leaders:Id List.
Decide,Input:Temporary AbsInterface(es;T). tag1a:Id.
(Paxos-spec9(es;T;leaders;failset;tag1a;Decide;Input)
(
leader:
Id
1a:Temporary AbsInterface(es;)
Paxos-spec8(es;T;leader;failset;1a;Decide;Input))) }
{ Proof }
Definitions occuring in Statement :
Paxos-spec9: Paxos-spec9(es;T;leaders;failset;tg1a;Decide;Input),
Paxos-spec8: Paxos-spec8{i:l}(Info; es; T; leader; failset; 1a; Decide; Input),
es-interface: Temporary AbsInterface(es;A),
Id: Id,
nat: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
function: x:A B[x],
list: type List,
universe: Type
Definitions :
equal: s = t,
function: x:A B[x],
all: x:A. B[x],
Paxos-spec8: Paxos-spec8{i:l}(Info; es; T; leader; failset; 1a; Decide; Input),
universe: Type,
product: x:A 
B[x],
prop: 
,
exists: x:A. B[x],
event_ordering: EO,
list: type List,
Id: Id,
nat_plus: 
,
Paxos-spec9-body: Paxos-spec9-body(es;T;f;acceptors;leaders;Input;Decide;...;...;...;...;...;...),
implies: P Q,
unit: Unit,
union: left + right,
es-valtype: Error :es-valtype,
subtype_rel: A 
r B,
Knd: Knd,
es-kind: Error :es-kind,
l_member: (x 
l),
es-E: E,
bool: 
,
not: 
A,
es-filtered-propagate-iff1: Error :es-filtered-propagate-iff1,
l_all: (xL.P[x]),
isrcv: isrcv(k),
assert: 
b,
set: {x:A| B[x]} ,
no_repeats: no_repeats(T;l),
le: A 
B,
subtype: S T,
multiply: n * m,
add: n + m,
int: 
,
pi2: snd(t),
pi1: fst(t),
es-collect-filter: Collect(size v's from X with maximum num[v] such that P[v]),
es-collect-opt-max: es-collect-opt-max,
it: 
,
inr: inr x ,
pair: <a, b>,
inl: inl x ,
lt_int: i <z j,
ifthenelse: if b then t else f fi ,
spreadn: spread3,
lambda: 
x.A[x],
es-filter-image: f[X],
es-interface-pair-prior: X;Y,
eq_int: (i =
j),
mapfilter-class: (f[v] where v from X such that P[v]),
es-is-interface: (e in X),
alle-lt: e<e'.P[e],
bfalse: ff,
es-interface-val: val(X,e),
es-le: e loc e' ,
es-E-interface: E(X),
le_int: i z j,
or: P 
Q,
es-locl: (e <loc e'),
apply: f a,
es-loc: loc(e),
nil: [],
cons: [car / cdr],
lnk: lnk(k),
lsrc: source(l),
es-interface-at: X@i,
es-propagate-iff1: X 
Y:T,
ldst: destination(l),
eq_id: a = b,
band: p 
q,
minus: -n,
imax: imax(a;b),
es-interface-accum: es-interface-accum(f;x;X),
es-prior-class-when: (X'?d) when Y,
spread: spread def,
map-class: (f[v] where v from X),
es-tagged-true-class: Tagged_tt(X),
accum-class: accum-class(a,x.f[a; x]; x.base[x]; X),
id-deq: IdDeq,
deq-member: deq-member(eq;x;L),
filter: filter(P;l),
let: let,
Paxos-spec9: Paxos-spec9(es;T;leaders;failset;tg1a;Decide;Input),
strong-subtype: strong-subtype(A;B),
atom: Atom$n,
Auto: Error :Auto,
links-from-to: links(tg) from srclocs to dstlocs,
rcvs-on: Rcvs(tg) on links,
es-in-ports: Error :es-in-ports,
round-robin: round-robin(L),
CollapseTHEN: Error :CollapseTHEN,
RepUR: Error :RepUR,
nat: ,
es-interface: Temporary AbsInterface(es;A),
member: t T,
length: ||as||,
natural_number: $n,
less_than: a < b,
and: P Q,
AssertBY: Error :AssertBY,
CollapseTHENA: Error :CollapseTHENA,
ExRepD: Error :ExRepD,
D: Error :D,
tactic: Error :tactic
Lemmas :
Paxos-spec9_wf,
event_ordering_wf,
Paxos-spec9-spec8',
Error :es-in-ports_wf,
rcvs-on_wf,
member_wf,
links-from-to_wf,
Knd_wf,
assert_wf,
isrcv_wf,
Id_wf,
round-robin_wf,
es-interface_wf,
nat_wf,
Paxos-spec8_wf
\mforall{}es:event\_system\{i:l\}. \mforall{}failset:Id List. \mforall{}T:Type. \mforall{}leaders:Id List.
\mforall{}Decide,Input:Temporary AbsInterface(es;T). \mforall{}tag1a:Id.
(Paxos-spec9(es;T;leaders;failset;tag1a;Decide;Input)
{}\mRightarrow{} (\mexists{}leader:\mBbbN{} {}\mrightarrow{} Id
\mexists{}1a:Temporary AbsInterface(es;\mBbbN{}). Paxos-spec8(es;T;leader;failset;1a;Decide;Input)))
Date html generated:
2010_08_28-PM-01_58_22
Last ObjectModification:
2010_07_15-PM-02_26_28
Home
Index