---

Step * 2 1 of Lemma permr_iff_eq_counts


1. s : DSet
2. bs : |s| List
3. ∀x:|s|. (0 = (x #∈ bs) ∈ ℤ)
⊢ ↑null(bs)
BY
{ (DVar `bs' THEN All Reduce THEN Auto) }

1
1. s : DSet
2. u : |s|
3. v : |s| List
4. ∀x:|s|. (0 = (b2i(u (=b) x) + (x #∈ v)) ∈ ℤ)
⊢ False

---

Latex:

---

Latex:

1.  s  :  DSet
2.  bs  :  |s|  List
3.  \mforall{}x:|s|.  (0  =  (x  \#\mmember{}  bs))
\mvdash{}  \muparrow{}null(bs)


By

---

Latex:
(DVar  `bs'  THEN  All  Reduce  THEN  Auto)

---

Home Index