---

Step * 1 of Lemma bag-double-summation

.....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
BY
{ ((RWW "bag-summation-single bag-combine-single-left bag-summation-map" 0 THENA Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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.  A  :  Type
8.  B  :  Type
9.  f  :  T  {}\mrightarrow{}  bag(A)
10.  g  :  T  {}\mrightarrow{}  B
11.  h  :  B  {}\mrightarrow{}  A  {}\mrightarrow{}  R
12.  L  :  T  List
13.  \mneg{}\muparrow{}null(L)
14.  ||L||  \mgeq{}  1 
15.  b  :  bag(T)
16.  firstn(||L||  -  1;L)  =  b
17.  \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)]
\mvdash{}  \mSigma{}(x\mmember{}\{last(L)\}).  \mSigma{}(y\mmember{}f[x]).  h[g[x];y]
=  \mSigma{}(p\mmember{}\mcup{}x\mmember{}\{last(L)\}.bag-map(\mlambda{}y.<g[x],  y>f[x])).  h[fst(p);snd(p)]


By

---

Latex:
((RWW  "bag-summation-single  bag-combine-single-left  bag-summation-map"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index