Nuprl Lemma : pv8_p1_threshold_wf
[accpts:bag(Id)]. (pv8_p1_threshold(accpts) 
)
Proof not projected
Definitions occuring in Statement :
pv8_p1_threshold: pv8_p1_threshold(accpts),
Id: Id,
uall: [x:A]. B[x],
member: t T,
int: ,
bag: bag(T)
Definitions :
false: False,
implies: P 
Q,
not: 
A,
nequal: a 
b T ,
pv8_p1_threshold: pv8_p1_threshold(accpts),
member: t T,
uall: [x:A]. B[x],
nat: 
Lemmas :
bag_wf,
nat_wf,
Id_wf,
bag-size_wf
\mforall{}[accpts:bag(Id)]. (pv8\_p1\_threshold(accpts) \mmember{} \mBbbZ{})
Date html generated:
2012_02_20-PM-07_16_36
Last ObjectModification:
2012_02_06-PM-02_02_57
Home
Index