---

Step * 2 1 1 of Lemma permr_iff_eq_counts


1. s : DSet
2. u : |s|
3. v : |s| List
4. ∀x:|s|. (0 = (b2i(u (=b) x) + (x #∈ v)) ∈ ℤ)
⊢ False
BY
{ ((With u (D (-1))) THENA Auto) }

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

---

Latex:

---

Latex:

1.  s  :  DSet
2.  u  :  |s|
3.  v  :  |s|  List
4.  \mforall{}x:|s|.  (0  =  (b2i(u  (=\msubb{})  x)  +  (x  \#\mmember{}  v)))
\mvdash{}  False


By

---

Latex:
((With  u  (D  (-1)))  THENA  Auto)

---

Home Index