---

Step * 1 of Lemma bag-summation-append


1. R : Type
2. add : R ⟶ R ⟶ R
3. zero : R
4. IsMonoid(R;add;zero)
5. Comm(R;add)
6. T : Type
7. f : T ⟶ R
8. c : bag(T)
9. bs : T List
⊢ Σ(x∈bs + c). f[x] = (Σ(x∈bs). f[x] add Σ(x∈c). f[x]) ∈ R
BY
{ (RenameVar `L' (-1)
   THEN MoveToConcl (-2)
   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 Try ((Reduce 0 THEN Symmetry THEN D 4 THEN CompleteAuto))⋅
   THEN (Assert Σ(x∈firstn(||L|| - 1;L)). f[x] ∈ R BY
               (GenConclAtAddrType ⌜bag(T)⌝ [2;3]⋅ THEN Auto))
   THEN RWW "bag-append-assoc -3" 0
   THEN Auto
   THEN GenConclAtAddr [2;2]
   THEN Thin (-1))⋅ }

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. f : T ⟶ R
8. L : T List
9. ¬↑null(L)
10. ||L|| ≥ 1 
11. ∀c:bag(T). (Σ(x∈firstn(||L|| - 1;L) + c). f[x] = (Σ(x∈firstn(||L|| - 1;L)). f[x] add Σ(x∈c). f[x]) ∈ R)
12. c : bag(T)
13. Σ(x∈firstn(||L|| - 1;L)). f[x] ∈ R
14. v : R
⊢ (v add Σ(x∈{last(L)} + c). f[x]) = ((v add Σ(x∈{last(L)}). f[x]) add Σ(x∈c). f[x]) ∈ R

---

Latex:

---

Latex:

1.  R  :  Type
2.  add  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
3.  zero  :  R
4.  IsMonoid(R;add;zero)
5.  Comm(R;add)
6.  T  :  Type
7.  f  :  T  {}\mrightarrow{}  R
8.  c  :  bag(T)
9.  bs  :  T  List
\mvdash{}  \mSigma{}(x\mmember{}bs  +  c).  f[x]  =  (\mSigma{}(x\mmember{}bs).  f[x]  add  \mSigma{}(x\mmember{}c).  f[x])


By

---

Latex:
(RenameVar  `L'  (-1)
  THEN  MoveToConcl  (-2)
  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  Try  ((Reduce  0  THEN  Symmetry  THEN  D  4  THEN  CompleteAuto))\mcdot{}
  THEN  (Assert  \mSigma{}(x\mmember{}firstn(||L||  -  1;L)).  f[x]  \mmember{}  R  BY
                          (GenConclAtAddrType  \mkleeneopen{}bag(T)\mkleeneclose{}  [2;3]\mcdot{}  THEN  Auto))
  THEN  RWW  "bag-append-assoc  -3"  0
  THEN  Auto
  THEN  GenConclAtAddr  [2;2]
  THEN  Thin  (-1))\mcdot{}

---

Home Index