Nuprl Lemma : paxos-state-reservation_wf
[T:Type]. [s:AcceptorState]. (Reservation(s) 
)
Proof not projected
Definitions occuring in Statement :
paxos-state-reservation: Reservation(s),
paxos-acceptor-state: AcceptorState,
nat: ,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
nat: ,
paxos-state-reservation: Reservation(s),
pi2: snd(t),
pi1: fst(t),
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
paxos-acceptor-state: AcceptorState
Lemmas :
paxos-acceptor-state_wf
\mforall{}[T:Type]. \mforall{}[s:AcceptorState]. (Reservation(s) \mmember{} \mBbbN{})
Date html generated:
2011_10_20-PM-04_27_35
Last ObjectModification:
2011_06_18-PM-01_54_47
Home
Index