Nuprl Definition : paxos-collect-def

paxos-collect-def(es;f;T;leader;Collect;VoteState;Input) ==

b,e such that e is first@ leader b s.t.
q.||filter(

e'.(Reservation(VoteState(e')) =

b);

(VoteState)(q))||
= (f + 1)

(

e

(Input)')

e'<e.(

e'

VoteState)

(Reservation(VoteState(e'))

b)
e

Collect with value
let l = mapfilter(

e'.VoteState(e');

e'.(Reservation(VoteState(e')) =

b);

(VoteState)(e)) in
let mx,vs = list-max(vs.Ballot(vs);l) in
<b, mx, if (mx =

-1) then (Input)'(e) else Value(vs) fi >

Definitions : es-class-def: es-class-def, nat:

, product: x:A

B[x], es-first-at: e is first@ i s.t. e.P[e], apply: f a, equal: s = t, int:

, length: ||as||, filter: filter(P;l), add: n + m, and: P

Q, alle-lt:

e<e'.P[e], implies: P

Q, assert:

b, in-eclass: e

X, le: A

B, let: let, mapfilter: mapfilter(f;P;L), lambda:

x.A[x], paxos-state-reservation: Reservation(s), es-interface-predecessors:

(X)(e), spread: spread def, list-max: list-max(x.f[x];L), paxos-state-ballot: Ballot(s), pair: <a, b>, ifthenelse: if b then t else f fi , eq_int: (i =

j), minus: -n, natural_number: $n, eclass-val: X(e), es-prior-val: (X)', paxos-state-value: Value(s)
FDL editor aliases : paxos-collect-def

paxos-collect-def(es;f;T;leader;Collect;VoteState;Input) == \mforall{}b,e such that e is first@ leader b s.t. q.||filter(\mlambda{}e'.(Reservation(VoteState(e')) =\msubz{} b); \mleq{}(VoteState)(q))|| = (f + 1) \mwedge{} (\muparrow{}e \mmember{}\msubb{} (Input)') \mwedge{} \mforall{}e'<e.(\muparrow{}e' \mmember{}\msubb{} VoteState) {}\mRightarrow{} (Reservation(VoteState(e')) \mleq{} b) e\mmember{}Collect with value let l = mapfilter(\mlambda{}e'.VoteState(e'); \mlambda{}e'.(Reservation(VoteState(e')) =\msubz{} b); \mleq{}(VoteState)(e)) in let mx,vs = list-max(vs.Ballot(vs);l) in <b, mx, if (mx =\msubz{} -1) then (Input)'(e) else Value(vs) fi > Date html generated: 2010_08_28-PM-12_48_32 Last ObjectModification: 2010_04_16-PM-01_49_53 Home Index