---

Step * 1 2 1 of Lemma bag-summation-partitions-primes-general

.....equality..... 
1. r : CRng
2. h : ℕ+ ⟶ ℕ+ ⟶ |r|
3. b : bag(Prime)
4. IntDeq ∈ EqDecider(Prime)
⊢ bag-map(λp.<Π(fst(p)), Π(snd(p))>;bag-partitions(IntDeq;b))
= mapfilter(λi.<i, Π(b) ÷ i>;λi.(Π(b) rem i =z 0);[1, Π(b) + 1))
∈ bag(ℕ+ × ℕ+)
BY
{ xxx(Unfold `mapfilter` 0 THEN Folds ``bag-filter bag-map`` 0)xxx }

1
1. r : CRng
2. h : ℕ+ ⟶ ℕ+ ⟶ |r|
3. b : bag(Prime)
4. IntDeq ∈ EqDecider(Prime)
⊢ bag-map(λp.<Π(fst(p)), Π(snd(p))>;bag-partitions(IntDeq;b))
= bag-map(λi.<i, Π(b) ÷ i>;[i∈[1, Π(b) + 1)|(Π(b) rem i =z 0)])
∈ bag(ℕ+ × ℕ+)

---

Latex:

---

Latex:
.....equality..... 
1.  r  :  CRng
2.  h  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  |r|
3.  b  :  bag(Prime)
4.  IntDeq  \mmember{}  EqDecider(Prime)
\mvdash{}  bag-map(\mlambda{}p.<\mPi{}(fst(p)),  \mPi{}(snd(p))>bag-partitions(IntDeq;b))
=  mapfilter(\mlambda{}i.<i,  \mPi{}(b)  \mdiv{}  i>\mlambda{}i.(\mPi{}(b)  rem  i  =\msubz{}  0);[1,  \mPi{}(b)  +  1))


By

---

Latex:
xxx(Unfold  `mapfilter`  0  THEN  Folds  ``bag-filter  bag-map``  0)xxx

---

Home Index