Nuprl Lemma : acceptor-adopts_wf
es:EO'. e:E. b:Ballot_Num(). AcceptorState:EClass'(acceptor-state()).
(acceptor-adopts(es; e; b; AcceptorState) 
')
Proof not projected
Definitions occuring in Statement :
acceptor-adopts: acceptor-adopts(es; e; b; AcceptorState),
acceptor-state: acceptor-state(),
Ballot_Num: Ballot_Num(),
Message: Message,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
prop: ,
all: x:A. B[x],
member: t T
Lemmas :
Message_wf,
event-ordering+_wf,
event-ordering+_inc,
es-base-E_wf,
subtype_rel_self,
es-E_wf,
acceptor-state_wf,
es-interface-subtype_rel2,
es-interface-top,
member_wf,
eclass_wf,
member-eclass_wf,
assert_wf,
Ballot_Num_wf,
bag_wf,
eclass_wf2,
eclass_wf3,
top_wf,
subtype_rel_wf,
not_wf,
primed-class-opt_wf,
classrel_wf,
ballot_num_wf,
single-bag_wf,
init-acceptor-state_wf
\mforall{}es:EO'. \mforall{}e:E. \mforall{}b:Ballot\_Num(). \mforall{}AcceptorState:EClass'(acceptor-state()).
(acceptor-adopts(es; e; b; AcceptorState) \mmember{} \mBbbP{}')
Date html generated:
2011_10_20-PM-11_57_14
Last ObjectModification:
2011_06_22-PM-12_25_45
Home
Index