---

Step * of Lemma count-bag-to-set

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  ((#x in bag-to-set(eq;bs)) ~ if 0 <z (#x in bs) then 1 else 0 fi )
BY
{ (InstLemma `count-bag-remove-repeats` [] THEN Fold `bag-to-set` (-1) THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].
    ((\#x  in  bag-to-set(eq;bs))  \msim{}  if  0  <z  (\#x  in  bs)  then  1  else  0  fi  )


By

---

Latex:
(InstLemma  `count-bag-remove-repeats`  []  THEN  Fold  `bag-to-set`  (-1)  THEN  Trivial)

---

Home Index