---

Step * 1 1 of Lemma bag-double-summation1

.....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
BY
{ ((GenConclTerm ⌜last(L)⌝⋅ THENA Auto)
   THEN (Subst' ⋃x∈{v}.bag-map(λy.<x, y>;f[x]) ~ bag-map(λy.<v, y>;f[v]) 0
         THENA ((InstLemma `bag-combine-single-left` [⌜T⌝;⌜x:T × A[x]⌝]⋅ THENA Auto) THEN BHyp -1 THEN Auto)
         )
   ) }

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. 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)
19. v : T
20. last(L) = v ∈ T
⊢ Σ(x∈{v}). Σ(y∈f[x]). h[x;y] = Σ(p∈bag-map(λy.<v, y>;f[v])). h[fst(p);snd(p)] ∈ R

---

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  :  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)]
16.  \mcup{}x\mmember{}b  +  \{last(L)\}.bag-map(\mlambda{}y.<x,  y>f[x])
=  (\mcup{}x\mmember{}b.bag-map(\mlambda{}y.<x,  y>f[x])  +  \mcup{}x\mmember{}\{last(L)\}.bag-map(\mlambda{}y.<x,  y>f[x]))
17.  \mSigma{}(p\mmember{}\mcup{}x\mmember{}b  +  \{last(L)\}.bag-map(\mlambda{}y.<x,  y>f[x])).  h[fst(p);snd(p)]
=  \mSigma{}(p\mmember{}\mcup{}x\mmember{}b.bag-map(\mlambda{}y.<x,  y>f[x])  +  \mcup{}x\mmember{}\{last(L)\}.bag-map(\mlambda{}y.<x,  y>f[x])).  h[fst(p);snd(p)]
18.  \mforall{}[f:(x:T  \mtimes{}  A[x])  {}\mrightarrow{}  R].  \mforall{}[b,c:bag(x:T  \mtimes{}  A[x])].
            (\mSigma{}(x\mmember{}b  +  c).  f[x]  =  (\mSigma{}(x\mmember{}b).  f[x]  add  \mSigma{}(x\mmember{}c).  f[x]))
\mvdash{}  \mSigma{}(x\mmember{}\{last(L)\}).  \mSigma{}(y\mmember{}f[x]).  h[x;y]  =  \mSigma{}(p\mmember{}\mcup{}x\mmember{}\{last(L)\}.bag-map(\mlambda{}y.<x,  y>f[x])).  h[fst(p);snd(p)]


By

---

Latex:
((GenConclTerm  \mkleeneopen{}last(L)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Subst'  \mcup{}x\mmember{}\{v\}.bag-map(\mlambda{}y.<x,  y>f[x])  \msim{}  bag-map(\mlambda{}y.<v,  y>f[v])  0
              THENA  ((InstLemma  `bag-combine-single-left`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x:T  \mtimes{}  A[x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  BHyp  -1
                            THEN  Auto)
              )
  )

---

Home Index