Nuprl Lemma : paxos_C1_wf
[accpts:Id List]. [es:EO']. (paxos_C1{i:l}(es;accpts) 
{i''})
Proof not projected
Definitions occuring in Statement :
paxos_C1: paxos_C1{i:l}(es;accpts),
Message: Message,
event-ordering+: EO+(Info),
Id: Id,
uall: [x:A]. B[x],
prop: ,
member: t T,
list: type List
Lemmas :
Id_wf,
PValue_wf,
compat-pvals_wf,
subtype_rel_wf,
eclass_wf,
name_wf,
mData_wf,
Message_wf,
restricted-baseclass_wf,
es-interface-top,
member_wf,
all-class-value-pairs+_wf,
event-ordering+_wf,
pi2_wf,
classrel_wf,
uall_wf,
es-E_wf,
event-ordering+_inc,
intensional-universe_wf,
eclass_wf3,
eclass_wf2,
true_wf,
squash_wf,
bag_wf,
subtype_rel_dep_function,
es-base-E_wf,
event_ordering_wf,
subtype_rel_record+,
subtype_rel_self,
subtype_rel_function,
pax_p2a_wf
\mforall{}[accpts:Id List]. \mforall{}[es:EO']. (paxos\_C1\{i:l\}(es;accpts) \mmember{} \mBbbP{}\{i''\})
Date html generated:
2011_10_21-AM-00_00_05
Last ObjectModification:
2011_06_22-PM-05_39_25
Home
Index