Nuprl Lemma : paxos_C2_wf
[Id-lt:Id 
Id 
]. [accpts:Id List]. [es:EO']. [AcceptorState:EClass'(acceptor-state())].
(paxos_C2{i:l}(Id-lt;accpts;AcceptorState;es) 
{i''})
Proof not projected
Definitions occuring in Statement :
paxos_C2: paxos_C2{i:l}(Id-lt;accpts;AcceptorState;es),
acceptor-state: acceptor-state(),
Message: Message,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
Id: Id,
uall: [x:A]. B[x],
prop: ,
member: t T,
function: x:A B[x],
list: type List
Lemmas :
Ballot_Num_wf,
l_member_wf,
PValue_wf,
all-class-values+_wf,
Id_wf,
restricted-baseclass_wf,
supercompat-pvals_wf,
Message_wf,
event-ordering+_wf,
eclass_wf2,
acceptor-state_wf,
eclass_wf3,
eclass_wf,
bag_wf,
event-ordering+_inc,
es-E_wf,
classrel_wf,
uall_wf,
at-majority-locs_wf,
es-base-E_wf,
subtype_rel_self,
at-majority-locs_wf2,
accepted_wf,
PVList_wf,
member_wf,
subtype_rel_wf,
mData_wf,
name_wf,
pi2_wf,
es-interface-top,
intensional-universe_wf,
nat_wf,
length_wf_nat,
select_wf,
top_wf,
true_wf,
squash_wf,
subtype_rel_dep_function,
event_ordering_wf,
subtype_rel_record+,
subtype_rel_function,
pax_p2a_wf
\mforall{}[Id-lt:Id {}\mrightarrow{} Id {}\mrightarrow{} \mBbbP{}]. \mforall{}[accpts:Id List]. \mforall{}[es:EO']. \mforall{}[AcceptorState:EClass'(acceptor-state())].
(paxos\_C2\{i:l\}(Id-lt;accpts;AcceptorState;es) \mmember{} \mBbbP{}\{i''\})
Date html generated:
2011_10_21-AM-00_00_31
Last ObjectModification:
2011_06_23-PM-12_43_01
Home
Index