Nuprl Lemma : paxos_A1_wf
[Id-lt:Id 
Id 
]. [es:EO']. [AcceptorState:EClass'(acceptor-state())].
(paxos_A1(Id-lt;es;AcceptorState) 
{i''})
Proof not projected
Error : references
\mforall{}[Id-lt:Id {}\mrightarrow{} Id {}\mrightarrow{} \mBbbP{}]. \mforall{}[es:EO']. \mforall{}[AcceptorState:EClass'(acceptor-state())].
(paxos\_A1(Id-lt;es;AcceptorState) \mmember{} \mBbbP{}\{i''\})
Date html generated:
2012_02_20-PM-07_50_51
Last ObjectModification:
2011_06_22-PM-12_23_45
Home
Index