---

Step * 1 1 of Lemma bag-count-combine


1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ bag(T2)
4. eq : EqDecider(T2)
5. z : T2
6. L : T1 List
7. ¬↑null(L)
8. ||L|| ≥ 1 
9. (#z in concat(map(λx.f[x];firstn(||L|| - 1;L))))
= accumulate (with value s and list item x):
   (#z in f[x]) + s
  over list:
    firstn(||L|| - 1;L)
  with starting value:
   0)
∈ ℕ
⊢ (#z in concat(map(λx.f[x];firstn(||L|| - 1;L))) @ f[last(L)])
= ((#z in f[last(L)])
  + accumulate (with value s and list item x):
     (#z in f[x]) + s
    over list:
      firstn(||L|| - 1;L)
    with starting value:
     0))
∈ ℕ
BY
{ ((RevHypSubst' (-1) 0 THEN Folds ``bag-map bag-union bag-append`` 0⋅)
   THEN (GenConcl ⌜firstn(||L|| - 1;L) = b ∈ bag(T1)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜f[last(L)] = c ∈ bag(T2)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜bag-union(bag-map(λx.f[x];b)) = d ∈ bag(T2)⌝⋅ THENA Auto))⋅ }

1
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ bag(T2)
4. eq : EqDecider(T2)
5. z : T2
6. L : T1 List
7. ¬↑null(L)
8. ||L|| ≥ 1 
9. (#z in concat(map(λx.f[x];firstn(||L|| - 1;L))))
= accumulate (with value s and list item x):
   (#z in f[x]) + s
  over list:
    firstn(||L|| - 1;L)
  with starting value:
   0)
∈ ℕ
10. b : bag(T1)
11. firstn(||L|| - 1;L) = b ∈ bag(T1)
12. c : bag(T2)
13. f[last(L)] = c ∈ bag(T2)
14. d : bag(T2)
15. bag-union(bag-map(λx.f[x];b)) = d ∈ bag(T2)
⊢ (#z in d + c) = ((#z in c) + (#z in d)) ∈ ℕ

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  f  :  T1  {}\mrightarrow{}  bag(T2)
4.  eq  :  EqDecider(T2)
5.  z  :  T2
6.  L  :  T1  List
7.  \mneg{}\muparrow{}null(L)
8.  ||L||  \mgeq{}  1 
9.  (\#z  in  concat(map(\mlambda{}x.f[x];firstn(||L||  -  1;L))))
=  accumulate  (with  value  s  and  list  item  x):
      (\#z  in  f[x])  +  s
    over  list:
        firstn(||L||  -  1;L)
    with  starting  value:
      0)
\mvdash{}  (\#z  in  concat(map(\mlambda{}x.f[x];firstn(||L||  -  1;L)))  @  f[last(L)])
=  ((\#z  in  f[last(L)])
    +  accumulate  (with  value  s  and  list  item  x):
          (\#z  in  f[x])  +  s
        over  list:
            firstn(||L||  -  1;L)
        with  starting  value:
          0))


By

---

Latex:
((RevHypSubst'  (-1)  0  THEN  Folds  ``bag-map  bag-union  bag-append``  0\mcdot{})
  THEN  (GenConcl  \mkleeneopen{}firstn(||L||  -  1;L)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}f[last(L)]  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}bag-union(bag-map(\mlambda{}x.f[x];b))  =  d\mkleeneclose{}\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index