---

Step * 1 of Lemma bag-double-summation1


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
BY
{ ((InstLemma `bag-combine-append-left` [⌜T⌝;⌜x:T × A[x]⌝;⌜b⌝;⌜{last(L)}⌝;⌜λ2x.bag-map(λy.<x, y>;f[x])⌝]⋅ THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜Σ(p∈Z). h[fst(p);snd(p)]⌝ ⌜R⌝ (-1)⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN (InstLemma `bag-summation-append` [⌜R⌝;⌜add⌝;⌜zero⌝;⌜x:T × A[x]⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN EqCDA
   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 : 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
16. ⋃x∈b + {last(L)}.bag-map(λy.<x, y>;f[x])
= (⋃x∈b.bag-map(λy.<x, y>;f[x]) + ⋃x∈{last(L)}.bag-map(λy.<x, y>;f[x]))
∈ bag(x:T × A[x])
17. Σ(p∈⋃x∈b + {last(L)}.bag-map(λy.<x, y>;f[x])). h[fst(p);snd(p)]
= Σ(p∈⋃x∈b.bag-map(λy.<x, y>;f[x]) + ⋃x∈{last(L)}.bag-map(λy.<x, y>;f[x])). h[fst(p);snd(p)]
∈ R
18. ∀[f:(x:T × A[x]) ⟶ R]. ∀[b,c:bag(x:T × A[x])].  (Σ(x∈b + c). f[x] = (Σ(x∈b). f[x] add Σ(x∈c). f[x]) ∈ R)
⊢ Σ(x∈{last(L)}). Σ(y∈f[x]). h[x;y] = Σ(p∈⋃x∈{last(L)}.bag-map(λy.<x, y>;f[x])). h[fst(p);snd(p)] ∈ 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.  A  :  T  {}\mrightarrow{}  Type
8.  f  :  x:T  {}\mrightarrow{}  bag(A[x])
9.  h  :  x:T  {}\mrightarrow{}  A[x]  {}\mrightarrow{}  R
10.  L  :  T  List
11.  \mneg{}\muparrow{}null(L)
12.  ||L||  \mgeq{}  1 
13.  b  :  bag(T)
14.  firstn(||L||  -  1;L)  =  b
15.  \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)]
\mvdash{}  (\mSigma{}(x\mmember{}b).  \mSigma{}(y\mmember{}f[x]).  h[x;y]  add  \mSigma{}(x\mmember{}\{last(L)\}).  \mSigma{}(y\mmember{}f[x]).  h[x;y])
=  \mSigma{}(p\mmember{}\mcup{}x\mmember{}b  +  \{last(L)\}.bag-map(\mlambda{}y.<x,  y>f[x])).  h[fst(p);snd(p)]


By

---

Latex:
((InstLemma  `bag-combine-append-left`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x:T  \mtimes{}  A[x]\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}\{last(L)\}\mkleeneclose{};
    \mkleeneopen{}\mlambda{}\msubtwo{}x.bag-map(\mlambda{}y.<x,  y>f[x])\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}\mSigma{}(p\mmember{}Z).  h[fst(p);snd(p)]\mkleeneclose{}  \mkleeneopen{}R\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (InstLemma  `bag-summation-append`  [\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}add\mkleeneclose{};\mkleeneopen{}zero\mkleeneclose{};\mkleeneopen{}x:T  \mtimes{}  A[x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  EqCDA
  THEN  Auto)

---

Home Index