Nuprl Lemma : pv11_p1_threshold_wf
∀[accpts:bag(Id)]. (pv11_p1_threshold(accpts) ∈ ℤ)
Proof
Definitions occuring in Statement :
pv11_p1_threshold: pv11_p1_threshold(accpts),
Id: Id,
uall: ∀[x:A]. B[x],
member: t ∈ T,
int: ℤ,
bag: bag(T)
Lemmas :
bag-size_wf,
Id_wf,
nat_wf,
not-equal-2,
decidable__le,
le_wf,
false_wf,
not-le-2,
condition-implies-le,
add-commutes,
add-associates,
minus-add,
zero-add,
add-swap,
or_wf,
bag_wf
Latex:
\mforall{}[accpts:bag(Id)]. (pv11\_p1\_threshold(accpts) \mmember{} \mBbbZ{})
Date html generated:
2015_07_23-PM-04_11_49
Last ObjectModification:
2015_01_29-PM-03_12_14
Home
Index