---

Step * of Lemma bag-count-append

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)]. ∀[x:T].  ((#x in as + bs) = ((#x in as) + (#x in bs)) ∈ ℤ)
BY
{ (Auto
   THEN (RWO  "bag-count-sqequal" 0 THENA Auto)
   THEN (RWO  "bag-filter-append" 0 THEN Auto)
   THEN RWO  "bag-size-append" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs:bag(T)].  \mforall{}[x:T].
    ((\#x  in  as  +  bs)  =  ((\#x  in  as)  +  (\#x  in  bs)))


By

---

Latex:
(Auto
  THEN  (RWO    "bag-count-sqequal"  0  THENA  Auto)
  THEN  (RWO    "bag-filter-append"  0  THEN  Auto)
  THEN  RWO    "bag-size-append"  0
  THEN  Auto)

---

Home Index