---

Step * 1 of Lemma fset_of_mset_count_bound


1. s : DSet
2. c : |s|
3. w : MSet{s}
⊢ SqStable((c #∈ fset_of_mset(s;w)) ≤ 1)
BY
{ Auto }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  c  :  |s|
3.  w  :  MSet\{s\}
\mvdash{}  SqStable((c  \#\mmember{}  fset\_of\_mset(s;w))  \mleq{}  1)


By

---

Latex:
Auto

---

Home Index