---

Step * of Lemma vs-double-bag-add

∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ bag(A[x])]. ∀[h:x:T ⟶ A[x] ⟶ Point(vs)].
∀[b:bag(T)].
  (Σ{Σ{h[x;y] | y ∈ f[x]} | x ∈ b} = Σ{h[fst(p);snd(p)] | p ∈ ⋃x∈b.bag-map(λy.<x, y>;f[x])} ∈ Point(vs))
BY
{ (Auto
   THEN Unfold `vs-bag-add` 0
   THEN InstLemma `bag-double-summation1` 
   [⌜Point(vs)⌝;⌜λx,y. x + y⌝;⌜0⌝;⌜T⌝;⌜A⌝;⌜f⌝;⌜h⌝;⌜b⌝]⋅
   THEN Auto
   THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[K:Rng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[T:Type].  \mforall{}[A:T  {}\mrightarrow{}  Type].  \mforall{}[f:x:T  {}\mrightarrow{}  bag(A[x])].  \mforall{}[h:x:T
                                                                                                                                                                            {}\mrightarrow{}  A[x]
                                                                                                                                                                            {}\mrightarrow{}  Point(vs)].
\mforall{}[b:bag(T)].
    (\mSigma{}\{\mSigma{}\{h[x;y]  |  y  \mmember{}  f[x]\}  |  x  \mmember{}  b\}  =  \mSigma{}\{h[fst(p);snd(p)]  |  p  \mmember{}  \mcup{}x\mmember{}b.bag-map(\mlambda{}y.<x,  y>f[x])\})


By

---

Latex:
(Auto
  THEN  Unfold  `vs-bag-add`  0
  THEN  InstLemma  `bag-double-summation1` 
  [\mkleeneopen{}Point(vs)\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  x  +  y\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto)))

---

Home Index