---

Step * 1 of Lemma bag-summation-add


1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. zero : R
5. f : T ⟶ R
6. g : T ⟶ R
7. b : bag(T)
8. IsMonoid(R;add;zero)
9. Comm(R;add)
⊢ Σ(x∈b). f[x] add g[x] = (Σ(x∈b). f[x] add Σ(x∈b). g[x]) ∈ R
BY
{ ((BagD 7 THENA Auto)
   THEN (Subst' bs = as ∈ bag(T) 0 THEN Try ((EqTypeCD THEN Auto)))
   THEN Auto
   THEN ThinVar `bs'
   THEN RenameVar `L' (-1)) }

1
1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. zero : R
5. f : T ⟶ R
6. g : T ⟶ R
7. IsMonoid(R;add;zero)
8. Comm(R;add)
9. L : T List
⊢ Σ(x∈L). f[x] add g[x] = (Σ(x∈L). f[x] add Σ(x∈L). g[x]) ∈ R

---

Latex:

---

Latex:

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


By

---

Latex:
((BagD  7  THENA  Auto)
  THEN  (Subst'  bs  =  as  0  THEN  Try  ((EqTypeCD  THEN  Auto)))
  THEN  Auto
  THEN  ThinVar  `bs'
  THEN  RenameVar  `L'  (-1))

---

Home Index