---

Step * of Lemma bag-double-summation1

∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
  ∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ bag(A[x])]. ∀[h:x:T ⟶ A[x] ⟶ 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
{ ((Auto THEN ExRepD)
   THEN BagD (-1)
   THEN (Subst' as = bs ∈ bag(T) 0
         THENA (Auto THEN (InstLemma `bag-summation_wf` [⌜x:T × A[x]⌝]⋅ THENA Auto) THEN BHyp -1 THEN Auto)
         )
   THEN Thin (-1)
   THEN ThinVar `as' 
   THEN RenameVar `L' (-1)
   THEN MoveToConcl (-1)
   THEN (InductionOnLast
         THEN Try (Fold `single-bag` 0)
         THEN Folds ``single-bag empty-bag bag-append single-bag`` 0
         THEN RWW "bag-combine-empty-left bag-summation-empty" 0
         THEN Auto
         THEN MoveToConcl (-1)
         THEN (GenConcl ⌜firstn(||L|| - 1;L) = b ∈ bag(T)⌝⋅ THENA Auto)
         THEN ((D 0 THENM RWO "bag-summation-append" 0)
               THENA (Auto THEN (InstLemma `bag-summation_wf` [⌜x:T × A[x]⌝]⋅ THENA Auto) THEN BHyp -1 THEN Auto)
               ))⋅) }

1
1. R : Type
2. add : R ⟶ R ⟶ R
3. zero : R
4. IsMonoid(R;add;zero)
5. Comm(R;add)
6. T : Type
7. A : T ⟶ Type
8. f : x:T ⟶ bag(A[x])
9. h : x:T ⟶ A[x] ⟶ R
10. L : T List
11. ¬↑null(L)
12. ||L|| ≥ 1 
13. b : bag(T)
14. firstn(||L|| - 1;L) = b ∈ bag(T)
15. Σ(x∈b). Σ(y∈f[x]). h[x;y] = Σ(p∈⋃x∈b.bag-map(λy.<x, y>;f[x])). h[fst(p);snd(p)] ∈ R
⊢ (Σ(x∈b). Σ(y∈f[x]). h[x;y] add Σ(x∈{last(L)}). Σ(y∈f[x]). h[x;y])
= Σ(p∈⋃x∈b + {last(L)}.bag-map(λy.<x, y>;f[x])). h[fst(p);snd(p)]
∈ R

---

Latex:

---

Latex:
\mforall{}[R:Type].  \mforall{}[add:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].
    \mforall{}[T:Type].  \mforall{}[A:T  {}\mrightarrow{}  Type].  \mforall{}[f:x:T  {}\mrightarrow{}  bag(A[x])].  \mforall{}[h:x:T  {}\mrightarrow{}  A[x]  {}\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:
((Auto  THEN  ExRepD)
  THEN  BagD  (-1)
  THEN  (Subst'  as  =  bs  0
              THENA  (Auto
                            THEN  (InstLemma  `bag-summation\_wf`  [\mkleeneopen{}x:T  \mtimes{}  A[x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  BHyp  -1
                            THEN  Auto)
              )
  THEN  Thin  (-1)
  THEN  ThinVar  `as' 
  THEN  RenameVar  `L'  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (InductionOnLast
              THEN  Try  (Fold  `single-bag`  0)
              THEN  Folds  ``single-bag  empty-bag  bag-append  single-bag``  0
              THEN  RWW  "bag-combine-empty-left  bag-summation-empty"  0
              THEN  Auto
              THEN  MoveToConcl  (-1)
              THEN  (GenConcl  \mkleeneopen{}firstn(||L||  -  1;L)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  ((D  0  THENM  RWO  "bag-summation-append"  0)
                          THENA  (Auto
                                        THEN  (InstLemma  `bag-summation\_wf`  [\mkleeneopen{}x:T  \mtimes{}  A[x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                        THEN  BHyp  -1
                                        THEN  Auto)
                          ))\mcdot{})

---

Home Index