Nuprl Lemma : paxos-state-ballot-lb
[T:Type]. [s:AcceptorState]. ((-1) 
Ballot(s))
Proof not projected
Definitions occuring in Statement :
paxos-state-ballot: Ballot(s),
paxos-acceptor-state: AcceptorState,
uall: [x:A]. B[x],
le: A B,
minus: -n,
natural_number: $n,
universe: Type
Definitions :
uall: [x:A]. B[x],
le: A B,
paxos-state-ballot: Ballot(s),
member: t 
T,
pi2: snd(t),
pi1: fst(t),
not: 
A,
implies: P 
Q,
false: False,
paxos-acceptor-state: AcceptorState,
nat: 
,
unit: Unit
Lemmas :
paxos-state-ballot_wf,
paxos-acceptor-state_wf
\mforall{}[T:Type]. \mforall{}[s:AcceptorState]. ((-1) \mleq{} Ballot(s))
Date html generated:
2011_10_20-PM-04_26_45
Last ObjectModification:
2011_06_18-PM-01_53_27
Home
Index