Nuprl Definition : acceptor-adopts

acceptor-adopts(es; e; b; AcceptorState) ==
(

member-eclass(es;e;AcceptorState))

(

as,as':acceptor-state().
(as

AcceptorState(e)

((b = ballot_num(as))

(as'

Prior(AcceptorState)?{init-acceptor-state()}(e)

(

(b = ballot_num(as')))))))

Proof not projected

Definitions occuring in Statement : ballot_num: ballot_num(astate), init-acceptor-state: init-acceptor-state(), acceptor-state: acceptor-state(), Ballot_Num: Ballot_Num(), primed-class-opt: Prior(X)?b, member-eclass: member-eclass(es;e;X), classrel: v

X(e), assert:

b, all:

x:A. B[x], not:

A, implies: P

Q, and: P

Q, equal: s = t, single-bag: {x}

acceptor-adopts(es; e; b; AcceptorState) == (\muparrow{}member-eclass(es;e;AcceptorState)) \mwedge{} (\mforall{}as,as':acceptor-state(). (as \mmember{} AcceptorState(e) {}\mRightarrow{} ((b = ballot\_num(as)) \mwedge{} (as' \mmember{} Prior(AcceptorState)?\{init-acceptor-state()\}(e) {}\mRightarrow{} (\mneg{}(b = ballot\_num(as'))))))) Date html generated: 2011_10_20-PM-11_57_03 Last ObjectModification: 2011_06_21-PM-06_17_10 Home Index