Nuprl Lemma : pv11_p1_overlapping_accs
∀[accpts,as,bs,cs:bag(Id)].
(↓∃i:Id. (i ↓∈ bs ∧ i ↓∈ cs)) supposing
(#([i∈accpts|¬bbag-deq-member(IdDeq;i;bs)]) < pv11_p1_threshold(accpts) and
#(as) < pv11_p1_threshold(accpts) and
(accpts = (as + cs) ∈ bag(Id)))
Proof
Definitions occuring in Statement :
pv11_p1_threshold: pv11_p1_threshold(accpts),
id-deq: IdDeq,
Id: Id,
bnot: ¬bb,
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
and: P ∧ Q,
equal: s = t ∈ T,
bag-deq-member: bag-deq-member(eq;x;b),
bag-member: x ↓∈ bs,
bag-size: #(bs),
bag-filter: [x∈b|p[x]],
bag-append: as + bs,
bag: bag(T)
Lemmas :
pv11_p1_about_threshold,
less_than_wf,
squash_wf,
true_wf,
add_functionality_wrt_eq,
bag-size_wf,
nat_wf,
bag_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,
iff_weakening_equal,
bag-split,
bag-deq-member_wf,
id-deq_wf,
bag-filter_wf,
bnot_wf,
subtype_rel_bag,
assert_wf,
bag-append-comm,
and_wf,
equal_wf,
Id_wf,
bag-intersection,
bag-append_wf,
bag-member-filter,
assert-bag-deq-member,
bag-member_wf,
pv11_p1_threshold_wf
Latex:
\mforall{}[accpts,as,bs,cs:bag(Id)].
(\mdownarrow{}\mexists{}i:Id. (i \mdownarrow{}\mmember{} bs \mwedge{} i \mdownarrow{}\mmember{} cs)) supposing
(\#([i\mmember{}accpts|\mneg{}\msubb{}bag-deq-member(IdDeq;i;bs)]) < pv11\_p1\_threshold(accpts) and
\#(as) < pv11\_p1\_threshold(accpts) and
(accpts = (as + cs)))
Date html generated:
2015_07_23-PM-05_00_12
Last ObjectModification:
2015_02_04-AM-07_51_59
Home
Index