---

Step * of Lemma free-vs-bag-add

∀[G:Type]. ∀[K:CRng]. ∀[S:Type]. ∀[f:S ⟶ bag(|K| × G)]. ∀[bs:bag(S)].
  (Σ{f[b] | b ∈ bs} = ⋃b∈bs.f[b] ∈ Point(free-vs(K;G)))
BY
{ (Intros
   THEN (SubsumeC ⌜basic-formal-sum(K;G)⌝⋅
         THENL [RepUR ``vs-bag-add free-vs mk-vs vs-add vs-0`` 0; (RepUR ``vs-point free-vs mk-vs`` 0 THEN Auto)]
   )
   THEN RepUR ``formal-sum-add basic-formal-sum bag-summation`` 0
   THEN RWO "bag-combine-as-accum<" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[G:Type].  \mforall{}[K:CRng].  \mforall{}[S:Type].  \mforall{}[f:S  {}\mrightarrow{}  bag(|K|  \mtimes{}  G)].  \mforall{}[bs:bag(S)].
    (\mSigma{}\{f[b]  |  b  \mmember{}  bs\}  =  \mcup{}b\mmember{}bs.f[b])


By

---

Latex:
(Intros
  THEN  (SubsumeC  \mkleeneopen{}basic-formal-sum(K;G)\mkleeneclose{}\mcdot{}
              THENL  [RepUR  ``vs-bag-add  free-vs  mk-vs  vs-add  vs-0``  0
                          ;  (RepUR  ``vs-point  free-vs  mk-vs``  0  THEN  Auto)]
  )
  THEN  RepUR  ``formal-sum-add  basic-formal-sum  bag-summation``  0
  THEN  RWO  "bag-combine-as-accum<"  0
  THEN  Auto)

---

Home Index