Nuprl Lemma : paxos-state-ballot_wf
[T:Type]. [s:AcceptorState]. (Ballot(s) 
)
Proof not projected
Definitions occuring in Statement :
paxos-state-ballot: Ballot(s),
paxos-acceptor-state: AcceptorState,
uall: [x:A]. B[x],
member: t T,
int: ,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
paxos-state-ballot: Ballot(s),
pi2: snd(t),
top: Top,
all: x:A. B[x],
subtype: S 
T,
paxos-acceptor-state: AcceptorState,
nat: 
Lemmas :
paxos-acceptor-state_wf,
pi1_wf_top,
nat_wf
\mforall{}[T:Type]. \mforall{}[s:AcceptorState]. (Ballot(s) \mmember{} \mBbbZ{})
Date html generated:
2011_10_20-PM-04_26_33
Last ObjectModification:
2011_06_18-PM-01_53_08
Home
Index