---

Step * of Lemma bag-double-summation2

∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
  ∀[T,A:Type]. ∀[f:T ⟶ bag(A)]. ∀[h:T ⟶ A ⟶ R]. ∀[b:bag(T)].
    (Σ(x∈b). Σ(y∈f[x]). h[x;y] = Σ(p∈⋃x∈b.bag-map(λy.<x, y>;f[x])). h[fst(p);snd(p)] ∈ R) 
  supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
BY
{ (InstLemma `bag-double-summation` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Auto
   THEN InstHyp [⌜T⌝;⌜A⌝;⌜T⌝;⌜f⌝;⌜λ2x.x⌝;⌜h⌝;⌜b⌝] 4⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[R:Type].  \mforall{}[add:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].
    \mforall{}[T,A:Type].  \mforall{}[f:T  {}\mrightarrow{}  bag(A)].  \mforall{}[h:T  {}\mrightarrow{}  A  {}\mrightarrow{}  R].  \mforall{}[b:bag(T)].
        (\mSigma{}(x\mmember{}b).  \mSigma{}(y\mmember{}f[x]).  h[x;y]  =  \mSigma{}(p\mmember{}\mcup{}x\mmember{}b.bag-map(\mlambda{}y.<x,  y>f[x])).  h[fst(p);snd(p)]) 
    supposing  IsMonoid(R;add;zero)  \mwedge{}  Comm(R;add)


By

---

Latex:
(InstLemma  `bag-double-summation`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  4\mcdot{}
  THEN  Auto)

---

Home Index