Nuprl Lemma : paxos-state-value_wf
[T:Type]. [s:AcceptorState]. Value(s) 
T supposing 
(Ballot(s) = (-1))
Proof not projected
Definitions occuring in Statement :
paxos-state-value: Value(s),
paxos-state-ballot: Ballot(s),
paxos-acceptor-state: AcceptorState,
uimplies: b supposing a,
uall: [x:A]. B[x],
not: A,
member: t T,
minus: -n,
natural_number: $n,
int: 
,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
paxos-state-ballot: Ballot(s),
member: t T,
paxos-state-value: Value(s),
pi2: snd(t),
outl: outl(x),
so_lambda: 
x.t[x],
prop: 
,
top: Top,
all: x:A. B[x],
subtype: S 
T,
paxos-acceptor-state: AcceptorState,
not: A,
nat: 
,
so_apply: x[s],
implies: P 
Q,
false: False
Lemmas :
pi2_wf,
nat_wf,
not_wf,
pi1_wf_top,
paxos-acceptor-state_wf,
paxos-state-ballot_wf
\mforall{}[T:Type]. \mforall{}[s:AcceptorState]. Value(s) \mmember{} T supposing \mneg{}(Ballot(s) = (-1))
Date html generated:
2011_10_20-PM-04_26_58
Last ObjectModification:
2011_06_18-PM-01_53_47
Home
Index