---

Step * of Lemma count_functionality

∀s:DSet. ∀a,a':|s|. ∀bs,bs':|s| List.  ((a = a' ∈ |s|) ⇒ (bs ≡(|s|) bs') ⇒ ((a #∈ bs) = (a' #∈ bs') ∈ ℤ))
BY
{ (Auto THEN Unfold `count` 0) }

1
1. s : DSet
2. a : |s|
3. a' : |s|
4. bs : |s| List
5. bs' : |s| List
6. a = a' ∈ |s|
7. bs ≡(|s|) bs'
⊢ (For{<ℤ+>} x ∈ bs. b2i(x (=b) a)) = (For{<ℤ+>} x ∈ bs'. b2i(x (=b) a')) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a,a':|s|.  \mforall{}bs,bs':|s|  List.    ((a  =  a')  {}\mRightarrow{}  (bs  \mequiv{}(|s|)  bs')  {}\mRightarrow{}  ((a  \#\mmember{}  bs)  =  (a'  \#\mmember{}  bs')))


By

---

Latex:
(Auto  THEN  Unfold  `count`  0)

---

Home Index