---

Step * of Lemma bag-double-summation

∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
  ∀[T,A,B:Type]. ∀[f:T ⟶ bag(A)]. ∀[g:T ⟶ B]. ∀[h:B ⟶ A ⟶ R]. ∀[b:bag(T)].
    (Σ(x∈b). Σ(y∈f[x]). h[g[x];y] = Σ(p∈⋃x∈b.bag-map(λy.<g[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 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 (RWO "bag-combine-append-left" 0 THENA (Auto THEN Auto))
         THEN MoveToConcl (-1)
         THEN (GenConcl ⌜firstn(||L|| - 1;L) = b ∈ bag(T)⌝⋅ THENA Auto)
         THEN Auto
         THEN (RWO "bag-summation-append" 0 THEN Auto THEN RevHypSubst (-1) 0 THEN Auto THEN EqCD THEN Auto)⋅)⋅) }

1
.....subterm..... T:t
3:n
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 : Type
8. B : Type
9. f : T ⟶ bag(A)
10. g : T ⟶ B
11. h : B ⟶ A ⟶ R
12. L : T List
13. ¬↑null(L)
14. ||L|| ≥ 1 
15. b : bag(T)
16. firstn(||L|| - 1;L) = b ∈ bag(T)
17. Σ(x∈b). Σ(y∈f[x]). h[g[x];y] = Σ(p∈⋃x∈b.bag-map(λy.<g[x], y>;f[x])). h[fst(p);snd(p)] ∈ R
⊢ Σ(x∈{last(L)}). Σ(y∈f[x]). h[g[x];y] = Σ(p∈⋃x∈{last(L)}.bag-map(λy.<g[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,A,B:Type].  \mforall{}[f:T  {}\mrightarrow{}  bag(A)].  \mforall{}[g:T  {}\mrightarrow{}  B].  \mforall{}[h:B  {}\mrightarrow{}  A  {}\mrightarrow{}  R].  \mforall{}[b:bag(T)].
        (\mSigma{}(x\mmember{}b).  \mSigma{}(y\mmember{}f[x]).  h[g[x];y]  =  \mSigma{}(p\mmember{}\mcup{}x\mmember{}b.bag-map(\mlambda{}y.<g[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  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  (RWO  "bag-combine-append-left"  0  THENA  (Auto  THEN  Auto))
              THEN  MoveToConcl  (-1)
              THEN  (GenConcl  \mkleeneopen{}firstn(||L||  -  1;L)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Auto
              THEN  (RWO  "bag-summation-append"  0
                          THEN  Auto
                          THEN  RevHypSubst  (-1)  0
                          THEN  Auto
                          THEN  EqCD
                          THEN  Auto)\mcdot{})\mcdot{})

---

Home Index