---

Step * 2 1 2 1 2 of Lemma bag-summation-partition


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 ↓∈ [u / v]} . (∃z:{A| (z ↓∈ c ∧ (↑case[x;z]))})
17. Σ(x∈v). f[x] = Σ(z@0∈c). Σ(x∈[x∈v|case[x;z@0]]). f[x] ∈ R
⊢ (f[u] add Σ(z@0∈c). Σ(x∈[x∈v|case[x;z@0]]). f[x]) = Σ(z@0∈c). Σ(x∈[x∈{u} + v|case[x;z@0]]). f[x] ∈ R
BY
{ Assert ⌜(Σ(z@0∈c). Σ(x∈[x∈{u}|case[x;z@0]]). f[x] add Σ(z@0∈c). Σ(x∈[x∈v|case[x;z@0]]). f[x])
          = Σ(z@0∈c). Σ(x∈[x∈{u} + v|case[x;z@0]]). f[x]
          ∈ R⌝⋅ }

1
.....assertion..... 
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 ↓∈ [u / v]} . (∃z:{A| (z ↓∈ c ∧ (↑case[x;z]))})
17. Σ(x∈v). f[x] = Σ(z@0∈c). Σ(x∈[x∈v|case[x;z@0]]). f[x] ∈ R
⊢ (Σ(z@0∈c). Σ(x∈[x∈{u}|case[x;z@0]]). f[x] add Σ(z@0∈c). Σ(x∈[x∈v|case[x;z@0]]). f[x])
= Σ(z@0∈c). Σ(x∈[x∈{u} + v|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 ↓∈ [u / v]} . (∃z:{A| (z ↓∈ c ∧ (↑case[x;z]))})
17. Σ(x∈v). f[x] = Σ(z@0∈c). Σ(x∈[x∈v|case[x;z@0]]). f[x] ∈ R
18. (Σ(z@0∈c). Σ(x∈[x∈{u}|case[x;z@0]]). f[x] add Σ(z@0∈c). Σ(x∈[x∈v|case[x;z@0]]). f[x])
= Σ(z@0∈c). Σ(x∈[x∈{u} + v|case[x;z@0]]). f[x]
∈ R
⊢ (f[u] add Σ(z@0∈c). Σ(x∈[x∈v|case[x;z@0]]). f[x]) = Σ(z@0∈c). Σ(x∈[x∈{u} + v|case[x;z@0]]). f[x] ∈ R

---

Latex:

---

Latex:

1.  A  :  Type
2.  \mforall{}x,y:A.    Dec(x  =  y)
3.  R  :  Type
4.  T  :  Type
5.  add  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
6.  zero  :  R
7.  case  :  T  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}
8.  f  :  T  {}\mrightarrow{}  R
9.  c  :  bag(A)
10.  IsMonoid(R;add;zero)
11.  Comm(R;add)
12.  bag-no-repeats(A;c)
13.  \mforall{}z1,z2:A.  \mforall{}x:T.    ((\muparrow{}case[x;z1])  {}\mRightarrow{}  (\muparrow{}case[x;z2])  {}\mRightarrow{}  (z1  =  z2))
14.  u  :  T
15.  v  :  T  List
16.  \mforall{}x:\{x:T|  x  \mdownarrow{}\mmember{}  [u  /  v]\}  .  (\mexists{}z:\{A|  (z  \mdownarrow{}\mmember{}  c  \mwedge{}  (\muparrow{}case[x;z]))\})
17.  \mSigma{}(x\mmember{}v).  f[x]  =  \mSigma{}(z@0\mmember{}c).  \mSigma{}(x\mmember{}[x\mmember{}v|case[x;z@0]]).  f[x]
\mvdash{}  (f[u]  add  \mSigma{}(z@0\mmember{}c).  \mSigma{}(x\mmember{}[x\mmember{}v|case[x;z@0]]).  f[x])  =  \mSigma{}(z@0\mmember{}c).  \mSigma{}(x\mmember{}[x\mmember{}\{u\}  +  v|case[x;z@0]]).  f[x]


By

---

Latex:
Assert  \mkleeneopen{}(\mSigma{}(z@0\mmember{}c).  \mSigma{}(x\mmember{}[x\mmember{}\{u\}|case[x;z@0]]).  f[x]  add  \mSigma{}(z@0\mmember{}c).  \mSigma{}(x\mmember{}[x\mmember{}v|case[x;z@0]]).  f[x])
                =  \mSigma{}(z@0\mmember{}c).  \mSigma{}(x\mmember{}[x\mmember{}\{u\}  +  v|case[x;z@0]]).  f[x]\mkleeneclose{}\mcdot{}

---

Home Index