---

Step * of Lemma count_diff

∀s:DSet. ∀as,bs:|s| List. ∀c:|s|.  ((c #∈ (as - bs)) = ((c #∈ as) -- (c #∈ bs)) ∈ ℤ)
BY
{ ((((UnivCD THENA Auto) THEN OnVar `as' MoveToConcl) THEN OnVar `bs' ListInd) THEN (D 0 THENA Auto)) }

1
1. s : DSet
2. c : |s|
3. as : |s| List
⊢ (c #∈ (as - [])) = ((c #∈ as) -- (c #∈ [])) ∈ ℤ

2
1. s : DSet
2. c : |s|
3. u : |s|
4. v : |s| List
5. ∀as:|s| List. ((c #∈ (as - v)) = ((c #∈ as) -- (c #∈ v)) ∈ ℤ)
6. as : |s| List
⊢ (c #∈ (as - [u / v])) = ((c #∈ as) -- (c #∈ [u / v])) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}as,bs:|s|  List.  \mforall{}c:|s|.    ((c  \#\mmember{}  (as  -  bs))  =  ((c  \#\mmember{}  as)  --  (c  \#\mmember{}  bs)))


By

---

Latex:
((((UnivCD  THENA  Auto)  THEN  OnVar  `as'  MoveToConcl)  THEN  OnVar  `bs'  ListInd)  THEN  (D  0  THENA  Auto))

---

Home Index