Nuprl Lemma : accepted_wf
[astate:acceptor-state()]. (accepted(astate) 
PVList())
Proof not projected
Definitions occuring in Statement :
accepted: accepted(astate),
acceptor-state: acceptor-state(),
PVList: PVList(),
uall: [x:A]. B[x],
member: t T
Definitions :
fpf: a:A fp-> B[a],
subtype: S 
T,
uimplies: b supposing a,
subtype_rel: A r B,
eclass: EClass(A[eo; e]),
union: left + right,
list: type List,
pi2: snd(t),
uall: [x:A]. B[x],
isect: 
x:A. B[x],
axiom: Ax,
all: x:A. B[x],
function: x:A 
B[x],
accepted: accepted(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,
PVList_wf,
member_wf
\mforall{}[astate:acceptor-state()]. (accepted(astate) \mmember{} PVList())
Date html generated:
2011_10_20-PM-11_56_49
Last ObjectModification:
2011_05_12-PM-02_26_57
Home
Index