Nuprl Lemma : ballot_num_wf
[astate:acceptor-state()]. (ballot_num(astate) 
Ballot_Num())
Proof not projected
Definitions occuring in Statement :
ballot_num: ballot_num(astate),
acceptor-state: acceptor-state(),
Ballot_Num: Ballot_Num(),
uall: [x:A]. B[x],
member: t T
Definitions :
void: Void,
top: Top,
pair: <a, b>,
pi1: fst(t),
uall: [x:A]. B[x],
isect: 
x:A. B[x],
axiom: Ax,
all: x:A. B[x],
function: x:A 
B[x],
ballot_num: ballot_num(astate),
equal: s = t,
acceptor-state: acceptor-state(),
product: x:A 
B[x],
PVList: PVList(),
Ballot_Num: Ballot_Num(),
member: t T
Lemmas :
acceptor-state_wf,
pi1_wf_top,
Ballot_Num_wf
\mforall{}[astate:acceptor-state()]. (ballot\_num(astate) \mmember{} Ballot\_Num())
Date html generated:
2011_10_20-PM-11_56_23
Last ObjectModification:
2011_05_12-PM-02_25_07
Home
Index