---

Step * of Lemma bag-summation-partition

∀[A:Type]
  ∀[R,T:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[case:T ⟶ A ⟶ 𝔹]. ∀[f:T ⟶ R]. ∀[c:bag(A)].
    Σ(x∈b). f[x] = Σ(z∈c). Σ(x∈[x∈b|case[x;z]]). f[x] ∈ R 
    supposing (IsMonoid(R;add;zero) ∧ Comm(R;add))
    ∧ (∀x:{x:T| x ↓∈ b} . (∃z:{A| (z ↓∈ c ∧ (↑case[x;z]))}))
    ∧ bag-no-repeats(A;c)
    ∧ (∀z1,z2:A. ∀x:T.  ((↑case[x;z1]) ⇒ (↑case[x;z2]) ⇒ (z1 = z2 ∈ A))) 
  supposing ∀x,y:A.  Dec(x = y ∈ A)
BY
{ (Auto THEN (BagToList 7 THENA Auto) THEN (MoveToConcl (-3) THEN ListInd 7) THEN Auto) }

1
1. A : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. R : Type
4. T : Type
5. add : R ⟶ R ⟶ R
6. zero : R
7. case : T ⟶ A ⟶ 𝔹
8. f : T ⟶ R
9. c : bag(A)
10. IsMonoid(R;add;zero)
11. Comm(R;add)
12. bag-no-repeats(A;c)
13. ∀z1,z2:A. ∀x:T.  ((↑case[x;z1]) ⇒ (↑case[x;z2]) ⇒ (z1 = z2 ∈ A))
14. ∀x:{x:T| x ↓∈ []} . (∃z:{A| (z ↓∈ c ∧ (↑case[x;z]))})
⊢ Σ(x∈[]). f[x] = Σ(z@0∈c). Σ(x∈[x∈[]|case[x;z@0]]). f[x] ∈ R

2
1. A : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. R : Type
4. T : Type
5. add : R ⟶ R ⟶ R
6. zero : R
7. case : T ⟶ A ⟶ 𝔹
8. f : T ⟶ R
9. c : bag(A)
10. IsMonoid(R;add;zero)
11. Comm(R;add)
12. bag-no-repeats(A;c)
13. ∀z1,z2:A. ∀x:T.  ((↑case[x;z1]) ⇒ (↑case[x;z2]) ⇒ (z1 = z2 ∈ A))
14. u : T
15. v : T List
16. (∀x:{x:T| x ↓∈ v} . (∃z:{A| (z ↓∈ c ∧ (↑case[x;z]))})) ⇒ (Σ(x∈v). f[x] = Σ(z@0∈c). Σ(x∈[x∈v|case[x;z@0]]). f[x] ∈ R\000C)
17. ∀x:{x:T| x ↓∈ [u / v]} . (∃z:{A| (z ↓∈ c ∧ (↑case[x;z]))})
⊢ Σ(x∈[u / v]). f[x] = Σ(z@0∈c). Σ(x∈[x∈[u / v]|case[x;z@0]]). f[x] ∈ R

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}[R,T:Type].  \mforall{}[add:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].  \mforall{}[b:bag(T)].  \mforall{}[case:T  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:T  {}\mrightarrow{}  R].
    \mforall{}[c:bag(A)].
        \mSigma{}(x\mmember{}b).  f[x]  =  \mSigma{}(z\mmember{}c).  \mSigma{}(x\mmember{}[x\mmember{}b|case[x;z]]).  f[x] 
        supposing  (IsMonoid(R;add;zero)  \mwedge{}  Comm(R;add))
        \mwedge{}  (\mforall{}x:\{x:T|  x  \mdownarrow{}\mmember{}  b\}  .  (\mexists{}z:\{A|  (z  \mdownarrow{}\mmember{}  c  \mwedge{}  (\muparrow{}case[x;z]))\}))
        \mwedge{}  bag-no-repeats(A;c)
        \mwedge{}  (\mforall{}z1,z2:A.  \mforall{}x:T.    ((\muparrow{}case[x;z1])  {}\mRightarrow{}  (\muparrow{}case[x;z2])  {}\mRightarrow{}  (z1  =  z2))) 
    supposing  \mforall{}x,y:A.    Dec(x  =  y)


By

---

Latex:
(Auto  THEN  (BagToList  7  THENA  Auto)  THEN  (MoveToConcl  (-3)  THEN  ListInd  7)  THEN  Auto)

---

Home Index